Document Open Access Logo

Now It Compiles! Certified Automatic Repair of Uncompilable Protocols

Authors Luís Cruz-Filipe , Fabrizio Montesi

PDF
Thumbnail PDF

File

LIPIcs.ITP.2023.11.pdf
  • Filesize: 0.7 MB
  • 19 pages

Document Identifiers

Author Details

Luís Cruz-Filipe
  • Department of Mathematics and Computer Science, University of Southern Denmark, Odense, Denmark
Fabrizio Montesi
  • Department of Mathematics and Computer Science, University of Southern Denmark, Odense, Denmark

Funding

This work was partially supported by Villum Fonden, grants no. 29518 and 50079, and the Independent Research Fund Denmark, grant no. 0135-00219.

Acknowledgements

We thank the anonymous reviewers for their useful comments, which helped us improve the quality of this article.

Cite AsGet BibTex

Luís Cruz-Filipe and Fabrizio Montesi. Now It Compiles! Certified Automatic Repair of Uncompilable Protocols. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ITP.2023.11

Abstract

Choreographic programming is a paradigm where developers write the global specification (called choreography) of a communicating system, and then a correct-by-construction distributed implementation is compiled automatically. Unfortunately, it is possible to write choreographies that cannot be compiled, because of issues related to an agreement property known as knowledge of choice. This forces programmers to reason manually about implementation details that may be orthogonal to the protocol that they are writing. Amendment is an automatic procedure for repairing uncompilable choreographies. We present a formalisation of amendment from the literature, built upon an existing formalisation of choreographic programming. However, in the process of formalising the expected properties of this procedure, we discovered a subtle counterexample that invalidates the original published and peer-reviewed pen-and-paper theory. We discuss how using a theorem prover led us to both finding the issue, and stating and proving a correct formulation of the properties of amendment.

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
  • Theory of computation → Automated reasoning
  • Software and its engineering → Concurrent programming languages
Keywords
  • choreographic programming
  • theorem proving
  • compilation
  • program repair

Metrics

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

Related Versions

References

  1. Samik Basu and Tevfik Bultan. Automated choreography repair. In Perdita Stevens and Andrzej Wasowski, editors, Procs. FASE, volume 9633 of Lecture Notes in Computer Science, pages 13-30. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49665-7_2.
  2. Samik Basu, Tevfik Bultan, and Meriem Ouederni. Deciding choreography realizability. In John Field and Michael Hicks, editors, Procs. POPL, pages 191-202. ACM, 2012. URL: https://doi.org/10.1145/2103656.2103680.
  3. Marco Carbone, Kohei Honda, and Nobuko Yoshida. Structured communication-centered programming for web services. ACM Trans. Program. Lang. Syst., 34(2):8:1-8:78, 2012. URL: https://doi.org/10.1145/2220365.2220367.
  4. Marco Carbone, Sam Lindley, Fabrizio Montesi, Carsten Schürmann, and Philip Wadler. Coherence generalises duality: A logical explanation of multiparty session types. In Josée Desharnais and Radha Jagadeesan, editors, Procs. CONCUR, volume 59 of LIPIcs, pages 33:1-33:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. Google Scholar
  5. Marco Carbone and Fabrizio Montesi. Deadlock-freedom-by-design: multiparty asynchronous global programming. In Roberto Giacobazzi and Radhia Cousot, editors, Procs. POPL, pages 263-274. ACM, 2013. URL: https://doi.org/10.1145/2429069.2429101.
  6. Giuseppe Castagna, Mariangiola Dezani-Ciancaglini, and Luca Padovani. On global types and multi-party sessions. In Roberto Bruni and Jürgen Dingel, editors, Procs. FORTE, volume 6722 of Lecture Notes in Computer Science, pages 1-28. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-21461-5_1.
  7. David Castro-Perez, Francisco Ferreira, Lorenzo Gheri, and Nobuko Yoshida. Zooid: a DSL for certified multiparty computation: from mechanised metatheory to certified multiparty processes. In Stephen N. Freund and Eran Yahav, editors, Procs. PLDI, pages 237-251. ACM, 2021. URL: https://doi.org/10.1145/3453483.3454041.
  8. Luís Cruz-Filipe, Lovro Lugović, and Fabrizio Montesi. Certified compilation of choreographies with hacc. In Formal Techniques for Distributed Objects, Components, and Systems - 43rd IFIP WG 6.1 International Conference, FORTE 2023, Held as Part of the 18th International Federated Conference on Distributed Computing Techniques, DisCoTec 2023, Lisbon, Portugal, June 19-23, 2023, Proceedings, pages 29-36, 2023. URL: https://doi.org/10.1007/978-3-031-35355-0_3.
  9. Luís Cruz-Filipe and Fabrizio Montesi. A core model for choreographic programming. In Olga Kouchnarenko and Ramtin Khosravi, editors, Procs. FACS, volume 10231 of Lecture Notes in Computer Science, pages 17-35. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-57666-4_3.
  10. 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.
  11. Luís Cruz-Filipe, Fabrizio Montesi, and Marco Peressotti. Certifying choreography compilation. In Antonio Cerone and Peter Csaba Ölveczky, editors, Procs. ICTAC, 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.
  12. Luís Cruz-Filipe, Fabrizio Montesi, and Marco Peressotti. Formalising a Turing-complete choreographic language in Coq. In Liron Cohen and Cezary Kaliszyk, editors, Procs. ITP, volume 193 of LIPIcs, pages 15:1-15:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ITP.2021.15.
  13. Luís Cruz-Filipe, Fabrizio Montesi, and Marco Peressotti. A formal theory of choreographic programming. J. Autom. Reason., 67(2):21, 2023. URL: https://doi.org/10.1007/s10817-023-09665-3.
  14. Mila Dalla Preda, Maurizio Gabbrielli, Saverio Giallorenzo, Ivan Lanese, and Jacopo Mauro. Dynamic choreographies: Theory and implementation. Log. Methods Comput. Sci., 13(2), 2017. URL: https://doi.org/10.23638/LMCS-13(2:1)2017.
  15. Alain Finkel and Étienne Lozes. Synchronizability of communicating finite state machines is not decidable. In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, Procs. ICALP, volume 80 of LIPIcs, pages 122:1-122:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.ICALP.2017.122.
  16. Saverio Giallorenzo, Fabrizio Montesi, and Marco Peressotti. Choreographies as objects. CoRR, abs/2005.09520, 2020. URL: https://arxiv.org/abs/2005.09520.
  17. Andrew K. Hirsch and Deepak Garg. Pirouette: higher-order typed functional choreographies. Proc. ACM Program. Lang., 6(POPL):1-27, 2022. URL: https://doi.org/10.1145/3498684.
  18. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. J. ACM, 63(1):9, 2016. Also: POPL, pages 273-284, 2008. URL: https://doi.org/10.1145/2827695.
  19. Jules Jacobs, Stephanie Balzer, and Robbert Krebbers. Multiparty GV: functional multiparty session types with certified deadlock freedom. Proc. ACM Program. Lang., 6(ICFP):466-495, 2022. URL: https://doi.org/10.1145/3547638.
  20. Sung-Shik Jongmans and Petra van den Bos. A predicate transformer for choreographies - computing preconditions in choreographic programming. In Ilya Sergey, editor, Procs. ESOP, volume 13240 of Lecture Notes in Computer Science, pages 520-547. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99336-8_19.
  21. Stephen Cole Kleene. Introduction to Metamathematics, volume 1. North-Holland Publishing Co., 1952. Google Scholar
  22. Ivan Lanese, Fabrizio Montesi, and Gianluigi Zavattaro. Amending choreographies. In António Ravara and Josep Silva, editors, Procs. WWW, volume 123 of EPTCS, pages 34-48, 2013. URL: https://doi.org/10.4204/EPTCS.123.5.
  23. Tanakorn Leesatapornwongsa, Jeffrey F. Lukman, Shan Lu, and Haryadi S. Gunawi. Taxdc: A taxonomy of non-deterministic concurrency bugs in datacenter distributed systems. In Tom Conte and Yuanyuan Zhou, editors, Procs. ASPLOS, pages 517-530. ACM, 2016. URL: https://doi.org/10.1145/2872362.2872374.
  24. Alberto Lluch-Lafuente, Flemming Nielson, and Hanne Riis Nielson. Discretionary information flow control for interaction-oriented specifications. In Narciso Martí-Oliet, Peter Csaba Ölveczky, and Carolyn L. Talcott, editors, Logic, Rewriting, and Concurrency, volume 9200 of Lecture Notes in Computer Science, pages 427-450. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-23165-5_20.
  25. Hugo A. López and Kai Heussen. Choreographing cyber-physical distributed control systems for the energy sector. In Ahmed Seffah, Birgit Penzenstadler, Carina Alves, and Xin Peng, editors, Procs. SAC, pages 437-443. ACM, 2017. URL: https://doi.org/10.1145/3019612.3019656.
  26. Petar Maksimovic and Alan Schmitt. HOCore in Coq. In Christian Urban and Xingyuan Zhang, editors, Procs. ITP, volume 9236 of Lecture Notes in Computer Science, pages 278-293. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-22102-1_19.
  27. Fabrizio Montesi. Choreographic Programming. Ph.D. Thesis, IT University of Copenhagen, 2013. URL: https://www.fabriziomontesi.com/files/choreographic-programming.pdf.
  28. Fabrizio Montesi. Introduction to Choreographies. Cambridge University Press, 2023. Google Scholar
  29. Roger M. Needham and Michael D. Schroeder. Using encryption for authentication in large networks of computers. Commun. ACM, 21(12):993-999, 1978. URL: https://doi.org/10.1145/359657.359659.
  30. 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 June Andronick and Leonardo de Moura, editors, Procs. ITP, volume 237 of LIPIcs, pages 27:1-27:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.ITP.2022.27.
  31. Alan M. Turing. Computability and λ-definability. J. Symb. Log., 2(4):153-163, 1937. URL: https://doi.org/10.2307/2268280.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact