Tue 16 Jun 2015 09:40 - 10:05 at PLDI Main BLUE (Portland 254-255) - Concurrency II Chair(s): Suresh Jagannathan

Under a relaxed memory model such as TSO or PSO, a concurrent program running on a shared-memory multiprocessor may observe two types of nondeterminism: the nondeterminism in thread scheduling and the nondeterminism in store buffering. Although there is a large body of work on mitigating the scheduling nondeterminism during runtime verification, methods for soundly mitigating the nondeterminism in store buffering are lacking. We propose the first dynamic partial order reduction (POR) algorithm for runtime verification of concurrent programs under TSO and PSO. Our method relies on modeling both types of nondeterminism in a unified framework, which allows us to extend existing POR techniques (persistent-set based reductions) to TSO/PSO without overhauling the verification algorithm. In addition to the sound POR method, we also propose a new buffer bounding method for more aggressively reducing the state space. We have implemented our new methods in a stateless software model checking tool and demonstrated their effectiveness on a set of multithreaded C benchmarks.