Comparing Deadlock-Free Session Typed Processes
Open Access
- 26 August 2015
- journal article
- Published by Open Publishing Association in Electronic Proceedings in Theoretical Computer Science
- Vol. 190, 1-15
- https://doi.org/10.4204/eptcs.190.1
Abstract
Besides respecting prescribed protocols, communication-centric systems should never "get stuck". This requirement has been expressed by liveness properties such as progress or (dead)lock freedom. Several typing disciplines that ensure these properties for mobile processes have been proposed. Unfortunately, very little is known about the precise relationship between these disciplines--and the classes of typed processes they induce. In this paper, we compare L and K, two classes of deadlock-free, session typed concurrent processes. The class L stands out for its canonicity: it results naturally from interpretations of linear logic propositions as session types. The class K, obtained by encoding session types into Kobayashi's usage types, includes processes not typable in other type systems. We show that L is strictly included in K. We also identify the precise condition under which L and K coincide. One key observation is that the degree of sharing between parallel processes determines a new expressiveness hierarchy for typed processes. We also provide a type-preserving rewriting procedure of processes in K into processes in L. This procedure suggests that, while effective, the degree of sharing is a rather subtle criteria for distinguishing typed processes.Comment: In Proceedings EXPRESS/SOS 2015, arXiv:1508.0634This publication has 18 references indexed in Scilit:
- Linear logic propositions as session typesMathematical Structures in Computer Science, 2014
- Recursive Session Types RevisitedElectronic Proceedings in Theoretical Computer Science, 2014
- Progress as Compositional Lock-FreedomLecture Notes in Computer Science, 2014
- Session types revisitedPublished by Association for Computing Machinery (ACM) ,2012
- A Graphical Approach to Progress for Structured Communication in Web ServicesElectronic Proceedings in Theoretical Computer Science, 2010
- Towards a unified approach to encodability and separation results for process calculiInformation and Computation, 2010
- Session Types as Intuitionistic Linear PropositionsLecture Notes in Computer Science, 2010
- On Progress for Structured CommunicationsPublished by Springer Science and Business Media LLC ,2008
- Language primitives and type discipline for structured communication-based programmingPublished by Springer Science and Business Media LLC ,1998
- Weak and strong fairness in CCSInformation and Computation, 1987