Method for verifying abstract memory models of shared memory multiprocessors

A method of verifying, for a computing system having a plurality of processors and a memory having a plurality of locations being shared by each of the plurality of processors, a protocol for sequential consistency, comprising:

• providing an executable description of an automaton for the protocol to be verified;
• providing an executable description of at least one constrain automaton;
• providing an executable description of at least one processor checking automaton, said at least one processor checking automaton having an error state and being configured to detect the presence of a cycle of a given size in a graph that is a union of partial orderings of memory events at the shared memory locations and of total orderings of the memory events at the processors, a cycle being present in the graph if the error state is reached in said at least one processor checking automaton;
• submitting the protocol automaton, said at least one processor checking automaton and said at least one constrain automaton to a model checker;
• running the model checker to reach a set of states of the protocol automaton that are permitted by said at least one constrain automaton;
• during the running of the model checker, determining whether said at least one processor checker automaton has reached its error state;
• and
• if said at least one processor checker automaton has reached its error state, providing an indication that there is a sequential consistency error in the protocol automaton.