Document Open Access Logo

Fair Termination of Asynchronous Binary Sessions

Authors Luca Padovani , Gianluigi Zavattaro

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2025.24.pdf
  • Filesize: 0.95 MB
  • 29 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Type structures
  • Theory of computation → Linear logic
  • Theory of computation → Program analysis
Keywords
  • Binary sessions
  • fair asynchronous subtyping
  • fair termination
  • linear logic

Metrics

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

Abstract

We study a theory of asynchronous session types ensuring that well-typed processes terminate under a suitable fairness assumption. Fair termination entails starvation freedom and orphan message freedom namely that all messages, including those that are produced early taking advantage of asynchrony, are eventually consumed. The theory is based on a novel fair asynchronous subtyping relation for session types that is coarser than the existing ones. The type system is also the first of its kind that is firmly rooted in linear logic: fair asynchronous subtyping is incorporated as a natural generalization of the cut and axiom rules of linear logic and asynchronous communication is modeled through a suitable set of commuting conversions and of deep cut reductions in linear logic proofs.

Cite As Get BibTex

Luca Padovani and Gianluigi Zavattaro. Fair Termination of Asynchronous Binary Sessions. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 24:1-24:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ECOOP.2025.24

Author Details

Luca Padovani
  • University of Bologna, Italy
Gianluigi Zavattaro
  • University of Bologna, Italy
  • INRIA OLAS team, Sophia Antipolis, France

Funding

The authors have been partially supported by the ANR project SmartCloud ANR-23-CE25-0012 and the PNRR project CN-HPC Spoke 9 Innovation Grant RTMER.

Acknowledgements

We are grateful to the ECOOP reviewers for their thoughtful feedback and questions.

References

  1. Davide Ancona, Francesco Dagnino, and Elena Zucca. Generalizing inference systems by coaxioms. 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 29-55. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54434-1_2.
  2. Krzysztof R. Apt, Nissim Francez, and Shmuel Katz. Appraising fairness in languages for distributed programming. In Conference Record of the Fourteenth Annual ACM Symposium on Principles of Programming Languages, Munich, Germany, January 21-23, 1987, pages 189-198. ACM Press, 1987. URL: https://doi.org/10.1145/41625.41642.
  3. David Baelde, Amina Doumane, and Alexis Saurin. Infinitary proof theory: the multiplicative additive case. In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France, volume 62 of LIPIcs, pages 42:1-42:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPICS.CSL.2016.42.
  4. Laura Bocchi, Andy King, and Maurizio Murgia. Asynchronous subtyping by trace relaxation. In Bernd Finkbeiner and Laura Kovács, editors, Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I, volume 14570 of Lecture Notes in Computer Science, pages 207-226. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-57246-3_12.
  5. Mario Bravetti, Marco Carbone, Julien Lange, Nobuko Yoshida, and Gianluigi Zavattaro. A sound algorithm for asynchronous session subtyping and its implementation. Log. Methods Comput. Sci., 17(1), 2021. URL: https://lmcs.episciences.org/7238.
  6. Mario Bravetti, Marco Carbone, and Gianluigi Zavattaro. Undecidability of asynchronous session subtyping. Inf. Comput., 256:300-320, 2017. URL: https://doi.org/10.1016/J.IC.2017.07.010.
  7. Mario Bravetti, Marco Carbone, and Gianluigi Zavattaro. On the boundary between decidability and undecidability of asynchronous session subtyping. Theor. Comput. Sci., 722:19-51, 2018. URL: https://doi.org/10.1016/J.TCS.2018.02.010.
  8. Mario Bravetti, Julien Lange, and Gianluigi Zavattaro. Fair asynchronous session subtyping. Log. Methods Comput. Sci., 20(4), 2024. URL: https://doi.org/10.46298/LMCS-20(4:5)2024.
  9. Mario Bravetti and Gianluigi Zavattaro. Asynchronous session subtyping as communicating automata refinement. Softw. Syst. Model., 20(2):311-333, 2021. URL: https://doi.org/10.1007/S10270-020-00838-X.
  10. Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logic propositions as session types. Math. Struct. Comput. Sci., 26(3):367-423, 2016. URL: https://doi.org/10.1017/S0960129514000218.
  11. Tzu-Chun Chen, Mariangiola Dezani-Ciancaglini, Alceste Scalas, and Nobuko Yoshida. On the preciseness of subtyping in session types. Log. Methods Comput. Sci., 13(2), 2017. URL: https://doi.org/10.23638/LMCS-13(2:12)2017.
  12. Luca Ciccone, Francesco Dagnino, and Luca Padovani. Fair termination of multiparty sessions. In Karim Ali and Jan Vitek, editors, 36th European Conference on Object-Oriented Programming, ECOOP 2022, June 6-10, 2022, Berlin, Germany, volume 222 of LIPIcs, pages 26:1-26:26. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.ECOOP.2022.26.
  13. Luca Ciccone, Francesco Dagnino, and Luca Padovani. Fair termination of multiparty sessions. J. Log. Algebraic Methods Program., 139:100964, 2024. URL: https://doi.org/10.1016/J.JLAMP.2024.100964.
  14. Luca Ciccone and Luca Padovani. Fair termination of binary sessions. Proc. ACM Program. Lang., 6(POPL):1-30, 2022. URL: https://doi.org/10.1145/3498666.
  15. Luca Ciccone and Luca Padovani. Inference systems with corules for combined safety and liveness properties of binary session types. Log. Methods Comput. Sci., 18(3), 2022. URL: https://doi.org/10.46298/LMCS-18(3:27)2022.
  16. Luca Ciccone and Luca Padovani. An infinitary proof theory of linear logic ensuring fair termination in the linear π-calculus. In Bartek Klin, Slawomir Lasota, and Anca Muscholl, editors, 33rd International Conference on Concurrency Theory, CONCUR 2022, September 12-16, 2022, Warsaw, Poland, volume 243 of LIPIcs, pages 36:1-36:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.CONCUR.2022.36.
  17. Bruno Courcelle. Fundamental properties of infinite trees. Theor. Comput. Sci., 25:95-169, 1983. URL: https://doi.org/10.1016/0304-3975(83)90059-2.
  18. Francesco Dagnino. Coaxioms: flexible coinductive definitions by inference systems. Log. Methods Comput. Sci., 15(1), 2019. URL: https://doi.org/10.23638/LMCS-15(1:26)2019.
  19. Francesco Dagnino and Luca Padovani. small caps: An infinitary linear logic for a calculus of pure sessions. In Alessandro Bruni, Alberto Momigliano, Matteo Pradella, Matteo Rossi, and James Cheney, editors, Proceedings of the 26th International Symposium on Principles and Practice of Declarative Programming, PPDP 2024, Milano, Italy, September 9-11, 2024, pages 4:1-4:13. ACM, 2024. URL: https://doi.org/10.1145/3678232.3678234.
  20. Ornela Dardha, Elena Giachino, and Davide Sangiorgi. Session types revisited. Inf. Comput., 256:253-286, 2017. URL: https://doi.org/10.1016/j.ic.2017.06.002.
  21. Ankush Das, Stephanie Balzer, Jan Hoffmann, Frank Pfenning, and Ishani Santurkar. Resource-aware session types for digital contracts. In 34th IEEE Computer Security Foundations Symposium, CSF 2021, Dubrovnik, Croatia, June 21-25, 2021, pages 1-16. IEEE, 2021. URL: https://doi.org/10.1109/CSF51468.2021.00004.
  22. Ankush Das, Jan Hoffmann, and Frank Pfenning. Work analysis with resource-aware session types. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 305-314. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209146.
  23. Ankush Das and Frank Pfenning. Rast: A language for resource-aware session types. Log. Methods Comput. Sci., 18(1), 2022. URL: https://doi.org/10.46298/LMCS-18(1:9)2022.
  24. Henry DeYoung, Luís Caires, Frank Pfenning, and Bernardo Toninho. Cut reduction in linear logic as asynchronous session-typed communication. In Patrick Cégielski and Arnaud Durand, editors, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL, CSL 2012, September 3-6, 2012, Fontainebleau, France, volume 16 of LIPIcs, pages 228-242. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: https://doi.org/10.4230/LIPICS.CSL.2012.228.
  25. Amina Doumane. On the infinitary proof theory of logics with fixed points. (Théorie de la démonstration infinitaire pour les logiques à points fixes). PhD thesis, Paris Diderot University, France, 2017. URL: https://tel.archives-ouvertes.fr/tel-01676953.
  26. Nissim Francez. Fairness. Texts and Monographs in Computer Science. Springer, 1986. URL: https://doi.org/10.1007/978-1-4612-4886-6.
  27. Simon J. Gay. Subtyping supports safe session substitution. In Sam Lindley, Conor McBride, Philip W. Trinder, and Donald Sannella, editors, A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, volume 9600 of Lecture Notes in Computer Science, pages 95-108. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-30936-1_5.
  28. Simon J. Gay and Malcolm Hole. Subtyping for session types in the pi calculus. Acta Informatica, 42(2-3):191-225, 2005. URL: https://doi.org/10.1007/S00236-005-0177-Z.
  29. Silvia Ghilezan, Jovanka Pantovic, Ivan Prokic, Alceste Scalas, and Nobuko Yoshida. Precise subtyping for asynchronous multiparty sessions. ACM Trans. Comput. Log., 24(2):14:1-14:73, 2023. URL: https://doi.org/10.1145/3568422.
  30. Orna Grumberg, Nissim Francez, and Shmuel Katz. Fair termination of communicating processes. In Proceedings of the Third Annual ACM Symposium on Principles of Distributed Computing, PODC '84, pages 254-265, New York, NY, USA, 1984. Association for Computing Machinery. URL: https://doi.org/10.1145/800222.806752.
  31. Alessio Guglielmi and Lutz Straßburger. Non-commutativity and MELL in the calculus of structures. In Laurent Fribourg, editor, Computer Science Logic, 15th International Workshop, CSL 2001. 10th Annual Conference of the EACSL, Paris, France, September 10-13, 2001, Proceedings, volume 2142 of Lecture Notes in Computer Science, pages 54-68. Springer, 2001. URL: https://doi.org/10.1007/3-540-44802-0_5.
  32. Kohei Honda. Types for dyadic interaction. In Eike Best, editor, CONCUR '93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993, Proceedings, volume 715 of Lecture Notes in Computer Science, pages 509-523. Springer, 1993. URL: https://doi.org/10.1007/3-540-57208-2_35.
  33. Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In Chris Hankin, editor, Programming Languages and Systems - ESOP'98, 7th European Symposium on Programming, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings, volume 1381 of Lecture Notes in Computer Science, pages 122-138. Springer, 1998. URL: https://doi.org/10.1007/BFB0053567.
  34. Ross Horne and Luca Padovani. A logical account of subtyping for session types. J. Log. Algebraic Methods Program., 141:100986, 2024. URL: https://doi.org/10.1016/J.JLAMP.2024.100986.
  35. Hans Hüttel, Ivan Lanese, Vasco T. Vasconcelos, Luís Caires, Marco Carbone, Pierre-Malo Deniélou, Dimitris Mostrous, Luca Padovani, António Ravara, Emilio Tuosto, Hugo Torres Vieira, and Gianluigi Zavattaro. Foundations of session types and behavioural contracts. ACM Comput. Surv., 49(1):3:1-3:36, 2016. URL: https://doi.org/10.1145/2873052.
  36. Julien Lange and Nobuko Yoshida. On the undecidability of asynchronous session subtyping. In Javier Esparza and Andrzej S. Murawski, editors, Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 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 10203 of Lecture Notes in Computer Science, pages 441-457, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_26.
  37. Sam Lindley and J. Garrett Morris. Talking bananas: structural recursion for session types. In Jacques Garrigue, Gabriele Keller, and Eijiro Sumii, editors, Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016, pages 434-447. ACM, 2016. URL: https://doi.org/10.1145/2951913.2951921.
  38. Barbara Liskov and Jeannette M. Wing. A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst., 16(6):1811-1841, 1994. URL: https://doi.org/10.1145/197320.197383.
  39. Dimitris Mostrous and Nobuko Yoshida. Session typing and asynchronous subtyping for the higher-order π-calculus. Inf. Comput., 241:227-263, 2015. URL: https://doi.org/10.1016/J.IC.2015.02.002.
  40. Dimitris Mostrous, Nobuko Yoshida, and Kohei Honda. Global principal typing in partially commutative asynchronous sessions. In Giuseppe Castagna, editor, Programming Languages and Systems, 18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, volume 5502 of Lecture Notes in Computer Science, pages 316-332. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-00590-9_23.
  41. Luca Padovani. Fair subtyping for multi-party session types. Math. Struct. Comput. Sci., 26(3):424-464, 2016. URL: https://doi.org/10.1017/S096012951400022X.
  42. Luca Padovani. On the fair termination of client-server sessions. In Delia Kesner and Pierre-Marie Pédrot, editors, 28th International Conference on Types for Proofs and Programs, TYPES 2022, June 20-25, 2022, LS2N, University of Nantes, France, volume 269 of LIPIcs, pages 5:1-5:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.TYPES.2022.5.
  43. Luca Padovani and Gianluigi Zavattaro. Fair termination of asynchronous binary sessions. Technical report, University of Bologna, 2025. URL: https://doi.org/10.48550/arXiv.2503.07273.
  44. Rob van Glabbeek and Peter Höfner. Progress, justness, and fairness. ACM Comput. Surv., 52(4):69:1-69:38, 2019. URL: https://doi.org/10.1145/3329125.
  45. Philip Wadler. Propositions as sessions. J. Funct. Program., 24(2-3):384-418, 2014. URL: https://doi.org/10.1017/S095679681400001X.
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