Think Stitch
  最近の更新


非決定性と状態爆発に対処するシナリオ検査

シナリオ検査とは対象とするシステムが与えられたシナリオに対応しているかどうかを確認する検査のことです.シナリオとは仕様で規定された入出力のシーケンスの1例で,より具体的にはイベントの列ということになります.

テストでは実際にシステムを動かし,入力を順に与えながら出力を確認するということをします.それに対してここではシステムのモデルを対象にイベント列を与えて,自動的に検査することを考えます.

実際に動かせる方が楽しいので,シナリオ検査のプログラムを書いてみます.ただしプログラムの部分を読み飛ばしてもポイントがわかるように努めたいと思います.テストを専門にしている人にも興味を持ってもらえるといいなと思います.

  1. シナリオの表現方法を決めます
  2. システムを記述する言語の構文を決めます
  3. 記述されたシステムが持つ遷移を計算する関数を定義します
  4. シナリオ検査を行う関数を定義します
  5. 例としてリーダ・ライタ問題を検査します

プログラミング言語は Scheme,処理系は Gauche を使います.

非決定性

「非決定性」という言葉を初めて聞いたという人のためにまえおきをすることにします.知っている人は次の節に進んでください.

例として,下図のように Application, Middleware, Driver の3層からなるシステムを考えます.

Application Middleware Driver

Middleware が持つ状態遷移を一部取り出してきたとします.ここで a, b は Middleware と Application がやり取りするイベント,x は Middleware と Driver がやり取りするイベントです.Middleware は Application とも Driver とも通信するので,このように両者の間での選択の形が現れることがよくあります.どちらか早く要求を出した方に対応することになります.

a b x b

上の遷移図では全体を俯瞰する設計者の立場から見ているので,すべてのイベントが見えています.しかし Application の立場,つまり Middleware を利用する立場から見ると,Middleware-Driver 間の通信は見えません.

Application Middleware Driver

したがって Application から見た状態遷移図は次のようになります:

a b b

イベント x による遷移からイベント名がなくなって点線になりました.これは内部遷移といって,Application の関与に関係なく自発的に発生する遷移です.元がなんであったかを考えれば自発的に発生してしまう理由がわかると思います.

いま Application が Middleware に対してイベント b で要求を出したとすると,これは必ず受け取られます.なぜかというと内部遷移が起こる前の状態にも起こった後の状態にも b による遷移があるからです.

これに対してイベント a で要求を出したとすると,必ず受け取られるとは限りません.それよりも早く内部遷移が発生してしまい,a による遷移のない状態へ行ってしまうかもしれないからです.

このように外部から操作に関係なく振る舞いが変化してしまう性質のことを非決定性といいます.非決定性は再現性の低いバグやタイミングによって発生したりしなかったりするバグの原因になります.

上の例のように複数の構成要素からなる並行システムでは非決定性を避けることはほとんどできません.したがって非決定性があったとしても正しく動くシステムを設計し検証することが開発上の重要な課題になります.

非決定性を考慮したシナリオの表現

一般にシステムは非決定性を持つので,あるイベントが指定されたとき,3つの可能性があります:

  1. イベントは必ず発生する
  2. イベントは発生する可能性がある
  3. イベントが発生する可能性はない

したがってイベント列についても単純に対応している/していないということにはなりません.そこでイベント列の中で 1 と 2 を区別することにします.2 は 1 を含むことに注意してください.

イベント列を例えば次のように表すことにします.これらはすべて 1 のタイプの必ず発生することを要求したイベント列です:

(req ack use close ok)

発生する可能性がある 2 のタイプのイベントはカッコでくくって表すことにします:

(req (nak) error)

このイベント列の意味は次のようになります:

  1. req には必ず応答する
  2. そのあと nak が発生する可能性がある(絶対に発生しないということはない)
  3. もし nak が発生したとしたら,そのあとは必ず error が発生する

このようにして非決定性を考慮したシナリオが記述できます.シナリオの中で必ず発生しなければならないイベントを必須イベント,発生する可能性があるイベントを可能イベントと呼ぶことにします.

システムの記述

検査対象となるシステムの記述は 並行システムの理論 CSP の構文を使って行うことにします.記述がどうあれ,最終的にシステムの振る舞いが状態遷移としてわかればよいので,シナリオ検査の考え方のポイントだけ知りたい人は,そのような状態遷移がある考えて,この節は読み飛ばしても構いません.

P ::= N
    |   STOP
    |   (! a P )
    |   (alt P ...)
    |   (ndc P P P ...)
    |   (par X P P P ...)
    |   (hide X P )

プロセスの定義は define-process というオペレータで行います.

(define-process N process-expr)

N はプロセス名,process-expr はプロセス式です.

システム記述の例

ミューテックスによって排他制御された2つのプロセス P, Q からなるシステムを記述します.

(define-process MUTEX
  (! lock (! unlock MUTEX)))

(define-process P
  (! lock (! p.start (! p.end (! unlock P)))))

(define-process Q
  (! lock (! q.start (! q.end (! unlock Q)))))

(define-process SYSTEM
  (hide (lock unlock)
    (par (lock unlock)
      (par () P Q)
      MUTEX)))

遷移の定義

各プロセスの遷移を計算する2つの関数 viz-trans, tau-trans を定義します.

この2つの関数は操作的意味論で定義された遷移をプログラムにしたものです.

viz-trans

まず演算子によって場合分けをします.

(define (viz-trans p)
  (match p
    ('STOP         '())
    (('! e q)      (list (cons e q)))
    (('alt . ps)   (viz-trans-alt ps))
    (('ndc . ps)   '())
    (('par x . ps) (viz-trans-par x ps))
    (('hide x q)   (viz-trans-hide x q))
    (_ (viz-trans (hash-table-get process-def p)))))

alt は各プロセスの遷移を合わせた遷移を持ちます.

(define (viz-trans-alt ps)
  (append-map viz-trans ps))

hide は非演算プロセスの遷移から隠蔽されないものを選びます.

(define (viz-trans-hide x p)
  (fold-left
    (lambda (acc e.q)
      (if (memq (car e.q) x)
          acc
          (cons (cons (car e.q) (list 'hide x (cdr e.q))) acc)))
    '() (viz-trans p)))

par は少し複雑です.まず各プロセスが持つ遷移のうち同期しないものを求めます.このとき同期するものについてはハッシュ表 sync に記録しておきます.このハッシュ表は同期判定にも流用します.

(define (viz-trans-par-async x ps)
  (let ((n (length ps))
        (sync (make-hash-table)))
    (for-each
      (lambda (e)
        (hash-table-put! sync e
          (make-vector n '())))
      x)
    (let loop ((k 0) (xs ps) (ys '()) (acc '()))
      (if (null? xs)
          (values acc sync)
          (let scan ((zs (viz-trans (car xs))) (acc acc))
            (if (null? zs)
                (loop (+ k 1) (cdr xs) (cons (car xs) ys) acc)
                (let ((e (caar zs))
                      (q (cdar zs)))
                  (if (hash-table-get sync e #f)
                      (begin
                        (add-sync sync e k q)
                        (scan (cdr zs) acc))
                      (scan (cdr zs)
                            (cons (cons e
                                        (cons* 'par x
                                               (append-reverse
                                                ys
                                                (cons q (cdr xs)))))
                                  acc))))))))))

ハッシュ表 sync のエントリはプロセス数と同じ長さを持つベクタにして,各スロットに対応するプロセスの遷移先をリストにして入れていきます.

(define (add-sync sync e k q)
  (let ((v (hash-table-get sync e)))
    (vector-set! v k (cons q (vector-ref v k)))))

同期しない遷移の計算が終わったら,次に同期する場合の遷移を求めます.各イベントに対応する各プロセスの遷移先が ハッシュ表 sync に入っていますから,これらの組み合わせが遷移先になります.

(define (viz-trans-par-sync acc x sync)
  (hash-table-fold sync
    (lambda (e v acc)
      (append
       (map (lambda (qs) (cons e (cons* 'par x qs)))
            (cartesian-product (vector->list v)))
       acc))
    acc))

以上を合わせて並行合成 par の遷移がすべて求まります.

(define (viz-trans-par x ps)
  (let-values (((acc sync) (viz-trans-par-async x ps)))
    (viz-trans-par-sync acc x sync)))

tau-trans

演算子によって場合分けをします.

(define (tau-trans p)
  (match p
    ('STOP         '())
    (('! e q)      '())
    (('alt . ps)   (tau-trans-alt ps))
    (('ndc . ps)   ps)
    (('par x . ps) (tau-trans-par x ps))
    (('hide x q)   (tau-trans-hide x q))
    (_ (tau-trans (hash-table-get process-def p)))))

隠蔽 hide ではプロセスがもともと持っている内部遷移に隠蔽される遷移を加えます.

(define (tau-trans-hide x p)
  (fold-left
    (lambda (acc e.q)
      (if (memq (car e.q) x)
          (cons (list 'hide x (cdr e.q)) acc)
          acc))
    (tau-trans p) (viz-trans p)))

選択 alt と並行合成 par では,各プロセスが持つ内部遷移がそのまま全体としても内部遷移になります.これらを共通の関数 tau-trans-tau で計算します.2番目の引数として演算子に対応する式を再構成する関数を渡します.

(define (tau-trans-alt ps)
  (tau-trans-tau ps (lambda (ps) (cons 'alt ps))))
(define (tau-trans-par x ps)
  (tau-trans-tau ps (lambda (ps) (cons* 'par x ps))))

各プロセスが持つ内部遷移を集めます.

(define (tau-trans-tau ps form)
  (let loop ((xs ps) (ys '()) (acc '()))
    (if (null? xs)
        acc
        (loop
         (cdr xs) (cons (car xs) ys)
         (append
          (map (lambda (q)
                 (form (append-reverse ys (cons q (cdr xs)))))
               (tau-trans (car xs)))
          acc)))))

以上で遷移が計算できるようになりました.

遷移の計算例

先ほど定義した排他制御システムの遷移を計算してみます.

まず SYSTEM は初期状態でイベントによる遷移を持っていません.最初に発生するイベント lock は隠蔽されているからです.これはシステムの内部動作を外から観測することはできないということを意味しています.

(viz-trans 'SYSTEM)
=> ()

内部遷移の遷移先は2つあります.P, Q どちらが先にロックを獲得するかということに対応しています.これは非決定的です.MUTEXP または MUTEXQ が同時に遷移していることがわかります.同期的相互作用だからです.

(tau-trans 'SYSTEM)
=>
((hide (lock unlock)
   (par (lock unlock)
     (par ()
       P
       (! q.start (! q.end (! unlock Q))))
     (! unlock MUTEX)))
 (hide (lock unlock)
   (par (lock unlock)
     (par ()
       (! p.start (! p.end (! unlock P)))
       Q)
     (! unlock MUTEX))))

次に上記1つ目の状態からの遷移を計算してみます.イベント q.start による遷移があることがわかります.プロセス Q 以外は遷移していません.このイベントは同期指定されていないからです.

(viz-trans
 '(hide (lock unlock)
    (par (lock unlock)
      (par ()
        P
        (! q.start (! q.end (! unlock Q))))
      (! unlock MUTEX))))
=>
((q.start . (hide (lock unlock)
              (par (lock unlock)
                (par ()
                  P
                  (! q.end (! unlock Q)))
                (! unlock MUTEX)))))

内部遷移はありません.

(tau-trans
 '(hide (lock unlock)
    (par (lock unlock)
      (par ()
        P
        (! q.start (! q.end (! unlock Q))))
      (! unlock MUTEX))))
=> ()

シナリオ検査

遷移を計算することができるようになったので,あとはイベント列を前から調べていけばシナリオ検査ができます.しかし非決定性に対応するためにはもう少し準備が必要です.

内部遷移と状態集合

まず初期状態を考えます.もし初期状態が内部遷移を持っている場合は,その遷移先も調べなければなりません.なぜなら内部遷移は自発的に発生してしまうことがあり,その遷移先には検査したいイベントによる遷移がないかもしれないからです.ですからイベントが必ず発生するというためには内部遷移のあとの状態も調べる必要があります.

内部遷移の遷移先がさらに内部遷移を持っている可能性がありますから,結局すべての内部遷移を経由してたどり着けるすべての状態を調べる必要があります.そこで内部遷移をたどってたどり着けるすべての状態の集合を tau-closure と呼ぶことにします.tau-closure の中には内部遷移を持っている状態と持っていない状態があります.内部遷移を持っていない状態,つまり外部との相互作用がない限りこれ以上遷移しない状態のことを安定状態といいます.これに対し,内部遷移を持っている状態を不安定状態といいます.

次の図でいうと,状態 P, Q は不安定状態,状態 A, B は安定状態です.

P Q B A a a a b b

調べたいイベントを e とすると,次のことがわかります:

したがってシナリオの中に含まれるイベントが必須か可能かに応じて上記条件を検査すればいいことになります.

上の図でいうと,イベント a は安定状態 A, B いずれにも遷移があるので必ず発生します.これに対してイベント b による遷移は B にしかないので,必ず発生するとはいえません.

もう1つ考慮すべきことがあります.状態の集合の中にはイベント e による遷移を持つものが複数あり得ますから,その遷移先はまた集合になります.そして各遷移先が内部遷移を持つ可能性がありますから,結局 tau-closure は状態の集合に対して計算する必要があることがわかります.例えば上の図でイベント b による遷移先は2つあります.

状態集合の表現

状態の集合はハッシュ表で表すことにします.キーがプロセス式で,値はなんでもよいので #t にしておきます.

ハッシュ表とリストを相互に変換する関数を用意しておきます.

(define (htset->list s)
  (hash-table-fold s
    (lambda (p _ acc) (cons p acc)) '()))
(define (list->htset xs)
  (let ((ht (make-hash-table 'equal?)))
    (for-each (lambda (x) (hash-table-put! ht x #t)) xs)
    ht))

tau-closure

ハッシュ表で表された状態集合に対して,tau-closure を計算する関数 tau-closure を定義します.内部遷移を計算する関数 tau-trans を使った典型的な深さ優先探索です.与えられた元のハッシュ表に直接遷移先を追加します.

(define (tau-closure s)
  (let loop ((f (htset->list s)))
    (if (null? f)
        s
        (let scan ((r (tau-trans (car f))) (f (cdr f)))
          (if (null? r)
              (loop f)
              (let ((q (car r)))
                (if (hash-table-get s q #f)
                    (scan (cdr r) f)
                    (begin
                      (hash-table-put! s q #t)
                      (scan (cdr r) (cons q f))))))))))

必須イベントの検査 check-event-nes

必須イベントであることを検査するには,すべての安定状態に該当する遷移があることを確認します.加えて少なくとも安定状態が1つはあることを確認します.

安定状態であるかどうかは (tau-trans p) が空かどうかでわかります.非効率ですけどわかりやすさを優先しておきます.

(define (check-event-nes e s)
  (let ((c 0))
    (let ((r
           (hash-table-fold s
             (lambda (p _ result)
               (and result
                    (if (null? (tau-trans p))  ; stable state?
                        (begin
                          (set! c (+ c 1))
                          (if (assq e (viz-trans p))
                              #t
                              (begin
                                (format #t "~S\n" p)
                                #f)))
                        #t)))
             #t)))
      (and r (> c 0)))))

可能イベントの検査 check-event-pos

可能イベントについては安定・不安定にかかわらず1つでも遷移があればよいということになります.

(define (check-event-pos e s)
  (hash-table-fold s
    (lambda (p _ result)
      (or result
          (assq e (viz-trans p))))
    #f))

遷移先状態集合の計算 next-state-set

イベントの検査が済んだら次の状態の集合を求めます.まずイベントに対応する遷移先を求めて,それから tau-closure を計算します.

(define (next-state-set e s)
  (let ((t (make-hash-table 'equal?)))
    (hash-table-for-each s
      (lambda (p _)
        (let ((x (assq e (viz-trans p))))
          (if x
              (hash-table-put! t (cdr x) #t)))))
    (tau-closure t)))

シナリオ検査関数 scenario-check

以上を組み合わせるとシナリオ検査の関数は次のようになります.

(define (scenario-check scenario process)
  (let loop ((xs scenario) (ys '())
             (s (tau-closure (list->htset (list process)))))
    (if (null? xs)
        #t
        (let ((e (car xs)))
          (if (or (and (pair? e) (check-event-pos (car e) s))
                  (and (symbol? e) (check-event-nes e s)))
              (loop (cdr xs) (cons e ys)
                    (next-state-set (if (symbol? e) e (car e)) s))
              (values e (reverse ys) (htset->list s)))))))

プロセス定義

最後になりましたが,プロセスを定義するマクロを用意します.

(define process-def (make-hash-table))
(define-macro (define-process name pexpr)
  `(hash-table-put! process-def ',name ',pexpr))

簡単な検査例

検査にパスした場合は #t が返ります.

(scenario-check '(a b) '(! a (! b (! c STOP))))
=> #t

必須イベントの検査に失敗すると4つ値が返ってきます.1つ目は必須イベントによる遷移がなかったプロセスです.2番目以降は可能イベントの場合と共通で,検査に失敗したイベント,そこまでのイベント列,現在の状態集合です.

(scenario-check '(a b c d) '(! a (! b (! c STOP))))
=>
STOP
d
(a b c)
(STOP)

イベント a と b から非決定的に選択する場合,必ず a が発生するとはいえません.

(scenario-check
 '(a)
 '(ndc
    (! a STOP)
    (! b STOP)))
=>
(! b STOP)
a
()
((! a STOP) (ndc (! a STOP) (! b STOP)) (! b STOP))

しかし可能イベントとすれば検査をパスします.

(scenario-check
 '((a))
 '(ndc
    (! a STOP)
    (! b STOP)))
=> #t

遷移がなければ可能イベントでも失敗します.

(scenario-check
 '((a))
 '(! b STOP))
=>
(a)
()
((! b STOP))

リーダ・ライタ問題

リーダ・ライタ問題とは,データベースのような共有データにアクセスする複数のリーダ・ライタを不整合が起こらないように制御する問題です.リーダはデータの読出しのみ行います.これに対してライタはデータの更新も行います.したがってリーダとライタが同時に動くと中間状態の不正なデータを読んでしまう危険があります.2つ以上のライタが同時に動くとデータの整合性を破壊してしまう可能性があります.そうならないように制御するということです.

条件は次の3つに整理することができます.

前の2つはいわゆる安全性の問題で,安全性検査で確認することができます.

最後の条件は効率を上げるための条件です.リーダは複数同時に動いても問題ないので,できるだけ並行に動かした方がよいわけです.ここではこれを検証します.

Shared Data R1 W0 W1 W2 R2 R0 R3

制御を行うために部品を3つ用意します.ミューテックス2つとカウンタ用の共有変数 SHVAR です.ミューテックスの1つ RWMUTEX はライタ間およびリーダ・ライタ間の排他制御で使います.もう1つ CNTMUTEX はリーダが共有するカウンタの排他制御で使います.このカウンタを使ってアクセスしているリーダの数を数えます.カウンタ値を見て,最初にアクセスを始めたリーダが RWMUTEX をロックし,最後に退出するリーダがアンロックします.

CMUTEX SHVAR RWMUTEX W0 W1 R0 R1

RWMUTEX

(define-process RWMUTEX
  (! rw.lock (! rw.unlock RWMUTEX)))

CNTMUTEX

イベントを除くと構造は RWMUTEX と同じです.

(define-process CNTMUTEX
  (! cnt.lock (! cnt.unlock CNTMUTEX)))

COUNTER

構文が制限されていて変数を使うことができないので,状態によってカウント値を表します.

(define-process COUNTER0
  (alt
    (! rd0 COUNTER0)
    (! up COUNTER1)))

(define-process COUNTER1
  (alt
    (! rd1 COUNTER1)
    (! down COUNTER0)
    (! up COUNTER2)))

(define-process COUNTER2
  (alt
    (! rd2 COUNTER2)
    (! down COUNTER1)))

WRITER

各ライタは RWMUTEX をロックしてから共有データにアクセスし,終わったらアンロックします.

(define-process WRITER
  (! rw.lock (! w.start (! w.end (! rw.unlock WRITER)))))

READER

リーダはまず CNTMUTEX をロックしてカウンタ値を読み出します.もしカウンタ値が 0 だったら最初のリーダということですから,RWMUTEX をロックします.

(define-process READER
  (! cnt.lock
     (alt
       (! rd0 (! up (! rw.lock READER2)))
       (! rd1 (! up READER2)))))

アクセス終了後,再度 CNTMUTEX をロックしてからカウンタ値を読み出し,最後のリーダだった場合は RWMUTEX をアンロックします.

(define-process READER2
  (! cnt.unlock
     (! r.start
        (! r.end
           (! cnt.lock
              (alt
                (! rd1 (! down (! cnt.unlock (! rw.unlock READER))))
                (! rd2 (! down (! cnt.unlock READER)))))))))

SYSTEM

プロセスを並行合成してシステムを組み立てます.

(define-process SYSTEM
  (par (rw.lock rw.unlock cnt.lock cnt.unlock
        rd0 rd1 rd2 up down)
    (par () READER READER WRITER WRITER)
    (par () RWMUTEX CNTMUTEX COUNTER0)))

システム内部で使われているイベントを隠蔽します.システム外部から観測できるのは r.start, r.end, w.start, w.end だけになります.

(define-process HSYS
  (hide (rw.lock rw.unlock cnt.lock cnt.unlock
         rd0 rd1 rd2 up down)
    SYSTEM))

検査

READER の単体検査

小手調べに READER を単体で検査してみます.

シナリオ検査の例です.まずカウンタ値が 0 の場合です.

(scenario-check '(cnt.lock rd0 up rw.lock cnt.unlock r.start r.end
                           cnt.lock rd1 down cnt.unlock rw.unlock)
                'READER)
=> #t

カウンタ値が 1 の場合です.

(scenario-check '(cnt.lock rd1 up cnt.unlock r.start r.end
                           cnt.lock rd2 down cnt.unlock)
                'READER)
=> #t

カウンタ値が 1 であるにもかからわず rw.lock を指定すればエラーになります.

(scenario-check '(cnt.lock rd1 up rw.lock cnt.unlock)
                'READER)
=>
READER2
rw.lock
(cnt.lock rd1 up)
(READER2)

SYSTEM の検査

隠蔽していないシステムを調べてみます.

WRITER がアクセスしているシナリオ

(scenario-check '(rw.lock w.start w.end rw.unlock)
                'SYSTEM)
=> #t

READER がアクセスしているシナリオ

(scenario-check '(cnt.lock rd0 up rw.lock cnt.unlock r.start r.end
                           cnt.lock rd1 down cnt.unlock rw.unlock)
                'SYSTEM)
=> #t

HSYS の検査

ではいよいよ本来のシステム全体の検査をしてみます.

まずはじめに r.start を実行するパスがあるはずですが,これはライタとの競合になるので必ず発生するとはいえません.したがって必須イベントにすると失敗します.

(scenario-check '(r.start) 'HSYS)
=>
(hide (rw.lock rw.unlock cnt.lock cnt.unlock rd0 rd1 rd2 up down)
  (par (rw.lock rw.unlock cnt.lock cnt.unlock rd0 rd1 rd2 up down)
    (par ()
      READER
      (! rw.lock READER2)
      (! w.start (! w.end (! rw.unlock WRITER)))
      WRITER)
    (par () (! rw.unlock RWMUTEX) (! cnt.unlock CNTMUTEX) COUNTER1)))
r.start
()
(...)

しかし可能イベントにすれば OK です.

(scenario-check '((r.start)) 'HSYS)
=> #t

そして本命の検査はこれです.1つ目のリーダがアクセスしているときに2つのリーダが必ず同時にアクセスできることがわかります.

(scenario-check '((r.start) r.start) 'HSYS)
=> #t

シナリオ検査と状態爆発

ここで紹介したシナリオ検査はいわゆる(広い意味での)モデル検査手法の1種ということになります.実際,わざわざシナリオ検査用のプログラムを用意しなくても,CSP の詳細化検査ができるツールがあればシナリオ検査はできます.しかし別のツールとする利点が2つあります.

  1. 詳細化検査ではすべての状態を展開するため,いわゆる状態爆発のために大規模なシステムは検査できない.しかしシナリオ検査は検査に関係する状態しか展開しないので状態爆発の可能性をずっと低くできる(内部的には既出状態の判定が不要なのでさらに効率がよい)
  2. 非決定性を考慮したシナリオを仕様として記述するのはそれなりに手間がかかる.ここで紹介した方法ならば簡単に書ける

コメント

2016/12/01

© 2013-2016 PRINCIPIA Limited