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.

Tue 16 Jun

Displayed 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
25m
Talk
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
25m
Talk
Dynamic Partial Order Reduction for Relaxed Memory Models
Research Papers
Naling Zhang Virginia Tech, Markus Kusano Virginia Tech, Chao Wang Virginia Tech
Media Attached
10:05
25m
Talk
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
25m
Talk
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