Thread-Modular Model Checking of Concurrent Programs under TSO using Code Rewriting

Abstract: Model checking is a well understood method for verifying correctness of concurrent programs. Commonly instructions in the verified programs are assumed to be executed in the order they occur in the programs. Most actual architectures, however, perform a number of optimizations when executing a program. Some such optimizations have the effect of reordering instructions or making the instructions appear to be reordered. The possible code reorderings are governed by the architecture's memory model. The particular memory model considered in this text is called TSO and is used on for example Intel x86 and SPARC V9. A method for verifying safety properties of concurrent programs under TSO by model checking is presented. The method works by exploring the set of reachable program states to verify that certain predefined error states can never be reached. The main optimization allowed by TSO is storing write instructions in an on-processor write buffer and later writing through the value to memory asynchronously with the other program instructions. Rather than concretely modelling the write buffers of a TSO architecture, the state exploration described in this paper works by successively rewriting the code of the program being analysed. The rewriting closely corresponds to the instruction reordering analogy sometimes used when describing the semantics of memory models. An extension of the method is also given, which allows verification of safety properties for programs with an unbounded number of threads.