Partial order reduction without the proviso

Journal ArticleIn this paper, we present a new partial order reduction algorithm that can help reduce both space and time requirements of on-the-fly explicit enumeration based verifiers. The partial order reduction algorithms described in [God95, HP94, Pel94, Pel96] were observed to yield very little savings in many practical examples. The reason was traced to the proviso in these algorithms that often caused their search to generate many unnecessary states. Our algorithm, called the two-phase algorithm, avoids the proviso, and follows an execution strategy consisting of alternating phases of partial order reduction of deterministic states and depth-first search. In this paper, we describe the two-phase algorithm, prove its correctness, describe a new verification tool employing it, and provide a number of significant examples, including directory based protocols of a multiprocessor, that demonstrate the superior performance of the two-phase algorithm