Ensuring The Correctness of Concurrent Programs under TSO Memory Models

For efficiency reasons, most modern processor architectures allow the reordering of CPU instructions, resulting in weak memory models. These models add extra program executions that are not intended by the programmer, often causing subtle run-time errors. To help solve this problem, such architectures also provide memory fences that allow to eliminate undesired behaviors. However, manual fence insertion, is a tedious and time- consuming activity, that also needs to be repeated each time the program is updated. Therefore, the development of efficient tools for automatic fence insertion is a crucial challenge in concurrent program design. In this thesis, we present, for the first time, a tool for automatic fence placement that is able to break the scalability barrier both concerning the added complexity due to the presence of event reorderings, and also concerning the number of threads that participate in the execution of the program. To this end, we propose a novel notion of correctness for concurrent programs, called persistence, that compares the behavior of the program under the weak memory semantics with that under the classical interleaving semantics. To make our ideas concrete, we consider the Total Store Ordering (TSO) memory model, and show how our method (i) allows modular reasoning that limits state space explosion due to the presence of parallel processes (threads), and (ii) abstracts away complex behaviors caused by weak memory models by translating the problem, in linear time, into a verification problem that is defined under the interleaving semantics. We have implemented a prototype and run it successfully on all standard benchmarks, together with several challenging examples that are beyond the capability of existing methods