Formalization and verification of shared-memory parallel programs in game semantics
| 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
|
| Project Status |
Completed (Fiscal Year 2015)
|
| Budget Amount *help |
¥5,330,000 (Direct Cost: ¥4,100,000、Indirect Cost: ¥1,230,000)
Fiscal Year 2015: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2014: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2013: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2012: ¥1,820,000 (Direct Cost: ¥1,400,000、Indirect Cost: ¥420,000)
|
|---|
| 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.
|
Report
(5 results)
Research Products
(5 results)
