Counter-example guided fence insertion under TSO. (English) Zbl 1352.68047

Flanagan, Cormac (ed.) et al., Tools and algorithms for the construction and analysis of systems. 18th international conference, TACAS 2012, held as part of the European joint conferences on theory and practice of software, ETAPS 2012, Tallinn, Estonia, March 24 – April 1, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-28755-8/pbk). Lecture Notes in Computer Science 7214, 204-219 (2012).
Summary: We give a sound and complete fence insertion procedure for concurrent finite-state programs running under the classical TSO memory model. This model allows “write to read” relaxation corresponding to the addition of an unbounded 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 reachability problem under SB. We present a simple and effective backward reachability analysis algorithm for the latter, and propose a counter-example guided fence insertion procedure. The procedure is augmented by a placement constraint that allows the user to choose places inside the program where fences may be inserted. 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 examples that are beyond the applicability of existing methods.
For the entire collection see [Zbl 1238.68014].


68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)


Full Text: DOI