Test Model Checking and Abstraction for Branching Networks

	       Michael Jones and Ganesh Gopalakrishnan

We discuss our recent verification of the parallel random access
memory (PRAM) memory model for the Hierarchical Caching Network (HCN)
developed at MIT.  In this case study, we verified that any 3
processors in any HCN network always satisfy PRAM using a combination
of abstraction and test model checking.  We sucessfully reused an
abstraction technique previously developed for multi-bus PCI networks.
The test model checking was done using the Murphi model checker and
required checking just over 600,000 states on three network
topologies.  The PRAM memory model is the sequential consistency
memory model, but without global serialization of writes.  Since HCN is
intended to have sequential consistency, it should come as no surprise
that the HCN also satisfies PRAM.  During the the test model checking
phase of one particular network topology we uncovered a subtle coding
error at a depth of 60 steps.  After fixing the coding error, all
network topologies passed the PRAM test.

In this short tutorial talk, we will discuss the HCN protocol, and the
practical issues involved with using abstraction and test model
checking to reason about memory models in branching parameterized
systems.