Counter-Example Guided Fence Insertion under TSO

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson, Ahmed Rezine

We give a sound and complete fence insertion procedure for concur- rent finite-state programs running under the classical TSO memory model. This model allows write to read relaxation corresponding to the addition of an un- bounded store buffer between each processor and the main memory. We introduce a novel machine model, called the Single-Buffer (SB) semantics, and show that the reachability problem for a program under TSO can be reduced to the reacha- bility problem under SB. We present a simple and effective backward reachability analysis algorithm for the latter, and propose a counter-example guided fence in- sertion procedure. The procedure is augmented by a placement constraint that allows the user to choose places inside the program where fences may be in- serted. For a given placement constraint, we automatically infer all minimal sets of fences that ensure correctness. We have implemented a prototype and run it successfully on all standard benchmarks together with several challenging exam- ples that are beyond the applicability of existing methods.

In Proceedings of the 18th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), 2012,

Last version (pdf) 2012