Manifest Deadlock-Freedom for Shared Session Types

Stephanie Balzer, Bernardo Toninho, Frank Pfenning

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Citations (Scopus)

Abstract

Shared session types generalize the Curry-Howard correspondence between intuitionistic linear logic and the session-typed σ-calculus with adjoint modalities that mediate between linear and shared session types, giving rise to a programming model where shared channels must be used according to a locking discipline of acquire-release. While this generalization greatly increases the range of programs that can be written, the gain in expressiveness comes at the cost of deadlock-freedom, a property which holds for many linear session type systems. In this paper, we develop a type system for logically-shared sessions in which types capture not only the interactive behavior of processes but also constrain the order of resources (i.e., shared processes) they may acquire. This type-level information is then used to rule out cyclic dependencies among acquires and synchronization points, resulting in a system that ensures deadlock-free communication for well-typed processes in the presence of shared sessions, higher-order channel passing, and recursive processes. We illustrate our approach on a series of examples, showing that it rules out deadlocks in circular networks of both shared and linear recursive processes, while still being permissive enough to type concurrent implementations of shared imperative data structures as processes.

Original languageEnglish
Title of host publicationProgramming 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, Proceedings
EditorsLuís Caires
Place of PublicationCham
PublisherSpringer Verlag
Pages611-639
Number of pages29
ISBN (Electronic)978-3-030-17184-1
ISBN (Print)978-3-030-17183-4
DOIs
Publication statusPublished - 9 Apr 2019
Event28th 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
Duration: 6 Apr 201911 Apr 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer Verlag
Volume11423 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference28th European Symposium on Programming, ESOP 2019 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019
CountryCzech Republic
CityPrague
Period6/04/1911/04/19

Keywords

  • Deadlock-freedom
  • Linear and shared session types

Fingerprint Dive into the research topics of 'Manifest Deadlock-Freedom for Shared Session Types'. Together they form a unique fingerprint.

Cite this