36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2015), June 13–17, 2015, Portland, OR, USA

Desktop Layout

Concurrency II
Research Papers
, Chair: Suresh Jagannathan
Dynamic Partial Order Reduction for Relaxed Memory Models
Naling Zhang, Markus Kusano, and Chao Wang
(Virginia Tech, USA)
Publisher's Version
Video
Abstract: 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 store buffering nondeterminism are lacking. We propose a new dynamic partial order reduction (POR) algorithm for verifying 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 to TSO and PSO without overhauling the verification algorithm. In addition to sound POR, we also propose a buffer-bounding method for more aggressively reducing the state space. We have implemented our new methods in a stateless model checking tool and demonstrated their effectiveness on a set of multithreaded C benchmarks.

Authors:


Time stamp: 2019-09-22T01:33:33+02:00