Ozone: Fully Out-of-Order Choreographies

Authors Dan Plyukhin , Marco Peressotti , Fabrizio Montesi



PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2024.31.pdf
  • Filesize: 2.11 MB
  • 28 pages

Document Identifiers

Author Details

Dan Plyukhin
  • University of Southern Denmark, Odense, Denmark
Marco Peressotti
  • University of Southern Denmark, Odense, Denmark
Fabrizio Montesi
  • University of Southern Denmark, Odense, Denmark

Cite AsGet BibTex

Dan Plyukhin, Marco Peressotti, and Fabrizio Montesi. Ozone: Fully Out-of-Order Choreographies. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 31:1-31:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ECOOP.2024.31

Abstract

Choreographic programming is a paradigm for writing distributed applications. It allows programmers to write a single program, called a choreography, that can be compiled to generate correct implementations of each process in the application. Although choreographies provide good static guarantees, they can exhibit high latency when messages or processes are delayed. This is because processes in a choreography typically execute in a fixed, deterministic order, and cannot adapt to the order that messages arrive at runtime. In non-choreographic code, programmers can address this problem by allowing processes to execute out of order - for instance by using futures or reactive programming. However, in choreographic code, out-of-order process execution can lead to serious and subtle bugs, called communication integrity violations (CIVs). In this paper, we develop a model of choreographic programming for out-of-order processes that guarantees absence of CIVs and deadlocks. As an application of our approach, we also introduce an API for safe non-blocking communication via futures in the choreographic programming language Choral. The API allows processes to execute out of order, participate in multiple choreographies concurrently, and to handle unordered data messages. We provide an illustrative evaluation of our API, showing that out-of-order execution can reduce latency and increase throughput by overlapping communication with computation.

Subject Classification

ACM Subject Classification
  • Computing methodologies → Concurrent computing methodologies
Keywords
  • Choreographic programming
  • Asynchrony
  • Concurrency

Metrics

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

References

  1. Manuel Adameit, Kirstin Peters, and Uwe Nestmann. Session types for link failures. In Ahmed Bouajjani and Alexandra Silva, editors, Formal Techniques for Distributed Objects, Components, and Systems - 37th IFIP WG 6.1 International Conference, FORTE 2017, Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017, Neuchâtel, Switzerland, June 19-22, 2017, Proceedings, volume 10321 of Lecture Notes in Computer Science, pages 1-16. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-60225-7_1.
  2. Gul Agha. ACTORS - a Model of Concurrent Computation in Distributed Systems. MIT Press Series in Artificial Intelligence. MIT Press, Cambridge, MA, 1990. Google Scholar
  3. Akka. https://akka.io/, 2024.
  4. Henry C. Baker and Carl Hewitt. The incremental garbage collection of processes. In James Low, editor, Proceedings of the 1977 Symposium on Artificial Intelligence and Programming Languages, USA, August 15-17, 1977, pages 55-59. ACM, 1977. URL: https://doi.org/10.1145/800228.806932.
  5. Mario Bravetti, Marco Carbone, Julien Lange, Nobuko Yoshida, and Gianluigi Zavattaro. A sound algorithm for asynchronous session subtyping and its implementation. Log. Methods Comput. Sci., 17(1), 2021. URL: https://lmcs.episciences.org/7238.
  6. Mario Bravetti, Ivan Lanese, and Gianluigi Zavattaro. Contract-driven implementation of choreographies. In Christos Kaklamanis and Flemming Nielson, editors, Trustworthy Global Computing, 4th International Symposium, TGC 2008, Barcelona, Spain, November 3-4, 2008, Revised Selected Papers, volume 5474 of Lecture Notes in Computer Science, pages 1-18. Springer, 2008. URL: https://doi.org/10.1007/978-3-642-00945-7_1.
  7. Marco Carbone, Kohei Honda, and Nobuko Yoshida. Structured Communication-Centered Programming for Web Services. ACM Transactions on Programming Languages and Systems, 34(2):1-78, June 2012. URL: https://doi.org/10.1145/2220365.2220367.
  8. 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, Italy - January 23 - 25, 2013, pages 263-274. ACM, 2013. URL: https://doi.org/10.1145/2429069.2429101.
  9. Luís Cruz-Filipe, Anne Madsen, Fabrizio Montesi, and Marco Peressotti. Modular choreographies: Bridging alice and bob notation to java. In Gokila Dorai, Maurizio Gabbrielli, Giulio Manzonetto, Aomar Osmani, Marco Prandini, Gianluigi Zavattaro, and Olaf Zimmermann, editors, Joint Post-proceedings of the Third and Fourth International Conference on Microservices, Microservices 2020/2022, May 10-12, 2022, Paris, France, volume 111 of OASIcs, pages 3:1-3:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/OASICS.MICROSERVICES.2020-2022.3.
  10. Luís Cruz-Filipe and Fabrizio Montesi. On Asynchrony and Choreographies. Electronic Proceedings in Theoretical Computer Science, 261:76-90, November 2017. URL: https://doi.org/10.4204/EPTCS.261.8.
  11. Luís Cruz-Filipe and Fabrizio Montesi. Procedural choreographic programming. In Ahmed Bouajjani and Alexandra Silva, editors, Formal Techniques for Distributed Objects, Components, and Systems - 37th IFIP WG 6.1 International Conference, FORTE 2017, Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017, Neuchâtel, Switzerland, June 19-22, 2017, Proceedings, volume 10321 of Lecture Notes in Computer Science, pages 92-107. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-60225-7_7.
  12. Luís Cruz-Filipe, Fabrizio Montesi, and Marco Peressotti. Communications in choreographies, revisited. In Hisham M. Haddad, Roger L. Wainwright, and Richard Chbeir, editors, Proceedings of the 33rd Annual ACM Symposium on Applied Computing, SAC 2018, Pau, France, April 09-13, 2018, pages 1248-1255. ACM, 2018. URL: https://doi.org/10.1145/3167132.3167267.
  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. Zak Cutner, Nobuko Yoshida, and Martin Vassor. Deadlock-free asynchronous message reordering in rust with multiparty session types. In Jaejin Lee, Kunal Agrawal, and Michael F. Spear, editors, PPoPP '22: 27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, Seoul, Republic of Korea, April 2 - 6, 2022, pages 246-261. ACM, 2022. URL: https://doi.org/10.1145/3503221.3508404.
  15. 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.
  16. Saverio Giallorenzo, Fabrizio Montesi, and Marco Peressotti. Choral: Object-oriented choreographic programming. ACM Trans. Program. Lang. Syst., 46(1):1:1-1:59, 2024. URL: https://doi.org/10.1145/3632398.
  17. Eva Graversen, Andrew K. Hirsch, and Fabrizio Montesi. Alice or bob?: Process polymorphism in choreographies. J. Funct. Program., 34, 2024. URL: https://doi.org/10.1017/S0956796823000114.
  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:1-9:67, 2016. URL: https://doi.org/10.1145/2827695.
  20. 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.
  21. Shun Kashiwa, Gan Shen, Soroush Zare, and Lindsey Kuper. Portable, efficient, and practical library-level choreographic programming. CoRR, abs/2311.11472, 2023. URL: https://doi.org/10.48550/arXiv.2311.11472.
  22. Ivan Lanese, Claudio Guidi, Fabrizio Montesi, and Gianluigi Zavattaro. Bridging the gap between interaction- and process-oriented choreographies. In Antonio Cerone and Stefan Gruner, editors, Sixth IEEE International Conference on Software Engineering and Formal Methods, SEFM 2008, Cape Town, South Africa, 10-14 November 2008, pages 323-332. IEEE Computer Society, 2008. URL: https://doi.org/10.1109/SEFM.2008.11.
  23. Lovro Lugović and Fabrizio Montesi. Real-world choreographic programming: Full-duplex asynchrony and interoperability. The Art, Science, and Engineering of Programming, 8(2), October 2023. URL: https://doi.org/10.22152/programming-journal.org/2024/8/8.
  24. Massimo Merro and Davide Sangiorgi. On asynchrony in name-passing calculi. Mathematical Structures in Computer Science, 14(5):715-767, October 2004. URL: https://doi.org/10.1017/S0960129504004323.
  25. Fabrizio Montesi. Choreographic Programming. Ph.D. thesis, IT University of Copenhagen, 2013. URL: https://www.fabriziomontesi.com/files/choreographic-programming.pdf.
  26. Fabrizio Montesi. Introduction to Choreographies. Cambridge University Press, Cambridge, 2023. Google Scholar
  27. Dan Plyukhin, Marco Peressotti, and Fabrizio Montesi. Ozone: Fully out-of-order choreographies. CoRR, abs/2401.17403, 2024. URL: https://doi.org/10.48550/arXiv.2401.17403.
  28. Johannes Aman 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, 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel, 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.
  29. 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.
  30. Zongyan Qiu, Xiangpeng Zhao, Chao Cai, and Hongli Yang. Towards the theoretical foundation of choreography. In Proceedings of the 16th International Conference on World Wide Web, pages 973-982, Banff Alberta Canada, May 2007. ACM. URL: https://doi.org/10.1145/1242572.1242704.
  31. Michael Scharf and Sebastian Kiesel. Head-of-line Blocking in TCP and SCTP: Analysis and Measurements. In Proceedings of the Global Telecommunications Conference, 2006. GLOBECOM '06, San Francisco, CA, USA, 27 November - 1 December 2006. IEEE, 2006. URL: https://doi.org/10.1109/GLOCOM.2006.333.
  32. Gan Shen, Shun Kashiwa, and Lindsey Kuper. Haschor: Functional choreographic programming for all (functional pearl). Proc. ACM Program. Lang., 7(ICFP):541-565, 2023. URL: https://doi.org/10.1145/3607849.
  33. Malte Viering, Raymond Hu, Patrick Eugster, and Lukasz Ziarek. A multiparty session typing discipline for fault-tolerant event-driven distributed programming. Proc. ACM Program. Lang., 5(OOPSLA):1-30, 2021. URL: https://doi.org/10.1145/3485501.
  34. Stephanie Wang, Eric Liang, Edward Oakes, Benjamin Hindman, Frank Sifei Luan, Audrey Cheng, and Ion Stoica. Ownership: A distributed futures system for fine-grained tasks. In James Mickens and Renata Teixeira, editors, 18th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2021, April 12-14, 2021, pages 671-686. USENIX Association, 2021. URL: https://www.usenix.org/conference/nsdi21/presentation/cheng.
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