Think Stitch
PRINCIPIA  最近の更新


Scheme でかんたんモデル検査器

実に怪しいタイトルですが,1時間ほどでできるかんたんなモデル検査器を作ってみます. かんたんですけど,けっこう楽しめますよ.

モデル記述

はじめにモデルの記述方法を決めます. 大げさにいうとモデル記述言語ということですけど,そんなたいそうなものではありません. S式を使うのでかんたんです. ここでは「コンピュータサイエンス入門 - 論理とプログラム意味論」という本で使われているリアクティブシステムの記法を参考にさせていただきました.

モデルの記述は,変数の宣言と状態マシンの記述からなるとします.

変数宣言

変数の宣言は,変数名と初期値をリストで並べるとします.

((変数名1 初期値1) (変数名2 初期値2) ...)

状態マシン

状態マシンの記述は次のようにします.

(状態マシン名 初期状態 状態遷移 ...)

状態マシン名と初期状態は単なる名前です. シンボルでも数でもいいとしましょう. 状態遷移は状態ごとに分けて記述することにします.

状態遷移 = (状態 遷移 ...)
遷移 = (遷移ラベル 遷移先状態 条件 変数変換)

状態は単なる名前です.シンボルでも数でもよいとしておきます.

遷移ラベルは遷移を区別するためのラベルで,これもシンボルでも数でもよいとしておきます. 条件は遷移が可能かどうかを判定する論理式です.いわゆるガードです. 条件では変数宣言で宣言した変数が参照できるものとします.

変数変換は,この遷移が発生したときに,各変数の値がどのように変化するのかを指定する式です. ここでは話を簡単にするために,すべての変数の値をリストで返すものとします. 例えば変数宣言が ((x 0) (y 0)) となっていたら,同じ順序で x, y の値をリストにして返すものとします.

モデル記述の全体と例

一般に状態マシンは複数ある(マルチプロセス)ので,リストで並べるものとします. モデルの全体例は次のようになります.

(define m
  (make-model
   ((x 0) (p 0) (q 0))
   ((P 0
       (0 (read  1 #t (list x x q)))
       (1 (write 2 #t (list (+ p 1) p q)))
       (2))
    (Q 0
       (0 (read  1 #t (list x p x)))
       (1 (write 2 #t (list (+ q 1) p q)))
       (2)))))

このモデルは3つの変数 x, p, q と2つの状態マシン P, Q があります. 変数はすべての状態マシンで共有するものとします. 変数 p, q はそれぞれ P, Q のローカル変数として使います.これはそういう約束にしている(他の状態マシンは参照・更新しない)というだけです. 変数 x は P, Q ともに更新します. どちらの状態マシンも,まず x の値をローカル変数に読み込み,続いてそれに +1 した値を変数 x に書き戻します.

状態 2 は遷移を持っていません.これはいわゆるデッドロック状態ですけど,ここでは停止状態として使っています.

この例では各状態に遷移が1つずつしかありませんが,一般には複数の遷移を並べて記述することができます.

モデル検査器は何をするのか?

ここで作るモデル検査器は何をするのかというと,モデルで記述された状態マシンをすべて並行に動かしたときに,デッドロック状態があるかどうかを調べます. そのために,状態マシンを合成して単一の状態遷移マシンに変換します.

インターリーブ合成

合成を行うには,状態マシンを並行に動かすとはどういうことなのかということが問題になります. ここではインターリーブ合成という合成方法を採用します. 名前は大げさですけど,慣れ親しんでいるマルチスレッドのプログラムに近い考え方です.

インターリーブ合成は2つのポイントで説明できます.1つは,合成したシステムを全体としてみたとき,その遷移はどれか1つの状態遷移マシンの遷移に対応するということです. つまり,かならずどれか1つの状態マシンの遷移が単独で発生するということです. もう1つは,遷移は不可分で,2つの遷移が入り交じって発生することはない,ということです.

システムの状態

次に合成したシステムの状態が何になるかを考えます. システムは複数の状態マシンから構成されていて,各状態マシンは固有の状態を持っています. したがってシステムの状態は,これら各状態マシンの状態の組み合わせになります.

加えて変数がありますから,結局,システムの状態とは,各状態マシンの状態の組み合わせと,変数の値とからなることがわかります.

そこで,システムの状態を次のように表すことにします.

((s1 s2 ...) (v1 v2 ...))

ここで,s1, s2, ...は各状態マシンの状態です.並び順は状態マシンの定義順と同じとします. v1, v2, ...は各変数の値です.これも宣言順と同じ順序で並べるものとします.

システムの遷移

次に,システムが状態 ((s1 s2 ...) (v1 v2 ...)) にあるとき,どのような遷移が可能かということを考えましょう.

一般に k 番目の状態マシンに着目すると,状態 sk から可能な遷移のリストがあるでしょう. このうち,実際に遷移が可能なものは,条件が真になるものだけです. これは各変数が値 v1, v2, ... を取るときに条件を評価すれば判定できます. このようにして可能な遷移を選別するわけです.

条件が成り立つとわかったら,次に遷移先状態での変数の値を計算します. これは変数変換の式を同じく評価すると求めることができます.

まとめると,状態マシン k のある遷移があって条件が成り立つ場合,遷移先状態を sk',変数の値が v1', v2', ...になるとすると,システムの遷移は次のようになります.

((s1 s2 ... sk ...) (v1 v2 ...)) → ((s1 s2 ... sk' ...) (v1' v2' ...))

遷移のラベルについては,状態マシンの遷移ラベルをそのまま使うと,どの状態マシンが遷移したのかわからなくなってしまうので,状態マシン名と遷移ラベルのペアで表すことにします. 例えば,状態マシン P が遷移 read を行った場合のシステムの遷移ラベルは (P . read) とします.

遷移を計算する

では実際に遷移を計算してみることにします. 先にモデルの記述を前処理して,条件の部分と変数変換の部分を関数にしておくとします. 関数のパラメータは宣言された変数です. この前処理については後で説明します.

ここでは,与えられた状態から可能な遷移のリストを返す関数を生成する関数を定義します. 生成する関数を next と呼ぶことにします.

next :: state => ((label . target-state) ...)
(define (make-next-func model)
  (lambda (s)    ; ((s1 s2 ...) (v1 v2 ...))
    (let ((ls (car s))
          (vs (cadr s)))
      (let loop ((ms (cadr model)) (ls ls) (ls-r '())
                 (trs '()))
        (if (null? ms)
            trs
            (let ((m (car ms))
                  (s (car ls)))
              (loop (cdr ms) (cdr ls) (cons (car ls) ls-r)
                    (fold-left
                     (lambda (trs tr)
                       (if (apply (caddr tr) vs) ; guard
                           (cons
                            (cons
                             ;; label
                             (cons (caar ms) (car tr))
                             ;; target state
                             (list
                              (append-reverse
                                ls-r
                                (cons (cadr tr) (cdr ls)))
                              (apply (cadddr tr) vs)))
                            trs)
                           trs))
                     trs (cdr (assq s (cddar ms)))))))))))

状態マシンを列挙し,その遷移を列挙し,条件を変数の値に適用して遷移が可能かどうかを判定し, 遷移が可能である場合には遷移先状態を作って集めるだけです.(car/cdr 生ですみません)

初期状態

初期状態はかんたんですね.

(define (make-initial-state model)
  (list (map cadr (cadr model))         ; initial states
        (map cadr (car model))))        ; initial values

状態遷移の計算

これで初期状態と,関数 next が手に入りましたから,あとは状態遷移の全体を求めるだけです. これは典型的なグラフの探索問題なので,深さ優先探索を行えばできます. 汎用的な深さ優先探索のコードを示します.

(define (dfs s0 next)
  (let ((ss (make-hashtable equal-hash equal?)))
    (hashtable-set! ss s0 #t)
    (let loop ((front (list s0)))
      (if (null? front)
          ss
          (let ((s (car front)))
            (let ((rs (next s)))
              (hashtable-set! ss s rs)
              (let scan ((xs rs) (fs (cdr front)))
                (if (null? xs)
                    (loop fs)
                    (let ((target (cdar xs)))
                      (if (hashtable-ref ss target #f)
                          (scan (cdr xs) fs)
                          (begin
                            (hashtable-set! ss target #t)
                            (scan (cdr xs) (cons target fs)))))))))))))

関数 next で生成された遷移先状態が既出がどうかを判定するためにハッシュテーブルを使っています. 1つの状態を何度も調べるのを避けるために,テーブルへの登録は2段階で行っています. まずはじめて登場したときに #t を登録し,同時に探索の front にも登録します. 次にそこからの遷移先を求めたときに,遷移先のリストを上書き登録しています. (こういうコードを書くと,最後の閉じ括弧を見て嫌われるんでしょうねえ)

条件と変数変換を関数に変換する

先送りにしておいた,遷移の条件と変数変換の部分を関数に変換する仕事を片付けます. ここではマクロを使います.Scheme なのに伝統的なマクロを使いますけど勘弁してください.

(define-macro (make-model var-decls state-machines)
  (let ((vars (map car var-decls)))
    `(list ',var-decls
           (list ,@(conv-guard-n-conv state-machines vars)))))

(define (conv-guard-n-conv state-machines vars)
  (map (lambda (machine)
         (dbind ((?name ?init-state . ?state-transitions) machine)
           `(list ',?name
                  ',?init-state
                  ,@(conv-gc-state-transitions ?state-transitions vars))))
       state-machines))

(define (conv-gc-state-transitions state-transitions vars)
  (map (lambda (s-trs)
         `(list ',(car s-trs)
                ,@(conv-gc-transitions (cdr s-trs) vars)))
       state-transitions))

(define (conv-gc-transitions transitions vars)
  (map (lambda (tr)
         (dbind ((?label ?target ?guard ?conv) tr)
           `(list ',?label
                  ',?target
                  (lambda ,vars ,?guard)   ; 条件
                  (lambda ,vars ,?conv)))) ; 変数変換
       transitions))

ちょっと長いですけど,単にモデル記述を掘っていって,条件と変数変換の部分を lambda 式に変換し,再構成しているだけです.

ここでは自前の(ちょっとはずかしい)dbind というマクロを使っています.Common Lisp の destructuring-bind と同じように,リストを分解して束縛するマクロです.括弧が多いのと,パターン変数を ? で始める点が違いますけど(? で始まらないシンボルはリテラルと見なされます).

例えば,先ほどのモデルを変換すると,次のようになります.

(((x 0) (p 0) (q 0))
 ((P 0
    (0
     (read 1 #<procedure:(lambda (x p q) #t)>
       #<procedure:(lambda (x p q) (list x x q))>))
    (1
     (write 2 #<procedure:(lambda (x p q) #t)>
       #<procedure:(lambda (x p q) (list (+ p 1) p q))>))
    (2))
  (Q 0
    (0
     (read 1 #<procedure:(lambda (x p q) #t)>
       #<procedure:(lambda (x p q) (list x p x))>))
    (1
     (write 2 #<procedure:(lambda (x p q) #t)>
       #<procedure:(lambda (x p q) (list (+ q 1) p q))>))
    (2))))

合成結果を視覚化する

最後に,合成結果を Graphviz を使って視覚化します. この際,デッドロック状態を判定して,赤く色をつけることにします.

(define (viz s0 ss)
  (let ((sv (hashtable-keys ss))
        (ht (make-hashtable equal-hash equal?)))
    ;; numbering
    (dotimes (k (vector-length sv))
      (let ((s (vector-ref sv k)))
        (hashtable-set! ht  s k)))
    ;; preamble
    (display "digraph mc {\n")
    ;; states
    (dotimes (k (vector-length sv))
      (let ((s (vector-ref sv k)))
        (cond ((equal? s s0)
               (format #t "~S [label=\"~A\",style=filled,color=green];~%" k s))
              ((null? (hashtable-ref ss s #f))
               (format #t "~S [label=\"~A\",style=filled,color=red];~%" k s))
              (else
               (format #t "~S [label=\"~A\"];~%" k s)))))
    ;; transitions
    (dotimes (k (vector-length sv))
      (let ((s (vector-ref sv k)))
        (for-each
         (lambda (p)
           (let ((j (hashtable-ref ht (cdr p) #f))) ; target id
             (format #t "~S -> ~S [label=\"~A\"];~%" k j (car p))))
         (hashtable-ref ss s #f))))
    ;; postamble
    (display "}\n") ))

実行例

まず先ほどのモデルを合成すると次のようになります.

実行順序によって,変数 x の最終的な値が 1 になる場合と 2 になる場合があることがわかります.

ミューテックス

ミューテックスを導入してみます. 遷移は不可分かつ排他的に発生するので,ロック状態を表す変数 m を用意すればかんたんにミューテックスが作れます.

(define m
  (make-model
   ((x 0) (m 0) (p 0) (q 0))
   ((P 0
       (0 (lock   1 (= m 0) (list x 1 p q)))
       (1 (read   2 #t      (list x m x q)))
       (2 (write  3 #t      (list (+ p 1) m p q)))
       (3 (unlock 4 #t      (list x 0 p q)))
       (4))
    (Q 0
       (0 (lock   1 (= m 0) (list x 1 p q)))
       (1 (read   2 #t      (list x m p x)))
       (2 (write  3 #t      (list (+ q 1) m p q)))
       (3 (unlock 4 #t      (list x 0 p q)))
       (4)))))

排他制御の様子がよくわかります.最終結果も必ず 2 になります.

2リソース問題

ミューテックスを2つ用意してロック・アンロックの順序を変えてみます. 最初はどちらも 1,2 とロックし,1,2 とアンロックします.

(define m
  (make-model
   ((m1 0) (m2 0))
   ((P 0
       (0 (lock1   1 (= m1 0) (list 1 m2)))
       (1 (lock2   2 (= m2 0) (list m1 1)))
       (2 (unlock1 3 #t       (list 0 m2)))
       (3 (unlock2 0 #t       (list m1 0))) )
    (Q 0
       (0 (lock1   1 (= m1 0) (list 1 m2)))
       (1 (lock2   2 (= m2 0) (list m1 1)))
       (2 (unlock1 3 #t       (list 0 m2)))
       (3 (unlock2 0 #t       (list m1 0))) ))))

1 からアンロックしているので,遷移が少し複雑です.

一方のアンロック順序を入れ替えてみます.

(define m
  (make-model
   ((m1 0) (m2 0))
   ((P 0
       (0 (lock1   1 (= m1 0) (list 1 m2)))
       (1 (lock2   2 (= m2 0) (list m1 1)))
       (2 (unlock2 3 #t       (list m1 0)))
       (3 (unlock1 0 #t       (list 0 m2))) )
    (Q 0
       (0 (lock1   1 (= m1 0) (list 1 m2)))
       (1 (lock2   2 (= m2 0) (list m1 1)))
       (2 (unlock1 3 #t       (list 0 m2)))
       (3 (unlock2 0 #t       (list m1 0))) ))))

ロックの順序を入れ替えるとデッドロックします.

(define m
  (make-model
   ((m1 0) (m2 0))
   ((P 0
       (0 (lock1   1 (= m1 0) (list 1 m2)))
       (1 (lock2   2 (= m2 0) (list m1 1)))
       (2 (unlock2 3 #t       (list m1 0)))
       (3 (unlock1 0 #t       (list 0 m2))) )
    (Q 0
       (0 (lock2   1 (= m2 0) (list m1 1)))
       (1 (lock1   2 (= m1 0) (list 1 m2)))
       (2 (unlock2 3 #t       (list m1 0)))
       (3 (unlock1 0 #t       (list 0 m2))) ))))

補足

デッドロックが見つけられるという点より,合成系が視覚化できるという点の方が面白いかもしれません.

さらに発展させて遊ぶことができると思います.

実は7,8年前に「コンピュータサイエンス入門 - 論理とプログラム意味論」を読んでこのコードを書いてから(ここにあるのは今日改めて書き起こしたものですが),いろいろ発展させたり書き直したりしているうちに SyncStitch になったのでした.

2013/11/02
© 2013,2014,2015 PRINCIPIA Limited