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.
Tue 16 JunDisplayed time zone: Tijuana, Baja California change
09:15 - 10:55 | Concurrency IIResearch Papers at PLDI Main BLUE (Portland 254-255) Chair(s): Suresh Jagannathan Purdue University | ||
09:15 25mTalk | Composing Concurrency Control Research Papers Ofri Ziv Tel Aviv University, Alex Aiken Stanford University, Guy Golan-Gueta Yahoo Labs, G. Ramalingam Microsoft Research, Mooly Sagiv Tel Aviv University Media Attached | ||
09:40 25mTalk | Dynamic Partial Order Reduction for Relaxed Memory Models Research Papers Media Attached | ||
10:05 25mTalk | Monitoring Refinement via Symbolic Reasoning Research Papers Michael Emmi , Constantin Enea LIAFA, Université Paris Diderot, Jad Hamza LIAFA, Université Paris Diderot Media Attached | ||
10:30 25mTalk | Preventing Glitches and Short Circuits in High-Level Self-Timed Chip Specifications Research Papers Stephen Longfield Cornell University, Brittany Nkounkou Cornell University, Rajit Manohar Cornell University, Ross Tate Cornell University Media Attached |