A specification and verification framework for developing weak shared memory consistency protocols

Abstract

A specification and verification methodology for Distributed Shared Memory consistency protocols implementing weakshared memory consistency models is proposed. Our approach uniformly describes a wide range of weakmemory models in terms of a single concept—the visibility order of loads, stores, and synchronization operations, as perceived by all the processors. A given implementation is correct with respect to a weakmemory model if it produces executions satisfying the visibility order for that memory model. Given an implementation, the designer annotates it with events from the visibility order, and runs reachability analysis to verify it against a specification that is also similarly annotated. A specification is obtained in two stages: first, the designer reverse engineers an intermediate abstraction from the implementation by replacing the coherence networkwith a logically equivalent concurrent data structure. The replacement is selected in a standard way, depending almost exclusively on the memory model. Verification of the intermediate abstraction against a visibility order specification can be accomplished using theorem-proving. The methodology was applied to four snoopybus protocols implementing aspects of the Alpha and Itanium memory models, with encouraging results. © Springer-Verlag Berlin Heidelberg 2002.