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

Institut for Datalogi

Publikation: Bidrag til tidsskrift/Konferencebidrag i tidsskrift /Bidrag til avis › Tidsskriftartikel › Forskning › peer review

6 Citationer (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.

Originalsprog	Engelsk
Artikelnummer	47
Tidsskrift	Proceedings of the ACM on Programming Languages
Vol/bind	8
Nummer	POPL
ISSN	2475-1421
DOI	https://doi.org/10.1145/3632889
Status	Udgivet - jan. 2024

Adgang til dokumentet

10.1145/3632889Licens: Ikke-specificeret

Citationsformater

@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.
I: Proceedings of the ACM on Programming Languages , Bind 8, Nr. POPL, 47, 01.2024.

Publikation: Bidrag til tidsskrift/Konferencebidrag i tidsskrift /Bidrag til avis › Tidsskriftartikel › Forskning › 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

Adgang til dokumentet

Fingeraftryk

Citationsformater