A New Partial Order Reduction Algorithm for Concurrent System Verification
Ratan Nalumasu, Ganesh Lalitha Gopalakrishnan · 1997
This paper presents a new partial order reduction algorithm called Two phase that is implemented in a verification tool, PV (Protocol Verifier). Two phase significantly reduces space and time requirements on many practically important protocols on which the partial order reduction algorithms implemented in previous tools (Godefroid 1995, Holzmann et al . 1994, Peled 1996) yield very little savings. This is primarily attributable to their use of a run-time proviso deciding which processes to run in a given state. Two phase avoids this proviso and follows a much simpler execution strategy that dramatically reduces the number of executions examined on a significant number of examples. We describe the Two phase algorithm, prove its correctness, and provide evidence of its superior performance on a number of examples including the directory based protocols of a multiprocessor under development.