Jules Jacobs · Publications
Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing
Jules Jacobs, Jonas Kastberg Hinrichsen and Robbert Krebbers. POPL'24.
Session types give deadlock freedom “for free” from linear type checking; this paper brings that to separation logic. LinearActris is a linear concurrent separation logic that guarantees deadlock and leak freedom for higher-order programs with mutable state and dependent protocols. Its adequacy is proved with a step-indexed model based on connectivity graphs, mechanized in Coq.
Read the paper
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.
Talks
Cite
@article{jacobs2024dlfactris,
title = {Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing},
volume = {8},
ISSN = {2475-1421},
url = {https://doi.org/10.1145/3632889},
DOI = {10.1145/3632889},
number = {POPL},
journal = {Proceedings of the ACM on Programming Languages},
publisher = {Association for Computing Machinery (ACM)},
author = {Jacobs, Jules and Hinrichsen, Jonas Kastberg and Krebbers, Robbert},
year = {2024},
month = Jan,
pages = {1385--1417}
}