WEKO3
アイテム
並行プログラムのPartialStoreOrderingでの実行をモデル検査するためのReleaseメモリバリア
https://ipsj.ixsq.nii.ac.jp/records/222566
https://ipsj.ixsq.nii.ac.jp/records/22256653b30692-fe52-4095-8e77-400b20c613d7
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-WPRO2019020.pdf (512.5 kB)
|
Copyright (c) 2019 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Symposium(1) | |||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 公開日 | 2019-01-11 | |||||||||||
| タイトル | ||||||||||||
| タイトル | 並行プログラムのPartialStoreOrderingでの実行をモデル検査するためのReleaseメモリバリア | |||||||||||
| タイトル | ||||||||||||
| 言語 | en | |||||||||||
| タイトル | Promela Model of Acquire Fence for Model Checking of Concurrent Programs against Partial Store Ordering | |||||||||||
| 言語 | ||||||||||||
| 言語 | jpn | |||||||||||
| キーワード | ||||||||||||
| 主題Scheme | Other | |||||||||||
| 主題 | メモリモデル，モデル検査 | |||||||||||
| 資源タイプ | ||||||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_5794 | |||||||||||
| 資源タイプ | conference paper | |||||||||||
| 著者所属 | ||||||||||||
| 高知工科大学 | ||||||||||||
| 著者所属 | ||||||||||||
| 高知工科大学 | ||||||||||||
| 著者所属 | ||||||||||||
| 高知工科大学 | ||||||||||||
| 著者所属(英) | ||||||||||||
| en | ||||||||||||
| Kochi University of Technology | ||||||||||||
| 著者所属(英) | ||||||||||||
| en | ||||||||||||
| Kochi University of Technology | ||||||||||||
| 著者所属(英) | ||||||||||||
| en | ||||||||||||
| Kochi University of Technology | ||||||||||||
| 著者名 |
鵜川, 始陽
× 鵜川, 始陽
× 松元, 稿如
× 飯干, 寛幸
|
|||||||||||
| 著者名(英) |
Tomoharu, Ugawa
× Tomoharu, Ugawa
× Kosuke, Matsumoto
× Hiroyuki, Iiboshi
|
|||||||||||
| 論文抄録 | ||||||||||||
| 内容記述タイプ | Other | |||||||||||
| 内容記述 | 我々は，並行プログラムの弱いメモリ一貫性モデルでの振舞いをモデル検査するためのモデル集（以下，モデル検査ライブラリ）であるMMLibを開発している．SPINモデル検査器で検査するために，Promelaで記述されたモデルに対して，共有変数のリードとライトを，MMLibが提供するマクロの呼出しに置き換えるだけで，TSOやPSOに従った振舞いを検査できるようになる．これまでMMLibにはacquire-releaseフェンスが存在しなかったため，それを用いたプログラムを検査できなかった．本研究では，このうちPSOのreleaseフェンスのモデルを実装した．releaseフェンスの使用に誤りがあることが分かっている並行GCをMMLibを使って検査し，誤りが検出されることを確認した． | |||||||||||
| 書誌情報 |
第60回プログラミング・シンポジウム予稿集 巻 2019, p. 119-128, 発行日 2019-01-11 |
|||||||||||
| 出版者 | ||||||||||||
| 言語 | ja | |||||||||||
| 出版者 | 情報処理学会 | |||||||||||
