|
19
|
1 \documentclass[twocolumn, a4j, twoside]{jarticle}
|
|
|
2 \usepackage{master_proc}
|
|
|
3 \usepackage[dvips]{graphicx}
|
|
|
4
|
|
|
5 % dvipdfm を使って PDF ファイルに日本語の栞をつける
|
|
|
6 % \usepackage[dvipdfm]{color}
|
|
|
7 % \usepackage[dvipdfm,bookmarks=true,bookmarksnumbered=true,%
|
|
|
8 % bookmarkstype=toc]{hyperref}
|
|
|
9
|
|
|
10 \jtitle{線形時相論理によるContinuation based Cプログラムの検証} %和文タイトル
|
|
|
11 \etitle{Verification of Continuation based C Program using Linear-time Temporal Logic} %英文タイトル
|
|
|
12 \author{下地 篤樹} %著者名
|
|
|
13 \studentid{068507B} %学籍番号
|
|
|
14 \teacher{河野 真治} %指導教官
|
|
|
15
|
|
|
16 \begin{document}
|
|
|
17 \maketitle
|
|
|
18 \section{はじめに}
|
|
|
19 リアルタイムプログラムや並列プログラムのような非決定性を含むプログラムは、
|
|
|
20 逐次型のプログラムに有効な二分法などによるデバッグ手法ではデバッグすることが
|
|
|
21 困難である。
|
|
|
22 そのため、非決定性を含むプログラムに対して有効なデバッグ手法や検証手法の
|
|
|
23 確立が重要な課題となっている。
|
|
|
24
|
|
|
25 そこで、本研究では、Continuation based C(CbC)言語による実装と
|
|
|
26 その実装に対する検証手法を提案している。
|
|
|
27 また、CbCで記述されたプログラムは状態遷移記述になるという性質がある。
|
|
|
28
|
|
|
29 本研究は、CbCプログラムが状態遷移記述になることに着目し、
|
|
22
|
30 状態遷移記述に対して有効であるタブロー法による状態の展開を行い、
|
|
19
|
31 状態を展開する際に、線形時相論理も同時に展開することにより検証を行う。
|
|
|
32
|
|
21
|
33 \vspace{-2mm}
|
|
20
|
34 \section{Continuation based Cの概要}
|
|
21
|
35 CbC は、C言語を制限したもので、
|
|
22
|
36 Cからループ制御構造と、サブルーチン・コールを取り除き、継続を導入した言語である。
|
|
|
37 この言語は、Cに継続専用のプログラム単位であるコード(code)と、
|
|
20
|
38 継続(goto)を導入した構成となっている。
|
|
|
39 継続とは、次に実行すべきコードを直接または間接的に指定する手法である。
|
|
22
|
40 CbC は、サブルーチンよりも小さいプログラム単位であるcodeを導入しているため、
|
|
20
|
41 C言語よりも細かく、アセンブラよりも高度な記述が可能であるという利点がある。
|
|
|
42
|
|
|
43 CbCはコードセグメントを引数付きgoto文で接続することで継続を実現している。
|
|
|
44 コードセグメントとは、codeという型で定義されるプログラム単位である。
|
|
22
|
45 このコードセグメントへの遷移は引数付きgoto文によってのみ行われる。
|
|
20
|
46 また、コードセグメントからの脱出も引数付きgoto文によってのみ行われる。
|
|
|
47
|
|
22
|
48 また、ここでは、CbCにおける並列度はコードセグメント単位を使用する。
|
|
20
|
49
|
|
22
|
50 CbCにCのサブルーチンへ戻るための環境付き継続を
|
|
|
51 導入することでCの上位言語となる。この言語をCwC(C with Continuation)と呼ぶ。
|
|
20
|
52 CwCでは、CbCから通常のC言語の関数を呼び出すことができる。
|
|
|
53
|
|
21
|
54 \vspace{-2mm}
|
|
|
55 \section{線形時相論理の概要}
|
|
|
56 線形時相論理(Linear-time Temporal Logic、LTL)は、
|
|
|
57 時間を様相として持つ様相論理の一つで、
|
|
|
58 状態遷移システムの単一の経路に関する性質を記述することが可能である。
|
|
|
59 表\ref{tab:LTL}にLTLの単項演算子を示す。
|
|
|
60 \begin{table}
|
|
|
61 {\footnotesize
|
|
|
62 \begin{center}
|
|
|
63 \begin{tabular}{|l|c|l|} \hline
|
|
|
64 \multicolumn{1}{|c|}{名称} & 記号表記 & \multicolumn{1}{|c|}{意味} \\ \hline
|
|
|
65 Always & □p & pは今後常に真である \\ \hline
|
|
|
66 Sometime & ◇p & pは将来のいずれかの時点で真である\\ \hline
|
|
|
67 Next & ○p & pは次の時点で真である \\ \hline
|
|
|
68 \end{tabular}
|
|
|
69 \vspace{-2mm}
|
|
|
70 \caption{線形時相論理の単項演算}
|
|
|
71 \label{tab:LTL}
|
|
|
72 \end{center}
|
|
|
73 }
|
|
|
74 \vspace{-8mm}
|
|
|
75 \end{table}
|
|
|
76 検証において、時相論理はシステムの要求仕様を記述する方法として形式的検証で利用さ
|
|
|
77 れる。
|
|
|
78
|
|
|
79 \vspace{-2mm}
|
|
22
|
80 \section{他のモデル検査ツール}
|
|
|
81 他のモデル検査ツールとしてSPINとJava PathFinder(JPF)がある。
|
|
20
|
82
|
|
22
|
83 SPIN\cite{bib:spin}は、プログラム変換的な手法で検証するツールで、
|
|
20
|
84 検証対象をPROMELA(PROcess MEta LAnguage)という言語で記述し、
|
|
|
85 それを基にC言語で記述された検証器を生成するものである。
|
|
|
86 チャネルを使っての通信や並列動作する有限オートマトンのモデル検査が可能である。
|
|
|
87 SPINでは、アサーション、デッドロック、到達性、進行制、LTL式の
|
|
|
88 性質について検査することができる。
|
|
|
89 また、SPINの並列動作はステートメント単位となる。
|
|
|
90
|
|
22
|
91 JPF\cite{bib:jpf}は、実行可能なJavaのバイトコードを検証するためのシステムである。
|
|
20
|
92 バイトコードを状態遷移モデルとして扱い、
|
|
|
93 実行時に遷移し得る状態を網羅的に検査することにより、デッドロックを検知したり、
|
|
22
|
94 キャッチされていない例外を検出することができる。
|
|
20
|
95 JPFで検査できる性質として、アサーション、デッドロック、キャッチされていない例外
|
|
|
96 があげられる。
|
|
21
|
97 また、JPFの並列動作はスレッド単位となる。
|
|
22
|
98 \vspace{-2mm}
|
|
20
|
99
|
|
|
100 \section{実装}
|
|
|
101 検証用のサンプルプログラムとしてDining Philosophers Problemを用いる。
|
|
|
102 これは資源共有問題の一つで、次のような内容である。
|
|
|
103 5人の哲学者が円卓についており、それぞれ思索と食事を交互に繰り返す。
|
|
|
104 円卓には5本のフォークが置かれており、哲学者は左右のフォーク2本を使って食事をする。
|
|
|
105 フォークが取れない場合はフォークが空くのを待つ。
|
|
|
106 この問題では、すべての哲学者が一斉に左手でフォークを取るとデッドロックが起きる。
|
|
|
107 例として、左手でフォークを取るコードセグメントを示す。
|
|
22
|
108
|
|
|
109 \vspace{-3mm}
|
|
20
|
110 {\footnotesize
|
|
|
111 \begin{verbatim}
|
|
|
112 code pickup_lfork(PhilsPtr self)
|
|
|
113 {
|
|
|
114 if (self->left_fork->owner == NULL) {
|
|
|
115 self->left_fork->owner = self;
|
|
|
116 goto pickup_rfork(self);
|
|
|
117 } else {
|
|
|
118 goto pickup_lfork(self);
|
|
|
119 }
|
|
|
120 }
|
|
|
121 \end{verbatim}
|
|
|
122 }
|
|
21
|
123 \vspace{-4mm}
|
|
22
|
124
|
|
20
|
125 codeがコードセグメントの定義であり、
|
|
|
126 コードセグメントの引数部分をインターフェースと呼ぶ。
|
|
|
127 このコードセグメントは左手でフォークが取れた場合は、
|
|
|
128 右手でフォークを取るコードセグメントへ遷移する。
|
|
|
129 取れなかった場合は、またこのコードセグメントへ遷移する。
|
|
|
130
|
|
|
131 次に、タブロー法による状態の展開の実装について説明する。
|
|
|
132
|
|
22
|
133 CbCプログラムのタブロー法による状態の展開の特徴として、
|
|
20
|
134 プログラムの可能な実行の組み合わせすべてを調べる、
|
|
22
|
135 プログラムの状態を展開するために状態の探索をDepth First Searchで行う、
|
|
20
|
136 プログラムの実行によって生成される状態は木構造で記録する、
|
|
22
|
137 同じ状態はすべて共有することでメモリ消費を減らすということ
|
|
20
|
138 があげられる。
|
|
|
139
|
|
22
|
140 まず、最初に状態として扱うすべてのメモリをBinary Tree構造で記録する。
|
|
20
|
141 そして、検証対象のプログラムのコードセグメントを実行して、
|
|
|
142 実行に伴う状態の変化をBinary Tree構造で記録していく。
|
|
|
143 このBinary Treeを状態データベースと呼ぶ。
|
|
|
144 すべての可能な実行の組み合わせを実行しながらそのときの状態を
|
|
22
|
145 状態データベースに登録していく。
|
|
20
|
146
|
|
21
|
147 以下にタブロー展開を行うためのtableauコードセグメントを示す。
|
|
|
148 このコードセグメントはCwCで記述している。
|
|
22
|
149
|
|
|
150 \vspace{-3mm}
|
|
20
|
151 {\footnotesize
|
|
|
152 \begin{verbatim}
|
|
|
153 code tableau(TaskPtr list)
|
|
|
154 {
|
|
|
155 StateDB out;
|
|
|
156 if (lookup_StateDB(&st, &state_db, &out)) {
|
|
|
157 while(!(list=next_task_iterator(task_iter))) {
|
|
|
158 TaskIteratorPtr prev_iter=task_iter->prev;
|
|
|
159 if (!prev_iter) {
|
|
|
160 memory_usage();
|
|
|
161 goto ret(0),env;
|
|
|
162 }
|
|
|
163 free_task_iterator(task_iter);
|
|
|
164 task_iter=prev_iter;
|
|
|
165 }
|
|
|
166 restore_memory(task_iter->state->memory);
|
|
|
167 } else {
|
|
|
168 task_iter=create_task_iterator(list,out,task_iter);
|
|
|
169 }
|
|
|
170 goto list->phils->next(list->phils,list);
|
|
|
171 }
|
|
|
172 \end{verbatim}
|
|
|
173 }
|
|
21
|
174 \vspace{-3mm}
|
|
22
|
175
|
|
20
|
176 検証対象プログラムのコードセグメントはこのtableauコードセグメントに遷移するようにする。
|
|
|
177 \verb|lookup_StateDB()|関数で状態データベースからコードセグメントの実行によって
|
|
|
178 得られた状態を検索・登録していく。登録する際にそのまま登録するのではなく、
|
|
22
|
179 メモリを記録したBinary Treeをコピーして登録していく。この際、同じメモリ内容が
|
|
20
|
180 あった場合は、同じ領域を指すことで状態を共有するようにする。
|
|
21
|
181 このtableauコードセグメントによりDFSで状態を探索していく。
|
|
20
|
182
|
|
22
|
183 また、タブロー展開を行う際に、
|
|
|
184 LTL式より生成されたコードセグメントを実行することで検証を行う。
|
|
|
185 検証対象プログラムからtableauコードセグメントに遷移する前に
|
|
|
186 生成された検証用コードセグメントを実行することで検証する。
|
|
21
|
187
|
|
22
|
188 ここでは、実装したDining Philosophers Problemに対して、デッドロックの検知を行う。
|
|
|
189 デッドロックとは、複数のプロセスが互いに相手の占有している資源の開放を待ってしまい、
|
|
|
190 結果としてプログラムが停止してしまうことである。
|
|
|
191 Dining Philosophers Problemにおいて、資源とはフォークのことである。
|
|
|
192 つまり、この場合のデッドロックはすべての哲学者(プロセス)が左手でフォークを持ち、
|
|
|
193 右手のフォークが空くのを待っている状態である。
|
|
|
194
|
|
|
195 デッドロックが起きる条件である、「哲学者が一斉に左手でフォークを取る」を
|
|
|
196 すべての状態で検査することでプログラムのデッドロックを検知する。
|
|
21
|
197
|
|
|
198 \vspace{-2mm}
|
|
|
199 \section{評価および考察}
|
|
|
200 Dining Philosophers Problemの検証をCbC、SPIN、JPFで行った。
|
|
22
|
201 それぞれの結果を表\ref{tab:time}に示す。
|
|
21
|
202 \begin{table}[htbp]
|
|
22
|
203 \vspace{-2mm}
|
|
21
|
204 {\footnotesize
|
|
|
205 \begin{center}
|
|
|
206 \begin{tabular}{|r|r|r|} \hline
|
|
22
|
207 \multicolumn{3}{|c|}{\textbf{CbCによる検証}} \\ \hline
|
|
21
|
208 プロセス数 & 状態数 & 実行時間(秒) \\ \hline
|
|
|
209 5 & 38,984 & 0.68 \\ \hline
|
|
|
210 6 & 159,299 & 3.90 \\ \hline
|
|
|
211 7 & 845,529 & 28.48 \\ \hline
|
|
|
212 8 & 3,915,727 & 201.04 \\ \hline
|
|
22
|
213 \multicolumn{3}{|c|}{\textbf{SPINによる検証}} \\ \hline
|
|
21
|
214 5 & 94 & 0.008 \\ \hline
|
|
|
215 6 & 212 & 0.01 \\ \hline
|
|
|
216 7 & 494 & 0.03 \\ \hline
|
|
|
217 8 & 1,172 & 0.04 \\ \hline
|
|
22
|
218 \multicolumn{3}{|c|}{\textbf{JPFによる検証}} \\ \hline
|
|
21
|
219 5 & 不明 & 3.98 \\ \hline
|
|
|
220 6 & 不明 & 7.33 \\ \hline
|
|
|
221 7 & 不明 & 26.29 \\ \hline
|
|
|
222 8 & 不明 & 123.16 \\ \hline
|
|
|
223 \end{tabular}
|
|
22
|
224 \vspace{-3mm}
|
|
|
225 \caption{検証の計測結果}
|
|
|
226 \label{tab:time}
|
|
21
|
227 \end{center}
|
|
|
228 }
|
|
22
|
229 \vspace{-7mm}
|
|
21
|
230 \end{table}
|
|
|
231 CbCの検証では、実際に実行可能なプログラムであり、プログラムで渡される引数全体と
|
|
|
232 大域変数全体が状態となるため、プロセス数が増えるにつれて状態数も指数関数的に
|
|
|
233 多くなっている。
|
|
|
234
|
|
|
235 SPINによる結果は、CbCでの検証と比べて状態数が少ない。
|
|
|
236 生成される状態数が少ないことが探索時間の短さにつながっていると考えられる。
|
|
|
237
|
|
|
238 JPFの探索時間が、プロセス数6個まではCbCの探索時間よりも遅く、
|
|
|
239 7個以上になるとCbCより速いのは、CbCの実装によるものだと推測される。
|
|
|
240
|
|
|
241 CbCでの実装では、メモリのBinary Treeをバランスさせていないため、
|
|
|
242 状態数が増えるにつれて探索時間が長くなっていると考えられる。
|
|
22
|
243
|
|
21
|
244 \vspace{-2mm}
|
|
|
245 \section{まとめ}
|
|
|
246 Dining Philosophers ProblemをCbCで記述し、
|
|
|
247 LTL式より生成された検証用コードセグメントを同時にタブロー展開することで
|
|
22
|
248 検証を行い、他のモデル検査ツールと比較した。
|
|
21
|
249 CbCの方が遅いという結果になったが、実用には耐えられるレベルである。
|
|
|
250 また、メモリのTreeをバランスさせることで探索時間の短縮を行うことが課題である。
|
|
22
|
251
|
|
21
|
252 \vspace{-2mm}
|
|
19
|
253 {\small
|
|
|
254 \begin{thebibliography}{9}
|
|
|
255 \bibitem{bib:jssst2000kono}
|
|
|
256 河野真治. ``継続を持つCの下位言語によるシステム記述''.
|
|
|
257 日本ソフトウェア科学会第17回大会, 2000.
|
|
|
258 \bibitem{bib:sigos2007}
|
|
|
259 下地篤樹, 河野真治. ``線形時相論理によるContinuation based Cプログラムの検証''.
|
|
|
260 情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS), April, 2007.
|
|
22
|
261 \bibitem{bib:spin}
|
|
|
262 ``Spin - Formal Verification''.
|
|
|
263 http://spinroot.com/spin/whatispin.html
|
|
|
264 \bibitem{bib:jpf}
|
|
|
265 ``Java PathFinder''.
|
|
|
266 http://javapathfinder.sourceforge.net/
|
|
19
|
267 \end{thebibliography}
|
|
|
268 }
|
|
|
269 \end{document}
|
