UCLA

Concurrent programming is often error-prone due to the non-deterministic nature of multi-thread executions. Programmers typically reason about their concurrent programs in the context of sequential consistency. Under sequential consistency, instructions in a concurrent program are executed to generate memory events in a linear global order that is consistent with the order specified by the source program, i.e., the program order. However, the assumption of sequential consistency is too strong in practice, given today’s processor designs. To achieve better performance, processors today often adopt a weak memory model. Under a weak memory model, instructions are not guaranteed to be executed consistently with the program order, due to optimizations such as out-of-order execution and instruction reordering. As a result, previous correctness results of software tools need to be re-visited with considerations of weak memory models. In this thesis, we demonstrate the issues of previous correctness results of software tools and provide new methods for reasoning about their correctness under weak memory models.