並行システムの検証と実装

この一冊で、並行プログラミングの基礎理論、検証技術、実装手法が分かる。並行システムの CSP によるモデル化技術、モデル検証器 FDR による検証技術、Java ライブラリ JCSP による実装手法を詳細に解説。

『並行システムの検証と実装』 (磯部 祥尚 著、東野 輝夫 監修、近代科学社、2012 年 12 月刊) は、並行システムを CSP という形式手法でモデル化し、モデル検査器 FDR で検証し、Java のライブラリ JCSP で実装するまでを 1 冊で通して学ぶ専門書です。副題は「形式手法 CSP に基づく高信頼並行システム開発入門」で、トップエスイー実践講座の第 6 巻にあたります。版元の紹介文は、マルチコア CPU を備える PC やスマホのほか、組込みやスマートグリッドの処理にも欠かせない並行システムについて、基礎理論 (プロセス代数) である CSP を用いた構築、検証、実装の方法を概説すると説明し、ソフトウェア開発者を中心に、並行プログラミングに挑戦したい人への一冊と位置づけています。

全 10 章の構成、CSP と FDR と JCSP の 3 本柱

第 1 章「CSP,FDR,JCSP 概論」で 3 つの道具の紹介と効果、検証例と実装例を見渡したあと、第 2 章から第 4 章で CSP、FDR、JCSP の入門に 1 章ずつ進みます。第 2 章は CSP の基本演算子、変数と送受信、並行合成とチャネルを扱い、食事する哲学者の例で CSP のモデルを組み立てます。第 3 章は FDR の構文と使い方、第 4 章は JCSP のチャネルとプロセスで、同じ食事する哲学者を Java で実装します。第 5 章と第 6 章は CSP の理論で、状態遷移図表示ツール ProBE を使った動作の表現と、トレース方式、安定失敗方式、失敗発散方式による動作の解析を取り上げます。第 7 章「FDR 検証」は詳細化関係による検証例、抽象化による検証例、匿名性の検証例を扱い、第 8 章「JCSP 実装」は共用チャネル、ネットワークチャネル、GUI へ進みます。第 9 章の応用でチャネル渡しと送受信待ちの取消を扱い、第 10 章「CSP,FDR,JCSP 実践」でモデル化、検証、実装をひと続きで行います。付録 A は JCSP、FDR、TypeChecker、ProBE のインストール方法、付録 B は第 1 章から第 8 章までの演習問題の解答です。

テストでは届かない並行性の不具合と、モデル検査の考え方

並行処理 を含むプログラムでは、複数のプロセスの動きが交互に入り混じる順序の数が、プロセスや手順が増えるにつれて急激に増えます。テストはその中のいくつかの順序を実際に走らせて確かめる方法なので、まれな順序でしか起きないデッドロックや、共有データの読み書きの順序で結果が変わるレースコンディションを取りこぼすことがあります。モデル検査は、システムの振る舞いを有限の 状態遷移 のモデルとして書き、到達しうる状態を道具で網羅的に調べる方法です。CSP では、プロセス同士がチャネルを通じて事象をやり取りする形で振る舞いを書き、FDR は、仕様として書いたモデルが許す振る舞いの範囲に、設計のモデルの振る舞いが収まっているかという詳細化の関係を確かめます。JCSP は、チャネルとプロセスという CSP の考え方を Java で使えるようにするライブラリです。

Java と理論の章、2012 年刊の道具立て

版元は並行プログラミングに挑戦したい開発者を読者の中心に置いており、第 4 章と第 8 章の実装は Java で進みます。第 5 章と第 6 章はプロセス代数の理論を扱います。第 1 章から第 8 章の末尾には演習問題があり、付録 B で解答を確かめられます。付録 A のインストール方法は、2012 年の刊行時点の各ツールを前提にしています。刊行時の著者紹介では、著者は産業技術総合研究所の主任研究員で、形式手法による並行システムの検証の研究に携わっていたと紹介されています。

版元が挙げる並行プログラミングに挑戦したい人や、形式手法を実際の道具で試してみたい人にとって、本書はモデル化から検証、実装までを同じ例題でつなぐ専門書です。