Think Stitch
  最近の更新

Translating C programs with POSIX thread into CSP for refinement checking

この記事は 2017/11/25 に首都大学東京秋葉原サテライトキャンパスで行われた第20回 CSP 研究会で発表した内容を文書化したものです.発表資料はこちらです.

0  Pthread Model Checker について

Pthread Model Checker は POSIX thread (pthread) を使った C 言語プログラムのためのモデル検査器です.

次のような特徴があります:

C言語と pthread を知っている人であればすぐにでも使い始めることができるでしょう.

1  Pthread Model Checker 内部のしくみ

Pthread Model Checker は与えられた C言語のプログラムを状態遷移モデルに変換します.つぎにこの状態遷移の上を網羅的に歩き回って検査するC言語のソースコードを生成します.生成されたコードをコンパイルして実行すれば検査が行われ,レポートが出力されます.

2  Pthread Model Checker の検査能力

Pthread Model Checker は assert を埋め込むだけで検査できるという簡便さが特徴ですが,その分検査できることには限界があります.

安全性についてはグローバルな assert という機能を使うと検査することができます.グローバルな assert とは,プログラムの実行経路に置かれるふつうの assert と異なり,プログラムの実行全体を通して常に監視される assert です.これは次の例のようにコメントの中で指定することができます.

int count;
// @ASSERT(count >= 0 && count <= N)

安全性についてはこのようにして検査することができますが,例えばつぎのような検査はできません:

3  C言語のプログラムを CSP に変換する

この弱点を克服するために,与えられた C言語のプログラムを CSP に変換することを考えました.そうすれば CSP の詳細化検査器 (refinement checker) SSG を使って様々な検査を行うことができるからです.

Pthread Model Checker の中ではC言語のプログラムが状態遷移モデルに変換されていますから,ここから CSP を生成すればよいことになります.

3.0  遷移

状態遷移モデルを CSP に変換するために考えるべきことは,各遷移をどのように変換するかということです.遷移の種類には次のものがあります:

これらに CSP のイベント(チャネル)を割り当てて変換します.

3.1  プロセス

各スレッドは CSP のプロセスに変換します.加えて次のようなプロセスが必要になります:

CSP の世界ではすべての相互作用がイベント同期(チャネル通信)であり,グローバルな共有変数はありません.そこでC言語のグローバル変数は,読み書きをチャネルを通じて行うプロセスとして表現します.このようなプロセスをメモプロセスといいます.

(defch rd-count Di)
(defch wr-count Di)
(def (GVS-count (x Di))
  (alt
    (! (rd-count x) (GVS-count x))
    (? wr-count (x) (GVS-count x))
    (! terminate SKIP)))

スレッドとグローバル変数に対応するプロセスは状態遷移モデルから生成します.図の水色の部分です.

これに対して緑色の部分は pthread ライブラリに対応するプロセスで,これらは汎用なのであらかじめ作っておいて合成します.

pthread の各関数にもチャネルを割り当てて,関数呼び出しをチャネル通信に翻訳します.

(defch ret          Ip)
(defch lock         Ip Im)
(defch unlock       Ip Im)
(defch wait         Ip Ic Im)
(defch signal       Ip Ic)
(defch broadcast    Ip Ic)

ミューテックスと条件変数は不可分操作で絡み合っているので,1つのプロセスとして実現します.

(deftype mutex-state Unlock (Lock Ip))
#|
  rs:   set of processes ready to ret
  ms:   list of mutex state,        length = Nm
  mss:  list of mutex wait set,     length = Nm
  css:  list of condvar wait set,   length = Nc
|#
(def (CVM (rs  (set Ip))
          (ms  (list mutex-state Nm))
          (mss (list (set Ip) Nm))
          (css (list (set Ip) Nc)))
  (alt
    (? lock (p m)
       (case (ref ms m)
         (Unlock
          (CVM (adjoin rs p) (update ms m (Lock p)) mss css))
         ((Lock q)
          (if (= p q)
              STOP
              (CVM rs ms (update mss m (adjoin (ref mss m) p)) css)))))
    (? unlock (p m)
       (= (ref ms m) (Lock p))
       (let ((s (ref mss m)))
         (if (= (card s) 0)
             (CVM rs (update ms m Unlock) mss css)
             (xndc q s
               (CVM (adjoin rs q) (update ms m (Lock q)) (update mss m (remove s q)) css)))))
    (? wait (p c m)
       (= (ref ms m) (Lock p))
       (let ((s (ref mss m)))
         (if (= (card s) 0)
             (CVM rs (update ms m Unlock) mss (update css c (adjoin (ref css c) p)))
             (xndc q s
               (CVM (adjoin rs q) (update ms m (Lock q)) (update mss m (remove s q))
                    (update css c (adjoin (ref css c) p)))))))
    (? signal (p c)
       (let ((s (ref css c)))
         (if (= (card s) 0)
             (CVM rs ms mss css)
             (xndc q s
               (CVM (adjoin rs q) ms mss (update css c (remove s q)))))))
    (? broadcast (p c)
       (CVM (union rs (ref css c)) ms mss (update css c (set))))
    (if (= (card rs) 0)
        STOP
        (xndc p rs (! (ret p) (CVM (remove rs p) ms mss css))))))

スレッドはすべて JOINABLE で,join によってステータスを引き取る必要があります.そのための管理プロセスを用意します.これも実質上はメモプロセスということになります.

(defch exit         Ip Di)
(defch join         Ip Di)
(deftype proc-state Running (Done Di))
(def (PM (xs (list proc-state Np)))
  (alt
    (? exit (pid retcode)
       (PM (update xs pid (Done retcode))))
    (? join (pid retcode)
       (= (Done retcode) (ref xs pid))
       (PM xs))
    (! terminate SKIP)))

変換は以上です.

4  検査の例

4.0  安全性検査としての assert 検査

C言語のプログラムに埋め込んだ assert は,違反時に assertion-violation というイベントを発生する形に変換しました.したがってこれを検出すれば CSP のレベルでも assert 検査を行うことができます.これは assertion-violation という悪いことが起こらないという意味で安全性検査ということになりますから,トレース意味論による詳細化検査を使います.

(def NO-ASSERTION-VIOLATION
  (RUN (diff event (set assertion-violation))))

(def (RUN A)
  (xalt e A
   (! e (RUN A))))

(check (deadlock SYSTEM))
(check (traces NO-ASSERTION-VIOLATION SYSTEM))

4.1  仕様との正当性検査の例

次は生産者・消費者問題の正当性検査例です.グローバルな配列変数 buf を循環バッファとしてデータをやりとりするスレッド群があるとします.これを外から観測して,バッファに入った値が順序を保って出て行くことを確認する仕様です.このように詳細な振る舞いの正当性(詳細化関係)を調べることができるようになります.

(def SPEC
  (let ((A (diff event
                 (chset rd-buf wr-buf assertion-violation))))
    (OBSERVER A (list))))

(def (OBSERVER (A (set event)) (xs (list Di L-buf)))
  (alt
    (? rd-buf (k x)
       (and (not (null? xs))
            (= x (car xs)))
       (OBSERVER A (cdr xs)))
    (? wr-buf (k x)
       (< (length xs) L-buf)
       (OBSERVER A (append1 xs x)))
    (xalt e A
      (! e (OBSERVER A xs)))))

5  まとめ

Pthread Model Checker で C言語のモデルを CSP に変換できるようにしました. SSG と組み合わせることで,詳細化検査等のより精密な検査ができるようになりました.

はじめは assert だけで簡単に検査を行い,assert だけでは捕まえられない問題が発生したら CSP に変換して詳細化検査をするといった使い分けができると思います.

2017/11/26

© 2013-2017 PRINCIPIA Limited