「並行プログラミング言語へのチャネル使用法宣言の導入」[論文誌Vol.48, No.SIG10(PRO33), pp. 101-113(2007)]

平成19年度論文賞受賞者の紹介

「並行プログラミング言語へのチャネル使用法宣言の導入」[論文誌Vol.48, No.SIG10(PRO33), pp. 101-113(2007)]

[論文概要]
 並行プログラムのデッドロック等の性質の検証のため,使用法表現という通信チャネルの使われ方を表す式を型推論によって求める枠組みが小林らによって提案されている.本研究では,使用法表現をプログラマが宣言できるようにこの型システムを拡張することで,通信がプログラマの意図どおりに行われるかどうかを静的に検証できるようにする.拡張に当たっての主な課題は,使用法表現間の部分型関係判定アルゴリズムの構築である.部分型関係は一般に決定不能であるため,宣言できる使用法を制限し,部分型関係判定問題をペトリネットの到達可能性判定問題に帰着する.

[推薦理由]
 並行プログラムの通信チャネルが正しく使われているかを型によって判定する方法を提案している.この型は単に送受信されるデータの型のみではなく,チャネルが送受信に使われる回数なども指定することができる.これにより,システムの動作を静的に検証することが可能になる.本論文では,チャネルの使用方法の表現力が従来よりも高くなっており(正規言語から決定性ペトリネット言語に拡張されている),その判定アルゴリズムをペトリネットの到達可能性問題に帰着するなど,十分な新規性がある.また,この型検査アルゴリズムを並行プログラミング言語Pictに試験的に実装するなど,今後実際の並行プログラムの検証への適用が期待できる.理論的にも実用的にも興味深く,論文賞に値する論文である.

須藤 崇 君  1983年生まれ。2008年東北大学大学院情報科学研究科情報基礎科学専攻博士課程前期2年の課程修了。同年よりパナソニックITS株式会社に勤務。

小林 直樹 君  1968年生.1991年東京大学理学部情報科学科卒.1993年同大学大学院理学系研究科情報科学専攻修士課程修了,同年博士課程進学.東京大学大学院理学系研究科情報科学専攻助手,講師,東京工業大学大学院情報理工学研究科助教授を経て2004年より東北大学大学院情報科学研究科教授,現在に至る.博士(理学).型理論,プログラム解析,並行計算などに興味を持つ.ACM,情報処理学会,各会員.2001年IFIP TC2 Manfred Paul Award,2003年日本IBM科学賞受賞.