Reference. Lawyer: Modular Obligations-Based Liveness Reasoning in Higher-Order Impredicative Concurrent Separation Logic
Higher-order concurrent separation logics, such as Iris, have been tremendously successful in verifying safety properties of concurrent programs. However, state-of-the-art attempts to verify liveness properties in such logics have so far either lacked modularity (the ability to compose specifications of independent modules), or they have been far too complex to mechanize in a proof assistant. In this work, we introduce Lawyer — a mechanized program logic for modular verification of (fair) termination of concurrent programs. Lawyer draws inspiration from state-of-the-art approaches that use obligations for specifying and proving termination. However, unlike these approaches, which incorporate obligations by instrumenting the source code with erasable auxiliary code and state, Lawyer avoids such instrumentations. Instead, Lawyer incorporates obligations into the logic by embedding them into a purely logical labeled transition system that the program is shown to refine — this makes Lawyer far more amenable to mechanization. We demonstrate the expressivity of Lawyer by verifying termination of a range of examples, including modular verification of a client program whose termination relies on correctness of a fair lock library, and (separately) proving that a ticket lock implementation implements that library’s interface. To the best of our knowledge, Lawyer is the first mechanized program logic that supports modular higher-order impredicative liveness specifications of program modules. All the results that appear in the paper have been mechanized in the Rocq proof assistant on top of the Iris separation logic framework.
Cite
Cited by (1)
Verifying Wait-Freedom for Concurrent Higher-Order Programs namakonov-2026-verifying
Wait-freedom is the strongest non-blocking progress guarantee for concurrent data structures, ensuring that every operation completes in a finite number of steps regardless of interference from other threads. While verification of wait-freedom has been studied for first-order languages, verifying it for higher-order programming languages with general references remains an open challenge. In such languages, operations may be used by arbitrary, unverified higher-order clients, making it unclear how to even define wait-freedom formally in terms of programs’ semantics, let alone prove it. In this paper, we present the first framework for verifying wait-freedom of concurrent programs written in a higher-order language with general references. Our approach is based on the Lawyer concurrent separation logic which has been recently introduced for termination verification. We identify a specification pattern in the Lawyer logic that captures wait-freedom. To establish this connection formally, we prove a novel adequacy theorem for Lawyer which states that programs which are proven correct in the Lawyer logic against a specification in the aforementioned specification pattern are wait-free. Proving wait-freedom requires to show that all calls made to operations by any arbitrary client terminate. Thus, as a part of proving the adequacy theorem above, we need to prove that the behavior of the client of the data structure is safe in the sense that it does not break the internal invariants of the data structure, e.g., by directly manipulating the data structure’s internal state. To this end, we develop a logical relations model that establishes safety for all clients once and for all. We demonstrate the effectiveness of our approach by proving wait-freedom for several representative examples, including a higher-order list map function, and a memory-efficient single-producer, single-consumer queue. For the latter, wait-freedom is conditional in that, as the name suggests, there can be at most one enqueuer thread and one dequeuer thread. To capture this formally, we introduce the notion of restricted wait-freedom as a variant of wait-freedom that restricts the number of concurrent threads, and show how our approach can support reasoning about restricted wait-freedom. All our results have been mechanized on top of the Rocq Prover and using the Iris separation logic framework that Lawyer is also based on.
Cites 38 works (7 here)
With notes (7)
Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement timany-2024-trillium
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. Stepindexing 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.
Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations gaher_etal_simuliris_2022
Today’s compilers employ a variety of non-trivial optimizations to achieve good performance. One key trick compilers use to justify transformations of concurrent programs is to assume that the source program has no data races: if it does, they cause the program to have undefined behavior (UB) and give the compiler free rein. However, verifying correctness of optimizations that exploit this assumption is a non-trivial problem. In particular, prior work either has not proven that such optimizations preserve program termination (particularly non-obvious when considering optimizations that move instructions out of loop bodies), or has treated all synchronization operations as external functions (losing the ability to reorder instructions around them).
In this work we present Simuliris, the first simulation technique to establish termination preservation (under a fair scheduler) for a range of concurrent program transformations that exploit UB in the source language. Simuliris is based on the idea of using ownership to reason modularly about the assumptions the compiler makes about programs with well-defined behavior. This brings the benefits of concurrent separation logics to the space of verifying program transformations: we can combine powerful reasoning techniques such as framing and coinduction to perform thread-local proofs of non-trivial concurrent program optimizations. Simuliris is built on a (non-step-indexed) variant of the Coq-based Iris framework, and is thus not tied to a particular language. In addition to demonstrating the effectiveness of Simuliris on standard compiler optimizations involving data race UB, we also instantiate it with Jung et al.’s Stacked Borrows semantics for Rust and generalize their proofs of interesting type-based aliasing optimizations to account for concurrency.
Transfinite Iris: resolving an existential dilemma of step-indexed separation logic spies-2021-transfinitex
Iris from the ground up: A modular foundation for higher-order concurrent separation logic jung_etal_iris_ground_up_2018
Iris is a framework for higher-order concurrent separation logic, which has been implemented in the Coq proof assistant and deployed very effectively in a wide variety of verification projects. Iris was designed with the express goal of simplifying and consolidating the foundations of modern separation logics, but it has evolved over time, and the design and semantic foundations of Iris itself have yet to be fully written down and explained together properly in one place. Here, we attempt to fill this gap, presenting a reasonably complete picture of the latest version of Iris (version 3.1), from first principles and in one coherent narrative.
A Higher-Order Logic for Concurrent Termination-Preserving Refinement tassarotti_jung_harper_2017
Compiler correctness proofs for higher-order concurrent languages are difficult: they involve establishing a termination-preserving refinement between a concurrent high-level source language and an implementation that uses low-level shared memory primitives. However, existing logics for proving concurrent refinement either neglect properties such as termination, or only handle first-order state. In this paper, we address these limitations by extending Iris, a recent higher-order concurrent separation logic, with support for reasoning about termination-preserving refinements. To demonstrate the power of these extensions, we prove the correctness of an efficient implementation of a higher-order, session-typed language. To our knowledge, this is the first program logic capable of giving a compiler correctness proof for such a language. The soundness of our extensions and our compiler correctness proof have been mechanized in Coq.
Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning jung-2015-iris
Verified Software Toolchain appel_vst_2011
External (31)
- Artifact for the "Lawyer: Modular Obligations-Based Liveness Reasoning in Higher-Order Impredicative Concurrent Separation Logic" paper of OOPSLA'26 (2026)
- Technical appendix for the Lawyer paper (2026)
- Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness (2025)
- Nola: Later-Free Ghost State for Verifying Termination in Iris (2025)
- A flexible specification approach for verifying total correctness of fine-grained concurrent modules (2024)
- Verifying Liveness Properties of Distributed Systems via Trace Refinement in Higher-Order Concurrent Separation Logic (2024)
- Fair Operational Semantics (2023)
- VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A (2023)
- Ghost Signals: Verifying Termination of Busy Waiting (2021)
- Ghost Signals: Verifying Termination of Busy-Waiting (Technical Report) (2021)
- TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs (2019)
- Certified concurrent abstraction layers (2018)
- Modular Termination Verification of Single-Threaded and Multithreaded Programs (2018)
- Safety and Liveness of MCS Lock - Layer by Layer (2017)
- Lecture Notes on Iris: Higher-Order Concurrent Separation Logic (2017)
- A program logic for concurrent objects under fair scheduling (2016)
- Modular Verification of Finite Blocking in Non-terminating Programs (2015)
- Deep Specifications and Certified Abstraction Layers (2015)
- Mechanized verification of fine-grained concurrent programs (2015)
- TaDA: A Logic for Time and Data Abstraction (2014)
- Impredicative Concurrent Abstract Predicates (2014)
- VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java (2011)
- A theory of indirection via approximation (2010)
- Deadlock-Free Channels and Locks (2010)
- A New Type System for Deadlock-Free Processes (2006)
- An indexed model of recursive types for foundational proof-carrying code (2001)
- Conjoining specifications (1995)
- Linearizability: a correctness condition for concurrent objects (1990)
- Information Processing 83, Proceedings of the IFIP 9th World Computer Congress, Paris, France, September 19-23 (1983)
- Proving termination with multiset orderings (1979)
- Verifying properties of parallel programs: an axiomatic approach (1976)