Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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, Lars Birkedal

TL;DR

Trillium introduces intensional refinement to overcome step-indexing limitations in Iris, enabling non-trivial safety and liveness reasoning for higher-order concurrent and distributed programs. The framework defines a language-agnostic trace-program logic and a liveness-first instantiation, Fairis, which uses a Fuel construction to handle fairness and finite stuttering, plus an Aneris-based distributed instantiation that refines to TLA+ models for protocols like Two-Phase Commit and Single-Decree Paxos. All results are formalized in Coq, with adequacy theorems guaranteeing that program traces refine model traces, thus transporting model properties to implementations. The work provides a practical, foundational approach to proving correctness and liveness of distributed systems through refinement against abstract specifications, offering a scalable path for verified protocol implementations and future modular reasoning about libraries and optimizations.

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.

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

TL;DR

Trillium introduces intensional refinement to overcome step-indexing limitations in Iris, enabling non-trivial safety and liveness reasoning for higher-order concurrent and distributed programs. The framework defines a language-agnostic trace-program logic and a liveness-first instantiation, Fairis, which uses a Fuel construction to handle fairness and finite stuttering, plus an Aneris-based distributed instantiation that refines to TLA+ models for protocols like Two-Phase Commit and Single-Decree Paxos. All results are formalized in Coq, with adequacy theorems guaranteeing that program traces refine model traces, thus transporting model properties to implementations. The work provides a practical, foundational approach to proving correctness and liveness of distributed systems through refinement against abstract specifications, offering a scalable path for verified protocol implementations and future modular reasoning about libraries and optimizations.

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.

Paper Structure

This paper contains 40 sections, 8 theorems, 42 equations, 11 figures.

Table of Contents

  1. Introduction
  2. Focus and Methodology
  3. Contributions
  4. Background and Key Observations
  5. Program Steps That Do Not Correspond to Steps in the Model
  6. Stutter-Lifting: Sound for Intensional Safety Trace Properties
  7. Fin-Stutter-Lifting: also Sound for Liveness Properties
  8. Step-Indexing and Finite Approximability
  9. Further Discussions
  10. Coming up with the Appropriate Model
  11. What about Transfinite Iris?
  12. What about the Approaches for Contextual Refinement?
  13. Trillium: A trace program logic framework
  14. Language Agnostic Framework.
  15. The Trillium Program Logic
  16. ...and 25 more sections

Key Result

lemma 1

Let $L_1$ and $L_2$ be two LTSs, and $\xi$ a relation on traces between these LTSs. Let $s_1 \in L_{1}$ and $s_2 \in L_{2}$ be two states such that $s_1 \xisim s_2$ (seen as singleton traces). For all possibly-infinite traces $\tau_{1}$ of $L_{1}$ such that $\mathit{first}(\tau_{1}) = s_{1}$ there e

Figures (11)

  • Figure 1: Two simple LTSs representing the infinite chain of natural numbers \ref{['lts:chain']}, and all finite chains of natural numbers \ref{['lts:finchains']}.
  • Figure 2: The program . Here is the (atomic) fetch-and-add operation which increments the integer stored in its first argument (a reference) by the given amount in the second argument. We assume that the value of $l$ is zero at the beginning.
  • Figure 3: The $\Yes$ and $\No$ threads.
  • Figure 4: The model $\mathcal{M}_{\mathsf{yes\_no}}$.
  • Figure 5: The rules of the Fairis program logic
  • ...and 6 more figures

Theorems & Definitions (14)

  • definition 1: $\xi$-forward simulation
  • definition 2: Intensional refinement
  • definition 3: Trace Relation Extension
  • lemma 1: Intensional refinement, lifting
  • definition 4
  • definition 5: Relative image-finiteness
  • theorem 1: Finite Approximation
  • Remark 2: Invariants and ghost resources in Iris
  • theorem 3: Adequacy
  • theorem 4: Fairis-Adequacy
  • ...and 4 more