A method of verifying a protocol for a shared-memory multiprocessor system for
sequential consistency. In the system there are n processors and m memory locations
that are shared by the processors. A protocol automaton, such as a cache coherence
protocol automaton, is developed. The protocol automaton and a plurality of checker
automata are provided to a model checker which exhaustively searches the state
space of the protocol automaton. During the search, the plurality of checker automata
check for the presence of cycles in a graph that is the union of the total orders
of the processor references and the partial orders at each memory location. If
the plurality of checker automata detect the presence of a cycle, then the protocol
does not meet the sequential consistency requirement.
