A Program Verification Theory of Memory Consistency Models on PGAS languages and its Implementation

2016 Fiscal Year Final Research Report

• 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
• Keywords: メモリ一貫性モデル / プログラム検証 / モデル検査 / プログラム論理

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.

Free Research Field

ソフトウェア