A Program Verification Theory of Memory Consistency Models on PGAS languages and its Implementation
| Project/Area Number |
25871113
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (B)
|
| Allocation Type | Multi-year Fund |
|---|
| Research Field |
High performance computing
Software
|
|---|
| Research Institution | Chiba Institute of Technology (2015-2016)
The Institute of Physical and Chemical Research (2013-2014) |
|---|
Principal Investigator |
Abe Tatsuya 千葉工業大学, 人工知能・ソフトウェア技術研究センター, 上席研究員 (50547388)
|
|---|
| Project Period (FY) |
2013-04-01 – 2017-03-31
|
| Project Status |
Completed (Fiscal Year 2016)
|
| Budget Amount *help |
¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2015: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
Fiscal Year 2014: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2013: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
|
|---|
| Keywords | メモリ一貫性モデル / プログラム検証 / モデル検査 / プログラム論理 / PGAS言語 / 形式的体系 |
|---|
| Outline of Final Research Achievements |
I have investigated various memory consistency models (MCMs) which are adopted by PGAS languages. I have proposed a program verfication theory to handle the MCMs, and developed and released McSPIN, a model checker with user-defined MCMs. Through the development, I have proposed some optimizations of model checking with MCMs. Six papers about them have been published. I have also constructed a program logic to handle MCMs, and one paper about the logic has been published. I have formally written the MCM which is adopted by a PGAS language XcalableMP in the description language of the program verification theory that I have proposed. The formal description of the MCM has been accepted by the XcalableMP working group, and will be published in the XcalableMP specification Version 1.3.
|
Report
(5 results)
Research Products
(19 results)
