Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2021
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866913475984359424 |
|---|---|
| author | Timany, Amin Gregersen, Simon Oddershede Stefanesco, Léo Hinrichsen, Jonas Kastberg Gondelman, Léon Nieto, Abel Birkedal, Lars |
| author_facet | Timany, Amin Gregersen, Simon Oddershede Stefanesco, Léo Hinrichsen, Jonas Kastberg Gondelman, Léon Nieto, Abel Birkedal, Lars |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2109_07863 |
| institution | arXiv |
| publishDate | 2021 |
| record_format | arxiv |
| spellingShingle | Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement Timany, Amin Gregersen, Simon Oddershede Stefanesco, Léo Hinrichsen, Jonas Kastberg Gondelman, Léon Nieto, Abel Birkedal, Lars Programming Languages Logic in Computer Science 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. |
| title | Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement |
| topic | Programming Languages Logic in Computer Science |
| url | https://arxiv.org/abs/2109.07863 |