Specification and verification of memory consistency models for shared-memory multiprocessor systems

In this paper we will formally specify and verify memory consistency models for shared-memory multiprocessor systems, focusing on causal memory consistency model, by use of a formal specification technique proposed by Taguchi and Araki. The formal specification technique includes a language, which is based on the combination of the Z notation and CCS (Calculus of Communicating Systems), and the state-based CCS semantics, which integrates Z and CCS semantics. Causal memory requires that a read operation obtains the value that is consistent with other causally related read and write operations. A formal definition, implementation and verification of the causal memory have already been presented by Ahamad and Hutto. We will formally specify the behavior of the causal memory by the combination of Z and CCS and verify that the specified causal memory meets the causal memory consistency condition using the extended state-based CCS semantics.