Symbolic Partial Order Methods for Rule Based, Parameterized Systems

by
Ritwik Bhattacharya

Advised by
Ganesh Gopalakrishnan

Explicit state enumeration based model checking is one of the key tools used in the verification of many of today's complex system designs, of which cache coherence protocols for modern multiprocessor systems are relevant examples. State explosion is often one of the biggest impediments to a successful verification run. Parital order reduction is one of a number of algorithms for state space reduction proposed in the literature. Partial order reduction methods rely on exploring a subset (often called the ample set) of all the enabled transitions from any given state. Ample sets depend crucially on the independence between transitions of a system. While it is possible to check independence syntactically, this analysis must necessarily be conservative, as only limited information is available at compile time. In particular, array references pose a difficult problem, and must often be conservatively approximated by a reference to potentially any element. In this paper, we first present a novel symbolic simulation and SAT based algorithm for computing indepenendence. In this simple approach, independence is formulated as a boolean proposition (possible since we only deal with finite systems), which can then be checked by a SAT solver for validity. The algorithm is presented in the context of Murphi, but is applicable to any explicit state enumeration based tool. Next, we present special heuristics for computing the ample set in a rule-based system such as Murphi, where the standard, process-based heuristics don't apply. These two techniques combine to give us a powerful partial order reduction algorithm for Murphi, as substantiated by the results presented. Finally, we present a proof that permits independence results to be carried over to higher instances of parameterized systems, under certain conditions. This achieves a considerable reduction of the overhead involved in computing independence for multiple instances of the same parameterized system.