Efficient Verification of Concurrent Programs Over TSO Memory Model

TL;DR

This paper introduces an efficient, incremental verification method for multi-threaded programs under the TSO memory model, using bounded buffers to simplify complex control state reachability analysis.

Contribution

It presents a novel bounded-buffer verification approach with a proven buffer bound for finite data domain programs, implemented in the ProofTraPar tool.

Findings

Verification is feasible with bounded buffers up to a certain size.

The approach is sound and complete for finite data domain programs.

Experimental results show promising performance against state-of-the-art tools.

Abstract

We address the problem of efficient verification of multi-threaded programs running over Total Store Order (TSO) memory model. It has been shown that even with finite data domain programs, the complexity of control state reachability under TSO is non-primitive recursive. In this paper, we first present a bounded-buffer verification approach wherein a bound on the size of buffers is placed; verification is performed incrementally by increasing the size of the buffer with each iteration of the verification procedure until the said bound is reached. For programs operating on finite data domains, we also demonstrate the existence of a buffer bound k such that if the program is safe under that bound, then it is also safe for unbounded buffers. We have implemented this technique in a tool ProofTraPar. Our results against memorax [2], a state-of-the-art sound and complete verifier for TSO memory model, have been encouraging.