文献

J-GLOBAL ID：202002279180698363   整理番号：20A0553758

SPINを用いたメモリモデルを意識したモデル検査の反例の可視化

Visualization of Counterexamples of Memory Model-aware Model Checking Using SPIN

著者 (2件)： Matsumoto Kosuke (Kochi University of Technology) ,  Ugawa Tomoharu (Kochi University of Technology)
資料名： Journal of Information Processing (Web)  (Journal of Information Processing (Web))
巻： 27  ページ： 489-498(J-STAGE)  発行年： 2019年 
JST資料番号： U0109A  ISSN： 1882-6652  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 英語 (EN)

抄録/ポイント： 現代の計算機処理装置において,プログラムにおけるメモリアクセス命令の順序(プログラム順序)は,命令がメモリ(メモリ順序)に反映する順序と必ずしも同じではない。このことは,並行プログラムを検証するとき,メモリ順序を考慮しなければならないことを意味する。以前に,SPINモデル検査器を使用するとき,メモリ順序を考慮に入れることによってプログラムのモデル検査を促進するライブラリ,MMLibを開発した。SPINへの入力は,命令型モデリング言語Promelaで書いたプログラムのモデルである。SPINが誤差を検出するとき,それは誤差に導く実行経路のトレースを生成する。誤差に導くものを決定するために,ユーザはこの反例を理解しなければならない。しかしながら,MMLibを用いて書いたモデルの反例は,内部MMLib実行ステップを含むため理解が困難であり,ユーザはメモリ順序を理解するためにMMLibの内部データ構造を解釈しなければならない。本論文では現在,MMLibを用いて書いたモデルの反例を可視化するためのソフトウェアを開発した。それは,反例の経路に沿って段階的にモデルステップの実行を可視化した。内部MMLibステップを可視化せず,ユーザモデルにおけるステートメントに対応する各ステップの実行のみを可視化した。それはまた,実行したがメモリに反映していないメモリアクセス命令を強調した。これにより,メモリの順序がプログラム順序と異なる時をユーザが認識した。(翻訳著者抄録)

シソーラス用語： *モデル検査 ,  記憶装置 ,  *計算機処理方式 ,  *接続 ,  順序 ,  言語 ,  誤差
準シソーラス用語： *SPIN ,  メモリ ,  *メモリアクセス ,  *計算機処理システム ,  反例 ,  命令型言語

著者キーワード (5件)： スピン ,  記憶モデル ,  モデル検査 ,  デバッグ ,  可視化

分類 (1件)： 計算機システム開発  (JD02010R)

引用文献 (16件)：

• [1] Abe, T. and Maeda, T.: A General Model Checking Framework for Various Memory Consistency Models, Proc. 19th High-Level Parallel Programming Models and Supportive Environments, pp.332-341 (2014).
• [2] Aljazzar, H., Leitner-Fischer, F., Leue, S. and Simeonov, D.: DiPro - A Tool for Probabilistic Counterexample Generation, Proc. 18th International SPIN Workshop on Model Checking Software, pp.183-187 (2011).
• [3] Behrmann, G., David, A., Guldstrand Larsen, K., Håkansson, J., Pettersson, P., Yi, W. and Hendriks, M.: Uppaal 4.0, Proc. 3rd International Conference on the Quantitative Evaluation of Systems, pp.125-126 (2006).
• [4] Czyz, J.K. and Jayaraman, B.: Declarative and Visual Debugging in Eclipse, Proc. 2007 OOPSLA Workshop on Eclipse Technology eXchange, pp.31-35 (2007).
• [5] Iiboshi, H. and Ugawa, T.: Towards Model Checking Library for Persistent Data Structures, Proc. 7th Non-Volatile Memory Systems and Applications Symposium, pp.119-120 (2018).

タイトルに関連する用語 (6件)： SPIN ,  モデル ,  意識 ,  モデル検査 ,  反例 ,  可視化