Maximally stateless model checking for concurrent bugs under relaxed memory models
Alan Huang · 2016
Shared-memory multiprocessor architectures are now ubiq-uitous. To achieve higher performance, the constraints on the memory models become weaker. This makes it more challenging to verify concurrent programs. It is known that sequential consistency (SC) [7] is the most intuitive memory model. However, even for SC, it is challenging enough to verify the correctness of concurrent programs, because the number of the interleavings grows exponentially with the number of threads and the size of the program. For relaxed memory models, the verification problem is more tough because operations from the same thread can be re-ordered and there is even no globally consistent order among the operations of different threads. For example, for the Total Store Order (TSO) [9] and Partial Store Order (PSO) memory models, the order between a write and a following read or a write to different memory locations [2] can be re-ordered non-deterministically in the store buffer.