Teaching an SMT Solver to Think About Threads

The problem with thread interleavings

Proving that a multi-threaded program is correct means accounting for every order in which threads can execute. The space of possible interleavings grows exponentially with thread count — a fact that has kept concurrent program verification largely out of reach for real-world codebases.

The standard engineering response is to encode the program as a formula and hand it to an SMT solver. The solver searches the formula space for a counterexample, or proves no counterexample exists. This works, but it treats the SMT solver as a black box: all the structure of the concurrent program gets flattened into a pile of constraints, and the solver has to rediscover that structure on its own.

Interference relations as solver guidance

Our key observation was that thread interferences in real programs have structure. An interference happens when one thread reads a memory location that another thread has written. But which threads write which locations, and when, is not arbitrary — it is determined by the program's control flow and data flow.

We define an interference relation: a statically computed map of which thread actions can actually affect which other threads. If thread A never writes to a variable that thread B reads, they cannot interfere on that variable, and the solver does not need to consider that ordering.

The prototype tool, Zpre, extracts this interference relation from the program before invoking the SMT backend. Instead of a monolithic formula, the solver receives guidance about which portions of the search space are reachable — turning a black-box query into a more directed one.

Memory models matter

Modern processors do not execute instructions in the order you write them. The memory consistency model defines which reorderings are permitted. We evaluated Zpre across three models:

- SC (Sequential Consistency) — the intuitive model: instructions execute in order across all threads. - TSO (Total Store Order) — used by x86; write operations can be delayed in a store buffer. - PSO (Partial Store Order) — a further relaxation where different memory locations can have independent store buffers.

Verification under TSO and PSO is harder than SC because the solver must also account for the additional behaviors introduced by the memory model. The interference relation approach generalises across all three, which was a non-obvious part of the design.

Results

We benchmarked Zpre against CBMC, the leading bounded model checker, using the ConcurrencySafety category from the 2019 SV-COMP competition. Across all three memory models, Zpre solved more benchmarks within the time limit and spent less time on the benchmarks both tools solved.

The improvement was not uniform — programs with tightly coupled threads and frequent shared-memory access benefited most, because those are exactly the cases where the interference relation is most selective. Programs where every thread touches the same variables saw smaller gains, since the relation rules out fewer orderings.