zbMATH — the first resource for mathematics

An efficient partial order reduction algorithm with an alternative proviso implementation. (English) Zbl 1017.68069
Summary: This paper presents a partial order reduction algorithm called Twophase that generates a significantly reduced state space on a large class of practical protocols over alternative algorithms in its class. The reduced statespace generated by Twophase preserves all CTL\(^*\)-X assertions. Twophase achieves this reduction by following an alternative implementation of the proviso step. In particular, Twophase avoids the in-stack check that other tools use in order to realize the proviso step. In this paper, we demonstrate that the in-stack check is inefficient in practice, and demonstrate a much simpler alternative method of realizing the proviso. Twophase can be easily combined with an on-the-fly model-checking algorithm to reduce memory requirements further. A simple but powerful selective caching scheme can also be easily added to Twophase.
A version of Twophase using on-the-fly model-checking and selective caching has been implemented in a model-checker called PV (Protocol Verifier) and is in routine use on large problems. PV accepts a proper subset of Promela and a never automaton expressing the LTL-X assertion to be verified. PV has helped us complete full state-space search several orders of magnitude faster than all alternative tools available in its class on dozens of real protocols. PV has helped us detect bugs in real distributed shared memory cache coherency protocols that were missed during incomplete search using alternate tools.

68Q65 Abstract data types; algebraic specification
Full Text: DOI