2015 Fiscal Year Research-status Report
PGAS言語のメモリ一貫性に関するプログラム検証理論とその実装
| Project/Area Number |
25871113
|
|---|
| Research Institution | Chiba Institute of Technology |
|---|
Principal Investigator |
安部 達也 千葉工業大学, 人工知能・ソフトウェア技術研究センター, 上席研究員 (50547388)
|
|---|
| Project Period (FY) |
2013-04-01 – 2017-03-31
|
| Keywords | メモリ一貫性モデル / プログラム検証 / モデル検査 |
|---|
| Outline of Annual Research Achievements |
開発しているモデル検査器の有用性に関する論文(国際ワークショップ議事録)の執筆・発表は平成26年度までに終えていたため、平成27年度はそれの広報と実際のプログラミング言語の仕様書への適用を行った。具体的には、国際ワークショップ The 6th Workshop on Syntax and Semantics of Low-Level Languages において、本研究課題で行っている研究の概要を発表した。また、国産並列プログラミング言語 XcalableMP の仕様策定のワーキンググループに参加し、本研究課題で行った形式化されたメモリ一貫性モデルによる仕様記述の次期仕様書への採用を目指し、XcalableMP のメモリ一貫性モデルに関する章のドラフトの執筆を行った。また、主にアメリカで開発されている並列プログラミング言語 Chapel の開発者から仕様書に掲載しているプログラム例がメモリ一貫性モデルの観点から正しいかの確認を依頼されたため、これのフィードバックを行った。
また、メモリ一貫性モデルを考慮したプログラム検証において、正しさを保証するためのプログラム論理を構築できたため、それを使ってこれまでにプログラム論理で正しさを保証されていないプログラムを検証することができることを紹介する論文を執筆した。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
研究実績の概要の最後に書いた論文の執筆について、採択までを平成27年度中に終える予定であったが、間に合わなかった。
|
| Strategy for Future Research Activity |
研究実績の概要の最後に書いた論文について、採択までを平成28年度中に終える予定である。
|
| Causes of Carryover |
国際会議向けに論文を執筆したが、投稿・採択までを平成27年度中に終えることができなかったため、その国際会議参加費用として計上していた予算に余りが生じた。
|
| Expenditure Plan for Carryover Budget |
国際会議参加費用に充てる。
|
| Remarks |
本研究課題で実装した検査器を公開しているウェブページ。
|
