| 研究課題/領域番号 |
16K21335
|
|---|
| 研究種目 |
若手研究(B)
|
| 配分区分 | 基金 |
|---|
| 研究分野 |
ソフトウェア
高性能計算
|
|---|
| 研究機関 | 千葉工業大学 |
|---|
研究代表者 |
安部 達也 千葉工業大学, 人工知能・ソフトウェア技術研究センター, 上席研究員 (50547388)
|
|---|
| 研究期間 (年度) |
2016-04-01 – 2019-03-31
|
| 研究課題ステータス |
完了 (2018年度)
|
| 配分額 *注記 |
4,160千円 (直接経費: 3,200千円、間接経費: 960千円)
2018年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2017年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2016年度: 1,820千円 (直接経費: 1,400千円、間接経費: 420千円)
|
|---|
| キーワード | プログラム検証 / メモリ一貫性モデル / モデル検査 / ガベージコレクション / プログラム論理 / Non-multi-copy atomicity / IRIW / 定理証明 / 数理論理学 |
|---|
| 研究成果の概要 |
メモリ一貫性モデルを考慮することでおこなえる、状態の統合やリオーダリングされる命令の制御による状態爆発の回避に関する方法を提案しました。Non-MCAなメモリ一貫性モデルにセンシティブなプログラムであるIRIWをも検証できるプログラム論理を構築しました。モデル検査器SPINをメモリ一貫性モデル込みで検査できるようにライブラリを開発しました。並列プログラミング言語XcalableMPのメモリ一貫性モデルの策定をおこないました。開発しているモデル検査器で並列コピーガベージコレクションの検査をおこないました。Non-MCAなメモリ一貫性モデルでのモデル検査で有効なLDRFという概念を提唱しました。
|
| 研究成果の学術的意義や社会的意義 |
プログラムを世に出す前にその安全性を検証する手法を研究・開発しました。本研究で開発した手法により、既存手法に対して検査時間の短縮と扱えるプログラムの範囲の拡張が実現されました。また、並列計算環境が普及した現代において広く使われているアルゴリズムである並行コピーガベージコレクションの検査を実演することで私たちの手法の有効性を示しました。研究したことは論文というかたちで出版されていることによりその内容を公知のものとし、また、開発したツールとプログラムをすべて公開したことでこれらを広く使用可能にしました。
|
