Patent ID: 6892319

Claim:
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.