弱いメモリモデル上でのプログラムの振舞いの検証

CPUはプログラムを書かれている通りには実行しません.

メモリはCPUに比べて反応が遅いので,最近のCPUはメモリにアクセスするロード命令やストア命令が完了するのを待たずに次の命令を実行したり,ロード命令やストア命令の順序を入れ替えたりまとめて実行したりして,なんとか高速にプログラムを実行しようとします.その結果,プログラムに書かれている通りに実行したのでは起こり得ないことが起こってしまいます.

このままではまともにプログラムが書けないので,通常のCPUは命令の順序の入れ替えによる影響を打ち消すような回路を持っていて,プログラムに書かれている通りの結果にしかならないように強制しています.しかし,それはシングルスレッドのプログラムに限った話です.マルチスレッドのプログラムでは,命令の実行順序が入れ替わっても正しく動作するようにプログラムすることは,プログラマの責任です.そして,実行順序が入れ替わる可能性も考慮したプログラムを書くことは非常に複雑で間違え易い仕事です.

実行順序の入れ替わり方もCPUによって様々です.パソコンで広く使われているx86アーキテクチャのCPUでは,限られた条件でしか入れ替わりません.一方スマートフォンやRaspberry Piで使われているARMアーキテクチャではx86よりも広い範囲の命令が入れ替わる可能性があります.

このプロジェクトでは,命令の実行順序が入れ替わったとしても正しく動作するプログラムかどうかを,プログラムを実行せずに検査するために,「モデル検査」という方法を研究しています.プログラムから本質を抜き出した「モデル」を作り,計算機の力を使って,そのモデルを実行させたときに起こり得る全ての計算機の状態(実行の途中状態や実行結果)を網羅的に調べる方法です.モデルを入力として,全ての状態を網羅的に調べるためのソフトウェアをモデル検査器と言います.

我々は,

  • 既存の命令の実行順序が入れ替わることを考慮していないモデル検査器で,命令の実行順序が入れ替わることまで考慮したモデル検査を行うようなモデルを作るための共通部品(ライブラリ)や,
  • 命令の実行順序が入れ替わることも考慮して全ての状態を調べることができるモデル検査器

を開発しています.また,これらを使ってソフトウェアのバグを探しています.

このプロジェクトでは千葉工業大学の安部達也氏と共同で研究しています.

発表

  • Tatsuya Abe, Tomoharu Ugawa, Toshiyuki Maeda and Kousuke Matsumoto: Reducing State Explosion for Software Model Checking with Relaxed Memory Consistency Models. SETTA 2016 (Beijing, China), 2016
  • 松元稿如, 鵜川始陽, 安部達也, メモリモデルを考慮したメモリアクセスを提供するSPIN用ライブラリ. FOSE 2016 (琴平温泉), 2016. IEEE Computer Society Japan Chapter FOSE Young Researcher Award 受賞