Method for verifying abstract memory models of shared memory multiprocessors

摘要

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.