Comparing type systems for deadlock freedom

DOI10.1016/J.JLAMP.2021.100717MaRDI QIDQ2667185zbMATH OpenOpenAlexFDO

Authors Ornela Dardha, Jorge A. Pérez

Publication date 24 November 2021

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/1810.00635

zbMATH Keywords

concurrencylinear logicsession typesprocess calculideadlock freedomlinear types

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: Message-passing software systems exhibit non-trivial forms of concurrency and distribution; they are expected to follow intended protocols among communicating services, but also to never "get stuck". This intuitive requirement has been expressed by liveness properties such as progress or (dead)lock freedom and various type systems ensure these properties for concurrent processes. Unfortunately, very little is known about the precise relationship between these type systems and the classes of typed processes they induce. This paper puts forward the first comparative study of different type systems for message-passing processes that guarantee deadlock freedom. We compare two classes of deadlock-free typed processes, here denoted L and K. The class L stands out for its canonicity: it results from Curry-Howard interpretations of linear logic propositions as session types. The class K, obtained by encoding session types into Kobayashi's linear types with usages, includes processes not typable in other type systems. We show that L is strictly included in K, and identify the precise conditions under which they coincide. We also provide two type-preserving translations of processes in K into processes in L.

Recommendations

• Comparing deadlock-free session typed processes
• Types for deadlock-free higher-order programs
• A type system for lock-free processes
• A New Type System for Deadlock-Free Processes
• A new linear logic for deadlock-free session-typed processes

Cites work

• scientific article; zbMATH DE number 1088044 (Why is no real title available?)
• scientific article; zbMATH DE number 1927554 (Why is no real title available?)
• scientific article; zbMATH DE number 1398002 (Why is no real title available?)
• A Hybrid Type System for Lock-Freedom of Mobile Processes
• A New Type System for Deadlock-Free Processes
• A calculus of mobile processes. I
• A fully abstract semantics for causality in the \(\pi\)-calculus
• A generic type system for the pi-calculus
• A graphical approach to progress for structured communication in web services
• A new linear logic for deadlock-free session-typed processes
• A type system for lock-free processes
• Comparing deadlock-free session typed processes
• Conflation confers concurrency
• Conversation Types
• Corecursion and non-divergence in session-typed processes
• Deadlock analysis of unbounded process networks
• Deadlock analysis of unbounded process networks
• Deadlock and lock freedom in the linear -calculus
• Expressiveness of process algebras
• Full abstraction for expressiveness: history, myths and facts
• Fundamentals of session types
• General conditions for full abstraction
• Global Progress in Dynamically Interleaved Multiparty Sessions
• Linear logic propositions as session types
• Linear logical relations and observational equivalences for session-based concurrency
• Linearity, control effects, and behavioral types
• 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
• Propositions as sessions
• Session types as intuitionistic linear propositions
• Session types revisited
• Subtyping for session types in the pi calculus
• Talking bananas: structural recursion for session types
• The -calculus: A theory of mobile processes
• Towards a unified approach to encodability and separation results for process calculi
• Towards static deadlock resolution in the -calculus
• Type systems for concurrent programs.
• Type systems for distributed programs: components and sessions
• Types and programing languages

Cited in

(12)

• EXPRESSing session types
• Types for deadlock-free higher-order programs
• scientific article; zbMATH DE number 1759483 (Why is no real title available?)
• Preface to the special issue on the 12th workshop on programming language approaches to concurrency and communication-centric software (PLACES) 2020
• Comparing deadlock-free session typed processes
• Asynchronous session-based concurrency: deadlock-freedom in cyclic process networks
• Deadlock freedom for asynchronous and cyclic process networks
• Comparing session type systems derived from linear logic
• Asynchronous functional sessions: cyclic and concurrent
• Manifest deadlock-freedom for shared session types
• A gentle overview of asynchronous session-based concurrency: deadlock freedom by typing
• A type system for lock-free processes

This page was built for publication: Comparing type systems for deadlock freedom

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2667185)