さあ、並行バグを見つけよう！ 〜作って学ぶ形式手法入門〜 by チェシャ猫

概要

本ハンズオンでは、モデル検査器を自作する体験を通して、その内部的な仕組みを探「求」します。

形式手法は、システムを何らかの数学的な対象によって記述し、理論的に分析する手法の総称です。特に今回扱うモデル検査では、Kripke モデルと呼ばれるグラフ構造を探索することで、非同期系のバグを網羅的に検出することができます。古くは 1980 年代から研「究」されてきた技術ですが、近年では AWS をはじめとしたクラウドベンダや OSS でも採用されており、まさに実用が花開く普「及」期と言えるでしょう。

今回は例題として、Web 開発でありがちな「同時実行によるデータ不整合」を取り上げます。冒頭でモデル検査の考え方を解説した後、用意したスケルトンを段階的に埋める形式で、参加者自身でモデル検査器の自作と検証を体験します。

ハンズオン内容

• ミニ言語の構文木からグラフ構造への変換
• グラフ構造の可視化
• 非同期プロセスのインタリーブ合成
• 不変条件（安全性）の定義と検査

このハンズオンで得られるもの

• 形式手法やモデル検査の基礎知識
• 非決定的システムの仕様を記述・検証する技法
• 計算機科学を Web 開発に利用できるイメージ

想定する受講者

• 非同期・並行処理のバグに苦しんだことのある方
• Go または Perl の基本的なプログラムが書ける方
• 形式手法やモデル検査の予備知識は仮定しません

なぜこのハンズオンが面白いのか？

既存ツールを使用するモデル検査のチュートリアルは巷に数多ありますが、単に「ツールを動かしてみた」だけでは、その背後にある動作原理は見えません。本ハンズオンではツール自体を自作する体験を通して、シンプルな記述から複雑な挙動が生まれる驚き、そして理論を実世界に応用する面白さが実感できます。