Document Open Access Logo

Designing Asynchronous Multiparty Protocols with Crash-Stop Failures

Authors Adam D. Barwell , Ping Hou , Nobuko Yoshida , Fangyi Zhou

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2023.1.pdf
  • Filesize: 1.27 MB
  • 30 pages

Document Identifiers

Author Details

Adam D. Barwell
  • University of St. Andrews, UK
  • University of Oxford, UK
Ping Hou
  • University of Oxford, UK
Nobuko Yoshida
  • University of Oxford, UK
Fangyi Zhou
  • Imperial College London, UK
  • University of Oxford, UK

Funding

Work supported by: EPSRC EP/T006544/2, EP/K011715/1, EP/K034413/1, EP/L00058X/1, EP/N027833/2, EP/N028201/1, EP/T014709/2, EP/V000462/1, EP/X015955/1, NCSS/EPSRC VeTSS, and Horizon EU TaRDIS 101093006.

Acknowledgements

We thank the anonymous reviewers for their useful comments and suggestions. We thank Jia Qing Lim for his contribution to the Effpi extension. We thank Alceste Scalas for useful discussions and advice in the development of this paper and for his assistance with Effpi.

Cite AsGet BibTex

Adam D. Barwell, Ping Hou, Nobuko Yoshida, and Fangyi Zhou. Designing Asynchronous Multiparty Protocols with Crash-Stop Failures. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 1:1-1:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ECOOP.2023.1

Abstract

Session types provide a typing discipline for message-passing systems. However, most session type approaches assume an ideal world: one in which everything is reliable and without failures. Yet this is in stark contrast with distributed systems in the real world. To address this limitation, we introduce Teatrino, a code generation toolchain that utilises asynchronous multiparty session types (MPST) with crash-stop semantics to support failure handling protocols. We augment asynchronous MPST and processes with crash handling branches. Our approach requires no user-level syntax extensions for global types and features a formalisation of global semantics, which captures complex behaviours induced by crashed/crash handling processes. The sound and complete correspondence between global and local type semantics guarantees deadlock-freedom, protocol conformance, and liveness of typed processes in the presence of crashes. Our theory is implemented in the toolchain Teatrino, which provides correctness by construction. Teatrino extends the Scribble multiparty protocol language to generate protocol-conforming Scala code, using the Effpi concurrent programming library. We extend both Scribble and Effpi to support crash-stop behaviour. We demonstrate the feasibility of our methodology and evaluate Teatrino with examples extended from both session type and distributed systems literature.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Source code generation
  • Software and its engineering → Concurrent programming languages
  • Theory of computation → Process calculi
  • Theory of computation → Distributed computing models
Keywords
  • Session Types
  • Concurrency
  • Failure Handling
  • Code Generation
  • Scala

Metrics

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

Related Versions

Supplementary Materials

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. Adam D. Barwell, Ping Hou, Nobuko Yoshida, and Fangyi Zhou. Designing Asynchronous Multiparty Protocols with Crash-Stop Failures, 2023. URL: https://arxiv.org/abs/2305.06238.
  3. Adam D. Barwell, Alceste Scalas, Nobuko Yoshida, and Fangyi Zhou. Generalised Multiparty Session Types with Crash-Stop Failures. In Bartek Klin, Sławomir Lasota, and Anca Muscholl, editors, 33rd International Conference on Concurrency Theory (CONCUR 2022), volume 243 of Leibniz International Proceedings in Informatics (LIPIcs), pages 35:1-35:25, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2022.35.
  4. Olivier Blanvillain, Jonathan Immanuel Brachthäuser, Maxime Kjaer, and Martin Odersky. Type-level programming with match types. Proc. ACM Program. Lang., 6(POPL):1-24, 2022. URL: https://doi.org/10.1145/3498698.
  5. Olav Bunte, Jan Friso Groote, Jeroen J. A. Keiren, Maurice Laveaux, Thomas Neele, Erik P. de Vink, Wieger Wesselink, Anton Wijs, and Tim A. C. Willemse. The mCRL2 Toolset for Analysing Concurrent Systems. In Tomáš Vojnar and Lijun Zhang, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 21-39, Cham, 2019. Springer International Publishing. Google Scholar
  6. Christian Cachin, Rachid Guerraoui, and Luís E. T. Rodrigues. Introduction to Reliable and Secure Distributed Programming (2. ed.). Springer, 2011. URL: https://doi.org/10.1007/978-3-642-15260-3.
  7. David Castro-Perez, Raymond Hu, Sung-Shik Jongmans, Nicholas Ng, and Nobuko Yoshida. Distributed programming using role-parametric session types in go: statically-typed endpoint APIs for dynamically-instantiated communication structures. Proc. ACM Program. Lang., 3(POPL):29:1-29:30, 2019. URL: https://doi.org/10.1145/3290342.
  8. Tushar Deepak Chandra and Sam Toueg. Unreliable Failure Detectors for Reliable Distributed Systems. J. ACM, 43(2):225-267, March 1996. URL: https://doi.org/10.1145/226643.226647.
  9. Guillermina Cledou, Luc Edixhoven, Sung-Shik Jongmans, and José Proença. API Generation for Multiparty Session Types, Revisited and Revised Using Scala 3. In Karim Ali and Jan Vitek, editors, 36th European Conference on Object-Oriented Programming (ECOOP 2022), volume 222 of Leibniz International Proceedings in Informatics (LIPIcs), pages 27:1-27:28, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://drops.dagstuhl.de/opus/volltexte/2022/16255.
  10. Zak Cutner, Nobuko Yoshida, and Martin Vassor. Deadlock-Free Asynchronous Message Reordering in Rust with Multiparty Session Types. In 27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, volume abs/2112.12693 of PPoPP '22, pages 261-246. ACM, 2022. URL: https://doi.org/10.1145/3503221.3508404.
  11. Romain Demangeon, Kohei Honda, Raymond Hu, Rumyana Neykova, and Nobuko Yoshida. Practical interruptible conversations: distributed dynamic verification with multiparty session types and Python. Formal Methods Syst. Des., 46(3):197-225, 2015. URL: https://doi.org/10.1007/s10703-014-0218-8.
  12. Romain Demangeon and Nobuko Yoshida. On the Expressiveness of Multiparty Sessions. In Prahladh Harsha and G. Ramalingam, editors, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015), volume 45 of Leibniz International Proceedings in Informatics (LIPIcs), pages 560-574, Dagstuhl, Germany, 2015. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2015.560.
  13. Pierre-Malo Deniélou and Nobuko Yoshida. Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session Types. In 40th International Colloquium on Automata, Languages and Programming, volume 7966 of LNCS, pages 174-186, Berlin, Heidelberg, 2013. Springer. URL: https://doi.org/10.1007/978-3-642-39212-2_18.
  14. Simon Fowler, Sam Lindley, J. Garrett Morris, and Sára Decova. Exceptional Asynchronous Session Types: Session Types without Tiers. Proc. ACM Program. Lang., 3(POPL):28:1-28:29, 2019. URL: https://doi.org/10.1145/3290341.
  15. Silvia Ghilezan, Svetlana Jaksic, Jovanka Pantovic, Alceste Scalas, and Nobuko Yoshida. Precise subtyping for synchronous multiparty sessions. J. Log. Algebraic Methods Program., 104:127-173, 2019. URL: https://doi.org/10.1016/j.jlamp.2018.12.002.
  16. Silvia Ghilezan, Jovanka Pantović, Ivan Prokić, Alceste Scalas, and Nobuko Yoshida. Precise Subtyping for Asynchronous Multiparty Sessions. Proc. ACM Program. Lang., 5(POPL), January 2021. URL: https://doi.org/10.1145/3434297.
  17. Saverio Giallorenzo, Fabrizio Montesi, and Marco Peressotti. Choreographies as objects. CoRR, abs/2005.09520, 2020. URL: https://arxiv.org/abs/2005.09520.
  18. Paul Harvey, Simon Fowler, Ornela Dardha, and Simon J. Gay. Multiparty Session Types for Safe Runtime Adaptation in an Actor Language. In Anders Møller and Manu Sridharan, editors, 35th European Conference on Object-Oriented Programming (ECOOP 2021), volume 194 of Leibniz International Proceedings in Informatics (LIPIcs), pages 10:1-10:30, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2021.10.
  19. Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In Chris Hankin, editor, Programming Languages and Systems, pages 122-138, Berlin, Heidelberg, 1998. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/BFb0053567.
  20. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty Asynchronous Session Types. In 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 273-284. ACM, 2008. URL: https://doi.org/10.1145/1328897.1328472.
  21. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty Asynchronous Session Types. Journal of the ACM, 63:1-67, 2016. URL: https://doi.org/10.1145/2827695.
  22. Raymond Hu and Nobuko Yoshida. Hybrid Session Verification through Endpoint API Generation. In 19th International Conference on Fundamental Approaches to Software Engineering, volume 9633 of LNCS, pages 401-418, Berlin, Heidelberg, 2016. Springer. URL: https://doi.org/10.1007/978-3-662-49665-7_24.
  23. Raymond Hu, Nobuko Yoshida, and Kohei Honda. Session-Based Distributed Programming in Java. In Jan Vitek, editor, ECOOP 2008 - Object-Oriented Programming, 22nd European Conference, Paphos, Cyprus, July 7-11, 2008, Proceedings, volume 5142 of Lecture Notes in Computer Science, pages 516-541. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-70592-5_22.
  24. Dimitrios Kouzapas, Ornela Dardha, Roly Perera, and Simon J. Gay. Typechecking protocols with mungo and stmungo. In James Cheney and Germán Vidal, editors, Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, Edinburgh, United Kingdom, September 5-7, 2016, pages 146-159. ACM, 2016. URL: https://doi.org/10.1145/2967973.2968595.
  25. Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida. Implementing Multiparty Session Types in Rust. In Simon Bliudze and Laura Bocchi, editors, Coordination Models and Languages - 22nd IFIP WG 6.1 International Conference, COORDINATION 2020, Held as Part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Valletta, Malta, June 15-19, 2020, Proceedings, volume 12134 of Lecture Notes in Computer Science, pages 127-136. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-50029-0_8.
  26. Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida. Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types. In Karim Ali and Jan Vitek, editors, 36th European Conference on Object-Oriented Programming (ECOOP 2022), volume 222 of Leibniz International Proceedings in Informatics (LIPIcs), pages 4:1-4:29, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://drops.dagstuhl.de/opus/volltexte/2022/16232.
  27. Matthew Alan Le Brun and Ornela Dardha. MAGπ: Types for Failure-Prone Communication. In Thomas Wies, editor, Programming Languages and Systems, pages 363-391, Cham, 2023. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-031-30044-8_14.
  28. Anson Miu, Francisco Ferreira, Nobuko Yoshida, and Fangyi Zhou. Communication-Safe Web Programming in TypeScript with Routed Multiparty Session Types. In International Conference on Compiler Construction, CC, pages 94-106, 2021. URL: https://doi.org/10.1145/3446804.3446854.
  29. Dimitris Mostrous and Vasco T. Vasconcelos. Affine Sessions. Logical Methods in Computer Science, Volume 14, Issue 4, November 2018. URL: https://doi.org/10.23638/LMCS-14(4:14)2018.
  30. Rumyana Neykova and Nobuko Yoshida. Multiparty Session Actors. Logical Methods in Computer Science, 13:1-30, 2017. URL: https://doi.org/10.23638/LMCS-13(1:17)2017.
  31. Rumyana Neykova and Nobuko Yoshida. Featherweight Scribble, pages 236-259. Springer International Publishing, Cham, 2019. URL: https://doi.org/10.1007/978-3-030-21485-2_14.
  32. Rumyana Neykova, Nobuko Yoshida, and Raymond Hu. SPY: Local Verification of Global Protocols. In Axel Legay and Saddek Bensalem, editors, Runtime Verification, pages 358-363, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-40787-1_25.
  33. Kirstin Peters, Uwe Nestmann, and Christoph Wagner. Fault-tolerant multiparty session types. In Mohammad Reza Mousavi and Anna Philippou, editors, Formal Techniques for Distributed Objects, Components, and Systems, pages 93-113, Cham, 2022. Springer International Publishing. URL: https://doi.org/10.1007/978-3-031-08679-3_7.
  34. Benjamin C. Pierce. Types and Programming Languages. The MIT Press, 1st edition, 2002. Google Scholar
  35. Davide Sangiorgi. Introduction to Bisimulation and Coinduction. Cambridge University Press, 2011. URL: https://doi.org/10.1017/CBO9780511777110.
  36. 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), volume 74 of Leibniz International Proceedings in Informatics (LIPIcs), pages 24:1-24:31, Dagstuhl, Germany, 2017. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2017.24.
  37. Alceste Scalas and Nobuko Yoshida. Less is More: Multiparty Session Types Revisited. Proc. ACM Program. Lang., 3(POPL):30:1-30:29, January 2019. URL: https://doi.org/10.1145/3290343.
  38. Alceste Scalas, Nobuko Yoshida, and Elias Benussi. Verifying Message-Passing Programs with Dependent Behavioural Types. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, pages 502-516, New York, NY, USA, 2019. Association for Computing Machinery. URL: https://doi.org/10.1145/3314221.3322484.
  39. Alceste Scalas, Nobuko Yoshida, and Elias Benussi. Effpi: verified message-passing programs in Dotty. In Jonathan Immanuel Brachthäuser, Sukyoung Ryu, and Nathaniel Nystrom, editors, Proceedings of the Tenth ACM SIGPLAN Symposium on Scala, Scala@ECOOP 2019, London, UK, July 17, 2019, pages 27-31. ACM, 2019. URL: https://doi.org/10.1145/3337932.3338812.
  40. Rob van Glabbeek, Peter Höfner, and Ross Horne. Assuming Just Enough Fairness to make Session Types Complete for Lock-freedom. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1-13. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470531.
  41. Malte Viering, Tzu-Chun Chen, Patrick Eugster, Raymond Hu, and Lukasz Ziarek. A Typing Discipline for Statically Verified Crash Failure Handling in Distributed Systems. In Amal Ahmed, editor, Programming Languages and Systems, pages 799-826, Cham, 2018. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-89884-1_28.
  42. 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), October 2021. URL: https://doi.org/10.1145/3485501.
  43. Nobuko Yoshida, Raymond Hu, Rumyana Neykova, and Nicholas Ng. The scribble protocol language. In 8th International Symposium on Trustworthy Global Computing - Volume 8358, TGC 2013, pages 22-41, Berlin, Heidelberg, 2014. Springer-Verlag. 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