|
0
|
1 \chapter{線形時相論理によるCbCプログラムの検証手法}
|
|
1
|
2 \label{chapter3}
|
|
0
|
3
|
|
|
4 \section{CbCによる並列プログラミング}
|
|
|
5 ここでは、例題に用いるサンプルプログラムの概要と、
|
|
|
6 そのプログラムの状態の分割およびCbCプログラムとの対応について説明する。
|
|
|
7 また、並列プログラムのシミュレーション方法についても述べる。
|
|
|
8
|
|
|
9 \subsection{Dining Philosophers Problemの概要}
|
|
|
10 検証用のサンプルプログラムとしてDining Philosophers Problemを用いる。
|
|
|
11 これは資源共有問題の一つで、次のような内容である。
|
|
|
12
|
|
|
13 5人の哲学者が円卓についている。各々の哲学者にはスパゲッティーを持った皿が出されている。
|
|
|
14 スパゲッティーはとても絡まっているので、2本のフォークを使わないと食べられない。
|
|
|
15 お皿の間には1本のフォークが置いてあるので、
|
|
|
16 5人の哲学者に対して5本のフォークが用意されていることになる(図\ref{fig:dpp_image})。
|
|
|
17 哲学者は思索と食事を交互に繰り返している。
|
|
|
18 空腹を覚えると、左右のフォークを手に取ろうと試み、
|
|
|
19 2本のフォークを取ることに成功するとしばし食事をし、
|
|
|
20 しばらくするとフォークを置いて思索に戻る。
|
|
|
21 隣の哲学者が食事中でフォークが手に取れない場合は、
|
|
|
22 そのままフォークが空くのを待つ。
|
|
|
23
|
|
|
24 \begin{figure}[htpb]
|
|
|
25 \begin{center}
|
|
|
26 \includegraphics[scale=.5]{figure/dpp_image.pdf}
|
|
|
27 \end{center}
|
|
|
28 \caption{Dining Philosophers Problemのイメージ}
|
|
|
29 \label{fig:dpp_image}
|
|
|
30 \end{figure}
|
|
|
31
|
|
|
32 各哲学者を一つのプロセスとすると、この問題では5個のプロセスが並列に動くことになる。
|
|
|
33 プロセスの並列実行はスケジューラによって制御することで実現する。
|
|
|
34
|
|
|
35 \subsection{状態の定義とコードセグメントとの対応}
|
|
|
36 Dining Philosophers ProblemをCbCで実装するにあたり、
|
|
|
37 プロセスを次のような8個の状態に分割した。
|
|
|
38 \begin{itemize}
|
|
|
39 \item 思索
|
|
|
40 \item フォークを持っていない場合の飢餓
|
|
|
41 \item 左手にフォークを持つ
|
|
|
42 \item 左手にフォークを持っている場合の飢餓
|
|
|
43 \item 右手にフォークを持つ
|
|
|
44 \item 食事
|
|
|
45 \item 右手のフォークを置く
|
|
|
46 \item 左手のフォークを置く
|
|
|
47 \end{itemize}
|
|
|
48
|
|
|
49 CbCではconcurrencyがコードセグメント単位であるため、
|
|
|
50 実装の方法により任意に細分化することができる。
|
|
|
51 今回は、状態数を8個とし、各状態に対応したコードセグメントを実装した。
|
|
|
52 以下にコードセグメントの例を示す。
|
|
|
53
|
|
|
54 \lstinputlisting[caption=「左手でフォークを持つ」コードセグメント,label=src:pickupL]
|
|
|
55 {src/pickupL.cbc}
|
|
|
56
|
|
|
57 ソースコード\ref{src:pickupL}はDining Philosophers Problemの
|
|
|
58 プログラムの一部である。
|
|
|
59 このコードセグメントは、「左手にフォークを持つ」状態に対応したものである。
|
|
|
60
|
|
|
61 処理の具体的な内容は、左手側のフォークがあればそのフォークを取り、
|
|
|
62 フォークを取ったプロセス(哲学者)のIDとフォークのIDを表示する。
|
|
|
63 その後、次の遷移先として「右手にフォークを持つ」状態である
|
|
|
64 pickup\_rforkコードセグメントをセットする。
|
|
|
65 もし、フォークがなければ次の遷移先として「フォークを持っていない場合の飢餓」状態である
|
|
|
66 hungry1コードセグメントをセットする。
|
|
|
67
|
|
|
68 各コードセグメントは、スケジューラに遷移するようにしている。
|
|
|
69 これは、複数のプロセスをスケジューラを用いて制御するためである。
|
|
|
70 状態遷移に必ずスケジューラを介すことで、
|
|
|
71 任意のプロセスのコードセグメントを実行することができる(図\ref{fig:scheduler})。
|
|
|
72
|
|
|
73 \begin{figure}[htpb]
|
|
|
74 \begin{center}
|
|
|
75 \includegraphics[scale=.7]{figure/scheduler.pdf}
|
|
|
76 \end{center}
|
|
|
77 \caption{スケジューラによる複数プロセスの制御}
|
|
|
78 \label{fig:scheduler}
|
|
|
79 \end{figure}
|
|
|
80
|
|
|
81 CbCプログラムはオートマトンと似た構造になっており、
|
|
|
82 コードセグメントと状態、引数付きgotoと状態遷移、
|
|
|
83 if制御文と遷移条件がそれぞれ対応している(表\ref{tab:automaton-cbc})。
|
|
|
84
|
|
|
85 \begin{table}
|
|
|
86 \centering
|
|
|
87 \begin{tabular}{|c|c|} \hline
|
|
|
88 オートマトン & CbC \\ \hline
|
|
|
89 状態 & コードセグメント \\
|
|
|
90 状態遷移 & 引数付きgoto \\
|
|
|
91 遷移条件 & if制御文 \\ \hline
|
|
|
92 \end{tabular}
|
|
|
93 \caption{オートマトンとCbCの対応}
|
|
|
94 \label{tab:automaton-cbc}
|
|
|
95 \end{table}
|
|
|
96
|
|
|
97 コードセグメントと状態の対応に関しては、実際にはコードセグメントを抜けるときに状態が
|
|
|
98 確定する。
|
|
|
99
|
|
|
100 並列実行をシミュレーションするために必要なスケジューラについて説明する。
|
|
|
101 スケジューラは、最初にプロセスの生成と初期化を行い、それをタスクリストに登録する。
|
|
|
102 その後、各プロセスに対してラウンドロビンやランダムといった任意の方式で実行する。
|
|
|
103 ラウンドロビンとは、各プロセスを一定時間ずつ順番に実行することである。
|
|
|
104
|
|
|
105 並列実行のシミュレーションに関しては、SPINを参考に各プロセスをランダムに
|
|
|
106 実行することで実現する。
|
|
|
107
|
|
|
108 \section{CbCプログラムのタブロー展開}
|
|
|
109 CbCプログラムのタブロー展開の特徴を以下に示す。
|
|
|
110 \begin{itemize}
|
|
|
111 \item プログラムの可能な実行の組み合わせすべてを調べる。
|
|
|
112 \item 状態の探索はDepth First Searchで行う。
|
|
|
113 \item プログラムの実行によって生成される状態は木構造で記録する。
|
|
|
114 \item 同じ状態はすべて共有される。
|
|
|
115 \end{itemize}
|
|
|
116
|
|
|
117 \subsection{状態の展開}
|
|
|
118 提案する手法では、プログラムの可能な実行の組み合わせをすべて調べることができる。
|
|
|
119 CbCプログラムにおける可能な実行の組み合わせとは、
|
|
|
120 CbCプログラムをオートマトンとみなすと、オートマトンの遷移経路にあたる。
|
|
|
121
|
|
|
122 例としてDining Philosophers Problemのプロセス(哲学者)を
|
|
|
123 状態遷移図で示す(図\ref{fig:dpp_automaton})。
|
|
|
124 本研究では、CbCで実装するにあたり状態を8個に分割している。
|
|
|
125 ここで、それぞれの状態をABCDEFGHと定義する。
|
|
|
126
|
|
|
127 \begin{description}
|
|
|
128 \item[A] 思索
|
|
|
129 \item[B] 飢餓
|
|
|
130 \item[C] 左手にフォークを持っている
|
|
|
131 \item[D] 左手にフォークを持つ場合の飢餓
|
|
|
132 \item[E] 両手にフォークを持っている
|
|
|
133 \item[F] 食事
|
|
|
134 \item[G] 右手のフォークを置いた
|
|
|
135 \item[H] 左手のフォークを置いた
|
|
|
136 \end{description}
|
|
|
137
|
|
|
138 このオートマトンは「プロセスを終了する」という入力がないと、
|
|
|
139 例えば、$A\to B\to B\to B\to\cdots$というように探索が無限に続いてしまう場合がある。
|
|
|
140 そうなると、一つの遷移経路が無限に続くことになり、
|
|
|
141 このオートマトンが取り得るすべての遷移経路を調べることができない。
|
|
|
142 そこで、「ひとつの遷移経路で同じ状態が表れた場合はその経路の探索を終了する」
|
|
|
143 という条件を付加する。
|
|
|
144 これにより、先ほどの経路の探索は$A\to B$で終了することができる。
|
|
|
145
|
|
|
146 このようにして、遷移経路を図\ref{fig:dpp_automaton}から求めると、
|
|
|
147 \begin{itemize}
|
|
|
148 \item $A\to B$
|
|
|
149 \item $A\to B\to C\to D$
|
|
|
150 \item $A\to B\to C\to D\to E\to F\to G\to H$
|
|
|
151 \item $A\to B\to C\to E\to F\to G\to H$
|
|
|
152 \end{itemize}
|
|
|
153 という結果が得られる。
|
|
|
154 これが、Dining Philosophers Problemのプロセスの可能な実行の組み合わせとなる。
|
|
|
155
|
|
|
156
|
|
|
157 \begin{figure}[htpb]
|
|
|
158 \begin{center}
|
|
3
|
159 \includegraphics[scale=.75]{figure/dpp_automaton.pdf}
|
|
0
|
160 \end{center}
|
|
|
161 \caption{Dining Philosophers Problemの状態遷移図}
|
|
|
162 \label{fig:dpp_automaton}
|
|
|
163 \end{figure}
|
|
|
164
|
|
|
165 例では単一のプロセスの場合を述べたが、実際には5個のプロセスを並列に実行することになる。
|
|
|
166 その場合、状態数は指数オーダーで増加する。
|
|
|
167 状態数が多い場合、特に並列プログラムに対する状態の展開を手作業で行うのは不可能に近い。
|
|
|
168
|
|
|
169 \newpage
|
|
|
170 \subsection{タブロー展開器の実装}
|
|
|
171 CbCプログラムの状態を自動的に展開するためのツールを作成した。
|
|
|
172 これをタブロー展開器と呼ぶ。
|
|
6
|
173 \\
|
|
0
|
174
|
|
|
175 タブロー展開器は、スケジューラと同様にCbCプログラムに組み込み、
|
|
|
176 複数プロセスを制御することで並列実行をシミュレーションすることができる。
|
|
|
177 また、タブロー展開器は、コードセグメントを一つずつ実行しながら状態を探索していく。
|
|
|
178 状態の探索はDFS(Depth First Search)で行う。
|
|
|
179 例えば、Dining Philosophers Problemの単一プロセスの状態探索木は
|
|
|
180 図\ref{fig:dpp_dfs}のようになる。
|
|
|
181
|
|
|
182 \begin{figure}[htpb]
|
|
|
183 \begin{center}
|
|
|
184 \includegraphics[scale=.8]{figure/dpp_dfs.pdf}
|
|
|
185 \end{center}
|
|
|
186 \caption{Dining Philosophers Problemの状態遷移図}
|
|
|
187 \label{fig:dpp_dfs}
|
|
|
188 \end{figure}
|
|
|
189
|
|
|
190 探索が終了すると、すべての状態が展開されたことになる。
|
|
6
|
191 \\
|
|
0
|
192
|
|
|
193 タブロー展開器の具体的な実装について説明する。
|
|
|
194
|
|
9
|
195 まず、始めに状態として扱うすべての変数のアドレスとそのレンジを
|
|
|
196 Binary Tree構造で記録する(図\ref{fig:memoryBtree})。
|
|
|
197 このBinary Treeをメモリツリーと呼ぶ。
|
|
|
198 変数はメモリ領域に格納されており、メモリ領域のアドレスとそのレンジで指定される。
|
|
|
199 新たに追加される変数がメモリツリーに既に登録されている場合、その変数は登録されない。
|
|
|
200
|
|
|
201 \begin{figure}[htpb]
|
|
|
202 \begin{center}
|
|
|
203 \includegraphics[scale=.8]{figure/memoryBtree.pdf}
|
|
|
204 \end{center}
|
|
|
205 \caption{変数のアドレスとそのレンジのBinary Tree}
|
|
|
206 \label{fig:memoryBtree}
|
|
|
207 \end{figure}
|
|
|
208
|
|
|
209
|
|
|
210 すべての変数が登録されたら、次にそのメモリツリーのコピーを生成し、
|
|
|
211 コピーを状態データベースに登録する。
|
|
|
212 メモリツリーをコピーするとき、そのままコピーするのではなく、
|
|
|
213 メモリのパターンに注目して同じパターンは共有されるようにコピーを生成する。
|
|
|
214 このメモリツリーのコピーによって生成されるBinary Treeをメモリパターンツリーと呼ぶ。
|
|
|
215
|
|
|
216 メモリのパターンとは、例えば変数Aと変数Bがメモリツリーに登録されているとして説明する。
|
|
|
217 変数Aと変数Bはアドレスが違うのでメモリツリーには別々に登録されている。
|
|
|
218 ここでもし、変数Aと変数Bの内容が両方とも0だった場合、
|
|
|
219 アドレスは違っていてもメモリ領域の内容は同じになる(図\ref{fig:memory_pattern})。
|
|
|
220 このメモリ領域の内容のことをメモリパターンと呼ぶ。
|
|
0
|
221
|
|
|
222 \begin{figure}[htpb]
|
|
|
223 \begin{center}
|
|
|
224 \includegraphics[scale=.8]{figure/memory_pattern.pdf}
|
|
|
225 \end{center}
|
|
9
|
226 \caption{メモリパターン}
|
|
0
|
227 \label{fig:memory_pattern}
|
|
|
228 \end{figure}
|
|
|
229
|
|
9
|
230
|
|
|
231 メモリパターンツリーの生成について説明する。
|
|
|
232
|
|
|
233 メモリパターンツリーはメモリパターンとそのレンジを要素としたBinary Treeである。
|
|
|
234 メモリツリーの要素をコピーし、それをメモリパターンツリーに登録していく。
|
|
|
235 登録する際に、メモリパターンツリーに同じメモリパターンがないか検索する。
|
|
|
236 もし、同じメモリパターンがあった場合、メモリツリーの要素をコピーせずに
|
|
|
237 メモリパターンツリーの同じパターンの要素を指すようにする(図\ref{fig:mem_pat_tree})。
|
|
|
238 つまり、同じ状態を共有するようにする。
|
|
|
239
|
|
|
240 これにより使用するメモリ量を減らすことができる。
|
|
6
|
241
|
|
|
242 \begin{figure}[htpb]
|
|
|
243 \begin{center}
|
|
9
|
244 \includegraphics[scale=.8]{figure/mem_pat_tree.pdf}
|
|
6
|
245 \end{center}
|
|
9
|
246 \caption{メモリパターンツリー}
|
|
|
247 \label{fig:mem_pat_tree}
|
|
6
|
248 \end{figure}
|
|
|
249
|
|
9
|
250
|
|
|
251 状態データベースとは、メモリパターンツリーとそのハッシュ値を
|
|
|
252 要素として持つBinary Treeである(図\ref{fig:stateDB})。
|
|
0
|
253
|
|
9
|
254 \begin{figure}[htpb]
|
|
|
255 \begin{center}
|
|
|
256 \includegraphics[scale=.8]{figure/stateDB.pdf}
|
|
|
257 \end{center}
|
|
|
258 \caption{状態データベース}
|
|
|
259 \label{fig:stateDB}
|
|
|
260 \end{figure}
|
|
|
261
|
|
|
262
|
|
|
263 コードセグメントを実行すると、メモリツリーに登録されている
|
|
|
264 変数の内容(メモリパターン)が変化する場合がある(図\ref{fig:change_mem_pat})。
|
|
0
|
265
|
|
|
266 \begin{figure}[htpb]
|
|
|
267 \begin{center}
|
|
|
268 \includegraphics[scale=.9]{figure/change_mem_pat.pdf}
|
|
|
269 \end{center}
|
|
|
270 \caption{コードセグメントの実行にともなうメモリパターンの変化}
|
|
|
271 \label{fig:change_mem_pat}
|
|
|
272 \end{figure}
|
|
|
273
|
|
9
|
274 メモリパターンが変化したメモリツリーから新たにメモリパターンツリーを生成する。
|
|
|
275 生成されたメモリパターンツリーを状態データベースに追加する場合、
|
|
|
276 メモリパターンツリーのハッシュ値をもとに状態データベースを検索する。
|
|
|
277 もし、同じハッシュ値のメモリパターンツリーが見つかった場合は
|
|
|
278 そのメモリパターンツリーは状態データベースに追加されない。
|
|
|
279 見つからなかった場合、状態データベースに追加される。
|
|
|
280 \\
|
|
0
|
281
|
|
|
282
|
|
|
283 次にDepth First Search(DFS)による状態の探索の実装について述べる。
|
|
|
284
|
|
|
285 本研究では、イテレータを用いてDFSを実装した。
|
|
|
286 イテレータとは、配列やリストなどのデータ構造の各要素に対する
|
|
|
287 繰り返し処理を抽象化する手法のことである。
|
|
|
288
|
|
|
289 タブロー展開器はスケジューラとしての機能を備えている。
|
|
|
290 そのため、プロセスを実行する順番をリストとして持ち、制御する。
|
|
|
291 これをタスクリストと呼ぶ(図\ref{fig:task_list})。
|
|
|
292
|
|
|
293 \begin{figure}[htpb]
|
|
|
294 \begin{center}
|
|
|
295 \includegraphics[scale=.9]{figure/task_list.pdf}
|
|
|
296 \end{center}
|
|
|
297 \caption{タスクリストの例}
|
|
|
298 \label{fig:task_list}
|
|
|
299 \end{figure}
|
|
|
300
|
|
|
301 状態を展開する際に、このタスクリストに登録された順番にプロセスを実行していく。
|
|
|
302 したがって、プログラムの状態を一つ進めるためにタスクリストからタスクを取りだし、
|
|
|
303 実行するという処理が繰り返し必要になる。
|
|
|
304 その繰り返し処理を抽象化することで、データ構造の要素に対して行いたい処理を
|
|
|
305 簡潔に記述することができる。
|
|
|
306
|
|
|
307
|
|
|
308 DFSの実装の具体的な内容について述べる。
|
|
|
309
|
|
|
310 タスクリストからタスクを取り出す機構としてタスクイテレータを実装した。
|
|
|
311 タスクイテレータはその時点のタスクリストと状態データベースおよび
|
|
9
|
312 ひとつ前の時点のタスクイテレータを保持している。
|
|
|
313 また、タスクリストから次のタスクを取り出す機能を持っている(図\ref{fig:task_iterator})。
|
|
0
|
314
|
|
|
315 \begin{figure}[htpb]
|
|
|
316 \begin{center}
|
|
|
317 \includegraphics[scale=.9]{figure/task_iterator.pdf}
|
|
|
318 \end{center}
|
|
|
319 \caption{タスクイテレータ}
|
|
|
320 \label{fig:task_iterator}
|
|
|
321 \end{figure}
|
|
|
322
|
|
9
|
323 まず、最初のメモリパターンツリーをメモリツリーより生成し、状態データベースに登録する。
|
|
0
|
324 タスクイテレータの処理によりタスクを取りだしコードセグメントを実行する。
|
|
9
|
325 その実行によって変化したメモリツリーよりメモリパターンツリーを生成し、
|
|
|
326 それを状態データベースから検索する。
|
|
|
327 同じメモリパターンツリーがなかった場合、状態データベースに追加する。
|
|
0
|
328 その後、１段深く探索するために新たにタスクイテレータを生成し、
|
|
|
329 その時点の状態データベースを登録する(図\ref{fig:dfs1})。
|
|
|
330
|
|
|
331 \begin{figure}[htpb]
|
|
|
332 \begin{center}
|
|
|
333 \includegraphics[scale=.9]{figure/dfs1.pdf}
|
|
|
334 \end{center}
|
|
|
335 \caption{タスクイテレータを用いたDFS 1}
|
|
|
336 \label{fig:dfs1}
|
|
|
337 \end{figure}
|
|
|
338
|
|
9
|
339 同じメモリパターンツリーがあった場合は、その経路の探索を終了し、
|
|
0
|
340 タスクイテレータにより次のタスクを取りだしコードセグメントを実行する。
|
|
|
341
|
|
|
342 タスクイテレータのタスクリストをすべて実行した場合、
|
|
|
343 そのタスクイテレータを破棄し、ひとつ前のタスクイテレータに戻る(図\ref{fig:dfs2})。
|
|
|
344 そこで探索可能な経路があればメモリパターンをレストアし探索を行う。
|
|
|
345
|
|
|
346 \begin{figure}[htpb]
|
|
|
347 \begin{center}
|
|
|
348 \includegraphics[scale=.8]{figure/dfs2.pdf}
|
|
|
349 \end{center}
|
|
|
350 \caption{タスクイテレータを用いたDFS 2}
|
|
|
351 \label{fig:dfs2}
|
|
|
352 \end{figure}
|
|
|
353
|
|
|
354 これを繰り返していき、タスクイテレータが根に到達した場合、
|
|
|
355 全状態の探索が完了したことになる(図\ref{fig:dfs3})。
|
|
|
356
|
|
|
357 \begin{figure}[htpb]
|
|
|
358 \begin{center}
|
|
|
359 \includegraphics[scale=.8]{figure/dfs3.pdf}
|
|
|
360 \end{center}
|
|
|
361 \caption{状態探索の完了}
|
|
|
362 \label{fig:dfs3}
|
|
|
363 \end{figure}
|
|
|
364
|
|
|
365
|
|
|
366 \newpage
|
|
|
367 ソースコード\ref{src:tableau}に実際にタブロー展開を行っているコードセグメントを示す。
|
|
|
368
|
|
|
369 \lstinputlisting[caption=タブローコードセグメント,label=src:tableau]
|
|
|
370 {src/tableau.cbc}
|
|
|
371
|
|
|
372 タブローコードセグメントは、関数呼び出しを使用するためCwCで記述している。
|
|
|
373
|
|
|
374 \verb|get_memory_hash()|関数によってメモリパターンのハッシュ値を取得する。
|
|
|
375 そのハッシュ値をもとに\verb|lookup_StateDB()|関数で状態データベースの検索を行っている。
|
|
|
376 \verb|next_task_iterator()|関数は次に実行するタスクを取り出すものである。
|
|
|
377
|
|
|
378 \verb|restore_memory()|関数は任意の時点の状態に戻すための関数である。
|
|
|
379
|
|
|
380 実際にコードセグメントを実行するのは\verb|goto list->phils->next()|である。
|
|
|
381 引数付きgotoで検証対象のプログラムのコードセグメントに遷移する。
|
|
|
382
|
|
|
383 タスクイテレータが根に達した場合、探索を終了するために
|
|
|
384 \verb|goto ret(0),env|を実行している。
|
|
|
385
|
|
|
386 %\section{LZW法を用いた状態の圧縮}
|
|
|
387
|
|
|
388 \section{線形時相論理による仕様の検証手法}
|
|
|
389 タブロー展開を行う際に、線形時相論理(Linear-time Temporal Logic、LTL)式より
|
|
|
390 生成されたコードセグメントを実行することで検証を行う。
|
|
|
391
|
|
|
392 \subsection{検証の実装}
|
|
9
|
393 検証対象のプログラムからスケジューラに遷移した後、
|
|
|
394 タブローコードセグメントに遷移する前に
|
|
0
|
395 LTL式より生成された検証用コードセグメントを実行する。
|
|
|
396 これにより、すべての状態において特定の性質を満たすことを調べることが可能である。
|
|
|
397
|
|
|
398 実装したDining Philosophers Problemプログラムに対してデッドロックの検出を行う。
|
|
|
399 デッドロックとは、複数のプロセスが互いに相手の占有している資源の開放を待ってしまい、
|
|
|
400 結果としてプログラムが停止してしまうことである。排他制御の欠陥で起こる。
|
|
|
401
|
|
|
402 Dining Philosophers Problemにおいて、資源とはフォークのことである。
|
|
|
403 つまり、この場合のデッドロックはすべての哲学者(プロセス)が左手でフォークを持ち、
|
|
|
404 右手のフォークが空くのを待っている状態である(図\ref{fig:dpp_deadlock})。
|
|
|
405
|
|
|
406 \begin{figure}[htpb]
|
|
|
407 \begin{center}
|
|
|
408 \includegraphics[scale=.5]{figure/dpp_deadlock.pdf}
|
|
|
409 \end{center}
|
|
|
410 \caption{Dining Philosophers Problemのデッドロック状態}
|
|
|
411 \label{fig:dpp_deadlock}
|
|
|
412 \end{figure}
|
|
|
413
|
|
|
414
|
|
|
415 デッドロックを検知するために、 命題pを「すべての哲学者が左手にフォークを持っている」
|
|
|
416 として、 命題pが決して起こらないことを検査する。
|
|
|
417 これをLTL式で表すと□~pである。
|
|
|
418 これは、LTLで表現できる重要な特性の一つの安全性特性である。
|
|
|
419
|
|
|
420 これを検査するための検証用コードセグメントをソースコード\ref{src:check}に示す。
|
|
|
421
|
|
|
422 \lstinputlisting[caption=検証用コードセグメント,label=src:check]
|
|
|
423 {src/ltl.cbc}
|
|
|
424
|
|
9
|
425 \verb|p()|関数は命題pに相当するもので、すべての哲学者(プロセス)が
|
|
|
426 左手にフォークを持っているかどうかを判定するものである。
|
|
0
|
427 checkコードセグメントがタブロー展開の際に実行されることで、
|
|
|
428 すべての状態において命題pが決して起こらないかどうかを検査することができる。
|
|
|
429
|
|
|
430 %%% end %%%
|
