Document Open Access Logo

Modular Compilation for Higher-Order Functional Choreographies

Authors Luís Cruz-Filipe , Eva Graversen , Lovro Lugović , Fabrizio Montesi , Marco Peressotti

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2023.7.pdf
  • Filesize: 1.07 MB
  • 37 pages

Document Identifiers

Author Details

Luís Cruz-Filipe
  • Department of Mathematics and Computer Science, University of Southern Denmark, Odense, Denmark
Eva Graversen
  • Department of Mathematics and Computer Science, University of Southern Denmark, Odense, Denmark
Lovro Lugović
  • 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
Marco Peressotti
  • 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.

Cite AsGet BibTex

Luís Cruz-Filipe, Eva Graversen, Lovro Lugović, Fabrizio Montesi, and Marco Peressotti. Modular Compilation for Higher-Order Functional Choreographies. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 7:1-7:37, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ECOOP.2023.7

Abstract

Choreographic programming is a paradigm for concurrent and distributed software, whereby descriptions of the intended communications (choreographies) are automatically compiled into distributed code with strong safety and liveness properties (e.g., deadlock-freedom). Recent efforts tried to combine the theories of choreographic programming and higher-order functional programming, in order to integrate the benefits of the former with the modularity of the latter. However, they do not offer a satisfactory theory of compilation compared to the literature, because of important syntactic and semantic shortcomings: compilation is not modular (editing a part might require recompiling everything) and the generated code can perform unexpected global synchronisations. In this paper, we find that these shortcomings are not mere coincidences. Rather, they stem from genuine new challenges posed by the integration of choreographies and functions: knowing which participants are involved in a choreography becomes nontrivial, and divergence in applications requires rethinking how to prove the semantic correctness of compilation. We present a novel theory of compilation for functional choreographies that overcomes these challenges, based on types and a careful design of the semantics of choreographies and distributed code. The result: a modular notion of compilation, which produces code that is deadlock-free and correct (it operationally corresponds to its source choreography).

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
  • Theory of computation → Distributed computing models
  • Computing methodologies → Distributed programming languages
Keywords
  • Choreographies
  • Concurrency
  • λ-calculus
  • Type Systems

Metrics

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

Related Versions

References

  1. 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.
  2. 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.
  3. Marco Carbone, Fabrizio Montesi, Carsten Schürmann, and Nobuko Yoshida. Multiparty session types as coherence proofs. Acta Informatica, 54(3):243-269, 2017. URL: https://doi.org/10.1007/s00236-016-0285-y.
  4. Giuseppe Castagna, Mariangiola Dezani-Ciancaglini, and Luca Padovani. On global types and multi-party session. Log. Methods Comput. Sci., 8(1), 2012. URL: https://doi.org/10.2168/LMCS-8(1:24)2012.
  5. Alonzo Church. A set of postulates for the foundation of logic. Annals of Mathematics, 33(2):346-366, 1932. URL: http://www.jstor.org/stable/1968337.
  6. Luís Cruz-Filipe, Eva Graversen, Lovro Lugović, Fabrizio Montesi, and Marco Peressotti. Functional choreographic programming. In Helmut Seidl, Zhiming Liu, and Corina S. Pasareanu, editors, Theoretical Aspects of Computing - ICTAC 2022 - 19th International Colloquium, Tbilisi, Georgia, September 27-29, 2022, Proceedings, volume 13572 of Lecture Notes in Computer Science, pages 212-237. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-17715-6_15.
  7. Luís Cruz-Filipe and Fabrizio Montesi. On asynchrony and choreographies. In Massimo Bartoletti, Laura Bocchi, Ludovic Henrio, and Sophia Knight, editors, Proceedings 10th Interaction and Concurrency Experience, ICE@DisCoTec 2017, Neuchâtel, Switzerland, 21-22nd June 2017, volume 261 of EPTCS, pages 76-90, 2017. URL: https://doi.org/10.4204/EPTCS.261.8.
  8. 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.
  9. 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.
  10. 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, June 29 to July 1, 2021, Rome, Italy (Virtual Conference), 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.
  11. Romain Demangeon and Kohei Honda. Nested protocols in session types. In Maciej Koutny and Irek Ulidowski, editors, CONCUR 2012 - Concurrency Theory - 23rd International Conference, CONCUR 2012, Newcastle upon Tyne, UK, September 4-7, 2012. Proceedings, volume 7454 of Lecture Notes in Computer Science, pages 272-286. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-32940-1_20.
  12. Pierre-Malo Deniélou and Nobuko Yoshida. Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types. In Fedor V. Fomin, Rusins Freivalds, Marta Z. Kwiatkowska, and David Peleg, editors, Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part II, volume 7966 of Lecture Notes in Computer Science, pages 174-186. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39212-2_18.
  13. Whitfield Diffie and Martin E. Hellman. New directions in cryptography. IEEE Trans. Inf. Theory, 22(6):644-654, 1976. URL: https://doi.org/10.1109/TIT.1976.1055638.
  14. Simon Fowler, Sam Lindley, and Philip Wadler. Mixing metaphors: Actors as channels and channels as actors. In Peter Müller, editor, 31st European Conference on Object-Oriented Programming, ECOOP 2017, June 19-23, 2017, Barcelona, Spain, volume 74 of LIPIcs, pages 11:1-11:28. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2017.11.
  15. Saverio Giallorenzo, Ivan Lanese, and Daniel Russo. Chip: A choreographic integration process. In Hervé Panetto, Christophe Debruyne, Henderik A. Proper, Claudio Agostino Ardagna, Dumitru Roman, and Robert Meersman, editors, Procs. OTM, part II, volume 11230 of Lecture Notes in Computer Science, pages 22-40. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-02671-4_2.
  16. Saverio Giallorenzo, Fabrizio Montesi, and Marco Peressotti. Object-oriented choreographic programming. CoRR, abs/2005.09520, 2020. URL: https://arxiv.org/abs/2005.09520.
  17. Saverio Giallorenzo, Fabrizio Montesi, Marco Peressotti, David Richter, Guido Salvaneschi, and Pascal Weisenburger. Multiparty Languages: The Choreographic and Multitier Cases. In 35th European Conference on Object-Oriented Programming, ECOOP 2021, July 12-17, 2021, Aarhus, Denmark (Virtual Conference), LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2021. To appear. Pre-print available at URL: https://fabriziomontesi.com/files/gmprsw21.pdf.
  18. 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.
  19. 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.
  20. Hans Hüttel, Ivan Lanese, Vasco T. Vasconcelos, Luís Caires, Marco Carbone, Pierre-Malo Deniélou, Dimitris Mostrous, Luca Padovani, António Ravara, Emilio Tuosto, Hugo Torres Vieira, and Gianluigi Zavattaro. Foundations of session types and behavioural contracts. ACM Comput. Surv., 49(1):3:1-3:36, 2016. URL: https://doi.org/10.1145/2873052.
  21. Sung-Shik Jongmans and Petra van den Bos. A predicate transformer for choreographies - computing preconditions in choreographic programming. In Ilya Sergey, editor, Programming Languages and Systems - 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, 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.
  22. Tanakorn Leesatapornwongsa, Jeffrey F. Lukman, Shan Lu, and Haryadi S. Gunawi. TaxDC: A taxonomy of non-deterministic concurrency bugs in datacenter distributed systems. In Proc. of ASPLOS, pages 517-530, 2016. Google Scholar
  23. Fabrizio Montesi. Choreographic Programming. Ph.D. Thesis, IT University of Copenhagen, 2013. URL: http://www.fabriziomontesi.com/files/choreographic-programming.pdf.
  24. Fabrizio Montesi. Introduction to Choreographies. Cambridge University Press, 2023. Google Scholar
  25. Tom Murphy VII, Karl Crary, Robert Harper, and Frank Pfenning. A symmetric modal lambda calculus for distributed computing. In 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings, pages 286-295. IEEE Computer Society, 2004. URL: https://doi.org/10.1109/LICS.2004.1319623.
  26. 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.
  27. 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.
  28. John Vollbrecht, James D. Carlson, Larry Blunk, Dr. Bernard D. Aboba, and Henrik Levkowetz. Extensible Authentication Protocol (EAP). RFC 3748, June 2004. URL: https://doi.org/10.17487/RFC3748.
  29. Pascal Weisenburger, Johannes Wirth, and Guido Salvaneschi. A survey of multitier programming. ACM Comput. Surv., 53(4):81:1-81:35, 2020. URL: https://doi.org/10.1145/3397495.
  30. Nobuko Yoshida, Raymond Hu, Rumyana Neykova, and Nicholas Ng. The scribble protocol language. In Martín Abadi and Alberto Lluch-Lafuente, editors, Trustworthy Global Computing - 8th International Symposium, TGC 2013, Buenos Aires, Argentina, August 30-31, 2013, Revised Selected Papers, volume 8358 of Lecture Notes in Computer Science, pages 22-41. Springer, 2013. URL: https://doi.org/10.1007/978-3-319-05119-2_3.
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