• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to project page

2015 Fiscal Year Annual Research Report

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

Research Project

Project/Area Number 24500014
Research InstitutionKyoto University

Principal Investigator

西村 進  京都大学, 理学(系)研究科(研究院), 准教授 (10283681)

Project Period (FY) 2012-04-01 – 2016-03-31
Keywords並列プログラム / ゲーム意味論 / プログラム検証
Outline of Annual Research Achievements

前年度までの研究で、wait-notifyゲーム(渡辺氏との共同研究)の提案等によりゲーム意味論の並列実行の形式化や公平性への対応を達成してきた。研究当初から、これらをそのまま並列プログラムの検証に適用するには、並列性に起因する状態数の爆発を抑える効果的な手法が必要であることは予想されており、研究計画では正規表現で言うところのshuffle表現により状態数爆発を抑えることを予定していたが、その効果は限定的であろうとの見込みが判明していた。
本年度の研究では、この局面を打開するための技術的手段として組合せ幾何的モデルの援用を検討し、これがかなり有望であるとの確信を得ることができた。組合せ幾何的モデルは分散コンピューティングの理論で近年研究が活発に行われている手法で、並列プロセス間のコミュニケーションによる組合せ的非決定性を組合せ幾何における単体的複体(点・線・面などの図形の組合せ)の形で抽象化して表現する。このような抽象化によって状態爆発の緩和を行う手法の研究を行った。具体的には、並列プログラムの仕様を組合せ幾何的モデルで与えたとき、この仕様から導出される単体的複体上である一定の部分複体の変形を発見することで仕様を満たすプログラムを導出できることが原理的に可能であることを見出した。問題はそのような複体変形を効率良く発見することができるかどうかだが、並列プロセスの数を制限する等の一定の条件のもとで、いくつかの組合せ論的アルゴリズムを組み合わせて適用することにより現実的な時間で解が導き出せることを確認している。まだ途上の成果であるが、これらの内容については国内の研究集会で口頭・ポスター発表を行っている。

  • Research Products

    (2 results)

All 2016 2015

All Presentation (2 results)

  • [Presentation] 組合せトポロジーによる分散並列プロトコル発見アルゴリズム2016

    • Author(s)
      西村 進
    • Organizer
      第18回プログラミングおよびプログラミング言語ワークショップ (PPL2016)
    • Place of Presentation
      ダイヤモンド瀬戸内マリンホテル
    • Year and Date
      2016-03-07 – 2016-03-09
  • [Presentation] 順序複体上の連続変形発見による分散プログラムの導出2015

    • Author(s)
      西村 進
    • Organizer
      第二十六回 ALGI(代数,論理,幾何と情報科学研究集会)
    • Place of Presentation
      鳥取環境大学
    • Year and Date
      2015-08-31 – 2015-09-01

URL: 

Published: 2017-01-06  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi