Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement


Amin Timany, Simon Oddershede Gregersen, Léo Stefanesco, Jonas Kastberg Hinrichsen, Léon Gondelman, Abel Nieto, and Lars Birkedal: Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement. In POPL 2024, January 2024, doi: 10.1145/3632851.
Journal Paper
Keywords: distributed systems, separation logic, refinement, higher-order logic, concurrency, formal verification
Abstract.

Expressive state-of-the-art separation logics rely on step-indexing to model semantically complex features and to support modular reasoning about imperative higher-order concurrent and distributed programs. Step-indexing comes, however, with an inherent cost: it restricts the adequacy theorem of program logics to a fairly simple class of safety properties.

In this paper, we explore if and how intensional refinement is a viable methodology for strengthening higher-order concurrent (and distributed) separation logic to prove non-trivial safety and liveness properties. Specifically, we introduce Trillium, a language-agnostic separation logic framework for showing intensional refinement relations between traces of a program and a model. We instantiate Trillium with a concurrent language and develop Fairis, a concurrent separation logic, that we use to show liveness properties of concurrent programs under fair scheduling assumptions through a fair liveness-preserving refinement of a model. We also instantiate Trillium with a distributed language and obtain an extension of Aneris, a distributed separation logic, which we use to show refinement relations between distributed systems and TLA+ models.

The bibtex source for this publication:
@article{DBLP:journals/pacmpl/TimanyGSHGNB24,
 author = {Amin Timany and
 Simon Oddershede Gregersen and
 L{\'{e}}o Stefanesco and
 Jonas Kastberg Hinrichsen and
 L{\'{e}}on Gondelman and
 Abel Nieto and
 Lars Birkedal},
 title = {Trillium: Higher-Order Concurrent and Distributed Separation Logic
 for Intensional Refinement},
 journal = {Proc. {ACM} Program. Lang.},
 volume = {8},
 number = {{POPL}},
 pages = {241--272},
 year = {2024},
 url = {https://doi.org/10.1145/3632851},
 doi = {10.1145/3632851},
 timestamp = {Mon, 05 Feb 2024 20:23:02 +0100},
 biburl = {https://dblp.org/rec/journals/pacmpl/TimanyGSHGNB24.bib},
 bibsource = {dblp computer science bibliography, https://dblp.org}
}