第４回（平成２０年度）野口研究奨励賞

受賞者

寺内 多智弘 （てらうち たちお）

東北大学大学院情報科学研究科

研究の概要

この研究では「競合状態（レースコンディション）」の新しい検証手法を提案しています。レースとは二つ以上のスレッドが同時に同じ共有メモリ領域にアクセスして、少なくとも一方のアクセスが書き込みアクセスである状態であります。レースの存在はプログラムがスレッドスケジュラーにより予期しない動作をするなどプログラムのバグの原因となることが多いため、レース検証は正しい並列プログラムの基盤と言えます。

従来のレース検証は「lockset」の概念を用いる手法が多く、速度や精度に問題がありました。対してこの研究ではレース問題を線形計画問題に帰着するという画期的な手法を試みています。従来のlocksetベースの手法と違い複雑なlock linearityなどを推論する必要がなく、検証器の設計および理論的健全性の証明が単純化され、また高速な線形計画問題ソルバを使用することにより高速な検証が可能になりました。また、この手法は単純なロックによる同期パターンだけでなく、スレッドジョイン、セマフォ、シグナルなど従来の解析では扱えなかった様々な同期パターンにも対応しています。結果、より多くのマルチスレッドプログラムにおいて正確なレース検証が可能になりました。

受賞の感想

このような賞をいただき、大変光栄に思っております。受賞を励みに今後も精進したいと思います。

授賞式（2009年5月27日）