| 講演名 | 1999/3/19 分散共有メモリの形式的仕様記述について 高田 司郎, 田口 研治, 城 和貴, 福田 晃, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 本稿では, ZとValue-passing CCSを統合した形式手法を用いて,分散共有メモリシステムの振る舞いを定義したメモリ・コンシステンシ・モデルとそれらの実現の形式的な仕様記述と検証を行う. メモリ・コンシステンシ・モデルは, ストア命令やロード命令などに諸々のプログラム順序を定義してメモリアクセスを制約するものと, いつどのようにこれら命令の同期を取るべきかというプログラマの指定によりメモリアクセスを制約するものに大別される. 本稿では, 前者の代表としてコーザル・メモリ・コンシステンシ・モデルを, 後者の代表としてリリース・コンシステンシ・モデルを取り上げる. これらの代表的な二つのモデルとそれらの実現の形式的仕様記述と検証を示すことで, この形式手法の分散共有メモリに対する有効性を確認した. |
| 抄録(英) | In this paper, we formally specify and verify some 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 this paper, we deal with "Causal Memory Consistency Model" as a representative of the former group and "Release Consistency Model" as 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. |
| キーワード(和) | メモリ・コンシステンシ・モデル / 分散共有メモリ / 形式手法 / Z / CCS |
| キーワード(英) | memory consistency model / distributed shared memory / formal method / Z / CCS |
| 資料番号 | SS98-65 |
| 発行日 |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 1999/3/19(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Software Science (SS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 分散共有メモリの形式的仕様記述について |
| サブタイトル（和） | |
| タイトル（英） | A Formal Specification of Distributed Shared Memory |
| サブタイトル（和） | |
| キーワード(1)（和/英） | メモリ・コンシステンシ・モデル / memory consistency model |
| キーワード(2)（和/英） | 分散共有メモリ / distributed shared memory |
| キーワード(3)（和/英） | 形式手法 / formal method |
| キーワード(4)（和/英） | Z / Z |
| キーワード(5)（和/英） | CCS / CCS |
| 第 1 著者 氏名（和/英） | 高田 司郎 / SHIRO TAKATA |
| 第 1 著者 所属（和/英） | 奈良先端科学技術大学院大学:けいはんな |
| 第 2 著者 氏名（和/英） | 田口 研治 / KENJI TAGUCHI |
| 第 2 著者 所属（和/英） | 九州大学大学院システム情報科学研究科 |
| 第 3 著者 氏名（和/英） | 城 和貴 / KAZUKI JOE |
| 第 3 著者 所属（和/英） | 和歌山大学システム工学部 |
| 第 4 著者 氏名（和/英） | 福田 晃 / AKIRA FUKUDA |
| 第 4 著者 所属（和/英） | 奈良先端科学技術大学院大学 |
| 発表年月日 | 1999/3/19 |
| 資料番号 | SS98-65 |
| 巻番号（vol） | vol.98 |
| 号番号（no） | 676 |
| ページ範囲 | pp.- |
| ページ数 | 8 |
| 発行日 | |