Think Stitch
PRINCIPIA  最近の更新


並行システムの検証と実装
第1章 1.3 並行システムの検証例/実装例

「並行システムの検証と実装」という本で解説されている例を SyncStitch で扱ってみることにします。

こちらに補足ページがあります。

モデル化

第1章 1.3 節に出てくる SRconc という並行システムを扱います。

チャネル定義

定数 N とチャネル chan, disp を定義します。

(define N 10)

(define-channel chan (x)
  (map list (interval 0 N)))

(define-channel disp (m x)
  (combinations
    (list '(send receive)
          (interval 0 N))))

Sender プロセス

Sender プロセスの状態遷移図(図 1.12, p.14)を書きます。横向きにしましたけど。

CSP の場合は次のよう書くことができます。

(define-process (Sender n)
  (! disp ('send n) (Sender2 n)))

(define-process (Sender2 n)
  (! chan (n) (Sender (mod (+ n 1) N))))

Receiver プロセス

同様に Receiver プロセスの状態遷移図を書きます。

CSP でも同様に書けます。

(define-process (Receiver m)
  (? chan (m) (Receiver2 m)))

(define-process (Receiver2 m)
  (! disp ('receive m) (Receiver m)))

SRconc プロセス

Sender と Receiver を並行合成して SRconc を作ります。 同期リストに chan を指定して並行合成した後,chan を隠蔽します。 (SyncStitch の場合は hpar を使えば上の合成を1度で行うことができます。)

(define-process SRconc
  (hide (list chan)
    (par (list chan)
      (Sender 0)
      (Receiver 0))))

SRseq プロセス

SRconc の動作を検査するために逐次システム SRseq を定義します。まず本体である SendRec プロセスを定義します。 状態遷移図は p.16 図 1.14 にあります。

CSP で書く場合は次のようになります。

(define-process (SendRec n m i K)
  (alt
    (if (< i K)
        (! disp ('send n)
           (SendRec (mod (+ n 1) N) m (+ i 1) K))
        STOP)
    (if (> i 0)
        (! disp ('receive m)
           (SendRec n (mod (+ m 1) N) (- i 1) K))
        STOP)))

最後に SRseq を定義します。

(define-process (SRseq K)
  (SendRec 0 0 0 K))

検証

SRconc と SRseq を比較します。本では失敗発散方式(p.186 の脚注 3) 参照)が使われていますが,SyncStitch は失敗発散方式をサポートしていないので安定失敗方式に置き換えます。いずれのプロセスも発散しないので問題はありません。

p.16 の解説にあるとおり,K=1 ではなく K=2 のときに2つのプロセスは一致することが分かります。

違反の様子はそれぞれ以下のようになります。send が連続して発生可能である様子がよくわかると思います。

(SRseq 1) [FD= SRcons の場合は disp.send.1 があるのでトレース違反になります。

逆に SRcons [FD= (SRseq 1) の場合は disp.send.1 を拒否するので拒否違反になります。

2014/03/29
© 2013,2014,2015 PRINCIPIA Limited