Mercurial > hg > Papers > 2016 > atton-ipsjpro
annotate paper/vmpcbc.tex @ 25:306c7ab881d8
Add figure
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 05 Jul 2016 17:53:06 +0900 |
parents | ada1caa13842 |
children | 83db914f0da3 |
rev | line source |
---|---|
9 | 1 \documentclass[submit,PRO]{ipsj} |
2 \usepackage{PROpresentation} | |
3 \PROheadtitle{y-n-(x): 情報処理学会プログラミング研究会 発表資料 Y年m月d日} | |
4 | |
18 | 5 \usepackage[dvipdfmx]{graphicx} |
9 | 6 \usepackage{latexsym} |
19 | 7 \usepackage{listings} |
8 \lstset{ | |
9 language={C}, | |
10 basicstyle={\small}, | |
11 commentstyle={\small\itshape}, | |
12 keywordstyle={\small\bfseries}, | |
13 stringstyle={\small}, | |
14 frame={trlb}, | |
15 breaklines=true, | |
16 columns=[l]{fullflexible}, | |
17 xrightmargin=0zw, | |
18 xleftmargin=3zw, | |
19 lineskip=-0.5ex, | |
20 captionpos=b, | |
21 moredelim=**[s][\color{red}]{\"compressed}{\"}, | |
22 } | |
23 \renewcommand{\lstlistingname}{Code} | |
9 | 24 |
25 \def\Underline{\setbox0\hbox\bgroup\let\\\endUnderline} | |
26 \def\endUnderline{\vphantom{y}\egroup\smash{\underline{\box0}}\\} | |
27 \def\|{\verb|} | |
28 | |
29 \setcounter{巻数}{57} | |
30 \setcounter{号数}{1} | |
31 \setcounter{page}{1} | |
32 | |
24 | 33 % TODO: Code Segment, Code Segment の統一 |
21 | 34 |
9 | 35 |
36 \受付{2015}{3}{4} | |
37 %\再受付{2015}{7}{16} %省略可能 | |
38 %\再再受付{2015}{7}{20} %省略可能 | |
39 \採録{2015}{8}{1} | |
40 | |
41 | |
42 | |
43 | |
44 \begin{document} | |
45 | |
46 | |
47 \title{Continuation based C を用いたプログラムの検証手法} | |
48 \etitle{Verification method of programs using Continuation based C} | |
49 | |
50 \affiliate{RUnivIe}{琉球大学 大学院 理工学研究科 情報工学専攻\\ | |
51 Infomation Engineering Course Graduate School of Engineering and Science University of the Ryukyus} | |
52 \affiliate{RUniv}{琉球大学\\ | |
53 University of the Ryukyus} | |
54 | |
55 | |
56 \author{比嘉 健太}{Yasutaka HIGA}{RUnivIe}[atton@cr.ie.u-ryukyu.ac.jp] | |
57 \author{河野 真治}{Shinji KONO}{RUniv}[kono@ie.u-ryukyu.ac.jp] | |
58 | |
59 \begin{abstract} | |
60 Continuation based C 言語によって記述されたプログラムのデータ構造の性質を検証する手法を提案する。 | |
61 Continuation based C とは当研究室が提案している Code Segment, Data Segment という単位でプログラムを記述する言語である。 | |
62 Code Segment とは処理の単位であり、データの単位である Data Segment を入力と出力に持つ。 | |
63 プログラム全体は Code Segment どうしの接続により表現され、あるCode Segment の出力は接続された次の Code Segment の入力となる。 | |
64 また、メモリ管理やエラーの処理など、本来中心に行ないたい処理と異なる処理はメタ計算として分離し、Meta Code Segment, Meta Data Segment として記述する。 | |
65 Code Segment の接続処理を Meta Code Segment として表現し、接続部分に検証を含めることで 元の Code Segment を変更することなくプログラムの検証を行なう。 | |
25 | 66 本論文では Continuatoin based C によって記述された赤黒木といったデータ構造の性質を検証する。 |
9 | 67 \end{abstract} |
68 | |
69 | |
70 \begin{jkeyword} | |
71 プログラミング言語, 検証, 赤黒木 | |
72 \end{jkeyword} | |
73 | |
74 \begin{eabstract} | |
25 | 75 We propose a verification method for executable programs using Continuation based C language. |
9 | 76 Our laboratory develops Continuation based C language which supports programming unit called Code Segment, Data Segment. |
77 Code segments are calculation units which have input/output data segments that data unit. | |
78 Programs are represented by connections among with code segments and code segments. | |
79 The output data segment of some code segment is converted to the input data segment of connected one. | |
80 We introduce meta computations which split main computations and complicated computations such as memory control, error handling and more. | |
81 Meta computations represented to meta code segment and meta data segment, which saves main computations. | |
25 | 82 In this paper, We define a meta computation which connects code segments with verifications and verify properties of data structures such as Red-Black Tree. |
9 | 83 \end{eabstract} |
84 | |
85 \begin{ekeyword} | |
86 Programming Language, Verification, Red-Black Tree | |
87 \end{ekeyword} | |
88 | |
89 \maketitle | |
90 | |
24 | 91 \section{Code SegmentとData Segment} |
10 | 92 本研究は実際に動作するプログラムの信頼性を保証することを目的とする。 |
93 プログラムの信頼性とは、定められた環境下においてプログラムの動作が必ず仕様を満たすことである。 | |
22
fca342b9dbd5
Add bibliographies
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
94 プログラムが仕様を満たすことを保証する手法として、プログラムの性質を証明する手法\cite{cite:agda}やプログラムの状態を全て数えあげるモデルチェッカ\cite{cite:cbmc}などが存在する。 |
10 | 95 しかし、証明では実際に動作するコードでなく証明用にコードを書き直したり、モデルチェッカでは高速化のために抽象化した記号実行によって性質が検証されるなど、実際に動作するコードとの乖離が発生してしまう。 |
23 | 96 よって、検証した環境では仕様が満たされていても、実装にバグが入り込み信頼性を保証できない可能性がある。 |
97 仕様とその実装コードの信頼性を保証するため、実際に動作するコードの検証を行なう。 | |
10 | 98 |
24 | 99 動作するコードを検証しやすいよう、本研究室ではCode SegmentとData Segmentを用いるプログラミングスタイルを提案している。 |
100 Code Segmentとは処理の単位であり、ループを含まない単純な処理のみを行なう。 | |
101 プログラムはCode Segmentどうしを組み合わせることで構築される(図\ref{fig:csds})。 | |
102 Code Segment間における値の受け渡しには、Data Segmentというデータの単位で行なう。 | |
103 なお、接続されたCode Segmentには依存関係が発生するが、依存関係が無いCode Segmentは並列に実行することが可能である。 | |
10 | 104 |
18 | 105 \begin{figure} |
106 \begin{center} | |
107 \includegraphics[scale=0.5]{fig/code_segment_data_segment.pdf} | |
24 | 108 \caption{Code Segmentどうしの組み合わせ} |
18 | 109 \label{fig:csds} |
110 \end{center} | |
111 \end{figure} | |
10 | 112 |
24 | 113 ここで、Code Segmentどうしの接続処理について考える。 |
114 処理を表すCode Segmentどうしの接続も処理であるため、Code Segmentで表現できる。 | |
115 このような計算を実現するための計算をメタ計算と呼び、メタ計算を行なうCode SegmentをMeta Code Segmentと呼ぶ。 | |
116 Meta Code SegmentはCode Segment間に存在する処理と考えることもできる(図\ref{fig:metaCSDS})。 | |
117 | |
118 \begin{figure}[htbp] | |
119 \begin{center} | |
120 \includegraphics[scale=0.5]{fig/meta_code_segment_and_meta_data_segment.pdf} | |
121 \caption{Meta Code Segment と Meta Data Segment} | |
122 \label{fig:metaCSDS} | |
123 \end{center} | |
124 \end{figure} | |
125 | |
126 また、メタ計算に必要なデータはMeta Data Segmentに格納し、通常の処理に必要なData Segmentも内包する。 | |
127 プログラムの性質を検証する機能をメタ計算として提供することで、ユーザが書いたCode Segmentを変更することなく、メタ計算を追加するだけでプログラムの信頼性を上げる。 | |
10 | 128 |
9 | 129 \section{Continuation based C} |
24 | 130 Code SegmentとData Segmentを用いたプログラミングスタイルで記述言語に Continuation based C\cite{cite:cbc-clang} 言語が存在する。 |
17
84f71cc1764a
Add bibliographies
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
15
diff
changeset
|
131 Continuation based C (以下 CbC)はOSや組込みシステムなどの記述を行なうことを目標に作られた、アセンブラとC言語の中間のような言語である。 |
24 | 132 CbC におけるCode SegmentはC言語における関数に、関数呼び出しが末尾のみである制約を加えようなものである。 |
133 Code Segmentどうしの接続は goto による軽量継続で表される(Code\ref{src:simpleCs})。 | |
11 | 134 |
24 | 135 \begin{lstlisting}[label=src:simpleCs, caption=code]%Code Segmentの接続例 (10加算して2倍する)] |
23 | 136 |
21 | 137 __code addTen(int a) { |
138 int b = a+10; | |
139 goto twice(b); | |
19 | 140 } |
141 | |
142 __code twice(int x) { | |
143 int y = 2*x; | |
144 goto showValue(y); | |
145 } | |
146 \end{lstlisting} | |
11 | 147 |
24 | 148 CbCにおけるCode Segmentは、C言語の関数宣言の返り値の型の部分に \verb/__code/ を記述して定義する。 |
149 Code Segment内部には変数の宣言やif文による分岐といったC言語の文法を用いて処理を記述する。 | |
150 Code\ref{src:simpleCs}の例では、2つのCode Segment \verb/addTen/ と \verb/twice/を定義している。 | |
21 | 151 \verb/addTen/では int の値を受けとり、10加算して \verb/twice/ を実行する。 |
23 | 152 \verb/twice/ では受けとったintの値を2倍して \verb/showValue/ を実行する。 |
21 | 153 |
24 | 154 また、CbCにおけるData SegmentはC言語における構造体と共用体を用いたデータ構造である。 |
155 各Code Segmentで必要な値を構造体で定義し、それらの共用体としてData Segmentを定義する(Code\ref{src:simpleDs})。 | |
21 | 156 |
24 | 157 \begin{lstlisting}[label=src:simpleDs, caption=data]%Data Segmentの例 (10加算して2倍する)] |
21 | 158 |
159 union Data { | |
160 struct Count { | |
161 int x; | |
162 } count; | |
163 struct Port { | |
164 unsigned int port; | |
165 } port; | |
166 }; | |
167 \end{lstlisting} | |
11 | 168 |
24 | 169 Code\ref{src:simpleDs}ではData Segmentとして int を持つ count と unsigned int を持つ port の2つを定義している。 |
170 Code Segmentに\verb/goto/する際に利用するData Segmentを指定することで、Data Segment内部の値で処理が行なえる(Code\ref{src:stub})。 | |
21 | 171 |
24 | 172 \begin{lstlisting}[label=src:stub, caption=stub]%Data Segmentの利用例 (countの値を2倍する)] |
21 | 173 |
174 __code addTen(union Data* ds, int a) { | |
175 int b = a+10; | |
176 goto twice_stub(ds); | |
177 } | |
178 | |
179 __code twice_stub(union Data* ds) { | |
180 goto twice(ds->count.x); | |
181 } | |
182 | |
183 __code twice(int x) { | |
184 int y = 2*x; | |
185 goto showValue(y); | |
186 } | |
187 \end{lstlisting} | |
188 | |
23 | 189 Code\ref{src:stub}では \verb/twice/ の処理で2倍する値が count の値であることを \verb/twice_stub/ 内で指定している。 |
24 | 190 CbC におけるMeta Code SegmentはCode\ref{src:stub} における \verb/twice_stub/ や goto する際に必ず通るCode Segment(Code\ref{src:meta}の \verb/meta/)のように表現される。 |
19 | 191 |
22
fca342b9dbd5
Add bibliographies
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
192 \begin{lstlisting}[label=src:meta, caption=meta ] %メタ計算として接続した例] |
19 | 193 |
21 | 194 struct Context { |
195 union Data *data; | |
196 /* メタ計算に必要なデータ */ | |
197 }; | |
198 | |
19 | 199 __code meta(struct Context* context, |
200 enum Code next) { | |
11 | 201 |
19 | 202 /* 接続時に行なうメタ計算を記述 */ |
203 switch (next) { | |
204 case AddTen: | |
24 | 205 /* 特定のCode Segmentへのメタ計算 */ |
21 | 206 goto addTen_stub(context); |
19 | 207 case Twice: |
21 | 208 goto twice_stub(context); |
19 | 209 } |
210 } | |
211 | |
21 | 212 __code addTen(struct Context* context, int a) { |
213 x = x+10; | |
19 | 214 goto meta(context, Twice); |
215 } | |
216 | |
21 | 217 __code twice(struct Context* context, int x) { |
218 x = x*2; | |
19 | 219 goto meta(context, ShowValue); |
21 | 220 } |
19 | 221 \end{lstlisting} |
222 | |
22
fca342b9dbd5
Add bibliographies
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
223 メタ計算の切り替えは \verb/meta/ を変更することで実現できる。 |
24 | 224 また、Meta Data Segmentに相当する \verb/Context/ はData Segmentをフィールドに持つ構造体として表現し、メタ計算に必要な処理は構造体にフィールドを追加することで表現できる. |
11 | 225 |
14 | 226 CbC におけるメタ計算の例にメモリ管理がある。 |
24 | 227 メモリの確保やポインタ演算をMeta Code Segmentのみで行なうことで、Code Segment側ではメモリに由来するエラーを排除することができる。 |
22
fca342b9dbd5
Add bibliographies
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
228 加えて、メタ計算を切り替えることでメモリの管理方法も切り替えることができるため、不要な領域の開放するよう拡張することも容易である。 |
23 | 229 また、通常の計算を保存するようメタ計算を定義することで、例外処理などを含む計算に拡張することができる\cite{cite:monad}。 |
11 | 230 |
9 | 231 \section{メタ計算を用いたデータ構造の性質の検証} |
22
fca342b9dbd5
Add bibliographies
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
232 CbC で記述されたデータ構造と、データ構造に対する処理の性質を実際に検証する。 |
fca342b9dbd5
Add bibliographies
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
233 検証の対象として、当研究室で CbC を用いて開発している Gears OS \cite{cite:gears-os}における非破壊赤黒木を用いる。 |
13 | 234 赤黒木とは木構造を持ったデータ構造であり、各ノードに赤と黒の色を割り当て、その色を用いて木の高さのバランスを取る。 |
235 また、非破壊であるため木にデータを挿入、削除した際に過去の木は変更されない。 | |
236 非破壊赤黒木に求められる性質には、挿入したデータを参照できること、削除できること、値の更新ができること、操作を行なった後の木はバランスしていること、などが存在する。 | |
14 | 237 本論文では任意の順番で木に要素を挿入しても木がバランスしていることを検証する。 |
238 | |
239 まず、検証を行なうために満たすべき仕様を定義する。 | |
240 仕様はデータ構造が常に満たすべき論理式として表現し、CbC のコードで記述する。 | |
20 | 241 検証する仕様として、木を根から辿った際に最も長い経路は最も短い経路の高々2倍に収まることを CbC で定義する(Code\ref{src:specification})。 |
19 | 242 |
243 \begin{lstlisting}[label=src:specification, caption=s]% 木の高さの仕様記述] | |
244 | |
245 if (akashaInfo.maxHeight > | |
246 2*akashaInfo.minHeight) { | |
247 goto meta(context, ShowTrace); | |
248 } | |
249 | |
250 \end{lstlisting} | |
251 | |
23 | 252 Code\ref{src:specification}で定義した仕様に対し、挿入する値と順番の全ての組み合わせに対して確認していく。 |
14 | 253 また、仕様を満たさない反例が存在する場合はその具体的な組み合わせの値を出力する。 |
13 | 254 |
22
fca342b9dbd5
Add bibliographies
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
255 当研究室で開発している検証用メタ計算ライブラリ akasha と、C言語の有限モデルチェッカ cbmc\cite{cite:cbmc} を用いてこの仕様を検証した。 |
24 | 256 akasha では検証用の仕様と検証用の処理をMeta Code Segmentに定義する。 |
23 | 257 挿入順の数え上げには深さ優先探索を用いる。 |
24 | 258 CbCには関数呼び出しが存在しないため、深さ優先探索を行なう際にスタックフレームに相当するMeta Data Segmentを自ら用意する。 |
23 | 259 各深さ毎の木を保存しておくことで、ある深さまでの探索が終了した際に木を再現ことができ、高速に探索を行なうことができる。 |
22
fca342b9dbd5
Add bibliographies
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
260 要素数13個までは任意の順で挿入を行なっても仕様が満たされることをakasha を用いて検証した。 |
23 | 261 また、赤黒木の処理内部にバグを追加した際にはakashaは反例を返した。 |
14 | 262 |
23 | 263 同じ仕様をC言語の有限モデルチェッカcbmcで検証する。 |
21 | 264 CbCは C とほぼ同様の構文を持つため、単純な置換でC言語に変換することができる。 |
23 | 265 CbCで記述された赤黒木のコードを置換でC言語に変換し、cbmcで検証を行なった。 |
266 cbmc における仕様は bool を返すコードとして記述するため、akashaと同じ仕様定義を用いることが可能である。 | |
24 | 267 また、ポインタへの不正アクセスといった一般的なバグへの検証コードが機能として存在する。 |
23 | 268 挿入順の数え上げにはcbmcの機能に存在する非決定的な入力を用いた。 |
269 しかし、cbmcで検証できる範囲内ではGearsの赤黒木の仕様を検証することはできなかった。 | |
270 有限モデルチェッカでは探索する状態空間を指定し、それを越える範囲は探索しない。 | |
14 | 271 cbmcで実行可能な最大の状態空間まで探索しても、バグを含んだ赤黒木に対する反例を得ることはできなかった。 |
13 | 272 |
23 | 273 よって、cbmcでは検証できない範囲の検証をakashaで行なうことが確認できた。 |
274 | |
9 | 275 \section{まとめと今後の課題} |
23 | 276 CbC で記述したプログラムに対する仕様の検証を行なうことができた。 |
24 | 277 CbC はCode SegmentとData Segmentを用いてプログラミングするため、検証用にコードを変更することなくメタ計算の切り替えで検証を行なうことができた。 |
15 | 278 |
279 今後の課題として、検証できる範囲の拡大や効率化、値の抽象化などがある。 | |
24 | 280 cbmcではポインタへの不正アクセスを行なう実行例を検出することができる。 |
281 akashaでも一般的なエラーに対するメタ計算などを定義したい。 | |
15 | 282 本論文では入力の組み合わせを全探索するため、過去に探索した形状の木に対しても探索を行なっていた。 |
283 木の形状を抽象化することで探索範囲を抑えて高速に検証ができると思われる。 | |
284 また、抽象度を上げることで有限回でなく無限回の操作も扱いたい。 | |
285 さらに、検証の際に証明を併用することで抽象化や状態数の削減が行なえると考えている。 | |
9 | 286 |
287 \begin{thebibliography}{9} | |
288 | |
22
fca342b9dbd5
Add bibliographies
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
289 \bibitem{cite:cbc-clang} 徳森海斗, 河野真治: Continuation based CのLLVM/clang 3.5上の実装について, 情報処理学会システムソフトウェアとオペレーティング・システム研究会 (OS) (2014) |
fca342b9dbd5
Add bibliographies
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
290 \bibitem{cite:gears-os} 伊波立樹, 東恩納琢偉, 河野真治: Code Gear、 Data Gear に基づく OS のプロトタイプ, 情報処理学会システムソフトウェアとオペレーティング・システム研究会 (OS) (2016) |
fca342b9dbd5
Add bibliographies
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
291 \bibitem{cite:cbmc} Clarke, Edmund and Kroening, Daniel and Lerda, Flavio: A Tool for Checking {ANSI-C} Programs, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004) |
fca342b9dbd5
Add bibliographies
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
292 \bibitem{cite:agda} \verb/The Agda Wiki - Agda/ \urlj{http://wiki.portal.chalmers.se/agda/pmwiki.php} \refdatej{2016-07-05}. |
fca342b9dbd5
Add bibliographies
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
21
diff
changeset
|
293 \bibitem{cite:monad} Moggi, Eugenio: Notions of Computation and Monads, Inf. Comput (1991). |
9 | 294 |
295 \end{thebibliography} | |
296 | |
20 | 297 \begin{biography} |
298 \profile{n}{比嘉健太}{2015年琉球大学工学部情報工学科卒業。2015年琉球大学大学院理工学研究科情報工学専攻入学。} | |
12 | 299 % TODO: update |
20 | 300 \profile{n}{河野真治}{1960年生.1982年情報処理大学理学部情報科学科卒業. |
9 | 301 1984年同大学大学院修士課程修了.1987年同博士課程修了.理学博士.1987年情報処 |
302 理大学助手.1992年架空大学助教授.1997年同大教授.オンライン出版の研究 | |
303 に従事.2010年情報処理記念賞受賞.電子情報通信学会,IEEE,IEEE-CS,ACM | |
304 各会員.} | |
305 \end{biography} | |
306 | |
307 | |
308 | |
309 \end{document} |