Distributed dynamic partial order reduction

Abstract. Runtime (dynamic) model checking is a promising verification methodology for real-world threaded software because of its many features, the prominent ones being: (i) it avoids the need to extract a model and instead runs the actual code, and (ii) the precision of information available at run-time allows techniques such as dynamic partial order reduction (DPOR) to dramatically cut down the number of interleavings examined. Unfortunately, DPOR does not have many implementations for real thread libraries such as POSIX Pthreads, and suffers from high computational overheads due to a stateless search that requires re-executions. In our previous work [1], we designed a runtime model checker, inspect, that overcomes the first of these drawbacks. Inspect has been shown capable of detecting data races, deadlocks and other incorrect API usages in real-world PThreads C/C++ programs. In this paper, we describe a distributed version of inspect, which implements an extended DPOR [2] alg...

• Type: Journal
• Year: 2010
• Where: STTT
• Authors: Yu Yang, Xiaofang Chen, Ganesh Gopalakrishnan, Robert M. Kirby
• Keywords: Dynamic Partial Order, Partial Order Reduction, Promising Verification Methodology, STTT 2010