The verified CakeML compiler backend. (English) Zbl 1493.68091
Summary: 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.
MSC:
| 68N18 | Functional programming and lambda calculus |
| 68N20 | Theory of compilers and interpreters |
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
References:
| [1] | 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. · Zbl 1505.68004 |
| [2] | 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. · Zbl 1445.68057 |
| [3] | 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. · Zbl 1367.68046 |
| [4] | Appel, A. W. (1992) Compiling with Continuations. Cambridge University Press. |
| [5] | 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.10.1145/2579080 |
| [6] | 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. · Zbl 1260.68227 |
| [7] | 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. |
| [8] | 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. |
| [9] | 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. · Zbl 1312.68044 |
| [10] | 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. |
| [11] | 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. · Zbl 1468.68065 |
| [12] | 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. |
| [13] | 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. |
| [14] | George, L. & Appel, A. W. (1996) Iterated register coalescing. ACM Trans. Program. Lang. Syst. 18(3), 300-324.10.1145/229542.229546 |
| [15] | Granlund, T., et al. (2017) GNU MP: The GNU Multiple Precision Arithmetic Library, 6.1.2 edn. http://gmplib.org/. |
| [16] | 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. · Zbl 1485.68030 |
| [17] | 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. |
| [18] | 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. · Zbl 1347.68085 |
| [19] | Kumar, R.2016Self-compilation and Self-verification. Technical report, UCAM-CL-TR-879, Computer Laboratory, University of Cambridge. |
| [20] | 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. · Zbl 1284.68405 |
| [21] | Leroy, X. (2009) A formally verified compiler back-end. J. Autom. Reasoning43(4), 363-446.10.1007/s10817-009-9155-4 · Zbl 1185.68215 |
| [22] | Matthews, D. (2017) Poly/ML, 5.7 edn. http://www.polyml.org/. |
| [23] | 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. · Zbl 1323.68136 |
| [24] | MLton Developers (2017). MLton. http://mlton.org/. |
| [25] | 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. |
| [26] | 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. |
| [27] | 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.10.1007/978-3-319-03545-1_5 |
| [28] | 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. · Zbl 1342.68297 |
| [29] | 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. |
| [30] | 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.10.1017/S0956796813000282 · Zbl 1297.68053 |
| [31] | 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. · Zbl 1360.68350 |
| [32] | 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. · Zbl 1361.68045 |
| [33] | 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. |
| [34] | Owens, S., Norrish, M., Kumar, R., Myreen, M. O. & Tan, Y. K. (2017) Verifying efficient function calls in CakeML. PACMPL1, 18:1-18:27. |
| [35] | 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. |
| [36] | Rideau, L., Serpette, B. P. & Leroy, X. (2008) Tilting at windmills with Coq: formal verification of a compilation algorithm for parallel moves. J. Autom. Reasoning40(4), 307-326.10.1007/s10817-007-9096-8 · Zbl 1140.68491 |
| [37] | Romanenko, S., Russo, C. & Sestoft, P. (2013) Moscow ML owner’s manual, version 2.10. 06. |
| [38] | Sevcík, J., Vafeiadis, V., Nardelli, F. Z., Jagannathan, S. & Sewell, P. (2013) CompCertTSO: a verified compiler for relaxed-memory concurrency. J. ACM60(3), 22:1-22:50. · Zbl 1281.68072 |
| [39] | 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. |
| [40] | 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. · Zbl 1165.68474 |
| [41] | SML/NJ Developers (2017). SML/NJ. http://www.smlnj.org/. |
| [42] | 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. · Zbl 1346.68056 |
| [43] | 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. · Zbl 1493.68091 |
| [44] | 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. |
| [45] | 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. |
| [46] | 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. |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
