| 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)
|
|---|
| 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.
|
