Document Open Access Logo

Fair Termination of Multiparty Sessions

Authors Luca Ciccone , Francesco Dagnino , Luca Padovani

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2022.26.pdf
  • Filesize: 0.85 MB
  • 26 pages

Document Identifiers

Author Details

Luca Ciccone
  • University of Torino, Italy
Francesco Dagnino
  • University of Genova, Italy
Luca Padovani
  • University of Torino, Italy

Funding

The second author was partially supported by the MUR project T-LADIES (PRIN 2020TL3X8X).

Acknowledgements

We are grateful to the anonymous ECOOP reviewers for their thoughtful and useful comments that helped us improving form and content of the paper.

Cite AsGet BibTex

Luca Ciccone, Francesco Dagnino, and Luca Padovani. Fair Termination of Multiparty Sessions. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 26:1-26:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ECOOP.2022.26

Abstract

There exists a broad family of multiparty sessions in which the progress of one session participant is not unconditional, but depends on the choices performed by other participants. These sessions fall outside the scope of currently available session type systems that guarantee progress. In this work we propose the first type system ensuring that well-typed multiparty sessions, including those exhibiting the aforementioned dependencies, fairly terminate. Fair termination is termination under a fairness assumption that disregards those interactions deemed unfair and therefore unrealistic. Fair termination, combined with the usual safety properties ensured within sessions, not only is desirable per se, but it entails progress and enables a compositional form of static analysis such that the well-typed composition of fairly terminating sessions results in a fairly terminating program.

Subject Classification

ACM Subject Classification
  • Theory of computation → Process calculi
  • Theory of computation → Type structures
  • Theory of computation → Program analysis
Keywords
  • Multiparty sessions
  • fair termination
  • fair subtyping
  • deadlock freedom

Metrics

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

Related Versions

References

  1. Samson Abramsky, Simon J. Gay, and Rajagopal Nagarajan. Interaction categories and the foundations of typed concurrent programming. In Manfred Broy, editor, Proceedings of the NATO Advanced Study Institute on Deductive Program Design, Marktoberdorf, Germany, pages 35-113, 1996. Google Scholar
  2. Davide Ancona, Viviana Bono, Mario Bravetti, Joana Campos, Giuseppe Castagna, Pierre-Malo Deniélou, Simon J. Gay, Nils Gesbert, Elena Giachino, Raymond Hu, Einar Broch Johnsen, Francisco Martins, Viviana Mascardi, Fabrizio Montesi, Rumyana Neykova, Nicholas Ng, Luca Padovani, Vasco T. Vasconcelos, and Nobuko Yoshida. Behavioral types in programming languages. Found. Trends Program. Lang., 3(2-3):95-230, 2016. URL: https://doi.org/10.1561/2500000031.
  3. 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.
  4. 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.
  5. Mario Bravetti and Gianluigi Zavattaro. A theory of contracts for strong service compliance. Math. Struct. Comput. Sci., 19(3):601-638, 2009. URL: https://doi.org/10.1017/S0960129509007658.
  6. 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.
  7. Marco Carbone and Søren Debois. A graphical approach to progress for structured communication in web services. In Simon Bliudze, Roberto Bruni, Davide Grohmann, and Alexandra Silva, editors, Proceedings Third Interaction and Concurrency Experience: Guaranteed Interaction, ICE 2010, Amsterdam, The Netherlands, 10th of June 2010, volume 38 of EPTCS, pages 13-27, 2010. URL: https://doi.org/10.4204/EPTCS.38.4.
  8. Marco Carbone, Sam Lindley, Fabrizio Montesi, Carsten Schürmann, and Philip Wadler. Coherence generalises duality: A logical explanation of multiparty session types. In Josée Desharnais and Radha Jagadeesan, editors, 27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Québec City, Canada, volume 59 of LIPIcs, pages 33:1-33:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2016.33.
  9. Marco Carbone, Fabrizio Montesi, Carsten Schürmann, and Nobuko Yoshida. Multiparty session types as coherence proofs. Acta Informatica, 54(3):243-269, 2017. URL: https://doi.org/10.1007/s00236-016-0285-y.
  10. Luca Ciccone, Francesco Dagnino, and Luca Padovani. Fair Termination of Multiparty Sessions. Technical report, Università di Torino and Università di Genova, 2022. URL: https://arxiv.org/abs/2205.08786.
  11. Luca Ciccone, Francesco Dagnino, and Elena Zucca. Flexible coinduction in agda. In Liron Cohen and Cezary Kaliszyk, editors, 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference), volume 193 of LIPIcs, pages 13:1-13:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ITP.2021.13.
  12. Luca Ciccone and Luca Padovani. FairCheck. GitHub repository, 2021. URL: https://github.com/boystrange/FairCheck.
  13. Luca Ciccone and Luca Padovani. Inference Systems with Corules for Fair Subtyping and Liveness Properties of Binary Session Types. In Nikhil Bansal, Emanuela Merelli, and James Worrell, editors, Proceedings of the 48superscriptth International Colloquium on Automata, Languages, and Programming (ICALP'21), volume 198 of LIPIcs, pages 125:1-125:16, Dagstuhl, Germany, 2021. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ICALP.2021.125.
  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. Mario Coppo, Mariangiola Dezani-Ciancaglini, Nobuko Yoshida, and Luca Padovani. Global progress for dynamically interleaved multiparty sessions. Math. Struct. Comput. Sci., 26(2):238-302, 2016. URL: https://doi.org/10.1017/S0960129514000188.
  16. 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.
  17. 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.
  18. Francesco Dagnino. Flexible Coinduction. PhD thesis, DIBRIS, University of Genoa, January 2021. Google Scholar
  19. 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.
  20. Ugo de'Liguoro and Luca Padovani. Mailbox types for unordered interactions. In Todd D. Millstein, editor, 32nd European Conference on Object-Oriented Programming, ECOOP 2018, July 16-21, 2018, Amsterdam, The Netherlands, volume 109 of LIPIcs, pages 15:1-15:28. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2018.15.
  21. Nissim Francez. Fairness. Texts and Monographs in Computer Science. Springer, 1986. URL: https://doi.org/10.1007/978-1-4612-4886-6.
  22. 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.
  23. 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.
  24. 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.
  25. 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.
  26. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. J. ACM, 63(1):9:1-9:67, 2016. URL: https://doi.org/10.1145/2827695.
  27. 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.
  28. Jules Jacobs, Stephanie Balzer, and Robbert Krebbers. Connectivity graphs: a method for proving deadlock freedom based on separation logic. Proc. ACM Program. Lang., 6(POPL):1-33, 2022. URL: https://doi.org/10.1145/3498662.
  29. Naoki Kobayashi. A type system for lock-free processes. Inf. Comput., 177(2):122-159, 2002. URL: https://doi.org/10.1006/inco.2002.3171.
  30. Naoki Kobayashi. A new type system for deadlock-free processes. In Christel Baier and Holger Hermanns, editors, CONCUR 2006 - Concurrency Theory, 17th International Conference, CONCUR 2006, Bonn, Germany, August 27-30, 2006, Proceedings, volume 4137 of Lecture Notes in Computer Science, pages 233-247. Springer, 2006. URL: https://doi.org/10.1007/11817949_16.
  31. Naoki Kobayashi and Cosimo Laneve. Deadlock analysis of unbounded process networks. Inf. Comput., 252:48-70, 2017. URL: https://doi.org/10.1016/j.ic.2016.03.004.
  32. Naoki Kobayashi, Benjamin C. Pierce, and David N. Turner. Linearity and the pi-calculus. ACM Trans. Program. Lang. Syst., 21(5):914-947, 1999. URL: https://doi.org/10.1145/330249.330251.
  33. Naoki Kobayashi and Davide Sangiorgi. A hybrid type system for lock-freedom of mobile processes. ACM Trans. Program. Lang. Syst., 32(5):16:1-16:49, 2010. URL: https://doi.org/10.1145/1745312.1745313.
  34. Wen Kokke, Fabrizio Montesi, and Marco Peressotti. Taking linear logic apart. In Thomas Ehrhard, Maribel Fernández, Valeria de Paiva, and Lorenzo Tortora de Falco, editors, Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications, Linearity-TLLA@FLoC 2018, Oxford, UK, 7-8 July 2018, volume 292 of EPTCS, pages 90-103, 2018. URL: https://doi.org/10.4204/EPTCS.292.5.
  35. Wen Kokke, Fabrizio Montesi, and Marco Peressotti. Better late than never: a fully-abstract semantics for classical processes. Proc. ACM Program. Lang., 3(POPL):24:1-24:29, 2019. URL: https://doi.org/10.1145/3290337.
  36. M.Z. Kwiatkowska. Survey of fairness notions. Information and Software Technology, 31(7):371-386, 1989. URL: https://doi.org/10.1016/0950-5849(89)90159-6.
  37. Leslie Lamport. Fairness and hyperfairness. Distributed Comput., 13(4):239-245, 2000. URL: https://doi.org/10.1007/PL00008921.
  38. 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.
  39. Susan S. Owicki and Leslie Lamport. Proving liveness properties of concurrent programs. ACM Trans. Program. Lang. Syst., 4(3):455-495, 1982. URL: https://doi.org/10.1145/357172.357178.
  40. Luca Padovani. Fair subtyping for open session types. In Fedor V. Fomin, Rusins Freivalds, Marta Z. Kwiatkowska, and David Peleg, editors, Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part II, volume 7966 of Lecture Notes in Computer Science, pages 373-384. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39212-2_34.
  41. Luca Padovani. Deadlock and lock freedom in the linear π-calculus. In Thomas A. Henzinger and Dale Miller, editors, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, pages 72:1-72:10. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603116.
  42. 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.
  43. Luca Padovani, Vasco Thudichum Vasconcelos, and Hugo Torres Vieira. Typing liveness in multiparty communicating systems. In eva Kühn and Rosario Pugliese, editors, Coordination Models and Languages - 16th IFIP WG 6.1 International Conference, COORDINATION 2014, Held as Part of the 9th International Federated Conferences on Distributed Computing Techniques, DisCoTec 2014, Berlin, Germany, June 3-5, 2014, Proceedings, volume 8459 of Lecture Notes in Computer Science, pages 147-162. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-43376-8_10.
  44. Jorge A. Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logical relations for session-based concurrency. In Helmut Seidl, editor, Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings, volume 7211 of Lecture Notes in Computer Science, pages 539-558. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-28869-2_27.
  45. Jean-Pierre Queille and Joseph Sifakis. Fairness and related properties in transition systems - A temporal logic to deal with fairness. Acta Informatica, 19:195-220, 1983. URL: https://doi.org/10.1007/BF00265555.
  46. Alceste Scalas and Nobuko Yoshida. Less is more: multiparty session types revisited. Proc. ACM Program. Lang., 3(POPL):30:1-30:29, 2019. URL: https://doi.org/10.1145/3290343.
  47. 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.
  48. 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.
  49. Philip Wadler. Propositions as sessions. J. Funct. Program., 24(2-3):384-418, 2014. URL: https://doi.org/10.1017/S095679681400001X.
  50. Nobuko Yoshida, Raymond Hu, Rumyana Neykova, and Nicholas Ng. The scribble protocol language. In Martín Abadi and Alberto Lluch-Lafuente, editors, Trustworthy Global Computing - 8th International Symposium, TGC 2013, Buenos Aires, Argentina, August 30-31, 2013, Revised Selected Papers, volume 8358 of Lecture Notes in Computer Science, pages 22-41. Springer, 2013. URL: https://doi.org/10.1007/978-3-319-05119-2_3.
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