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

• Item type: Trans(1)
• 公開日: 1999-12-15
• タイトル: リリース・コンシステンシ・モデルとその現実の形式的仕様記述について
• タイトル / 言語: en
• タイトル: A Formal Specification of a Release Consistency Model and Its Implementation
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: オリジナル論文
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 奈良先端科学技術大学院大学 けいはんな
• 著者所属: 北九州大学大学院システム情報科学研究科 現在 筑紫女学園大学アジア文化学科
• 著者所属: 和歌山大学システム工学部 現在 奈良女子大学理学部情報科学科
• 著者所属: 奈良先端科学技術大学院大学
• 著者所属(英): en
• 著者所属(英): Nara Institute of Science and Technology Keihanna Interaction Plaza Inc.
• 著者所属(英): en
• 著者所属(英): Graduate School of Information Science and Electrical Engineering, Kyushu University Presently with Chikushi Jogakuen University, Department of Asian Studies
• 著者所属(英): en
• 著者所属(英): Faculty of Systems Engineering, Wakayama University Presently with Faculty of Science, Nara Women's University
• 著者所属(英): en
• 著者所属(英): Nara Institute of Science and Technology
• 著者名: 高田, 司郎; 田口, 研治; 城和貴; 福田, 晃
• 著者名(英): Shiro, Takata; Kenji, Taguchi; Kazuki, Joe; Akira, Fukuda
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 我々は 形式的仕様記述言語Zの表記法とプロセス代数value-passing CCSを統合した形式手法を用いて 分散共有メモリシステムの振る舞いを定義したメモリ・コンシステンシ・モデルとそれらの実現の形式的な仕様記述と検証の研究を行っている.メモリ・コンシステンシ・モデルは ストア命令やロード命令などに諸々のプログラム順序を定義してメモリアクセスを制約するものと いつどのようにこれら命令の同期を取るべきかというプログラマの指定によりメモリアクセスを制約するものに大別される.我々は 以前 前者の代表としてコーザル・メモリ・コンシステンシ・モデルを取り上げ このモデルと現実の形式的な仕様記述と検証に対するこの形式手法の有効性を報告した.そこで 本論文では 後者の代表としてリリース・コンシステンシ・モデルを取り上げ このモデルを取り上げ このモデルと実現の形式的な仕様記述と検証を行なう.これら代表的な二つのモデルと実現の形式的仕様記述と検証を示すことで この形式手法のメモリ・コンシステンシ・モデルに対する有効性を確認した.
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: 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.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464803
• 書誌情報: 情報処理学会論文誌数理モデル化と応用（TOM）; 巻 40, 号 SIG09(TOM2), p. 1-17, 発行日 1999-12-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7780
• 出版者 / 言語: ja
• 出版者: 情報処理学会