Document Open Access Logo

Contrasting Deadlock-Free Session Processes

Authors Juan C. Jaramillo , Jorge A. Pérez

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2025.17.pdf
  • Filesize: 1.25 MB
  • 29 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Type structures
  • Theory of computation → Program analysis
  • Theory of computation → Process calculi
Keywords
  • session types
  • process calculi
  • deadlock freedom

Metrics

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

Abstract

Deadlock freedom is a crucial property for message-passing programs. Over the years, several different type systems for concurrent processes that ensure deadlock freedom have been proposed; this diversity raises the question of how they compare. We address this question, considering two type systems not covered in prior work: Kokke et al.’s HCP, a type system based on a linear logic with hypersequents, and Padovani’s priority-based type system for asynchronous processes, dubbed 𝖯. Their distinctive features make formal comparisons relevant and challenging. Our findings are two-fold: (1) the hypersequent setting does not drastically change the class of deadlock-free processes induced by linear logic, and (2) we relate the classes of deadlock-free processes induced by HCP and 𝖯. We prove that our results hold under both synchronous and asynchronous communication. Our results provide new insights into the essential mechanisms involved in statically avoiding deadlocks in concurrency.

Cite As Get BibTex

Juan C. Jaramillo and Jorge A. Pérez. Contrasting Deadlock-Free Session Processes. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 17:1-17:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ECOOP.2025.17

Author Details

Juan C. Jaramillo
  • Unversity of Groningen, The Netherlands
Jorge A. Pérez
  • Unversity of Groningen, The Netherlands

Funding

  • Jaramillo, Juan C.: Ministry of Science of Colombia (Minciencias).

Acknowledgements

We are grateful to Channa Dias Perera for initial discussions on the topics of this paper. We also thank Andreia Mordido and the anonymous reviewers for their helpful suggestions.

References

  1. Stephanie Balzer, Bernardo Toninho, and Frank Pfenning. Manifest deadlock-freedom for shared session types. In Luís Caires, editor, Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, volume 11423 of Lecture Notes in Computer Science, pages 611-639. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17184-1_22.
  2. Gérard Boudol. Asynchrony and the π-calculus (note). Technical report, Rapport de Recherche 1702, INRIA, Sophia-Antipolis, 1992. Google Scholar
  3. Luís Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In Paul Gastin and François Laroussinie, editors, CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings, volume 6269 of Lecture Notes in Computer Science, pages 222-236. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15375-4_16.
  4. Luís Caires and Bernardo Toninho. The session abstract machine. In Stephanie Weirich, editor, Programming Languages and Systems - 33rd European Symposium on Programming, ESOP 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 14576 of Lecture Notes in Computer Science, pages 206-235. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-57262-3_9.
  5. 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.
  6. Tzu-Chun Chen, Mariangiola Dezani-Ciancaglini, and Nobuko Yoshida. On the preciseness of subtyping in session types. In Olaf Chitil, Andy King, and Olivier Danvy, editors, Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming, Kent, Canterbury, United Kingdom, September 8-10, 2014, pages 135-146. ACM, 2014. URL: https://doi.org/10.1145/2643135.2643138.
  7. Ornela Dardha and Simon J. Gay. A new linear logic for deadlock-free session-typed processes. In Christel Baier and Ugo Dal Lago, editors, Foundations of Software Science and Computation Structures - 21st International Conference, FOSSACS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, volume 10803 of Lecture Notes in Computer Science, pages 91-109. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89366-2_5.
  8. Ornela Dardha, Elena Giachino, and Davide Sangiorgi. Session types revisited. In Proc. of PPDP'12, pages 139-150. ACM, 2012. URL: https://doi.org/10.1145/2370776.2370794.
  9. Ornela Dardha and Jorge A. Pérez. Comparing type systems for deadlock freedom. Journal of Logical and Algebraic Methods in Programming, 124:100717, 2022. (Preliminary version in the Proceedings of EXPRESS/SOS 2015). URL: https://doi.org/10.1016/j.jlamp.2021.100717.
  10. 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, CSL, 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.
  11. Mariangiola Dezani-Ciancaglini, Ugo de'Liguoro, and Nobuko Yoshida. On progress for structured communications. In Gilles Barthe and Cédric Fournet, editors, Trustworthy Global Computing, Third Symposium, TGC 2007, Sophia-Antipolis, France, November 5-6, 2007, Revised Selected Papers, volume 4912 of Lecture Notes in Computer Science, pages 257-275. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-78663-4_18.
  12. Simon Fowler, Wen Kokke, Ornela Dardha, Sam Lindley, and J. Garrett Morris. Separating sessions smoothly. 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 36:1-36:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPICS.CONCUR.2021.36.
  13. Simon Fowler, Wen Kokke, Ornela Dardha, Sam Lindley, and J. Garrett Morris. Separating sessions smoothly. Logical Methods in Computer Science, Volume 19, Issue 3, July 2023. URL: https://doi.org/10.46298/lmcs-19(3:3)2023.
  14. Simon J. Gay and Vasco Thudichum Vasconcelos. Linear type theory for asynchronous session types. J. Funct. Program., 20(1):19-50, 2010. URL: https://doi.org/10.1017/S0956796809990268.
  15. Silvia Ghilezan, Jovanka Pantović, Ivan Prokić, Alceste Scalas, and Nobuko Yoshida. Precise subtyping for asynchronous multiparty sessions. Proc. ACM Program. Lang., 5(POPL), January 2021. URL: https://doi.org/10.1145/3434297.
  16. Kohei Honda and Mario Tokoro. On asynchronous communication semantics. In Object-Based Concurrent Computing, number 612, in LNCS, 1992. Google Scholar
  17. Keigo Imai, Rumyana Neykova, Nobuko Yoshida, and Shoji Yuen. Multiparty Session Programming With Global Protocol Combinators. In Robert Hirschfeld and Tobias Pape, editors, 34th European Conference on Object-Oriented Programming (ECOOP 2020), volume 166 of Leibniz International Proceedings in Informatics (LIPIcs), pages 9:1-9:30, Dagstuhl, Germany, 2020. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2020.9.
  18. Jules Jacobs and Stephanie Balzer. Higher-order leak and deadlock free locks. Proc. ACM Program. Lang., 7(POPL):1027-1057, 2023. URL: https://doi.org/10.1145/3571229.
  19. Juan C. Jaramillo and Jorge A. Pérez. Contrasting deadlock-free session processes (extended version), 2025. URL: https://arxiv.org/abs/2504.15845.
  20. Naoki Kobayashi. TyPiCal: Type-based Static Analyzer for the Pi-Calculus. https://www-kb.is.s.u-tokyo.ac.jp/~koba/typical/. Accessed: 2025-03-13.
  21. Naoki Kobayashi. A new type system for deadlock-free processes. In CONCUR'06, volume 4137 of LNCS, pages 233-247, 2006. URL: https://doi.org/10.1007/11817949_16.
  22. 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.
  23. Wen Kokke, Fabrizio Montesi, and Marco Peressotti. Better late than never: A fully-abstract semantics for classical processes. Proceedings of the ACM on Programming Languages, 3(POPL), 2019. URL: https://doi.org/10.1145/3290337.
  24. Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida. Stay Safe Under Panic: Affine Rust Programming with Multiparty Session Types. In Karim Ali and Jan Vitek, editors, 36th European Conference on Object-Oriented Programming (ECOOP 2022), volume 222 of Leibniz International Proceedings in Informatics (LIPIcs), pages 4:1-4:29, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2022.4.
  25. Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida. Fencing off go: liveness and safety for channel-based programming. In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 748-761. ACM, 2017. URL: https://doi.org/10.1145/3009837.3009847.
  26. Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida. A static verification framework for message passing in go using behavioural types. In Michel Chaudron, Ivica Crnkovic, Marsha Chechik, and Mark Harman, editors, Proceedings of the 40th International Conference on Software Engineering, ICSE 2018, Gothenburg, Sweden, May 27 - June 03, 2018, pages 1137-1148. ACM, 2018. URL: https://doi.org/10.1145/3180155.3180157.
  27. Luca Padovani. Deadlock and lock freedom in the linear π-calculus. In Proceedings of the 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, New York, NY, USA, 2014. Association for Computing Machinery. URL: https://doi.org/10.1145/2603088.2603116.
  28. Luca Padovani. A simple library implementation of binary sessions. J. Funct. Program., 27:e4, 2017. URL: https://doi.org/10.1017/S0956796816000289.
  29. Luca Padovani and Luca Novara. Types for deadlock-free higher-order programs. In Susanne Graf and Mahesh Viswanathan, editors, Formal Techniques for Distributed Objects, Components, and Systems - 35th IFIP WG 6.1 International Conference, FORTE 2015, Held as Part of the 10th International Federated Conference on Distributed Computing Techniques, DisCoTec 2015, Grenoble, France, June 2-4, 2015, Proceedings, volume 9039 of Lecture Notes in Computer Science, pages 3-18. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-19195-9_1.
  30. Jorge A. Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logical relations and observational equivalences for session-based concurrency. Information and Computation, 239:254-302, 2014. URL: https://doi.org/10.1016/j.ic.2014.08.001.
  31. Zesen Qian, G. A. Kavvos, and Lars Birkedal. Client-server sessions in linear logic. Proc. ACM Program. Lang., 5(ICFP), August 2021. URL: https://doi.org/10.1145/3473567.
  32. Davide Sangiorgi and David Walker. PI-Calculus: A Theory of Mobile Processes. Cambridge University Press, USA, 2001. Google Scholar
  33. Alceste Scalas, Ornela Dardha, Raymond Hu, and Nobuko Yoshida. A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming. In Peter Müller, editor, 31st European Conference on Object-Oriented Programming (ECOOP 2017), volume 74 of Leibniz International Proceedings in Informatics (LIPIcs), pages 24:1-24:31, Dagstuhl, Germany, 2017. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2017.24.
  34. Bernardo Toninho and Nobuko Yoshida. Interconnectability of session-based logical processes. ACM Trans. Program. Lang. Syst., 40(4):17:1-17:42, 2018. URL: https://doi.org/10.1145/3242173.
  35. Bas van den Heuvel and Jorge A. Pérez. A gentle overview of asynchronous session-based concurrency: Deadlock freedom by typing. In Clément Aubert, Cinzia Di Giusto, Simon Fowler, and Violet Ka I Pun, editors, Proceedings 17th Interaction and Concurrency Experience, ICE 2024, Groningen, The Netherlands, 21st June 2024, volume 414 of EPTCS, pages 1-20, 2024. URL: https://doi.org/10.4204/EPTCS.414.1.
  36. Vasco T. Vasconcelos. Fundamentals of session types. Inf. Comput., 217:52-70, 2012. URL: https://doi.org/10.1016/j.ic.2012.05.002.
  37. 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