リリース・コンシステンシ・モデルとその実現の形式的仕様記述について

概要

論文の詳細を見る
我々は,形式的仕様記述言語Zの表記法とプロセス代数value-passing CCSを統合した形式手法を用いて,分散共有メモリシステムの振る舞いを定義したメモリ・コンシステンシ・モデルとそれらの実現の形式的な仕様記述と検証の研究を行っている.メモリ・コンシステンシ・モデルは,ストア命令やロード命令などに諸々のプログラム順序を定義してメモリアクセスを制約するものと,いつどのようにこれら命令の同期を取るべきかというプログラマの指定によりメモリアクセスを制約するものに大別される.我々は,以前,前者の代表としてコーザル・メモリ・コンシステンシ・モデルを取り上げ,このモデルと実現の形式的な仕様記述と検証に対するこの形式手法の有効性を報告した.そこで,本論文では,後者の代表としてリリース・コンシステンシ・モデルを取り上げ,このモデルと実現の形式的な仕様記述と検証を行なう.これら代表的な二つのモデルと実現の形式的仕様記述と検証を示すことで,この形式手法のメモリ・コンシステンシ・モデルに対する有効性を確認した.
一般社団法人情報処理学会の論文
1999-12-15