Document Open Access Logo

Generalised Multiparty Session Types with Crash-Stop Failures

Authors Adam D. Barwell , Alceste Scalas , Nobuko Yoshida , Fangyi Zhou

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2022.35.pdf
  • Filesize: 1.1 MB
  • 25 pages

Document Identifiers

Author Details

Adam D. Barwell
  • Imperial College London, UK
Alceste Scalas
  • DTU Compute, Technical University of Denmark, Lyngby, Denmark
Nobuko Yoshida
  • Imperial College London, UK
Fangyi Zhou
  • Imperial College London, UK

Funding

Work supported by: EU Horizon 2020 project 830929; EPSRC grants EP/K011715/1, EP/K034413/1, EP/L00058X/1, EP/N027833/1, EP/N028201/1, EP/T006544/1, EP/T014709/1, EP/V000462/1, and NCSS/EPSRC VeTSS; Danmarks Industriens Fond 2020-0489.

Cite AsGet BibTex

Adam D. Barwell, Alceste Scalas, Nobuko Yoshida, and Fangyi Zhou. Generalised Multiparty Session Types with Crash-Stop Failures. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 35:1-35:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.CONCUR.2022.35

Abstract

Session types enable the specification and verification of communicating systems. However, their theory often assumes that processes never fail. To address this limitation, we present a generalised multiparty session type (MPST) theory with crash-stop failures, where processes can crash arbitrarily. Our new theory validates more protocols and processes w.r.t. previous work. We apply minimal syntactic changes to standard session π-calculus and types: we model crashes and their handling semantically, with a generalised MPST typing system parametric on a behavioural safety property. We cover the spectrum between fully reliable and fully unreliable sessions, via optional reliability assumptions, and prove type safety and protocol conformance in the presence of crash-stop failures. Introducing crash-stop failures has non-trivial consequences: writing correct processes that handle all crash scenarios can be difficult. Yet, our generalised MPST theory allows us to tame this complexity, via model checking, to validate whether a multiparty session satisfies desired behavioural properties, e.g. deadlock-freedom or liveness, even in presence of crashes. We implement our approach using the mCRL2 model checker, and evaluate it with examples extended from the literature.

Subject Classification

ACM Subject Classification
  • Theory of computation → Distributed computing models
  • Theory of computation → Process calculi
  • Software and its engineering → Model checking
Keywords
  • Session Types
  • Concurrency
  • Failure Handling
  • Model Checking

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. Roberto M. Amadio. An asynchronous model of locality, failure and process mobility. In David Garlan and Daniel Le Métayer, editors, Coordination Languages and Models, Second International Conference, COORDINATION '97, Berlin, Germany, September 1-3, 1997, Proceedings, volume 1282 of Lecture Notes in Computer Science, pages 374-391. Springer, 1997. URL: https://doi.org/10.1007/3-540-63383-9_92.
  3. Adam D. Barwell, Alceste Scalas, Nobuko Yoshida, and Fangyi Zhou. Generalised Multiparty Session Types with Crash-Stop Failures, 2022. URL: https://doi.org/10.48550/arXiv.2207.02015.
  4. 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
  5. 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.
  6. Luís Caires and Jorge A. Pérez. Linearity, Control Effects, and Behavioral Types. In Hongseok Yang, editor, Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10201 of Lecture Notes in Computer Science, pages 229-259. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54434-1_9.
  7. Sara Capecchi, Elena Giachino, and Nobuko Yoshida. Global escape in multiparty sessions. Math. Struct. Comput. Sci., 26(2):156-205, 2016. URL: https://doi.org/10.1017/S0960129514000164.
  8. Marco Carbone, Kohei Honda, and Nobuko Yoshida. Structured Interactional Exceptions in Session Types. In Franck van Breugel and Marsha Chechik, editors, CONCUR 2008 - Concurrency Theory, 19th International Conference, CONCUR 2008, Toronto, Canada, August 19-22, 2008. Proceedings, volume 5201 of Lecture Notes in Computer Science, pages 402-417. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-85361-9_32.
  9. Ilaria Castellani. Process algebras with localities. In Jan A. Bergstra, Alban Ponse, and Scott A. Smolka, editors, Handbook of Process Algebra, pages 945-1045. North-Holland / Elsevier, 2001. URL: https://doi.org/10.1016/b978-044482830-9/50033-3.
  10. Sagar Chaki, Sriram K. Rajamani, and Jakob Rehof. Types as models: Model checking message-passing programs. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '02, pages 45-57, New York, NY, USA, 2002. Association for Computing Machinery. URL: https://doi.org/10.1145/503272.503278.
  11. 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.
  12. Tzu-Chun Chen, Malte Viering, Andi Bejleri, Lukasz Ziarek, and Patrick Eugster. A Type Theory for Robust Failure Handling in Distributed 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 96-113. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-39570-8_7.
  13. Mario Coppo, Mariangiola Dezani-Ciancaglini, Nobuko Yoshida, and Luca Padovani. Global progress for dynamically interleaved multiparty sessions. MSCS, 760, 2015. URL: https://doi.org/10.1017/S0960129514000188.
  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. Julia Gabet and Nobuko Yoshida. Static Race Detection and Mutex Safety and Liveness for Go Programs. In Robert Hirschfeld and Tobias Pape, editors, 34th European Conference on Object-Oriented Programming (ECOOP 2020), volume 166 of Leibniz International Proceedings in Informatics (LIPIcs), pages 4:1-4:30, Dagstuhl, Germany, 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2020.4.
  16. Simon Gay and António Ravara. Behavioural Types: From Theory to Tools. River Publishers, Series in Automation, Control and Robotics, 2017. URL: https://doi.org/10.13052/rp-9788793519817.
  17. 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.
  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, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In POPL, 2008. Full version in [Honda et al., 2016]. URL: https://doi.org/10.1145/1328438.1328472.
  20. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty Asynchronous Session Types. J. ACM, 63(1), 2016. URL: https://doi.org/10.1145/2827695.
  21. Raymond Hu and Nobuko Yoshida. Explicit Connection Actions in Multiparty Session Types. In FASE, 2017. URL: https://doi.org/10.1007/978-3-662-54494-5_7.
  22. Naoki Kobayashi and Davide Sangiorgi. A Hybrid Type System for Lock-Freedom of Mobile Processes. TOPLAS, 32(5), 2010. URL: https://doi.org/10.1145/1745312.1745313.
  23. Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida. A Static Verification Framework for Message Passing in Go Using Behavioural Types. In 2018 IEEE/ACM 40th International Conference on Software Engineering (ICSE), pages 1137-1148, 2018. URL: https://doi.org/10.1145/3180155.3180157.
  24. 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.
  25. Rumyana Neykova and Nobuko Yoshida. Let It Recover: Multiparty Protocol-Induced Recovery. In CC, 2017. URL: https://doi.org/10.1145/3033019.3033031.
  26. 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 - 42nd IFIP WG 6.1 International Conference, FORTE 2022, Held as Part of the 17th International Federated Conference on Distributed Computing Techniques, DisCoTec 2022, Lucca, Italy, June 13-17, 2022, Proceedings, volume 13273 of Lecture Notes in Computer Science, pages 93-113. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-08679-3_7.
  27. James Riely and Matthew Hennessy. Distributed processes and location failures (extended abstract). In Pierpaolo Degano, Roberto Gorrieri, and Alberto Marchetti-Spaccamela, editors, Automata, Languages and Programming, 24th International Colloquium, ICALP'97, Bologna, Italy, 7-11 July 1997, Proceedings, volume 1256 of Lecture Notes in Computer Science, pages 471-481. Springer, 1997. URL: https://doi.org/10.1007/3-540-63165-8_203.
  28. Davide Sangiorgi. Introduction to Bisimulation and Coinduction. Cambridge University Press, 2011. URL: https://doi.org/10.1017/CBO9780511777110.
  29. 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.
  30. Alceste Scalas and Nobuko Yoshida. mpstk: the Multiparty Session Types ToolKit, 2019. Peer-reviewed artifact of [Scalas and Yoshida, 2019]. (Latest version available at: https://alcestes.github.io/mpstk). URL: https://doi.org/10.1145/3291638.
  31. 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.
  32. 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.
  33. 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. Google Scholar
  34. 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.
  35. Fangyi Zhou, Francisco Ferreira, Raymond Hu, Rumyana Neykova, and Nobuko Yoshida. Statically Verified Refinements for Multiparty Protocols. Proc. ACM Program. Lang., 4(OOPSLA):148:1-148:30, 2020. URL: https://doi.org/10.1145/3428216.
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