Document Open Access Logo

Kalas: A Verified, End-To-End Compiler for a Choreographic Language

Authors Johannes Åman Pohjola, Alejandro Gómez-Londoño , James Shaker, Michael Norrish

PDF
Thumbnail PDF

File

LIPIcs.ITP.2022.27.pdf
  • Filesize: 0.92 MB
  • 18 pages

Document Identifiers

Author Details

Johannes Åman Pohjola
  • University of New South Wales, Sydney, Australia
Alejandro Gómez-Londoño
  • Chalmers University of Technology, Gothenburg, Sweden
James Shaker
  • Australian National University, Canberra, Australia
Michael Norrish
  • Australian National University, Canberra, Australia

Acknowledgements

We are grateful to Marco Carbone, Rob van Glabbeek and Magnus Myreen for insightful discussion on this work.

Cite AsGet BibTex

Johannes Åman Pohjola, Alejandro Gómez-Londoño, James Shaker, and Michael Norrish. Kalas: A Verified, End-To-End Compiler for a Choreographic Language. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 27:1-27:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ITP.2022.27

Abstract

Choreographies are an abstraction for globally describing deadlock-free communicating systems. A choreography can be compiled into multiple endpoints preserving the global behavior, providing a path for concrete system implementations. Of course, the soundness of this approach hinges on the correctness of the compilation function. In this paper, we present a verified compiler for Kalas, a choreographic language. Its machine-checked end-to-end proof of correctness ensures all generated endpoints adhere to the system description, preserving the top-level communication guarantees. This work uses the verified CakeML compiler and Hol4 proof assistant, allowing for concrete executable implementations and statements of correctness at the machine code level for multiple architectures.

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
  • Software and its engineering → Software verification
  • Software and its engineering → Compilers
Keywords
  • Choreographies
  • Interactive Theorem Proving
  • Compiler Verification

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Andreas Abel, Stephan Adelsberger, and Anton Setzer. Interactive programming in Agda - Objects and graphical user interfaces. J. Funct. Program., 27:e8, 2017. URL: https://doi.org/10.1017/S0956796816000319.
  2. Marco Carbone and Fabrizio Montesi. Deadlock-freedom-by-design: Multiparty asynchronous global programming. In Roberto Giacobazzi and Radhia Cousot, editors, The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, Rome, pages 263-274. ACM, 2013. URL: https://doi.org/10.1145/2429069.2429101.
  3. David Castro, Francisco Ferreira, and Nobuko Yoshida. EMTST: engineering the meta-theory of session types. In Armin Biere and David Parker, editors, Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Dublin, Ireland. Proceedings, Part II, volume 12079 of Lecture Notes in Computer Science, pages 278-285. Springer, 2020. URL: http://doi.org/10.1007/978-3-030-45237-7_17, URL: https://doi.org/10.1007/978-3-030-45237-7_17.
  4. Coq Development Team. The Coq proof assistant, version 8.11.0, January 2020. URL: https://doi.org/10.5281/zenodo.3744225.
  5. Luís Cruz-Filipe and Fabrizio Montesi. A core model for choreographic programming. Theor. Comput. Sci., 802:38-66, 2020. URL: https://doi.org/10.1016/j.tcs.2019.07.005.
  6. Luís Cruz-Filipe, Fabrizio Montesi, and Marco Peressotti. Certifying choreography compilation. In Antonio Cerone and Peter Csaba Ölveczky, editors, Theoretical Aspects of Computing - ICTAC 2021 - 18th International Colloquium, Virtual Event, Nur-Sultan, Kazakhstan, September 8-10, 2021, Proceedings, volume 12819 of Lecture Notes in Computer Science, pages 115-133. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-85315-0_8.
  7. Luís Cruz-Filipe, Fabrizio Montesi, and Marco Peressotti. Formalising a Turing-complete choreographic language in Coq. In Liron Cohen and Cezary Kaliszyk, editors, 12th International Conference on Interactive Theorem Proving, ITP 2021. Rome, Italy (Virtual Conference), volume 193 of LIPIcs, pages 15:1-15:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: http://doi.org/10.4230/LIPIcs.ITP.2021.15, URL: https://doi.org/10.4230/LIPIcs.ITP.2021.15.
  8. Mariangiola Dezani-Ciancaglini, Dimitris Mostrous, Nobuko Yoshida, and Sophia Drossopoulou. Session types for object-oriented languages. In Dave Thomas, editor, ECOOP 2006 - Object-Oriented Programming, 20th European Conference, Nantes, France. Proceedings, volume 4067 of Lecture Notes in Computer Science, pages 328-352. Springer, 2006. URL: https://doi.org/10.1007/11785477_20.
  9. Matthew Fernandez, June Andronick, Gerwin Klein, and Ihor Kuz. Automated verification of RPC stub code. In Nikolaj Bjørner and Frank S. de Boer, editors, FM 2015: Formal Methods - 20th International Symposium, Oslo, Norway. Proceedings, volume 9109 of Lecture Notes in Computer Science, pages 273-290. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-19249-9_18.
  10. Simon J. Gay and Vasco Thudichum Vasconcelos. Linear type theory for asynchronous session types. J. Funct. Program., 20(1):19-50, 2010. URL: https://doi.org/10.1017/S0956796809990268.
  11. Alejandro Gómez-Londoño, Johannes Åman Pohjola, Hira Taqdees Syeda, Magnus O. Myreen, and Yong Kiam Tan. Do you have space for dessert? a verified space cost semantics for CakeML programs. Proc. ACM Program. Lang., 4(OOPSLA):204:1-204:29, 2020. URL: https://doi.org/10.1145/3428272.
  12. Rayan Hallal, Mohamad Jaber, and Rasha Abdallah. From global choreography to efficient distributed implementation. In 2018 International Conference on High Performance Computing & Simulation, HPCS 2018, Orleans, France, July 16-20, 2018, pages 756-763. IEEE, 2018. URL: http://doi.org/10.1109/HPCS.2018.00122, URL: https://doi.org/10.1109/HPCS.2018.00122.
  13. Andrew K. Hirsch and Deepak Garg. Pirouette: Higher-order typed functional choreographies. Proc. ACM Program. Lang., 6(POPL), January 2022. URL: https://doi.org/10.1145/3498684.
  14. Kohei Honda. Types for dyadic interaction. In Eike Best, editor, CONCUR '93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993, Proceedings, volume 715 of Lecture Notes in Computer Science, pages 509-523. Springer, 1993. URL: https://doi.org/10.1007/3-540-57208-2_35.
  15. Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In Chris Hankin, editor, Programming Languages and Systems - ESOP'98, 7th European Symposium on Programming, Lisbon. Proceedings, volume 1381 of Lecture Notes in Computer Science, pages 122-138. Springer, 1998. URL: https://doi.org/10.1007/BFb0053567.
  16. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. J. ACM, 63(1):9:1-9:67, 2016. URL: https://doi.org/10.1145/2827695.
  17. Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. sel4: formal verification of an operating-system kernel. Commun. ACM, 53(6):107-115, 2010. URL: https://doi.org/10.1145/1743546.1743574.
  18. Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. CakeML: a verified implementation of ML. In Suresh Jagannathan and Peter Sewell, editors, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, pages 179-192. ACM, 2014. URL: https://doi.org/10.1145/2535838.2535841.
  19. Ihor Kuz, Yan Liu, Ian Gorton, and Gernot Heiser. CAmkES: a component model for secure microkernel-based embedded systems. J. Syst. Softw., 80(5):687-699, 2007. URL: https://doi.org/10.1016/j.jss.2006.08.039.
  20. Fabrizio Montesi. Choreographic Programming. Ph.D. thesis, IT University of Copenhagen, 2013. URL: http://www.fabriziomontesi.com/files/choreographic_programming.pdf.
  21. Magnus O. Myreen and Scott Owens. Proof-producing synthesis of ML from higher-order logic. In Peter Thiemann and Robby Bruce Findler, editors, ACM SIGPLAN International Conference on Functional Programming, ICFP'12, Copenhagen, Denmark, September 9-15, 2012, pages 115-126. ACM, 2012. URL: https://doi.org/10.1145/2364527.2364545.
  22. Matthias Neubauer and Peter Thiemann. An implementation of session types. In Bharat Jayaraman, editor, Practical Aspects of Declarative Languages, 6th International Symposium, PADL 2004, Dallas, TX, USA, June 18-19, 2004, Proceedings, volume 3057 of Lecture Notes in Computer Science, pages 56-70. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-24836-1_5.
  23. Randy Pollack. Closure under alpha-conversion. In Henk Barendregt and Tobias Nipkow, editors, Types for Proofs and Programs, International Workshop TYPES'93, Nijmegen, The Netherlands, May 24-28, 1993, Selected Papers, volume 806 of Lecture Notes in Computer Science, pages 313-332. Springer, 1993. URL: https://doi.org/10.1007/3-540-58085-9_82.
  24. Konrad Slind and Michael Norrish. A brief overview of HOL4. In Otmane Aït Mohamed, César A. Muñoz, and Sofiène Tahar, editors, Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montréal. Proceedings, volume 5170 of Lecture Notes in Computer Science, pages 28-32. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-71067-7_6.
  25. Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, and Michael Norrish. The verified CakeML compiler backend. J. Funct. Program., 29:e2, 2019. URL: https://doi.org/10.1017/S0956796818000229.
  26. Joseph Tassarotti, Ralf Jung, and Robert Harper. A higher-order logic for concurrent termination-preserving refinement. In Hongseok Yang, editor, Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Uppsala, Sweden. Proceedings, volume 10201 of Lecture Notes in Computer Science, pages 909-936. Springer, 2017. URL: http://doi.org/10.1007/978-3-662-54434-1_34, URL: https://doi.org/10.1007/978-3-662-54434-1_34.
  27. Peter Thiemann. Intrinsically-typed mechanized semantics for session types. In Ekaterina Komendantskaya, editor, Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages, PPDP 2019, Porto, Portugal, pages 19:1-19:15. ACM, 2019. URL: http://doi.org/10.1145/3354166.3354184, URL: https://doi.org/10.1145/3354166.3354184.
  28. Rob J. van Glabbeek. On the validity of encodings of the synchronous in the asynchronous π-calculus. Inf. Process. Lett., 137:17-25, 2018. URL: https://doi.org/10.1016/j.ipl.2018.04.015.
  29. Vasco Thudichum Vasconcelos, Simon J. Gay, and António Ravara. Type checking a multithreaded functional language with session types. Theor. Comput. Sci., 368(1-2):64-87, 2006. URL: https://doi.org/10.1016/j.tcs.2006.06.028.
  30. Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. Interaction trees: representing recursive and impure programs in coq. Proc. ACM Program. Lang., 4(POPL):51:1-51:32, 2020. URL: https://doi.org/10.1145/3371119.
  31. Nobuko Yoshida and Vasco Thudichum Vasconcelos. Language primitives and type discipline for structured communication-based programming revisited: Two systems for higher-order session communication. Electron. Notes Theor. Comput. Sci., 171(4):73-93, 2007. URL: https://doi.org/10.1016/j.entcs.2007.02.056.
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact