Document Open Access Logo

Modular Choreographies: Bridging Alice and Bob Notation to Java

Authors Luís Cruz-Filipe , Anne Madsen, Fabrizio Montesi , Marco Peressotti

PDF
Thumbnail PDF

File

OASIcs.Microservices.2020-2022.3.pdf
  • Filesize: 0.73 MB
  • 18 pages

Document Identifiers

Author Details

Luís Cruz-Filipe
  • University of Southern Denmark, Odense, Denmark
Anne Madsen
  • University of Southern Denmark, Odense, Denmark
Fabrizio Montesi
  • University of Southern Denmark, Odense, Denmark
Marco Peressotti
  • University of Southern Denmark, Odense, Denmark

Funding

  • Montesi, Fabrizio: Work 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, Anne Madsen, Fabrizio Montesi, and Marco Peressotti. Modular Choreographies: Bridging Alice and Bob Notation to Java. In Joint Post-proceedings of the Third and Fourth International Conference on Microservices (Microservices 2020/2022). Open Access Series in Informatics (OASIcs), Volume 111, pp. 3:1-3:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/OASIcs.Microservices.2020-2022.3

Abstract

We present Modular Choreographies, a new choreographic programming language that features modular functions. Modular Choreographies is aimed at simplicity: its communication abstraction follows the simple tradition from the "Alice and Bob" notation. We develop a compiler toolchain that translates choreographies into modular Java libraries, which developers can use to participate correctly in choreographies. The key novelty is to compile through the Choral language, which was previously proposed to define object-oriented choreographies: our toolchain compiles Modular Choreographies to Choral, and then leverages the existing Choral compiler to generate Java code. Our work is the first to bridge the simplicity of traditional choreographic programming languages with the requirement of generating modular libraries in a mainstream language (Java).

Subject Classification

ACM Subject Classification
  • Theory of computation → Distributed computing models
  • Computing methodologies → Distributed programming languages
  • Applied computing → Service-oriented architectures
Keywords
  • Choreographic Programming
  • Choreographies
  • Modularity

Metrics

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

Supplementary Materials

References

  1. Davide Ancona, Viviana Bono, Mario Bravetti, Joana Campos, Giuseppe Castagna, Pierre-Malo Deniélou, Simon J. Gay, Nils Gesbert, Elena Giachino, Raymond Hu, Einar Broch Johnsen, Francisco Martins, Viviana Mascardi, Fabrizio Montesi, Rumyana Neykova, Nicholas Ng, Luca Padovani, Vasco T. Vasconcelos, and Nobuko Yoshida. Behavioral types in programming languages. Foundations and Trends in Programming Languages, 3(2-3):95-230, 2016. URL: https://doi.org/10.1561/2500000031.
  2. Alessandro Bruni, Marco Carbone, Rosario Giustolisi, Sebastian Mödersheim, and Carsten Schürmann. Security protocols as choreographies. In Daniel Dougherty, José Meseguer, Sebastian Alexander Mödersheim, and Paul D. Rowe, editors, Protocols, Strands, and Logic - Essays Dedicated to Joshua Guttman on the Occasion of his 66.66th Birthday, volume 13066 of Lecture Notes in Computer Science, pages 98-111. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-91631-2_5.
  3. Marco Carbone, Kohei Honda, and Nobuko Yoshida. Structured communication-centered programming for web services. ACM Trans. Program. Lang. Syst., 34(2):8, 2012. URL: https://doi.org/10.1145/2220365.2220367.
  4. Marco Carbone and Fabrizio Montesi. Deadlock-freedom-by-design: multiparty asynchronous global programming. In POPL, pages 263-274. ACM, 2013. URL: https://doi.org/10.1145/2429069.2429101.
  5. 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.
  6. Edmund M. Clarke, William Klieber, Milos Novácek, and Paolo Zuliani. Model checking and the state explosion problem. In Bertrand Meyer and Martin Nordio, editors, Tools for Practical Software Verification, LASER, International Summer School 2011, Elba Island, Italy, Revised Tutorial Lectures, volume 7682 of Lecture Notes in Computer Science, pages 1-30. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-35746-6_1.
  7. Luís Cruz-Filipe, Eva Graversen, Fabrizio Montesi, and Marco Peressotti. Reasoning about choreographic programs. In Sung-Shik Jongmans and Antónia Lopes, editors, Coordination Models and Languages - 25th IFIP WG 6.1 International Conference, COORDINATION 2023, Held as Part of the 18th International Federated Conference on Distributed Computing Techniques, DisCoTec 2023, Lisbon, Portugal, June 19-23, 2023, Proceedings, volume 13908 of Lecture Notes in Computer Science, pages 144-162. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-35361-1_8.
  8. Luís Cruz-Filipe, Kim S. Larsen, and Fabrizio Montesi. The paths to choreography extraction. In Javier Esparza and Andrzej S. Murawski, editors, FoSSaCS, volume 10203 of LNCS, pages 424-440. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_25.
  9. Luís Cruz-Filipe, Lovro Lugovic, and Fabrizio Montesi. Certified compilation of choreographies with hacc. In Marieke Huisman and António Ravara, editors, 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, volume 13910 of Lecture Notes in Computer Science, pages 29-36. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-35355-0_3.
  10. Luís Cruz-Filipe and Fabrizio Montesi. Choreographies in practice. In FORTE, volume 9688 of LNCS, pages 114-123. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-39570-8_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 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.
  13. 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.
  14. 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.
  15. 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.
  16. 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.
  17. Mila Dalla Preda, Maurizio Gabbrielli, Saverio Giallorenzo, Ivan Lanese, and Jacopo Mauro. Dynamic choreographies: Theory and implementation. Logical Methods in Computer Science, 13(2), 2017. URL: https://doi.org/10.23638/LMCS-13(2:1)2017.
  18. 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.
  19. Nicola Dragoni, Saverio Giallorenzo, Alberto Lluch Lafuente, Manuel Mazzara, Fabrizio Montesi, Ruslan Mustafin, and Larisa Safina. Microservices: yesterday, today, and tomorrow. In Present and Ulterior Software Engineering, pages 195-216. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-67425-4_12.
  20. Saverio Giallorenzo, Fabrizio Montesi, and Marco Peressotti. Choral: Object-oriented choreographic programming. ACM Trans. Program. Lang. Syst., Nov 2023. Accepted. URL: https://doi.org/10.1145/3632398.
  21. Saverio Giallorenzo, Fabrizio Montesi, Marco Peressotti, David Richter, Guido Salvaneschi, and Pascal Weisenburger. Multiparty languages: The choreographic and multitier cases (pearl). In Anders Møller and Manu Sridharan, editors, 35th European Conference on Object-Oriented Programming, ECOOP 2021, July 11-17, 2021, Aarhus, Denmark (Virtual Conference), volume 194 of LIPIcs, pages 22:1-22:27. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPICS.ECOOP.2021.22.
  22. Andrew K. Hirsch and Deepak Garg. Pirouette: Higher-order typed functional choreographies. Proc. ACM Program. Lang., 6(POPL), jan 2022. URL: https://doi.org/10.1145/3498684.
  23. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty Asynchronous Session Types. J. ACM, 63(1):9, 2016. URL: https://doi.org/10.1145/2827695.
  24. 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.
  25. Sung-Shik Jongmans and Petra van den Bos. A predicate transformer for choreographies - computing preconditions in choreographic programming. In Programming Languages and Systems - 31st European Symposium on Programming, ESOP 2022, Proceedings, volume To appear of Lecture Notes in Computer Science. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99336-8_19.
  26. Tanakorn Leesatapornwongsa, Jeffrey F. Lukman, Shan Lu, and Haryadi S. Gunawi. TaxDC: A taxonomy of non-deterministic concurrency bugs in datacenter distributed systems. In ASPLOS, pages 517-530. ACM, 2016. URL: https://doi.org/10.1145/2872362.2872374.
  27. 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 - Essays dedicated to José Meseguer on the Occasion of His 65th Birthday, 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.
  28. 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, Proceedings of the Symposium on Applied Computing, SAC 2017, Marrakech, Morocco, April 3-7, 2017, pages 437-443. ACM, 2017. URL: https://doi.org/10.1145/3019612.3019656.
  29. Hugo A. López, Flemming Nielson, and Hanne Riis Nielson. Enforcing availability in failure-aware communicating systems. In Elvira Albert and Ivan Lanese, editors, Formal Techniques for Distributed Objects, Components, and Systems - 36th IFIP WG 6.1 International Conference, FORTE 2016, Held as Part of the 11th International Federated Conference on Distributed Computing Techniques, DisCoTec 2016, Heraklion, Crete, Greece, June 6-9, 2016, Proceedings, volume 9688 of Lecture Notes in Computer Science, pages 195-211. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-39570-8_13.
  30. Lovro Lugovic and Fabrizio Montesi. Real-world choreographic programming: An experience report. CoRR, abs/2303.03983, 2023. URL: https://doi.org/10.48550/ARXIV.2303.03983.
  31. Fabrizio Montesi. Choreographic Programming. Ph.D. Thesis, IT University of Copenhagen, 2013. URL: https://www.fabriziomontesi.com/files/choreographic-programming.pdf.
  32. Fabrizio Montesi. Introduction to Choreographies. Cambridge University Press, 2023. Google Scholar
  33. R.M. Needham and M.D. Schroeder. Using encryption for authentication in large networks of computers. Commun. ACM, 21(12):993-999, dec 1978. URL: https://doi.org/10.1145/359657.359659.
  34. Nicholas Ng and Nobuko Yoshida. Pabble: parameterised scribble. Serv. Oriented Comput. Appl., 9(3-4):269-284, 2015. URL: https://doi.org/10.1007/S11761-014-0172-8.
  35. Peter W. O'Hearn. Experience developing and deploying concurrency analysis at facebook. In Andreas Podelski, editor, Static Analysis - 25th International Symposium, SAS 2018, Freiburg, Germany, August 29-31, 2018, Proceedings, volume 11002 of Lecture Notes in Computer Science, pages 56-70. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-99725-4_5.
  36. Kirstin Peters and Nobuko Yoshida. On the expressiveness of mixed choice sessions. In Valentina Castiglioni and Claudio Antares Mezzina, editors, Proceedings Combined 29th International Workshop on Expressiveness in Concurrency and 19th Workshop on Structural Operational Semantics, EXPRESS/SOS 2022, and 19th Workshop on Structural Operational Semantics Warsaw, Poland, 12th September 2022, volume 368 of EPTCS, pages 113-130, 2022. URL: https://doi.org/10.4204/EPTCS.368.7.
  37. Benjamin C. Pierce. Types and Programming Languages. MIT Press, MA, USA, 2002. Google Scholar
  38. 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, 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.
  39. Alceste Scalas, Ornela Dardha, Raymond Hu, and Nobuko Yoshida. A linear decomposition of multiparty sessions for safe distributed programming. 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 24:1-24:31. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPICS.ECOOP.2017.24.
  40. Gan Shen, Shun Kashiwa, and Lindsey Kuper. Haschor: Functional choreographic programming for all (functional pearl). CoRR, abs/2303.00924, 2023. URL: https://doi.org/10.48550/ARXIV.2303.00924.
  41. Ton Smeele and Sung-Shik Jongmans. Choreographic programming of isolated transactions. Electronic Proceedings in Theoretical Computer Science, 378:49-60, apr 2023. URL: https://doi.org/10.4204/EPTCS.378.5.
  42. Vasco T. Vasconcelos, Francisco Martins, Hugo-Andrés López, and Nobuko Yoshida. A type discipline for message passing parallel programs. ACM Trans. Program. Lang. Syst., 44(4):26:1-26:55, 2022. URL: https://doi.org/10.1145/3552519.
  43. 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.
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