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

pldi2015-papers
09:15 - 10:55: Research Papers - Concurrency II at PLDI Main BLUE (Portland 254-255)
Chair(s): Suresh JagannathanPurdue University
pldi2015-papers09:15 - 09:40
Talk
Ofri ZivTel Aviv University, Alex AikenStanford University, Guy Golan-GuetaYahoo Labs, G. RamalingamMicrosoft Research, Mooly SagivTel Aviv University
Media Attached
pldi2015-papers09:40 - 10:05
Talk
Naling ZhangVirginia Tech, Markus KusanoVirginia Tech, Chao WangVirginia Tech
Media Attached
pldi2015-papers10:05 - 10:30
Talk
Michael Emmi, Constantin EneaLIAFA, Université Paris Diderot, Jad HamzaLIAFA, Université Paris Diderot
Media Attached
pldi2015-papers10:30 - 10:55
Talk
Stephen LongfieldCornell University, Brittany NkounkouCornell University, Rajit ManoharCornell University, Ross TateCornell University
Media Attached