Document Open Access Logo

On the Send-Synchronizability Problem for Mailbox Communication

Authors Romain Delpy , Anca Muscholl , Grégoire Sutre

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2025.15.pdf
  • Filesize: 1.08 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Concurrent programming
  • Mailbox communication
  • Verification
  • Synchronizability

Metrics

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

Abstract

A system of communicating automata is send-synchronizable if its set of send sequences (i.e., the projection on send actions of its executions) is the same when communications are asynchronous and when they are rendez-vous synchronizations. Send-synchronizability was claimed to be decidable for the mailbox semantics (Basu and Bultan, 2011) and for the peer-to-peer semantics (Basu and Bultan, 2016). Finkel and Lozes showed in 2017 that the proofs of these results are flawed, and they proved that send-synchronizability is in fact undecidable for peer-to-peer systems. The send-synchronizability problem for mailbox systems was left open. A partial solution was recently proposed in (Di Giusto, Laversa and Peters, 2024). In this paper, we revisit the send-synchronizability problem for mailbox systems. Firstly, we show that send-synchronizability is undecidable for mailbox systems, thus closing the question left open in (Finkel and Lozes, 2023) and (Di Giusto, Laversa and Peters, 2024). Secondly, we show that send-synchronizability is decidable for the class of 1-schedulable mailbox systems. A system is 1-schedulable if every execution can be re-scheduled into an equivalent execution where each send is either immediately followed by its matching receive, or is never matched. Despite the apparent similarity between send-synchronizability and 1-schedulability, the proof that send-synchronizability is decidable for 1-schedulable mailbox systems is quite involved. We believe that the techniques that we develop in this proof could be used to address other problems on mailbox systems, such as the realizability problem.

Cite As Get BibTex

Romain Delpy, Anca Muscholl, and Grégoire Sutre. On the Send-Synchronizability Problem for Mailbox Communication. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 15:1-15:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CONCUR.2025.15

Author Details

Romain Delpy
  • LaBRI, Univ. Bordeaux, CNRS, Bordeaux INP, Talence, France
Anca Muscholl
  • LaBRI, Univ. Bordeaux, CNRS, Bordeaux INP, Talence, France
Grégoire Sutre
  • LaBRI, Univ. Bordeaux, CNRS, Bordeaux INP, Talence, France

Funding

This work was (partially) supported by the grant ANR-23-CE48-0005 of the French National Research Agency ANR (project PaVeDyS).

References

  1. Parosh Aziz Abdulla and Bengt Jonsson. Verifying programs with unreliable channels. Information and Computation, 127(2):91-101, 1996. URL: https://doi.org/10.1006/INCO.1996.0053.
  2. Samik Basu and Tevfik Bultan. Choreography conformance via synchronizability. In Sadagopan Srinivasan, Krithi Ramamritham, Arun Kumar, M. P. Ravindra, Elisa Bertino, and Ravi Kumar, editors, Proceedings of the 20th International Conference on World Wide Web, WWW 2011, Hyderabad, India, March 28 - April 1, 2011, pages 795-804. ACM, 2011. URL: https://doi.org/10.1145/1963405.1963516.
  3. Samik Basu and Tevfik Bultan. On deciding synchronizability for asynchronously communicating systems. Theoretical Computer Science, 656:60-75, 2016. URL: https://doi.org/10.1016/J.TCS.2016.09.023.
  4. Samik Basu, Tevfik Bultan, and Meriem Ouederni. Synchronizability for verification of asynchronously communicating systems. In Viktor Kuncak and Andrey Rybalchenko, editors, Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Philadelphia, PA, USA, January 22-24, 2012. Proceedings, volume 7148 of Lecture Notes in Computer Science, pages 56-71. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-27940-9_5.
  5. Benedikt Bollig, Cinzia Di Giusto, Alain Finkel, Laetitia Laversa, Étienne Lozes, and Amrita Suresh. A unifying framework for deciding synchronizability. In 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.
  6. 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, volume 10982 of Lecture Notes in Computer Science, pages 372-391. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-96142-2_23.
  7. Daniel Brand and Pitro Zafiropulo. On communicating finite-state machines. Journal of the ACM, 30(2):323-342, 1983. URL: https://doi.org/10.1145/322374.322380.
  8. 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, September 9-13, 2024, Calgary, Canada, volume 311 of LIPIcs, pages 22:1-22:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPICS.CONCUR.2024.22.
  9. Cinzia Di Giusto, Laetitia Laversa, and Kirstin Peters. Synchronisability in mailbox communication. In Proceedings Combined 31st International Workshop onTheoretical Computer Science Expressiveness in Concurrencyand 21st Workshop on Structural Operational Semantics, Calgary, Canada, 9th September 2024, volume 412 of Electronic Proceedings in Theoretical Computer Science, pages 19-34. Open Publishing Association, 2024. URL: https://doi.org/10.4204/EPTCS.412.3.
  10. Alain Finkel and Étienne Lozes. Synchronizability of communicating finite state machines is not decidable. In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland, volume 80 of LIPIcs, pages 122:1-122:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPICS.ICALP.2017.122.
  11. Alain Finkel and Étienne Lozes. Synchronizability of communicating finite state machines is not decidable. Logical Methods in Computer Science, 19(4), 2023. URL: https://doi.org/10.46298/LMCS-19(4:33)2023.
  12. Alain Finkel and Philippe Schnoebelen. Well-structured transition systems everywhere! Theoretical Computer Science, 256(1-2):63-92, 2001. URL: https://doi.org/10.1016/S0304-3975(00)00102-X.
  13. Xiang Fu, Tevfik Bultan, and Jianwen Su. Synchronizability of conversations among web services. IEEE Transactions on Software Engineering, 31(12):1042-1055, 2005. URL: https://doi.org/10.1109/TSE.2005.141.
  14. Blaise Genest, Dietrich Kuske, and Anca Muscholl. On communicating automata with bounded channels. Fundamenta Informaticae, 80(1-3):147-167, 2007. URL: http://content.iospress.com/articles/fundamenta-informaticae/fi80-1-3-09.
  15. Cinzia Di Giusto, Davide Ferré, Laetitia Laversa, and Étienne Lozes. A partial order view of message-passing communication models. Proceedings of the ACM on Programming Languages, 7(POPL):1601-1627, 2023. URL: https://doi.org/10.1145/3571248.
  16. Cinzia Di Giusto, Laetitia Laversa, and Étienne Lozes. On the k-synchronizability of systems. In Foundations of Software Science and Computation Structures - 23rd International Conference, FOSSACS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, volume 12077 of Lecture Notes in Computer Science, pages 157-176. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-45231-5_9.
  17. Cinzia Di Giusto, Laetitia Laversa, and Étienne Lozes. Guessing the buffer bound for k-synchronizability. International Journal of Foundations of Computer Science, 34(8):1051-1076, 2023. URL: https://doi.org/10.1142/S0129054122430018.
  18. Jesper G. Henriksen, Madhavan Mukund, K. Narayan Kumar, Milind A. Sohoni, and P. S. Thiagarajan. A theory of regular MSC languages. Information and Computation, 202(1):1-38, 2005. URL: https://doi.org/10.1016/J.IC.2004.08.004.
  19. John E. Hopcroft and Jeffrey D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979. Google Scholar
  20. Dietrich Kuske and Anca Muscholl. Communicating automata. In 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.
  21. Leslie Lamport. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 21(7):558-565, 1978. URL: https://doi.org/10.1145/359545.359563.
  22. Elaine Li, Felix Stutz, Thomas Wies, and Damien Zufferey. Complete multiparty session type projection with automata. In 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.
  23. Rupak Majumdar, Madhavan Mukund, Felix Stutz, and Damien Zufferey. Generalising projection in asynchronous multiparty session types. In 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.
  24. Felix Stutz. Asynchronous multiparty session type implementability is decidable - lessons learned from message sequence charts. In 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.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact