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

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

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

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

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

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

我々は,

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

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

開発したライブラリをGithub上で公開しました.[Githubへのリンク]

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

発表

  • 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, November 9-11, 2016
  • 松元稿如, 鵜川始陽, 安部達也, メモリモデルを考慮したメモリアクセスを提供するSPIN用ライブラリ. FOSE 2016, 香川県琴平温泉, 2016年12月1日〜3日. IEEE Computer Society Japan Chapter FOSE Young Researcher Award 受賞
  • 松元稿如, 鵜川始陽, 安部達也, SPINで弱いメモリ順序のメモリモデルでのプログラムの実行を検査するためのライブラリの改良, 第115回プログラミング研究会 (PRO-2017-2), 秋田県, 2017年7月26日(水)〜7月28日(金)
  • Tatsuya Abe, Tomoharu Ugawa, and Toshiyuki Maeda:
    Reordering control approaches to state explosion in model checking with memory consistency models.
    VSTTE 2017, Heidelberg, Germany, July 22-23, 2017.
  • Tomoharu Ugawa, Tatsuya Abe, Toshiyuki Maeda:
    Model Checking Copy Phases of Concurrent Copying Garbage Collection with Various Memory Models.
    ACM PACMPL, Vol. 1, Issue OOPSLA, pp. 53:1 — 53:26, Vancouver, Canada, October 25-27, 2017.
    doi:10.1145/3133877 [slide]
  • Kosuke Matsumoto, Tomoharu Ugawa:
    Modelling Acquire and Release Fences for Promela Models of TSO and PSO Using Store Buffers.
    15th Asian Symposium on Programming Languages and Systems (APLAS 2017), poster session, Suzhou, China, November 27-29, 2017.
  • 飯干 寛幸, 松元 稿如, 鵜川 始陽,
    SPIN用メモリモデルライブラリmmlibを使った並行コピーGCのモデル検査,
    第20回プログラミングおよびプログラミング言語ワークショップ(PPL 2018) ポスターセッション, 鳥取県 皆生温泉, 2018年3月5日(月)〜3月7日(水).
  • Kosuke Matsumoto, Tomoharu Ugawa, Tatsuya Abe:
    Improvement of a Library for Model Checking under Weakly Ordered Memory Model with SPIN.
    Journal of Information Processing, Vol. 26, pp. 314-326, 2018.
    DOI: https://doi.org/10.2197/ipsjjip.26.314