Talks
Reduction for Structured Concurrent Programs
Sept 2025
Summer School on Verification Technology, Systems & Applications (VTSA) 2025
University of Liège, Belgium
Abstract:
Commutativity reasoning based on Lipton's movers is a powerful technique for verification of concurrent programs. The idea is to define a program transformation that preserves a subset of the initial set of interleavings, which is sound modulo reorderings of commutative actions. Scaling commutativity reasoning to routinely used features in software systems, such as procedures and dynamic thread creation, remains a significant challenge.
In this work, we introduce a novel reduction technique for structured concurrent programs that unifies two key advances. First, we present a reduction strategy that soundly replaces thread forking and joining with sequential composition. Second, we generalize Lipton’s reduction to support atomic sections containing (potentially recursive) procedure calls. Crucially, these two foundational strategies can be composed arbitrarily, greatly expanding the scope and flexibility of reduction-based reasoning.
We implemented this technique in Civl and demonstrated its effectiveness on a number of challenging case studies, including a snapshot object, a fault-tolerant and linearizable register, the FLASH cache coherence protocol, and a non-trivial variant of Two-Phase Commit. I demonstrate this technique using an implementation of a concurrent snapshot object, which aims to return a consistent view of memory despite concurrent updates.
University of Liège, Belgium
Abstract:
Commutativity reasoning based on Lipton's movers is a powerful technique for verification of concurrent programs. The idea is to define a program transformation that preserves a subset of the initial set of interleavings, which is sound modulo reorderings of commutative actions. Scaling commutativity reasoning to routinely used features in software systems, such as procedures and dynamic thread creation, remains a significant challenge.
In this work, we introduce a novel reduction technique for structured concurrent programs that unifies two key advances. First, we present a reduction strategy that soundly replaces thread forking and joining with sequential composition. Second, we generalize Lipton’s reduction to support atomic sections containing (potentially recursive) procedure calls. Crucially, these two foundational strategies can be composed arbitrarily, greatly expanding the scope and flexibility of reduction-based reasoning.
We implemented this technique in Civl and demonstrated its effectiveness on a number of challenging case studies, including a snapshot object, a fault-tolerant and linearizable register, the FLASH cache coherence protocol, and a non-trivial variant of Two-Phase Commit. I demonstrate this technique using an implementation of a concurrent snapshot object, which aims to return a consistent view of memory despite concurrent updates.
Commutativity Based Refinement Proofs Using Civl
May 2025
Workshop on Verification of Distributed Systems (VDS) 2025
Rabat, Morocco
Abstract:
Civl is a static verifier for concurrent programs based on the idea of layered refinement. A program at a lower layer (such as a concrete, low-level implementation) refines a program at a higher layer (such as a high-level specification) in such a way that proving correctness of the higher layer implies proving correctness of the lower layer. One form of refinement is reducing the space of possible executions of a concurrent program. This can be achieved by exploiting the commutativity of statements, defined as movers in Lipton's reduction. A statement is a left (right) mover if it can be commuted to the left (right) of every other statement executed by a different thread, without altering the outcome of the execution. I describe a new refinement proof rule based on commutativity and use it to prove correctness of a snapshot algorithm. The goal of the algorithm is to return a snapshot of the entire memory, despite concurrent updates to different locations.
Rabat, Morocco
Abstract:
Civl is a static verifier for concurrent programs based on the idea of layered refinement. A program at a lower layer (such as a concrete, low-level implementation) refines a program at a higher layer (such as a high-level specification) in such a way that proving correctness of the higher layer implies proving correctness of the lower layer. One form of refinement is reducing the space of possible executions of a concurrent program. This can be achieved by exploiting the commutativity of statements, defined as movers in Lipton's reduction. A statement is a left (right) mover if it can be commuted to the left (right) of every other statement executed by a different thread, without altering the outcome of the execution. I describe a new refinement proof rule based on commutativity and use it to prove correctness of a snapshot algorithm. The goal of the algorithm is to return a snapshot of the entire memory, despite concurrent updates to different locations.