Code Rewriting Used for Thread-Modular Model Checking of Concurrent Programs Under TSO

Abstract: A method for verifying safety properties of concurrent programs under TSO by model checking is presented. Rather than concretely modelling the write-buffers of a TSO architecture, this method works by succesively rewriting the code of the program being analyzed. The rewriting closely corresponds to the instruction reordering analogy sometimes used when describing the semantics of memory models (e.g. in Adve and Gharachorloo, Shared Memory Consistency Models: A Tutorial). The method is extended to, thread-modularly, verify systems with an unbounded number of threads.