A Specification and Verification Framework for Developing Weak Shared Memory Consistency Protocols

A specification and verification methodology for Distributed Shared Memory consistency protocols implementing weak shared memory consistency models is proposed. We propose an approach that enables a large range of weak memory models to be captured in terms of a single visibility order---an ordering of loads, stores, and synchronization operations, as perceived by all the processors. A given implementation is correct with respect to a weak memory model if it produces executions satisfying the visibility order for that memory model. Given an implementation, a designer annotates it with the events of the visibility order, and compares it against a reliable specification that exhibits the visibility order for the memory model, using reachability analysis