Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing

Jules Jacobs; Jonas Kastberg Hinrichsen; Robbert Krebbers

doi:10.1145/3632889

Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing

Jules Jacobs, Jonas Kastberg Hinrichsen, Robbert Krebbers

Department of Computer Science

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

6 Citations (Scopus)

Abstract

We introduce a linear concurrent separation logic, called LinearActris, designed to guarantee deadlock and leak freedom for message-passing concurrency. LinearActris combines the strengths of session types and concurrent separation logic, allowing for the verification of challenging higher-order programs with mutable state through dependent protocols. The key challenge is to prove the adequacy theorem of LinearActris, which says that the logic indeed gives deadlock and leak freedom "for free"from linearity. We prove this theorem by defining a step-indexed model of separation logic, based on connectivity graphs. To demonstrate the expressive power of LinearActris, we prove soundness of a higher-order (GV-style) session type system using the technique of logical relations. All our results and examples have been mechanized in Coq.

Original language	English
Article number	47
Journal	Proceedings of the ACM on Programming Languages
Volume	8
Issue	POPL
ISSN	2475-1421
DOIs	https://doi.org/10.1145/3632889
Publication status	Published - Jan 2024

Keywords

Coq
deadlocks
Iris
Message passing
separation logic
session types

Access to Document

10.1145/3632889Licence: Unspecified

Cite this

@article{4f3fd2844cc4491ca6c4f8d6365b35ee,

title = "Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing",

abstract = "We introduce a linear concurrent separation logic, called LinearActris, designed to guarantee deadlock and leak freedom for message-passing concurrency. LinearActris combines the strengths of session types and concurrent separation logic, allowing for the verification of challenging higher-order programs with mutable state through dependent protocols. The key challenge is to prove the adequacy theorem of LinearActris, which says that the logic indeed gives deadlock and leak freedom {"}for free{"}from linearity. We prove this theorem by defining a step-indexed model of separation logic, based on connectivity graphs. To demonstrate the expressive power of LinearActris, we prove soundness of a higher-order (GV-style) session type system using the technique of logical relations. All our results and examples have been mechanized in Coq.",

keywords = "Coq, deadlocks, Iris, Message passing, separation logic, session types",

author = "Jules Jacobs and Hinrichsen, {Jonas Kastberg} and Robbert Krebbers",

note = "Publisher Copyright: {\textcopyright} 2024 Owner/Author.",

year = "2024",

month = jan,

doi = "10.1145/3632889",

language = "English",

volume = "8",

journal = "Proceedings of the ACM on Programming Languages ",

issn = "2475-1421",

publisher = "Association for Computing Machinery",

number = "POPL",

}

Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing. / Jacobs, Jules; Hinrichsen, Jonas Kastberg; Krebbers, Robbert.
In: Proceedings of the ACM on Programming Languages , Vol. 8, No. POPL, 47, 01.2024.

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

TY - JOUR

T1 - Deadlock-Free Separation Logic

T2 - Linearity Yields Progress for Dependent Higher-Order Message Passing

AU - Jacobs, Jules

AU - Hinrichsen, Jonas Kastberg

AU - Krebbers, Robbert

PY - 2024/1

Y1 - 2024/1

N2 - We introduce a linear concurrent separation logic, called LinearActris, designed to guarantee deadlock and leak freedom for message-passing concurrency. LinearActris combines the strengths of session types and concurrent separation logic, allowing for the verification of challenging higher-order programs with mutable state through dependent protocols. The key challenge is to prove the adequacy theorem of LinearActris, which says that the logic indeed gives deadlock and leak freedom "for free"from linearity. We prove this theorem by defining a step-indexed model of separation logic, based on connectivity graphs. To demonstrate the expressive power of LinearActris, we prove soundness of a higher-order (GV-style) session type system using the technique of logical relations. All our results and examples have been mechanized in Coq.

AB - We introduce a linear concurrent separation logic, called LinearActris, designed to guarantee deadlock and leak freedom for message-passing concurrency. LinearActris combines the strengths of session types and concurrent separation logic, allowing for the verification of challenging higher-order programs with mutable state through dependent protocols. The key challenge is to prove the adequacy theorem of LinearActris, which says that the logic indeed gives deadlock and leak freedom "for free"from linearity. We prove this theorem by defining a step-indexed model of separation logic, based on connectivity graphs. To demonstrate the expressive power of LinearActris, we prove soundness of a higher-order (GV-style) session type system using the technique of logical relations. All our results and examples have been mechanized in Coq.

KW - Coq

KW - deadlocks

KW - Iris

KW - Message passing

KW - separation logic

KW - session types

U2 - 10.1145/3632889

DO - 10.1145/3632889

M3 - Journal article

AN - SCOPUS:85182264413

SN - 2475-1421

VL - 8

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

IS - POPL

M1 - 47

ER -

Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing

Abstract

Keywords

Access to Document

Fingerprint

Cite this