|
PGAS言語で採用されているメモリ一貫性モデルを調査し、それらを統一的に扱うプログラム検証理論の一つを提案し、ユーザ定義可能なメモリ一貫性モデルまでも考慮することができるモデル検査を行うための実装McSPINを開発・公開した。いくつかの最適化を提案し、それに関する論文を雑誌・国際会議に投稿し、採択された。プログラム論理の構築にも成功し、これを記載した論文を雑誌に投稿し、採択された。また、検証理論で使用する記述言語で、実際のPGAS言語であるところのXcalableMPのメモリ一貫性モデルを記述した。これはXcalableMPの仕様策定の規格部会で採用が承認され1.3版から収録される予定である。
|
