ゲーム意味論による共有メモリ型並列プログラムの定式化と検証

• 研究課題/領域番号: 24500014
• 研究種目: 基盤研究(C)
• 配分区分: 基金
• 応募区分: 一般
• 研究分野: 情報学基礎
• 研究機関: 京都大学
• 研究代表者: 西村 進 京都大学, 理学(系)研究科(研究院), 准教授 (10283681)
• 研究期間 (年度): 2012-04-01 – 2016-03-31
• 研究課題ステータス: 完了 (2015年度)
• 配分額: 5,330千円 (直接経費: 4,100千円、間接経費: 1,230千円); 2015年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円); 2014年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円); 2013年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円); 2012年度: 1,820千円 (直接経費: 1,400千円、間接経費: 420千円)
• キーワード: 並列プログラミング / ゲーム意味論 / wait-notifyゲーム / 並列プログラム / プログラム検証

研究成果の概要

共有メモリ型並列プログラムのゲーム意味論を、wait-notifyゲームを用いることによって構築した。wait-notifyゲームが構成する圏において、可換強モナドの計算構造が誘導されることを示し、これによって関数型言語に書き換え可能変数を加えたAlgol言語の並列拡張の意味論がゲームのKleisli圏における射として与えられることと、full absraction定理を示した。公平性を考慮した並列実行に関しても、wait-notifyゲームにおいて非決定的選択も計算資源の一種であるとみなすことによって、WN有界戦略を構成することによって意味論を与えることができた。

研究成果

• [雑誌論文] May&Must-Equivalence of Shared Variable Parallel Programs in Game Semantics (2012)
  • 著者名/発表者名: Keisuke Watanabe, Susumu Nishimura
  • 雑誌名: Information Processing Society of Japan Transactions on Programming ({PRO}) 巻: 5(4)
  • NAID: 130003324428
  • 査読あり
• [学会発表] 組合せトポロジーによる分散並列プロトコル発見アルゴリズム (2016)
  • 著者名/発表者名: 西村 進
  • 学会等名: 第18回プログラミングおよびプログラミング言語ワークショップ (PPL2016)
  • 発表場所: ダイヤモンド瀬戸内マリンホテル
  • 年月日: 2016-03-07
• [学会発表] 順序複体上の連続変形発見による分散プログラムの導出 (2015)
  • 著者名/発表者名: 西村 進
  • 学会等名: 第二十六回 ALGI（代数，論理，幾何と情報科学研究集会）
  • 発表場所: 鳥取環境大学
  • 年月日: 2015-08-31
• [学会発表] 公平な並列実行のためのゲーム意味論 (2014)
  • 著者名/発表者名: 西村進
  • 学会等名: 日本ソフトウェア科学会第３１回大会
  • 発表場所: 名古屋大学
  • 年月日: 2014-09-09
• [学会発表] A Fully Abstract Game Semantics for Parallelism with Non-Blocking Synchronization on Shared Variables (2013)
  • 著者名/発表者名: Susumu Nishimura
  • 学会等名: Computer Science Logic 2013 (CSL 2013)
  • 発表場所: イタリア・トリノ大学