Document Open Access Logo

Unreliability in Practical Subclasses of Communicating Systems

Authors Amrita Suresh , Nobuko Yoshida

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSTTCS.2025.52.pdf
  • Filesize: 1.33 MB
  • 22 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
  • Theory of computation → Distributed computing models
  • Theory of computation → Automata extensions
Keywords
  • Communicating automata
  • lossy channel
  • corruption
  • out of order
  • session types
  • crash-stop failure

Metrics

Abstract

Systems of communicating automata are prominent models for peer-to-peer message-passing over unbounded channels, but in the general scenario, most verification properties are undecidable. To address this issue, two decidable subclasses, Realisable with Synchronous Communication (RSC) and k-Multiparty Compatibility (k-MC), were proposed in the literature, with corresponding verification tools developed and applied in practice. Unfortunately, both RSC and k-MC are not resilient under failures: (1) their decidability relies on the assumption of perfect channels and (2) most standard protocols do not satisfy RSC or k-MC under failures. To address these limitations, this paper studies the resilience of RSC and k-MC under two distinct failure models: interference and crash-stop failures. For interference, we relax the conditions of RSC and k-MC and prove that the inclusions of these relaxed properties remain decidable under interference, preserving their known complexity bounds. We then propose a novel crash-handling communicating system that captures wider behaviours than existing multiparty session types (MPST) with crash-stop failures. We study a translation of MPST with crash-stop failures into this system integrating RSC and k-MC properties, and establish their decidability results. Finally, by verifying representative protocols from the literature using RSC and k-MC tools extended to interferences, we evaluate the relaxed systems and demonstrate their resilience.

Cite As Get BibTex

Amrita Suresh and Nobuko Yoshida. Unreliability in Practical Subclasses of Communicating Systems. In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 52:1-52:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.FSTTCS.2025.52

Author Details

Amrita Suresh
  • University of Oxford, UK
Nobuko Yoshida
  • University of Oxford, UK

Funding

This work is supported by EPSRC EP/T006544/2, EP/T014709/2, EP/Y005244/1, EP/V000462/1, EP/X015955/1, EP/Z0005801/1, EU Horizon TARDIS 101093006 (UKRI number 10066667) and ARIA.

Acknowledgements

We thank Martin Vassor for his comments on an early version of this paper.

Supplementary Materials

References

  1. P. Abdulla and B. Jonsson. Verifying programs with unreliable channels. In [1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science, pages 160-170, June 1993. URL: https://doi.org/10.1109/LICS.1993.287591.
  2. 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, pages 1-16, Cham, 2017. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-60225-7_1.
  3. Adam D. Barwell, Ping Hou, Nobuko Yoshida, and Fangyi Zhou. Designing Asynchronous Multiparty Protocols With Crash Stop Failures. In European Conference on Object Oriented Programming, volume 263, pages 1:1-1:30, 2023. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2023.1.
  4. Adam D. Barwell, Ping Hou, Nobuko Yoshida, and Fangyi Zhou. Designing Asynchronous Multiparty Protocols with Crash-Stop Failures, May 2023. arXiv:2305.06238 [cs]. URL: https://doi.org/10.48550/arXiv.2305.06238.
  5. Adam D. Barwell, Ping Hou, Nobuko Yoshida, and Fangyi Zhou. Crash-Stop Failures in Asynchronous Multiparty Session Types. Logical Methods in Computer Science, 2025. URL: https://arxiv.org/abs/2311.11851.
  6. Adam D. Barwell, Alceste Scalas, Nobuko Yoshida, and Fangyi Zhou. Generalised Multiparty Session Types with Crash-Stop Failures. In Bartek Klin, Slawomir 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. ISSN: 1868-8969. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2022.35.
  7. Bernard Boigelot and Patrice Godefroid. Symbolic verification of communication protocols with infinite state spaces using QDDs. In Rajeev Alur and Thomas A. Henzinger, editors, Computer Aided Verification, Lecture Notes in Computer Science, pages 1-12, Berlin, Heidelberg, 1996. Springer. URL: https://doi.org/10.1007/3-540-61474-5_53.
  8. Benedikt Bollig, Cinzia Di Giusto, Alain Finkel, Laetitia Laversa, Etienne Lozes, and Amrita Suresh. A Unifying Framework for Deciding Synchronizability. In Serge Haddad and Daniele Varacca, editors, 32nd International Conference on Concurrency Theory (CONCUR 2021), volume 203 of Leibniz International Proceedings in Informatics (LIPIcs), pages 14:1-14:18, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. ISSN: 1868-8969. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2021.14.
  9. Benedikt Bollig, Dietrich Kuske, and Ingmar Meinecke. Propositional Dynamic Logic for Message-Passing Systems. Logical Methods in Computer Science, Volume 6, Issue 3, September 2010. URL: https://doi.org/10.2168/LMCS-6(3:16)2010.
  10. Ahmed Bouajjani, Constantin Enea, Kailiang Ji, and Shaz Qadeer. On the Completeness of Verifying Message Passing Programs Under Bounded Asynchrony. In Hana Chockler and Georg Weissenbacher, editors, Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II, Lecture Notes in Computer Science, pages 372-391, Cham, 2018. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-96142-2_23.
  11. Daniel Brand and Pitro Zafiropulo. On Communicating Finite-State Machines. J. ACM, 30(2):323-342, April 1983. URL: https://doi.org/10.1145/322374.322380.
  12. Zak Cutner, Nobuko Yoshida, and Martin Vassor. Deadlock-free asynchronous message reordering in Rust with multiparty session types. In Proceedings of the 27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP '22, pages 246-261, New York, NY, USA, March 2022. Association for Computing Machinery. URL: https://doi.org/10.1145/3503221.3508404.
  13. Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, and Filip Mazowiecki. The Reachability Problem for Petri Nets Is Not Elementary. J. ACM, 68(1):7:1-7:28, 2021. URL: https://doi.org/10.1145/3422822.
  14. Gérard Cécé and Alain Finkel. Verification of programs with half-duplex communication. Information and Computation, 202(2):166-190, November 2005. URL: https://doi.org/10.1016/j.ic.2005.05.006.
  15. Pierre-Malo Deniélou and Nobuko Yoshida. Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session Types. In Fedor V. Fomin, Rūsiņš Freivalds, Marta Kwiatkowska, and David Peleg, editors, Automata, Languages, and Programming, Lecture Notes in Computer Science, pages 174-186, Berlin, Heidelberg, 2013. Springer. URL: https://doi.org/10.1007/978-3-642-39212-2_18.
  16. Loïc Desgeorges and Loïc Germerie Guizouarn. RSC to the ReSCu: Automated Verification of Systems of Communicating Automata. In Sung-Shik Jongmans and Antónia Lopes, editors, Coordination Models and Languages, Lecture Notes in Computer Science, pages 135-143, Cham, 2023. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-031-35361-1_7.
  17. Cinzia Di Giusto, Loïc Germerie Guizouarn, and Etienne Lozes. Multiparty half-duplex systems and synchronous communications. Journal of Logical and Algebraic Methods in Programming, 131:100843, February 2023. URL: https://doi.org/10.1016/j.jlamp.2022.100843.
  18. Cinzia Di Giusto, Loïc Germerie Guizouarn, and Etienne Lozes. Towards Generalised Half-Duplex Systems. Electron. Proc. Theor. Comput. Sci., 347:22-37, October 2021. arXiv:2110.00145 [cs]. URL: https://doi.org/10.4204/EPTCS.347.2.
  19. Cinzia Di Giusto, Laetitia Laversa, and Etienne Lozes. On the k-synchronizability of Systems. In Jean Goubault-Larrecq and Barbara König, editors, Foundations of Software Science and Computation Structures - 23rd International Conference, FOSSACS 2020, Proceedings, Lecture Notes in Computer Science, pages 157-176, Cham, 2020. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-45231-5_9.
  20. Alan Fekete, Nancy Lynch, Yishay Mansour, and John Spinelli. The impossibility of implementing reliable communication in the face of crashes. J. ACM, 40(5):1087-1107, November 1993. URL: https://doi.org/10.1145/174147.169676.
  21. Alain Finkel. Decidability of the termination problem for completely specified protocols. Distrib Comput, 7(3):129-135, March 1994. URL: https://doi.org/10.1007/BF02277857.
  22. 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.
  23. Blaise Genest, Dietrich Kuske, and Anca Muscholl. On Communicating Automata with Bounded Channels. Fundamenta Informaticae, 80(1-3):147-167, January 2007. Publisher: IOS Press. URL: https://content.iospress.com/articles/fundamenta-informaticae/fi80-1-3-09.
  24. Blaise Genest, Anca Muscholl, and Dietrich Kuske. A Kleene Theorem for a Class of Communicating Automata with Effective Algorithms. In Cristian Calude, Elena Calude, and Michael J. Dinneen, editors, Developments in Language Theory, 8th International Conference, DLT 2004, Auckland, New Zealand, December 13-17, 2004, Proceedings, volume 3340 of Lecture Notes in Computer Science, pages 30-48. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30550-7_4.
  25. Matthias Güdemann, Gwen Salaün, and Meriem Ouederni. Counterexample guided synthesis of monitors for realizability enforcement. In ATVA 2012, pages 238-253, 2012. URL: https://doi.org/10.1007/978-3-642-33386-6_20.
  26. Sylvain Hallé and Tevfik Bultan. Realizability analysis for message-based interactions using shared-state projections. In SIGSOFT 2010, pages 27-36, 2010. URL: https://doi.org/10.1145/1882291.1882298.
  27. Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. Language primitives and type disciplines for structured communication-based programming. In Proceedings of ESOP 1998, volume 1381 of Lecture Notes in Computer Science, pages 22-138. Springer, 1998. Google Scholar
  28. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL '08, pages 273-284, New York, NY, USA, January 2008. Association for Computing Machinery. URL: https://doi.org/10.1145/1328438.1328472.
  29. Ping Hou, Nicolas Lagaillardie, and Nobuko Yoshida. Fearless Asynchronous Communications with Timed Multiparty Session Protocols. In ECOOP 2024. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2024.19.
  30. Keigo Imai, Julien Lange, and Rumyana Neykova. Kmclib: Automated inference and verification of session types from OCaml programs. In Dana Fisman and Grigore Rosu, editors, Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I, volume 13243 of Lecture Notes in Computer Science, pages 379-386. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99524-9_20.
  31. Shokoufeh Kazemlou and Borzoo Bonakdarpour. Crash-Resilient Decentralized Synchronous Runtime Verification. In 2018 IEEE 37th Symposium on Reliable Distributed Systems (SRDS), pages 207-212, October 2018. ISSN: 2575-8462. URL: https://doi.org/10.1109/SRDS.2018.00032.
  32. Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida. Stay Safe under Panic: Affine Rust Programming with Multiparty Session Types. In 36th European Conference on Object-Oriented Programming, volume 222 of LIPIcs, pages 4:1-4:29. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2022.4.
  33. Leslie Lamport. The part-time parliament. ACM Trans. Comput. Syst., 16(2):133-169, 1998. URL: https://doi.org/10.1145/279227.279229.
  34. Julien Lange, Emilio Tuosto, and Nobuko Yoshida. From communicating machines to graphical choreographies. In POPL 2015, pages 221-232, 2015. URL: https://doi.org/10.1145/2676726.2676964.
  35. Julien Lange and Nobuko Yoshida. Verifying Asynchronous Interactions via Communicating Session Automata. In Isil Dillig and Serdar Tasiran, editors, Computer Aided Verification, Lecture Notes in Computer Science, pages 97-117, Cham, 2019. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-25540-4_6.
  36. Markus Lohrey and Anca Muscholl. Bounded MSC Communication. In Mogens Nielsen and Uffe Engberg, editors, Foundations of Software Science and Computation Structures, 5th International Conference, FOSSACS 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8-12, 2002, Proceedings, volume 2303 of Lecture Notes in Computer Science, pages 295-309. Springer, 2002. URL: https://doi.org/10.1007/3-540-45931-6_21.
  37. Etienne Lozes and Jules Villard. Reliable Contracts for Unreliable Half-Duplex Communications. In Marco Carbone and Jean-Marc Petit, editors, Web Services and Formal Methods, Lecture Notes in Computer Science, pages 2-16, Berlin, Heidelberg, 2012. Springer. URL: https://doi.org/10.1007/978-3-642-29834-9_2.
  38. Dimitris Mostrous and Vasco Thudichum Vasconcelos. Affine sessions. In International Conference on Coordination Languages and Models, pages 115-130, Berlin, Heidelberg, 2014. Springer. URL: https://doi.org/10.1007/978-3-662-43376-8_8.
  39. OMG. Business Process Model and Notation, 2018. URL: https://www.omg.org/spec/BPMN/2.0/.
  40. Roly Perera, Julien Lange, and Simon J. Gay. Multiparty compatibility for concurrent objects. In PLACES 2016, pages 73-82, 2016. URL: https://doi.org/10.4204/EPTCS.211.8.
  41. Introduction to protocol engineering. Available at http://cs.uccs.edu/~cs522/pe/pe.htm, 2006.
  42. Gwen Salaün, Lucas Bordeaux, and Marco Schaerf. Describing and reasoning on web services using process algebra. IJBPIM, 1(2):116-128, 2006. URL: https://doi.org/10.1504/IJBPIM.2006.010025.
  43. 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.
  44. Philippe Schnoebelen. Verifying lossy channel systems has nonprimitive recursive complexity. Inf. Process. Lett., 83(5):251-261, 2002. URL: https://doi.org/10.1016/S0020-0190(01)00337-4.
  45. Amrita Suresh and Nobuko Yoshida. The full version of this paper, 2025. Google Scholar
  46. Kaku Takeuchi, Kohei Honda, and Makoto Kubo. An Interaction-based Language and its Typing System. In PARLE'94, volume 817 of Lecture Notes in Computer Science, pages 398-413, 1994. URL: https://doi.org/10.1007/3-540-58184-7_118.
  47. Martin Vassor and Nobuko Yoshida. Refinements for multiparty message-passing protocols: Specification-agnostic theory and implementation. In Jonathan Aldrich and Guido Salvaneschi, editors, 38th European Conference on Object-Oriented Programming, ECOOP 2024, September 16-20, 2024, Vienna, Austria, volume 313 of LIPIcs, pages 41:1-41:29. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPICS.ECOOP.2024.41.
  48. 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.
  49. Daniel M. Yellin and Robert E. Strom. Protocol specifications and component adaptors. ACM Trans. Program. Lang. Syst., 19(2):292-333, 1997. URL: https://doi.org/10.1145/244795.244801.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact