Hostname: page-component-586b7cd67f-dsjbd Total loading time: 0 Render date: 2024-11-23T17:05:37.372Z Has data issue: false hasContentIssue false
  • English
  • Français

The verified CakeML compiler backend

Part of: JFP Research Articles

Published online by Cambridge University Press:  04 February 2019

YONG KIAM TAN ,
MAGNUS O. MYREEN ,
RAMANA KUMAR ,
ANTHONY FOX ,
SCOTT OWENS  and
MICHAEL NORRISH
YONG KIAM TAN*
Affiliation:
Computer Science Department, Carnegie Mellon University, Pittsburgh, PA 15213, USA (e-mail: [email protected])
MAGNUS O. MYREEN
Affiliation:
CSE, Chalmers University of Technology, Gothenburg 412 96, Sweden (e-mail: [email protected])
RAMANA KUMAR
Affiliation:
Data61, CSIRO / CSE, University of New South Wales, Kensington, NSW 2033, Australia (e-mail: [email protected])
ANTHONY FOX
Affiliation:
Department of Computer Science and Technology, University of Cambridge, Cambridge CB3 0FD, UK (e-mail: [email protected])
SCOTT OWENS
Affiliation:
School of Computing, University of Kent, Canterbury CT2 7NF, UK (e-mail: [email protected])
MICHAEL NORRISH
Affiliation:
Data61, CSIRO / Research School of Computer Science, Australian National University, Canberra, ACT 2600, Australia (e-mail: [email protected])
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

The CakeML compiler is, to the best of our knowledge, the most realistic verified compiler for a functional programming language to date. The architecture of the compiler, a sequence of intermediate languages through which high-level features are compiled away incrementally, enables verification of each compilation pass at an appropriate level of semantic detail. Parts of the compiler’s implementation resemble mainstream (unverified) compilers for strict functional languages, and it supports several important features and optimisations. These include efficient curried multi-argument functions, configurable data representations, efficient exceptions, register allocation, and more. The compiler produces machine code for five architectures: x86-64, ARMv6, ARMv8, MIPS-64, and RISC-V. The generated machine code contains the verified runtime system which includes a verified generational copying garbage collector and a verified arbitrary precision arithmetic (bignum) library. In this paper, we present the overall design of the compiler backend, including its 12 intermediate languages. We explain how the semantics and proofs fit together and provide detail on how the compiler has been bootstrapped inside the logic of a theorem prover. The entire development has been carried out within the HOL4 theorem prover.

Type
Regular Paper
Information
Journal of Functional Programming , Volume 29 , 2019 , e2
Copyright
© Cambridge University Press 2019 

References

Abrahamsson, O. & Myreen, M. O. (2017) Automatically introducing tail recursion in CakeML. In Trends in Functional Programming - 18th International Symposium, (TFP) 2017, Canterbury, UK, June 19–21, 2017, Revised Selected Papers, Wang, M. & Owens, S. (eds), Lecture Notes in Computer Science, vol. 10788. Springer, pp. 118–134.Google Scholar
Amadio, R. M., Ayache, N., Bobot, F., Boender, J., Campbell, B., Garnier, I., Madet, A., McKinna, J., Mulligan, D. P., Piccolo, M., Pollack, R., Régis-Gianas, Y., Coen, C. S., Stark, I. & Tranquilli, P. (2013) Certified complexity (CerCo). In Foundational and Practical Aspects of Resource Analysis - Third International Workshop, FOPARA 2013, Bertinoro, Italy, August 29–31, 2013, Revised Selected Papers, Lago, U. D. & Peña, R. (eds). Lecture Notes in Computer Science, vol. 8552. Springer, pp. 1–18.Google Scholar
Amadio, R. M. & Régis-Gianas, Y. (2011) Certifying and reasoning on cost annotations of functional programs. In Foundational and Practical Aspects of Resource Analysis - Second International Workshop, FOPARA 2011, Madrid, Spain, May 19, 2011, Revised Selected Papers, Peña, R., van Eekelen, M. C. J. D. & Shkaravska, O. (eds). Lecture Notes in Computer Science, vol. 7177. Springer, pp. 72–89.Google Scholar
Appel, A. W. (1992) Compiling with Continuations. Cambridge University Press.Google Scholar
Barthe, G., Demange, D. & Pichardie, D. (2014). Formal verification of an SSA-based middle-end for CompCert. ACM Trans. Program. Lang. Syst. 36(1), 4:1–4:35.CrossRefGoogle Scholar
Blazy, S., Robillard, B. & Appel, A. W. (2010) Formal verification of coalescing graph-coloring register allocation. In Programming Languages and Systems, 19th European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20–28, 2010, Proceedings, Gordon, A. D. (ed). Lecture Notes in Computer Science, vol. 6012. Springer, pp. 145–164.CrossRefGoogle Scholar
Buchwald, S., Lohner, D. & Ullrich, S. (2016) Verified construction of static single assignment form. In Proceedings of the 25th International Conference on Compiler Construction, CC 2016, Barcelona, Spain, March 12–18, 2016, Zaks, A. & Hermenegildo, M. V. (eds). ACM, pp. 67–76.CrossRefGoogle Scholar
Carbonneaux, Q., Hoffmann, J., Ramananandro, T. & Shao, Z. (2014) End-to-end verification of stack-space bounds for C programs. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, Edinburgh, UK, June 09–11, 2014, O’Boyle, M. F. P. & Pingali, K. (eds). ACM, pp. 270–281.CrossRefGoogle Scholar
Chlipala, A. (2010) A verified compiler for an impure functional language. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17–23, 2010, Hermenegildo, M. V. & Palsberg, J. (eds). ACM, pp. 93–106.CrossRefGoogle Scholar
Demange, D., Pichardie, D. & Stefanesco, L. (2015) Verifying fast and sparse SSA-based optimizations in Coq. In Compiler Construction - 24th International Conference, CC 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11–18, 2015, Proceedings, Franke, B. (ed). Lecture Notes in Computer Science, vol. 9031. Springer, pp. 233–252.CrossRefGoogle Scholar
Ericsson, A. S., Myreen, M. O. & Pohjola, J. Å. (2017) A verified generational garbage collector for CakeML. In Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26–29, 2017, Proceedings, Ayala-Rincón, M. & Muñoz, C. A. (eds). Lecture Notes in Computer Science, vol. 10499. Springer, pp. 444–461.Google Scholar
Fox, A. C. J., Myreen, M. O., Tan, Y. K. & Kumar, R. (2017) Verified compilation of CakeML to multiple machine-code targets. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16–17, 2017, Bertot, Y. & Vafeiadis, V. (eds). ACM, pp. 125–137.CrossRefGoogle Scholar
Gammie, P., Hosking, A. L. & Engelhardt, K. (2015) Relaxing safely: verified on-the-fly garbage collection for x86-TSO. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15–17, 2015, Grove, D. & Blackburn, S. (eds). ACM, pp. 99–109.CrossRefGoogle Scholar
George, L. & Appel, A. W. (1996) Iterated register coalescing. ACM Trans. Program. Lang. Syst. 18(3), 300–324.CrossRefGoogle Scholar
Granlund, T., et al. (2017) GNU MP: The GNU Multiple Precision Arithmetic Library, 6.1.2 edn. http://gmplib.org/.Google Scholar
Guéneau, A., Myreen, M. O., Kumar, R. & Norrish, M. (2017) Verified characteristic formulae for CakeML. In Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017, Proceedings, Yang, H. (ed). Lecture Notes in Computer Science, vol. 10201. Springer, pp. 584–610.CrossRefGoogle Scholar
Hjort, R., Holmgren, J. & Persson, C. (2017) The CakeML compiler explorer – Tracking intermediate representations in a verified compiler. In Trends in Functional Programming - 18th International Symposium, (TFP) 2017, Canterbury, UK, June 19–21, 2017, Revised Selected Papers, Wang, M. & Owens, S. (eds), Lecture Notes in Computer Science, vol. 10788. Springer, pp. 135–148.Google Scholar
Kang, J., Kim, Y., Hur, C.-K., Dreyer, D. & Vafeiadis, V. (2016) Lightweight verification of separate compilation. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20–22, 2016, Bodík, R. & Majumdar, R. (eds). ACM, pp. 178–190.CrossRefGoogle Scholar
Kumar, R. 2016 Self-compilation and Self-verification. Technical report, UCAM-CL-TR-879, Computer Laboratory, University of Cambridge.Google Scholar
Kumar, R., Myreen, M. O., Norrish, M. & Owens, S. (2014) CakeML: a verified implementation of ML. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, San Diego, CA, USA, January 20–21, 2014, Jagannathan, S. & Sewell, P. (eds). ACM, pp. 179–192.CrossRefGoogle Scholar
Leroy, X. (2009) A formally verified compiler back-end. J. Autom. Reasoning 43(4), 363–446.CrossRefGoogle Scholar
Matthews, D. (2017) Poly/ML, 5.7 edn. http://www.polyml.org/.Google Scholar
McCreight, A., Chevalier, T. & Tolmach, A. P. (2010) A certified framework for compiling and executing garbage-collected languages. In Proceeding of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP 2010, Baltimore, Maryland, USA, September 27–29, 2010, Hudak, P. & Weirich, S. (eds). ACM, pp. 273–284.CrossRefGoogle Scholar
MLton Developers (2017). MLton. http://mlton.org/.Google Scholar
Mullen, E., Zuniga, D., Tatlock, Z. & Grossman, D. (2016) Verified peephole optimizations for CompCert. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13–17, 2016, Krintz, C. & Berger, E. (eds). ACM, pp. 448–461.CrossRefGoogle Scholar
Myreen, M. O. (2010). Reusable verification of a copying collector. In Verified Software: Theories, Tools, Experiments, Third International Conference, VSTTE 2010, Edinburgh, UK, August 16–19, 2010, Proceedings, Leavens, G. T., O’Hearn, P. W. & Rajamani, S. K. (eds). Lecture Notes in Computer Science, vol. 6217. Springer, pp. 142–156.CrossRefGoogle Scholar
Myreen, M. O. & Curello, G. (2013) Proof pearl: a verified bignum implementation in x86-64 machine code. In Certified Programs and Proofs (CPP), Gonthier, G. & Norrish, M. (eds). Lecture Notes in Computer Science, vol. 8307. Springer, pp. 66–81.CrossRefGoogle Scholar
Myreen, M. O., & Davis, J. (2011) A verified runtime for a verified theorem prover. In Interactive Theorem Proving - Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22–25, 2011, Proceedings, van Eekelen, M. C. J. D., Geuvers, H., Schmaltz, J. & Wiedijk, F. (eds). Lecture Notes in Computer Science, vol. 6898. Springer, pp. 265–280.CrossRefGoogle Scholar
Myreen, M. O., Gordon, M. J. C. & Slind, K. (2012) Decompilation into logic – improved. In Formal Methods in Computer-Aided Design, FMCAD 2012, Cambridge, UK, October 22–25, 2012, Cabodi, G. & Singh, S. (eds). IEEE, pp. 78–81.Google Scholar
Myreen, M. O. & Owens, S. (2014) Proof-producing translation of higher-order logic into pure and stateful ML. J. Funct. Program. 24(2–3), 284–315.CrossRefGoogle Scholar
Neis, G., Hur, C.-K., Kaiser, J.-O., McLaughlin, C., Dreyer, D. & Vafeiadis, V. (2015) Pilsner: a compositionally verified compiler for a higher-order imperative language. In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, Vancouver, BC, Canada, September 1–3, 2015, Fisher, K. & Reppy, J. H. (eds). ACM, pp. 166–178.CrossRefGoogle Scholar
O’Connor, L., Chen, Z., Rizkallah, C., Amani, S., Lim, J., Murray, T. C., Nagashima, Y., Sewell, T. & Klein, G. (2016) Refinement through restraint: bringing down the cost of verification. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18–22, 2016, Garrigue, J., Keller, G. & Sumii, E. (eds). ACM, pp. 89–102.CrossRefGoogle Scholar
Owens, S., Myreen, M. O., Kumar, R. & Tan, Y. K. (2016) Functional big-step semantics. In Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2–8, 2016, Proceedings, Thiemann, P. (ed). Lecture Notes in Computer Science, vol. 9632. Springer, pp. 589–615.CrossRefGoogle Scholar
Owens, S., Norrish, M., Kumar, R., Myreen, M. O. & Tan, Y. K. (2017) Verifying efficient function calls in CakeML. PACMPL 1, 18:1–18:27.Google Scholar
Rideau, S. & Leroy, X. (2010) Validating register allocation and spilling. In Compiler Construction, 19th International Conference, CC 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20–28, 2010, Proceedings, Gupta, R. (ed). Lecture Notes in Computer Science, vol. 6011. Springer, pp. 224–243.CrossRefGoogle Scholar
Rideau, L., Serpette, B. P. & Leroy, X. (2008) Tilting at windmills with Coq: formal verification of a compilation algorithm for parallel moves. J. Autom. Reasoning 40(4), 307–326.CrossRefGoogle Scholar
Romanenko, S., Russo, C. & Sestoft, P. (2013) Moscow ML owner’s manual, version 2.10. 06.Google Scholar
Sevcík, J., Vafeiadis, V., Nardelli, F. Z., Jagannathan, S. & Sewell, P. (2013) CompCertTSO: a verified compiler for relaxed-memory concurrency. J. ACM 60(3), 22:1–22:50.CrossRefGoogle Scholar
Sewell, T. A. L., Myreen, M. O. & Klein, G. (2013) Translation validation for a verified OS kernel. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013, Seattle, WA, USA, June 16–19, 2013, Boehm, H.-J. & Flanagan, C. (eds). ACM, pp. 471–482.CrossRefGoogle Scholar
Slind, K. & Norrish, M. (2008) A brief overview of HOL4. In Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18–21, 2008, Proceedings, Mohamed, O. A., Muñoz, C. A. & Tahar, S. (eds). Lecture Notes in Computer Science, vol. 5170. Springer, pp. 28–32.CrossRefGoogle Scholar
SML/NJ Developers (2017). SML/NJ. http://www.smlnj.org/.Google Scholar
Stewart, G., Beringer, L., Cuellar, S. & Appel, A. W. (2015) Compositional CompCert. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15–17, 2015, Rajamani, S. K. & Walker, D. (eds). ACM, pp. 275–287.CrossRefGoogle Scholar
Tan, Y. K., Myreen, M. O., Kumar, R., Fox, A. C. J., Owens, S. & Norrish, M. (2016) A new verified compiler backend for CakeML. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18–22, 2016, Garrigue, J., Keller, G. & Sumii, E. (eds). ACM, pp. 60–73.CrossRefGoogle Scholar
Tan, Y. K., Owens, S. & Kumar, R. (2015) A verified type system for CakeML. In Proceedings of the 27th Symposium on the Implementation and Application of Functional Programming Languages, IFL 2015, Koblenz, Germany, September 14–16, 2015, Lämmel, R. (ed). ACM, pp. 7:1–7:12.CrossRefGoogle Scholar
Yang, X., Chen, Y., Eide, E. & Regehr, J. (2011) Finding and understanding bugs in C compilers. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4–8, 2011, Hall, M. W. & Padua, D. A. (eds). ACM, pp. 283–294.CrossRefGoogle Scholar
Zhao, J., Nagarakatte, S., Martin, M. M. K. & Zdancewic, S. (2013) Formal verification of SSA-based optimizations for LLVM. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013, Seattle, WA, USA, June 16–19, 2013, Boehm, H.-J. & Flanagan, C. (eds). ACM, pp. 175–186.CrossRefGoogle Scholar
Submit a response

Discussions

No Discussions have been published for this article.