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

TL;DR

Trillium introduces a novel separation logic framework that enables reasoning about complex safety and liveness properties in concurrent and distributed systems through intensional refinement, overcoming limitations of step-indexed logics.

Contribution

It presents Trillium, a language-agnostic framework for intensional refinement, and instantiates it with Fairis and Aneris to verify safety and liveness in concurrent and distributed programs.

Findings

Successfully verified liveness properties under fair scheduling.

Extended Aneris to relate distributed systems with TLA+ models.

Demonstrated the applicability of intensional refinement to complex properties.

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.