LIPIcs.CONCUR.2024.22.pdf
- Filesize: 1.07 MB
- 19 pages
Document
An Automata-Based Approach for Synchronizable Mailbox Communication
Authors
Romain Delpy 
,
Anca Muscholl ,
-
Part of:
Volume:
35th International Conference on Concurrency Theory (CONCUR 2024)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Concurrency Theory (CONCUR) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2024-08-29
File
Document Identifiers
Author Details
Cite AsGet BibTex
Romain Delpy, Anca Muscholl, and Grégoire Sutre. An Automata-Based Approach for Synchronizable Mailbox Communication. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 22:1-22:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CONCUR.2024.22
https://doi.org/10.4230/LIPIcs.CONCUR.2024.22
Abstract
We revisit finite-state communicating systems with round-based communication under mailbox semantics. Mailboxes correspond to one FIFO buffer per process (instead of one buffer per pair of processes in peer-to-peer systems). Round-based communication corresponds to sequences of rounds in which processes can first send messages, then only receive (and receives must be in the same round as their sends). A system is called synchronizable if every execution can be re-scheduled into an equivalent execution that is a sequence of rounds. Previous work mostly considered the setting where rounds have fixed size. Our main contribution shows that the problem whether a mailbox communication system complies with the round-based policy, with no size limitation on rounds, is PSPACE-complete. For this we use a novel automata-based approach, that also allows to determine the precise complexity (PSPACE) of several questions considered in previous literature.
Subject Classification
ACM Subject Classification
- Theory of computation → Logic and verification
Keywords
- Concurrent programming
- Mailbox communication
- Verification
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Parosh Aziz Abdulla and Bengt Jonsson. Verifying programs with unreliable channels. Inf. Comput., 127(2):91-101, 1996. URL: https://doi.org/10.1006/INCO.1996.0053.
- Benedikt Bollig, Cinzia Di Giusto, Alain Finkel, Laetitia Laversa, Étienne 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, August 24-27, 2021, Virtual Conference, volume 203 of LIPIcs, pages 14:1-14:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPICS.CONCUR.2021.14.
-
Ahmed Bouajjani, Constantin Enea, Kailiang Ji, and Shaz Qadeer. On the completeness of verifying message passing programs under bounded asynchrony. In 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 30, pages 372-391. Springer, 2018.
-
Daniel Brand and Pitro Zafiropulo. On communicating finite-state machines. Journal of the ACM (JACM), 30(2):323-342, 1983.
- Bernadette Charron-Bost and André Schiper. The Heard-Of model: computing in distributed systems with benign faults. Distributed Comput., 22(1):49-71, 2009. URL: https://doi.org/10.1007/S00446-009-0084-6.
- Romain Delpy, Anca Muscholl, and Grégoire Sutre. An automata-based approach for synchronizable mailbox communication, 2024. URL: https://arxiv.org/abs/2407.06968.
-
Cinzia Di Giusto, Laetitia Laversa, and Etienne Lozes. On the k-synchronizability of systems. In 23rd International Conference on Foundations of Software Science and Computer Systems (FOSSACS 2020), volume 12077, pages 157-176. Springer, 2020.
- Emanuele D'Osualdo, Jonathan Kochems, and C.-H. Luke Ong. Automatic verification of erlang-style concurrency. In Francesco Logozzo and Manuel Fähndrich, editors, Static Analysis - 20th International Symposium, SAS 2013, Seattle, WA, USA, June 20-22, 2013. Proceedings, volume 7935 of Lecture Notes in Computer Science, pages 454-476. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-38856-9_24.
- Alain Finkel and Philippe Schnoebelen. Well-structured transition systems everywhere! Theor. Comput. Sci., 256(1-2):63-92, 2001. URL: https://doi.org/10.1016/S0304-3975(00)00102-X.
-
Blaise Genest, Dietrich Kuske, and Anca Muscholl. On communicating automata with bounded channels. Fundamenta Informaticae, 80(1-3):147-167, 2007.
- Blaise Genest, Anca Muscholl, Helmut Seidl, and Marc Zeitoun. Infinite-state high-level mscs: Model-checking and realizability. J. Comput. Syst. Sci., 72(4):617-647, 2006. URL: https://doi.org/10.1016/J.JCSS.2005.09.007.
- Cinzia Di Giusto, Laetitia Laversa, and Étienne Lozes. Guessing the buffer bound for k-synchronizability. Int. J. Found. Comput. Sci., 34(8):1051-1076, 2023. URL: https://doi.org/10.1142/S0129054122430018.
-
Loïc Hélouët and Pierre Le Maigat. Decomposition of message sequence charts. In Edel Sherratt, editor, SAM 2000, 2nd Workshop on SDL and MSC, Col de Porte, Grenoble, France, June 26-28, 2000, pages 47-60. Verimag, IRISA, SDL Forum, 2000.
- Dietrich Kuske and Anca Muscholl. Communicating automata. In Jean-Éric Pin, editor, Handbook of Automata Theory, pages 1147-1188. European Mathematical Society Publishing House, Zürich, Switzerland, 2021. URL: https://doi.org/10.4171/AUTOMATA-2/9.
-
Leslie Lamport. Time, clocks, and the ordering of events in a distributed system. Commun. ACM, 21(7):558-565, 1978.
- Elaine Li, Felix Stutz, Thomas Wies, and Damien Zufferey. Complete multiparty session type projection with automata. In Constantin Enea and Akash Lal, editors, Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part III, volume 13966 of Lecture Notes in Computer Science, pages 350-373. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-37709-9_17.
- Rupak Majumdar, Madhavan Mukund, Felix Stutz, and Damien Zufferey. Generalising projection in asynchronous multiparty session types. In Serge Haddad and Daniele Varacca, editors, 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference, volume 203 of LIPIcs, pages 35:1-35:24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPICS.CONCUR.2021.35.
- Felix Stutz. Asynchronous multiparty session type implementability is decidable - lessons learned from message sequence charts. In Karim Ali and Guido Salvaneschi, editors, 37th European Conference on Object-Oriented Programming, ECOOP 2023, July 17-21, 2023, Seattle, Washington, United States, volume 263 of LIPIcs, pages 32:1-32:31. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.ECOOP.2023.32.