|
12
|
1 \chapter{Gears Agda によるモデル検査}
|
|
|
2 定理証明では数学的な証明をするため状態爆発を起こさず検証を行うことが
|
|
17
|
3 できる。しかし、専門的な知識が多く難易度が高いという欠点がある。
|
|
18
|
4 加えて、CbCでは並列処理も実行できる\cite{parusu-master}が、
|
|
17
|
5 並列処理を定理証明するには検証する状態が膨大になり困難である。
|
|
18
|
6 そのため、並列処理はモデル検査にて検証する方が良い。
|
|
12
|
7
|
|
|
8 \section{モデル検査とは}
|
|
18
|
9 モデル検査 (Model Cheking) とは、検証手法のひとつである。
|
|
16
|
10 これはプログラムが入力に対して仕様を満たした動作を
|
|
17
|
11 行うことを網羅的に検証することを指す。
|
|
18
|
12 しかし、モデル検査と定理証明を比較した際に、モデル検査は入力が無限になる
|
|
17
|
13 状態爆発が起こり得るという問題がある。
|
|
18
|
14 実際にモデル検査で行うことは、検証したい内容の時相理論式 $\varphi$ を作り、対象のシステムの初期状態 s のモデル M があるとき、M, s が $\varphi$ を満たすかを調べる。
|
|
12
|
15
|
|
7
|
16 \section{Dining Philosophers Problem}
|
|
|
17 今回はモデル検査を行う対象として Dining Philosophers Problem (以下DPP)
|
|
17
|
18 を用いることとした。
|
|
|
19 DPP とは資源共有問題であり、モデル検査をする際に挙げられる代表的な問題
|
|
|
20 である。
|
|
7
|
21
|
|
17
|
22 DPPのストーリーを\figref{DPP} に示している。
|
|
7
|
23
|
|
|
24 \begin{figure}[htpb]
|
|
|
25 \begin{center}
|
|
|
26 \scalebox{0.5}{\includegraphics{fig/Dining.pdf}}
|
|
|
27 \end{center}
|
|
9
|
28 \caption{Dining Philosophers Program のイメージ図}
|
|
7
|
29 \label{fig:DPP}
|
|
9
|
30 \end{figure}
|
|
7
|
31
|
|
17
|
32 したがって、哲学者は以下のようなフローを独立して並列に繰り返し実行することとなる。
|
|
7
|
33
|
|
|
34 \begin{enumerate}
|
|
|
35 \item しばらくの間思考を行う
|
|
|
36 \item 食事をするために右のフォークを取る
|
|
17
|
37 \item 右のフォークを取ったら、次は左のフォークを取る
|
|
|
38 \item 両方のフォークを取ったら、しばらく食事をする
|
|
7
|
39 \item 思考に戻るために左手に持っているフォークをテーブルに置く
|
|
|
40 \item 左手のフォークを置いたあとは右のフォークをテーブルに置く
|
|
|
41 \end{enumerate}
|
|
|
42
|
|
17
|
43 この際、すべての哲学者が同時に右のフォークを取った場合のことを考える。
|
|
|
44 すべての哲学者はフォークを持っている。次に哲学者は左のフォークを取ろうと
|
|
|
45 する。しかしフォークは哲学者の人数と同じ数だけ存在しているため、
|
|
|
46 テーブルの上にフォークはすでにひとつも存在しない。
|
|
7
|
47 すべての哲学者は左のフォークを取ろうとするが
|
|
17
|
48 誰も右のフォークを置くことがないため、すべての哲学者の動作がこの状態で止まる。（dead lock）
|
|
|
49 これが起こることを Gears Agda で検出したい。
|
|
7
|
50
|
|
|
51 \section{SPINによるモデル検査}% 内容にそぐわない場合は使わない
|
|
|
52
|
|
18
|
53 SPIN(Simple Promela INterpreter) \cite{spin}とは一般的にモデル検査に使用されるツールである。これは使用記述言語 PROMELA(Process Meta Language) による記述を元にプログラムが取る状態を網羅し、モデル検査を行うことができる。
|
|
7
|
54
|
|
18
|
55 今回 Gears Agda でのモデル検査と比較するために、SPINでのDPPプログラムのモデル検査に必要なコードの一部を\coderef{spin-dpp}に載せる。
|
|
7
|
56
|
|
|
57 \lstinputlisting[caption= SPINにてDPPをモデル検査する際のコードの一部 , label=code:spin-dpp]{src/dpp-verif/spin.pml}
|
|
|
58
|
|
17
|
59 コードを簡単に説明する。哲学者がThinkの状態から食事をしようとしだした際の状態の変化が4行目と5行目になっている。
|
|
18
|
60 forkの状態を配列で管理している。0 である状態が誰もそのforkを持っていない状態である。ここでは、5人目の人が右手にあるフォークを取ろうとした際に配列の最初を取ることが5行目に記述されている。
|
|
7
|
61
|
|
17
|
62 左手のフォークを取る動作も同じように記述する。
|
|
18
|
63 SPINではこのコードを元にプログラムが取りうる状態全てを網羅し、モデル検査を行うことができる。
|
|
7
|
64
|
|
17
|
65 \figref{DPP-model}はこのPromelaから作成された状態遷移図になる。
|
|
18
|
66 SPINではコードからプログラムの状態遷移図を出力することができる他、プログラムのstep実行など幅広くモデル検査を行うことができる。
|
|
7
|
67
|
|
|
68 \begin{figure}[htpb]
|
|
|
69 \begin{center}
|
|
22
|
70 \scalebox{0.5}{\includegraphics{fig/dpp-model.pdf}}
|
|
7
|
71 \end{center}
|
|
|
72 \caption{SPINにて作成した状態遷移図}
|
|
|
73 \label{fig:DPP-model}
|
|
|
74 \end{figure}
|
|
|
75
|
|
11
|
76 |
