Formalization and verification of shared-memory parallel programs in game semantics

2015 Fiscal Year Final Research Report

• Project/Area Number: 24500014
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Research Field: Fundamental theory of informatics
• Research Institution: Kyoto University
• Principal Investigator: Nishimura Susumu 京都大学, 理学(系)研究科(研究院), 准教授 (10283681)
• Project Period (FY): 2012-04-01 – 2016-03-31
• Keywords: 並列プログラミング / ゲーム意味論 / wait-notifyゲーム

Outline of Final Research Achievements

A game semantics for share-memory parallel programs was given by developing the wait-notify game. In the category of wait-notify games, it was shown that a computational structure of a commutative strong monad is induced and the strong monad gives rise to a Kleisli category, in which a game semantics for a parallel extension of an Algol-like language with mutable variables is defined by the arrows in the Kleisli category. It was also shown that the game semantics is fully abstract. Furthermore, it was also shown that a game semantics for fair execution of parallel programs can be formulated in a game model with WN-bounded strategies, a variant of wait-notify game where nondetermistic choice is also regarded as a shared computational resource.

Free Research Field

計算機科学