Cartesian Partial-Order Reduction

Verifying concurrent programs is challenging since the number of thread interleavings that need to be explored can be huge even for moderate programs. We present a cartesian semantics that reduces the amount of nondeterminism in concurrent programs by delaying unnecessary context switches. Using this semantics, we construct a novel dynamic partial-order reduction algorithm. We have implemented our algorithm and evaluate it on a small set of benchmarks. Our preliminary experimental results show a significant potential saving in the number of explored states and transitions.

• Type: Conference
• Year: 2007
• Where: SPIN
• Authors: Guy Gueta, Cormac Flanagan, Eran Yahav, Mooly Sagiv
• Keywords: Concurrent Programs, Partial-order Reduction Algorithm, SPIN 2007, Theoretical Computer Science, Unnecessary Context Switches