TL;DR — Verifying concurrent programs is hard enough under sequential consistency. Under relaxed memory models (TSO, PSO), processors can reorder operations, making verification even harder. This paper introduces effective abstractions that make verification under relaxed models tractable.
The Problem
Modern processors do not execute memory operations in the order a programmer writes them. Under relaxed memory models like TSO (Total Store Order) and PSO (Partial Store Order), writes can be delayed in processor-local store buffers before becoming visible to other threads. This means that different threads can observe different values for shared variables at the same time.
For sequential consistency (SC), the state space is already large. Under TSO or PSO, the store buffers add an entirely new dimension: every pending write occupies a slot, and flushing can happen at any point. The result is an explosion of states that makes direct verification infeasible for all but the tiniest programs.
// A classic example: Dekker's mutual exclusion
Thread 1: Thread 2:
x = 1 y = 1
r1 = y r2 = x
// Under SC: r1=0 AND r2=0 is impossible
// Under TSO: r1=0 AND r2=0 CAN happen (both writes buffered)
The Key Idea
The core insight is simple but powerful: we do not need to track the exact contents of every store buffer. Instead, we can abstract the buffers, keeping only the information relevant for verification. The abstraction must be sound (it over-approximates the concrete behaviors), so any property verified on the abstract model also holds on the concrete one.
Specifically, the paper proposes tracking a bounded set of predicates about the buffer contents — such as "variable x has a pending write with value 1" — rather than maintaining the full ordered queue of buffered writes. This collapses many concrete buffer states into a single abstract state, dramatically reducing the state space.
Interactive Demo: Store Buffer Abstraction
Store Buffer Simulation
Store Buffer (Thread 1)
Store Buffer (Thread 2)
Shared Memory
| Variable | Value |
|---|---|
| x | 0 |
| y | 0 |
| r1 | - |
| r2 | - |
Execution Log
State Space: Concrete vs. Abstract
Toggle between memory models to see how abstraction reduces the state space. Each circle represents a reachable state in the verification.
SC: No buffers, so concrete and abstract have the same state count. Switch to TSO or PSO to see the impact of abstraction.
How It Works
Buffer Abstraction
In TSO and PSO, each processor has a FIFO store buffer that holds pending writes. The concrete state includes the full buffer contents and ordering. The abstract state replaces each buffer with a set of predicates that capture whether a variable has a pending write, and what value it holds, without tracking the exact queue order or multiplicity.
// Concrete buffer state (TSO, Thread 1):
buffer = [ (x, 1), (y, 3), (x, 2) ] // ordered queue
// Abstract buffer state:
{ x ∈ {1, 2}, y ∈ {3} } // set of pending values per variable
This abstraction is a sound over-approximation: every behavior of the concrete system is captured by the abstract one. The abstract system may include some behaviors that are not actually possible (spurious counterexamples), but it will never miss a real bug.
Sound Over-Approximation
Because the abstraction collapses multiple concrete states into one, it may introduce infeasible executions. However, this is safe for verification: if a property (e.g., mutual exclusion) holds in the abstract model, it must hold in the concrete one. If a counterexample is found in the abstract model, it may be either real or spurious.
Counterexample-Guided Refinement
When the verifier finds a potential violation in the abstract model, it checks whether the counterexample is feasible in the concrete model. If it is not (a spurious counterexample), the abstraction is refined — tracking more predicates about the buffer contents — and the verification is repeated. This loop, known as CEGAR (Counterexample-Guided Abstraction Refinement), ensures that the abstraction is only as detailed as it needs to be.
Key insight: By abstracting away buffer ordering and multiplicity, the state space shrinks dramatically. The CEGAR loop ensures soundness while keeping the abstraction as coarse as possible.
Results
The approach enables automatic verification of concurrent algorithms — such as mutual exclusion protocols, concurrent queues, and lock-free data structures — under TSO and PSO memory models. In many cases, the abstract model reduces the state space by an order of magnitude or more compared to full buffer enumeration, making previously intractable verification problems solvable.
- Dekker's, Peterson's, and Lamport's mutual exclusion algorithms verified under TSO and PSO.
- State-space reductions of 4x to 10x or more compared to concrete buffer enumeration.
- Counterexample-guided refinement eliminates spurious violations efficiently.
- The technique is general and applies to any program verified via predicate abstraction under relaxed memory.