SWETグループが考える形式手法の現在とこれからの可能性

こんにちは、SWETの鈴木穂高（@hoddy3190）です。

私は、こちらの記事で紹介されているようなAndroidテストの教育活動をする傍ら、形式手法という技術の可能性を模索しています。今回は、形式手法についての簡単な説明や、調べていくにつれてわかってきた実用可能性等をご紹介できればと思います。

動機

まず、なぜ私が形式手法について調べようと思ったのかをご説明します。

SWETに所属する前、私は、別の部署で4年ほどゲーム開発に携わっていました。
そこでよく課題に感じていたのは、日本語で書かれる仕様の不備（考慮漏れ、記載漏れ、矛盾など）により、大きな手戻りにつながることが多いということでした。
開発プロセス上でそのような問題が発生すると、当然再発防止策MTGが開かれます。有識者のレビューを開発フェーズのより早い段階で組み込むようにするフロー改善や、考慮漏れを防ぐためのチェックリストなどがよく再発防止策として施行されます。

しかし、プロダクト特有の属人性の高い知識が求められるレビューやチェックリストの目視チェックは、段々と運用の綻びが出てきます。再発防止策として全く機能しないとまでは言いませんが、策の運用が崩れる様子を何度も目にしてきた中で、技術的なアプローチでこれらを解決できないかを考えるようになりました。

そこで出会ったのが、形式手法という技術です。

形式手法とは

形式手法とは、仕様を明確に記述したり、記述された設計の性質を機械的に検証する手法の総称です。形式手法にもいくつか種類がありますが、いずれも数学に基づく科学的な裏付けを持ちます。

種類	説明	代表的な記述言語・ツール
形式仕様記述	矛盾がなく論理的に正しい仕様を作成する	VDM++/Event-B/Z/Alloy etc.
モデル検査	プログラムの状態をモデル化することで、プログラムが期待される性質を満たすことを検証する	Promela/TLA+ etc.
定理証明	法則や説明に基づき、理論的に性質が成り立つことを示していく	Coq/Isabelle etc.

形式手法という言葉を聞いたことがないという方も多くおられると思いますが、実は形式手法自体の研究は1970年ごろから始まっており、その歴史は深いです。

日本ではまだあまり多くの導入事例は公開されていはいませんが、形式手法を適用して品質向上につながったという事例は、欧米を中心に多く報告されています。

導入事例としてどのようなものがあるのかは、形式手法の実践ポータルがよくまとまっていると思います。航空宇宙や鉄道など、高い信頼性が必要とされる分野での事例が多いです。 IT業界でも、AmazonのAWSに導入されているという事例はありますが、公開されている事例は多くありません。

私はまず、形式仕様記述とモデル検査について、調べてみたり、実際に触ってみたりして、前述した仕様書の問題への解決に活用できそうかを検討しました。その結果、形式仕様記述、モデル検査ともに、開発へ適用する際のコストの高さや、仕様書問題への解決策として本当に効果的かという点に懸念が出ました。

しかし、モデル検査においては、設計や実装の考慮漏れを防げる可能性がありそうだということがわかってきました。早くも動機の部分とずれが生じてしまいましたが、形式手法の可能性をさらに深掘る投資の価値はありそうだということで、モデル検査についてさらに詳しく調べてみることにしました。なお、仕様書問題に対しても、現在、形式仕様記述とはまた別のアプローチの解決策を模索していますが、今回は触れません。

モデル検査について

モデル検査とは、システムを有限個の状態を持つモデルで表現し、モデルが取りうるすべての状態を機械的かつ網羅的に検査することで、システムが仕様を満たすことを確認する手法です。

例えば、1から3の整数値を取りうる変数a, bがあったとし、「aとbの積が常に9以下である」が成り立つのかを確認したいとしましょう。モデル検査の手順としては、次のようになります。

検査したいもの（仕様書、ソースコードなど）から専用のモデリング言語でモデルを作成する
検査対象が満たすべき性質から検査式を作成する
モデル検査ツールにかける

モデルを作成すると下のようになります。検査式は、assertから始まる部分になります。モデル検査のモデルを書くための言語にはいくつか種類があるのですが、ここではPromelaという言語で記述しています。

sample.pml

inline Choose(n) {
    // 他のプログラミング言語でよく見るif文とは意味が異なり、
    // "::"で始まる3つの文のうち、非決定的に（ランダムに）実行される
    // 網羅的な検査をするときは、ここで取りうるすべてのパターンが探索される
    if
    :: n = 1
    :: n = 2
    :: n = 3
    fi
}

active proctype P() {
    int a = 0, b = 0
    Choose(a) // 上で定義しているChooseがインライン展開され、aには1から3のいずれかの値が代入される。
    Choose(b)
    assert(a * b <= 9)
}

モデル検査ツールにはSpinというツールを使います。コマンドラインで検査にかけることができます。

$ spin -a -o2 ./sample.pml # spinはHomebrewでインストール可能
$ gcc -o pan pan.c
$ ./pan -c0 -e
$ spin -pglsr -t1 sample.pml   # 結果出力

検査のロジックとしては、 (a, b) = (1, 1), (1, 2), ...,(3, 2), (3, 3)と取りうるすべての組み合わせを網羅的に探索した上で、a * b <= 9を満たすことを確認します。モデルに一切そういうロジックを書かずに、このような網羅的な探索ができるのも、モデル検査の良いところです。

では、検査式をassert(a * b < 9)に置き換えるとどうなるでしょう。その場合、a * b < 9を満たさなかったaとbのすべての組を反例として示してくれます。

using statement merging
  1:    proc  0 (P:1) a.pml:5 (state 3) [a = 3]
  2:    proc  0 (P:1) a.pml:5 (state 9) [b = 3]
spin: a.pml:13, Error: assertion violated
spin: text of failed assertion: assert(((a*b)<9))
  2:    proc  0 (P:1) a.pml:13 (state 13)   [assert(((a*b)<9))]
spin: trail ends after 2 steps
#processes: 1
  2:    proc  0 (P:1) a.pml:14 (state 14) <valid end state>
1 process created

(a, b) = (3, 3)のときに、検査式を満たさなかったことがわかります。

このように、モデル検査は、自動的に網羅的な検査をしてくれます。
そのため、並列システムの不整合のような再現させづらいタイミングで発生する不具合や、場合分け不足など設計の考慮不足が起因の不具合などを効果的に見つけてくれます。品質の高いソフトウェアを開発するための有効な手段の1つになるだろうと考えています。

一方、モデル作成の難易度が高いというデメリットもあります。プログラミング言語とは少し違うモデリング言語独特の文法で記述しないといけないことに加え、取りうる状態が膨大になればなるほど検査にかかる時間が増える（状態爆発）こともよくあり、実際のシステムをうまく抽象化してモデルを作成するスキルも求められます。

ここまでの内容に関して、詳しくは、私が2019/03/07のAndroid Test Night#6で発表した、「形式手法について調べてみた」に掲載しております。お時間があれば是非ご覧になってください。

PoCづくり

モデル検査の仕組みがわかったところで、プロダクトに適用できるのかどうかを確かめるために、いくつかの簡単なPoCを作ってみることにしました。 PoCとは、Proof of Conceptの略で、ここではモデル検査の実用性を確かめるために、簡単なデモを作ることを指しています。 PoCの題材決めに際しては、プロダクトに適用する可能性も加味し、プロダクト開発でよく起きる設計・実装上の問題にフォーカスすることを心がけました。

そこで、テーマとして挙げたのは、MySQLです。 MySQLは、トランザクション分離レベルごとの挙動の把握が難しく、障害につながることがよくあると思います。今回はMySQLにおけるdeadlockの検知をするモデルのご紹介をしたいと思います。

MySQLのlockの仕組みをかなり簡略化したモデルを作成し、複数のプロセスから、CRUDのクエリをランダムにそのモデルに投げ、異常が起きるかどうかを検査します。

/**
 *  MySQL 5.6
 *  REPEATABLE READ
 */

mtype {P1, P2}         // MySQLにクエリを発行するトランザクションの識別子
bool gap_lock_by_P1[6] // 共有ロック
bool gap_lock_by_P2[6] // 共有ロック

/**
 *
 *    negative infinity
 *  ---------------------
 *           |
 *           | gap0
 *           |
 *    +--------------+
 *    |    record    |
 *    +--------------+
 *           |
 *           | gap1
 *           |
 *    +--------------+
 *    |    record    |
 *    +--------------+
 *           |
 *           | gap2
 *           |
 *    +--------------+
 *    |    record    |
 *    +--------------+
 *           |
 *           | gap3
 *           |
 *  ---------------------
 *    positive infinity
 *    
 */

// row_num は select or update or deleteの検索対象（スキャン対象ではない）
inline lock_gap(proc_id, row_num) {
    if
    :: proc_id == P1 -> gap_lock_by_P1[row_num] = true
    :: proc_id == P2 -> gap_lock_by_P2[row_num] = true
    fi
}

// gap lockをかける処理であれば、実際はupdateでもdeleteでも良い
inline select_for_update(proc_id, row_num) {
    lock_gap(proc_id, row_num) // gap lockを起こす
}

inline insert(row_num) {
    // gap_lock_by_P1[row_num]とgap_lock_by_P2[row_num]が共にfalseになるまで待つ
    !gap_lock_by_P1[row_num] && !gap_lock_by_P2[row_num]

    // データ挿入は今回検査したい対象ではない
    // 書いても状態数を増やすことにつながるため書かない
}

inline commit(proc_id, row_num) {
    if
    :: proc_id == P1 -> gap_lock_by_P1[row_num] = false
    :: proc_id == P2 -> gap_lock_by_P2[row_num] = false
    fi
}

// トランザクション内の処理
inline exec(proc_id, row_num) {
    select_for_update(proc_id, row_num); insert(row_num); commit(proc_id, row_num)
}

proctype P(mtype proc_id) {
    // P1, P2はMySQLへの操作を、非決定的に繰り返し行う
    do
    :: exec(proc_id, 0)
    :: exec(proc_id, 1)
    :: exec(proc_id, 2)
    :: exec(proc_id, 3)
    od
}

// 一番最初に呼ばれる処理
init {
    atomic { // atomicで囲まれた部分は不可分処理となる（`run P(P1)`と`run P(P2)`の間に、他の処理がinterruptしないことが保証される）
        // 同じ処理を行うプロセスP1、P2を起動する
        run P(P1)
        run P(P2)
    }
}

では、モデル検査ツールにかけてみましょう。そうすると、invalid end stateというメッセージが出力されます。これは、網羅的な検査をしていく中で、実行可能な文がなくなったことを意味します。

spin -a -o2 ./deadlock.pml
gcc -DREACH -o ./pan ./pan.c
./pan -c0 -e
pan:1: invalid end state (at depth 5)
（中略）
spin -k deadlock.pml1.trail -t ./deadlock.pml
spin: trail ends after 6 steps
#processes: 3
        gap_lock_by_P1[0] = 1
        gap_lock_by_P1[1] = 0
        gap_lock_by_P1[2] = 0
        gap_lock_by_P1[3] = 0
        gap_lock_by_P1[4] = 0
        gap_lock_by_P1[5] = 0
        gap_lock_by_P2[0] = 1
        gap_lock_by_P2[1] = 0
        gap_lock_by_P2[2] = 0
        gap_lock_by_P2[3] = 0
        gap_lock_by_P2[4] = 0
        gap_lock_by_P2[5] = 0
  6:    proc  2 (P:1) ./deadlock.pml:53 (state 10)
  6:    proc  1 (P:1) ./deadlock.pml:53 (state 10)
  6:    proc  0 (:init::1) ./deadlock.pml:90 (state 4) <valid end state>
3 processes created

出力された結果を見ると、53行目のinsertの中で処理が先に進めなくなったことがわかります。 2つのプロセスP1、P2がgap0に対しselect for updateで共有ロックをとったものの、お互いinsertに進行ができなくなったようです。これがMySQLでいうところのdeadlockに相当します。

また、今回トランザクション内の処理（execの中身）は、select for update -> insert -> commitとしていますが、実際の運用では、このトランザクション内の処理を、プロダクトコード内の処理にあわせてCRUDの組み合わせや順番を変更することを想定しています。先に書いたとおり、モデル検査には「モデル作成の難易度が高い」というハードルがあります。それに対しては、例えば、MySQLのlockの機構のモデルをライブラリという形で提供し、query logからexecの中身を自動生成するようなことができれば、より低コストでモデル検査を行える可能性があると考えています。

設計確認としてのモデル検査

UIのようなイベント駆動での非同期処理の設計確認にもモデル検査が使えます。少し簡略化して書きますが、APIから取得した要素をリストビューに追加し、追加要素の中心となる位置までスクロールするという処理を実装した際、以下のような設計ミスに気づいた事例がありました。

意図していた挙動
- 追加するリスト要素を取得
- 要素を追加表示
- 中心となる要素の位置を計算
- その位置までスクロールする
起きてしまった意図しない挙動
- 追加するリスト要素を取得
- 中心となる要素の位置を計算
- その位置までスクロールする（追加表示が完了していないので、実際はスクロールは行われなかった）
- 要素を追加表示

非同期処理のように考慮漏れが起きやすい処理の設計の検証にもモデル検査が有効です。

/**
 *
 * 想定する仕様:
 * もともと、要素数が5のリストに、4つの要素を追加して、全体として9つの要素にする
 * 9つの要素が表示されたら、7番目の要素の位置までスクロールをする
 *
 */

int item_num = 5 // 初期の要素数
int position = 3 // 初期のスクロール位置

chan position_request = [0] of { bool } // スクロール位置更新リクエスト用の変数
chan item_num_request = [0] of { bool } // リスト更新リクエスト用の変数

chan position_reply = [0] of { bool } // スクロール位置更新リクエストの返信用の変数
chan item_num_reply = [0] of { bool } // リスト更新リクエストの返信用の変数

active proctype Items() {
    int new_item_num = 9
end:
    do
    :: item_num_request ? _ -> // リスト更新のリクエスト受信待ち
        // リスト更新のリクエストを受け取ったら、リストの要素数を9にする
        // 本来のプロダクトなら、"9"を導き出すロジックがあるはずだが、
        // モデル検査においてはそのロジックは関係ないので割愛
        item_num = new_item_num
        item_num_reply ! true
    od
}


active proctype Position() {
    int new_position = 7
end:
    do
    :: position_request ? _ -> // position更新のリクエスト受信待ち
        // スクロール位置更新のリクエストを受け取ったら、スクロール位置を更新する
        // ただし、要求されたスクロール位置が、リストに存在しない場合は更新処理をskipする
        if
        :: item_num >= new_position ->
            position = new_position
        :: else -> skip
        fi
        position_reply ! true
    od
}

proctype ClientA() {
    item_num_request ! true -> item_num_reply ? _ // リスト更新のリクエストを投げ、返信として新しい要素数が返るのを待つ
}

proctype ClientB() {
    position_request ! true -> position_reply ? _ // スクロール位置更新のリクエストを投げ、返信として新しいスクロール位置が返るのを待つ
}

init {
    atomic {
        run ClientA()
        run ClientB()
    }
    // 必ず、「9つの要素が表示されたら、7番目の要素の位置までスクロールをする」が満たされることを検査する
    (_nr_pr <= 3) -> assert(item_num == 9 && position == 7)
}

モデル検査にかけると、反例として、「要素数は9だが、スクロール位置は3」が経路と合わせて出力されます。

spin -pglsr -k rx.pml1.trail -t ./rx.pml
using statement merging
Starting ClientA with pid 3
  1:    proc  2 (:init::1) ./rx.pml:58 (state 1)    [(run ClientA())]
Starting ClientB with pid 4
  2:    proc  2 (:init::1) ./rx.pml:59 (state 2)    [(run ClientB())]
  3:    proc  4 (ClientB:1) ./rx.pml:53 (state 1)   [position_request!1]
  4:    proc  1 (Position:1) ./rx.pml:36 (state 1)  [position_request?_]
  5:    proc  3 (ClientA:1) ./rx.pml:49 (state 1)   [item_num_request!1]
  6:    proc  0 (Items:1) ./rx.pml:22 (state 1) [item_num_request?_]
  7:    proc  1 (Position:1) ./rx.pml:42 (state 4)  [else]
  8:    proc  1 (Position:1) ./rx.pml:42 (state 5)  [(1)]
  9:    proc  1 (Position:1) ./rx.pml:44 (state 8)  [position_reply!1]
 10:    proc  4 (ClientB:1) ./rx.pml:53 (state 2)   [position_reply?_]
 11: proc 4 terminates
 12:    proc  0 (Items:1) ./rx.pml:26 (state 2) [item_num = new_item_num]
 13:    proc  0 (Items:1) ./rx.pml:27 (state 3) [item_num_reply!1]
 14:    proc  3 (ClientA:1) ./rx.pml:49 (state 2)   [item_num_reply?_]
 15: proc 3 terminates
 16:    proc  2 (:init::1) ./rx.pml:62 (state 4)    [((_nr_pr<=3))]
spin: ./rx.pml:62, Error: assertion violated
spin: text of failed assertion: assert(((item_num==9)&&(position==7)))
 17:    proc  2 (:init::1) ./rx.pml:62 (state 5)    [assert(((item_num==9)&&(position==7)))]
spin: trail ends after 17 steps
#processes: 3
        item_num = 9
        position = 3
 17:    proc  2 (:init::1) ./rx.pml:63 (state 6) <valid end state>
 17:    proc  1 (Position:1) ./rx.pml:35 (state 9) <valid end state>
 17:    proc  0 (Items:1) ./rx.pml:21 (state 4) <valid end state>
5 processes created

今回の実装で問題だったのは、別々のストリームで非同期処理をおこなっていたことによるものでした。ログを見ると、

中心位置取得のリクエストが投げられる
追加するリスト要素を取得するリクエストが投げられる
中心位置取得のリクエストの結果が返ってくる
追加するリスト要素を取得するリクエストの結果が返ってくる

となっており、意図していた挙動とは異なることがわかります。

別々のストリームで非同期を走らせると、処理順番は常に同じにならないというのは、非同期処理を扱う上で基本的な話ではあります。しかし、設計の欠陥に実装した後気づくのと、実装の前に気づくのとでは手戻りのインパクトが異なります。今回の場合、別々のストリームを作るのではなく、単一のストリームで実装すればよいわけですが、これは、非同期処理実装時の注意の勘所がわかっていないと気づくのは難しいです。自分が考えている設計が本当にこれでよいのか、考慮漏れはなさそうかを確認するためにも有効だろう思いました。

今後の展望

いくつかのPoC作りを通して、モデリング言語で表現できる範囲がわかってきました。これからは、実際のプロダクトコードにモデル検査を適用できる部分を探してみたいと思います。もともと私が感じていた仕様書問題に対するアプローチという動機からは少し変わり、設計・実装に対するアプローチとなっておりますが、まずはその方向でさらなる可能性を見極めていきたいと思います。