2016 Fiscal Year Annual Research Report
Transactional Symbolic Execution
| Project/Area Number |
26730033
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
荒堀 喜貴 東京工業大学, 情報理工学院, 助教 (50613460)
|
|---|
| Project Period (FY) |
2014-04-01 – 2017-03-31
|
| Keywords | 並行バグ / 記号実行 / トランザクション / 並行制御 / プログラム解析 / テスト / デバッグ |
|---|
| Outline of Annual Research Achievements |
本研究は，ソフトウェアによる並行処理のバグを高い精度で効率良く網羅する検査技術の確率を目的とする．この目的を達成するために，逐次処理のバグの高精度かつ高効率な網羅的検査技術として有効性が確認された動的記号実行と呼ばれる検査技術を並行処理のバグを扱えるよう拡張する．既存の動的記号実行では大規模な並行プログラムのバグを効率良く網羅できないという問題があるが，本研究はトランザクション並行制御と類似する方式に基づき動的記号実行を制御することにより，この問題の解決を図る．
本年度は，まず，共有資源アクセスの観測順序をもとに計算した危ういアクセス順序を並行制御の巻戻しの技術を応用することで効率的に再現する方式を実現した．次に，この方式に基づく動的記号実行系を，競合状態を引き起こしうる小規模なベンチマークプログラム群および大規模な実用並行プログラム群に適用し，競合の検出精度・効率を計測した．最後に，競合に起因する原始性違反等の並行脆弱性の検出機構を上記の動的記号実行系に実装し，その検出精度と効率を評価した．
|
