Think Stitch
  最近の更新


0  プログラムの正当性検査ツール SSG の紹介

SSG というプログラムの正しさを検査するツールを開発したので,かんたんに紹介したいと思います.

プログラムの正しさといってもいろいろあります.SSG が対象にしているのは主に振る舞いに関する側面で,設計したプログラムの振る舞いが仕様で規定されているとおりにできているかどうかを検査するというものです.

ここで想定しているプログラムは,コンパイラや数値計算のプログラムのように入力から出力を計算して停止するようなものではなくて,ユーザや他のシステムと継続的なやり取りをするプログラムです.このようなプログラムをリアクティブプログラムといいます.家電や車載システム用の組込みプログラムとか,スマートフォンのアプリケーションとか,あるいはサーバ上のプログラムなどです.

このようなプログラムあるいはシステムは,一般に複数のコンポーネントを組み合わせて作ります.コンポーネントの中には自律的に他と並行して動くものがありますから,全体としての振る舞いはとても複雑なものになることがあります.そうすると設計段階で全体の振る舞いが期待しているものになっているかどうか,他に変なものが入っていないかどうか確認することがとても難しくなります.

SSG はこのような複数のコンポーネントからなるシステム全体の振る舞いをすべて計算して,網羅的に仕様と比較することで正しさを保証します.もし比較の途中で仕様と設計との間に違いを見つけたら,詳細なレポートを出力してくれます.設計者はこのレポートを見て,設計を修正することができます.

振る舞いをすべて計算して比較するとなると,その計算量は膨大なものになります.SSG はマルチコアを生かして並列に計算と検査を実行できます.最近はクラウド上でパワーもメモリもある仮想マシンをかんたんに利用することができます.SSG はこのクラウドを活用できるような設計になっています.

1  SSG でできる検査

SSG はプログラムの正しさ(正当性,あるいは詳細化関係ともいいます)を検査するツールです.正当性は大きく分けて安全性(悪いことは起こらない)と活性(できるべきことができる)の2つからなります. SSG はこの2つの検査を行うことができます.

加えて,複数のコンポーネントからなるシステムにはデッドロックとライブロックというよく知られた問題があります.デッドロックはシステムが停止して動けなくなってしまう問題,ライブロックはシステムが空回りして進捗しなくなってしまう問題です.SSG はこれら2つの問題を発見する機能を持っています.

2  仕様と設計・実装の記述

SSG は CSP という理論を基礎にしています.CSP は Communicating Sequential Processes の略で,並行システムの振る舞いを記述し,論証するための数学的理論です.発明者はクイックソート等で有名な Hoare さんです.

SSG ではこの CSP と型付き関数型プログラミングを融合したモデリング言語を定義して,これを使って仕様と,設計あるいは実装を記述します.主に通信の部分は CSP のオペレータを使い,内部の計算の部分では関数型言語を使います.

関数型言語の部分には論理型,整数型,リスト,集合,あるいはユーザ定義による代数的データ型など一般的なデータ型とプリミティブな組み込み関数が用意されています.

3  SSG を使う手順

SSG は直接検査を実行するのではなくて,実は検査を行うプログラムを生成するコンパイラという感じになっています.下図のように利用手順は大きく2つに分かれています.

まず CSP で記述した仕様と設計を SSG に入れます.そうすると C言語のソースコードが出てきます.これが実際に検査を行うプログラムのソースコードです.これを gcc でコンパイルして SSG の支援ライブラリ libssg をリンクすると検査プログラムができます.

検査プログラムを実行すると検査が行われてレポートが出力されます.検査の実行は上記のソースコード生成&コンパイルを行った計算機とは異なる計算機で実行することができます.つまりパワーのあるクラウドに持っていって実行できるのです.

4  SSG による検査の実行例とパフォーマンス

例としてリーダ・ライタ問題の安全性を検査してみました.リーダ・ライタ問題というのは,データベースのように複数の利用者が同時にデータを利用する際に,データの一貫性を壊さないように制御する問題です.具体的には複数のリーダは同時にアクセスしてもかまいませんが,一人でもライタ(データを更新するもの)がいるときには,他のリーダやライタを待たせないとデータを壊してしまう危険があります.この制御がうまくいっているかどうかが安全性の検査です.

ここでは制御のプロセスが4つ,リーダ・ライタがそれぞれ10,合計24プロセスの場合を検査しました.検査に使用したのは Google Compute Engine 上の仮想マシンで,スペックは次のとおりです:

測定結果は次のようになりました.横軸はスレッド数,縦軸はスレッドが1個の時の検査時間を1としたときの速度比です.つまりスレッドを増やしていった時にどれだけ速くなったかという指標です.

ご覧のとおり,32物理コアのところまでほぼ線形に性能が伸びます.32のところでグラフが折れているのは,そこから先が物理コアではなくハイパースレッドだからです.いくつか調べてみたところによると,ハイパースレッドの性能は物理コアの 0%〜30% くらいのようです.(マイナスになることもあるようですが^^;).

実装のモデルは約1,670万状態ありました.SSG はこれを5.5秒で検査してしまう能力を持っています.使用したメモリは約3.2GiB でした.この VM には 240GiB のメモリがあるので,かなりの規模の検査ができるでしょう.

興味を持ってもらえると幸いです.また機会があったら別の検査例を紹介したいと思います.

2017/7/1

© 2013-2017 PRINCIPIA Limited