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

情報処理学会 Web Site 被引用文献1件 参考文献27件

書誌事項

タイトル別名
  • リリース・コンシステンシ・モデルとその実現の形式的仕様記述について
  • リリース コンシステンシ モデル ト ソノ ジツゲン ノ ケイシキテキ シヨウ キジュツ ニ ツイテ
  • A Formal Specification of a Release Consistency Model and Its Implementation

この論文をさがす

説明

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

We study on the formal specification and verification of the memory consistency models and their implementations that define the behavior of multiple memory accesses on distributed shared memory systems, using a formal method that combines the Z notation and value-passing CCS. Memory consistency models can be classified into two groups. One group includes systems which constrain memory accesses by specifying various program orders of write and read operations. The other includes systems which constrain memory accesses by programmers specifying how and when synchronization of write and read operations should be made. In a separate paper, we applied this formal method to formally specify and verify "Causal Memory Consistency Model"that is a representative of the former group mentioned above. We showed in the paper that this formal method is feasible enough for the formal specification and verification of that type of memory consistency model. In this paper, we apply the same formal method to formally specify and verify "Release Consistency Model"that is a representative of the latter group. We conclude that this formal method is feasible enough for the formal specification and verification of both types of memory consistency models.

収録刊行物

被引用文献 (1)*注記

もっと見る

参考文献 (27)*注記

もっと見る

キーワード

詳細情報 詳細情報について

問題の指摘

ページトップへ