Specification and Verification of Memory Consistency Models for Shared-Memory Multiprocessor Systems

概要

論文の詳細を見る
In this paper we formally specify and verify memory consistency models for shared-memory multiprocessor systems, focusing on the causal memory consistency model, by use of a formal method proposed by Taguchi and Araki. This formal method includes the combination of the Z notation and value-passing CCS (Calculus of Communicating Systems), and the state-based CCS semantics which has the ability to describe the evolution of processes and the transition of states simultaneously. So we specify separately the functional aspects and the concurrent aspects of the causal memory in the Z notation and value-passing CCS respectively and define the causal memory consistency model in terms of the state-based CCS semantics. We also verify that the specified causal memory meets the defined causal memory consistency model.
一般社団法人情報処理学会の論文
1999-02-15