Mercurial > hg > Papers > 2016 > atton-ipsjpro
annotate paper/vmpcbc.tex @ 21:879272af0acd
Add sample codes
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 05 Jul 2016 12:00:31 +0900 |
| parents | ea7b331f263a |
| children | fca342b9dbd5 |
| 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 | |
| 21 | 33 % TODO: コードセグメント, Code Segment の統一 |
| 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} | |
| 12 | 60 % TODO: update |
| 9 | 61 Continuation based C 言語によって記述されたプログラムのデータ構造の性質を検証する手法を提案する。 |
| 62 Continuation based C とは当研究室が提案している Code Segment, Data Segment という単位でプログラムを記述する言語である。 | |
| 63 Code Segment とは処理の単位であり、データの単位である Data Segment を入力と出力に持つ。 | |
| 64 プログラム全体は Code Segment どうしの接続により表現され、あるCode Segment の出力は接続された次の Code Segment の入力となる。 | |
| 65 また、メモリ管理やエラーの処理など、本来中心に行ないたい処理と異なる処理はメタ計算として分離し、Meta Code Segment, Meta Data Segment として記述する。 | |
| 66 Code Segment の接続処理を Meta Code Segment として表現し、接続部分に検証を含めることで 元の Code Segment を変更することなくプログラムの検証を行なう。 | |
| 67 本論文では Continuatoin based C によって記述された赤黒木や Synchronized Queue といったデータ構造の性質を検証する。 | |
| 68 \end{abstract} | |
| 69 | |
| 70 | |
| 71 \begin{jkeyword} | |
| 72 プログラミング言語, 検証, 赤黒木 | |
| 73 \end{jkeyword} | |
| 74 | |
| 75 \begin{eabstract} | |
| 12 | 76 % TODO: update |
| 9 | 77 We propose a verification method for programs using Continuation based C language. |
| 78 Our laboratory develops Continuation based C language which supports programming unit called Code Segment, Data Segment. | |
| 79 Code segments are calculation units which have input/output data segments that data unit. | |
| 80 Programs are represented by connections among with code segments and code segments. | |
| 81 The output data segment of some code segment is converted to the input data segment of connected one. | |
| 82 We introduce meta computations which split main computations and complicated computations such as memory control, error handling and more. | |
| 83 Meta computations represented to meta code segment and meta data segment, which saves main computations. | |
| 84 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 and Synchronized Queue. | |
| 85 \end{eabstract} | |
| 86 | |
| 87 \begin{ekeyword} | |
| 88 Programming Language, Verification, Red-Black Tree | |
| 89 \end{ekeyword} | |
| 90 | |
| 91 \maketitle | |
| 92 | |
| 93 \section{コードセグメントとデータセグメント} | |
| 10 | 94 本研究は実際に動作するプログラムの信頼性を保証することを目的とする。 |
| 95 プログラムの信頼性とは、定められた環境下においてプログラムの動作が必ず仕様を満たすことである。 | |
| 96 プログラムが仕様を満たすことを保証する手法として、プログラムの性質を証明する手法やプログラムの状態を全て数えあげるモデルチェッカなどが存在する。 % TODO ref | |
| 97 しかし、証明では実際に動作するコードでなく証明用にコードを書き直したり、モデルチェッカでは高速化のために抽象化した記号実行によって性質が検証されるなど、実際に動作するコードとの乖離が発生してしまう。 | |
| 98 | |
| 99 実際に動作するコードを検証しやすいよう、本研究室ではコードセグメントとデータセグメントを用いるプログラミングスタイルを提案している。 % TODO ref? | |
| 100 コードセグメントとは処理の単位であり、ループを含まない単純な処理のみを行なう。 | |
| 18 | 101 プログラムはコードセグメントどうしを組み合わせることにより構築される(図\ref{fig:csds})。 |
| 10 | 102 組み合わせる際のコードセグメント間における値の受け渡しにはデータセグメントを用いる。 |
| 103 データセグメントとはデータの単位である。 | |
| 104 なお、接続されたコードセグメントには依存関係が発生するが、依存関係が無いコードセグメントは並列に実行することが可能である。 | |
| 105 | |
| 18 | 106 \begin{figure} |
| 107 \begin{center} | |
| 108 \includegraphics[scale=0.5]{fig/code_segment_data_segment.pdf} | |
| 109 \caption{コードセグメントどうしの組み合わせ} | |
| 110 \label{fig:csds} | |
| 111 \end{center} | |
| 112 \end{figure} | |
| 10 | 113 |
| 114 ここで、コードセグメントどうしの接続処理について考える。 | |
| 21 | 115 処理を表すコードセグメントどうしの接続も処理であるため、コードセグメントで表現できる。 |
| 116 このような計算を実現するための計算をメタ計算と呼び、メタ計算を行なうコードセグメントをメタコードセグメントと呼ぶ。 | |
| 10 | 117 メタコードセグメントはコードセグメント間に存在する処理と考えることもできる。 |
| 118 また、メタ計算に必要なデータはメタデータセグメントに格納する。 | |
| 21 | 119 メタデータセグメントは通常の処理に必要なデータセグメントの拡張である。 |
| 120 プログラムの性質を検証する機能をメタ計算として提供することで、ユーザが書いたコードセグメントを変更することなく、メタ計算を追加するだけでプログラムの信頼性を上げる。 | |
| 10 | 121 |
| 9 | 122 \section{Continuation based C} |
|
17
84f71cc1764a
Add bibliographies
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
15
diff
changeset
|
123 コードセグメントとデータセグメントを用いたプログラミングスタイルで記述言語に Continuation based C\cite{cbc-clang} 言語が存在する。 |
|
84f71cc1764a
Add bibliographies
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
15
diff
changeset
|
124 Continuation based C (以下 CbC)はOSや組込みシステムなどの記述を行なうことを目標に作られた、アセンブラとC言語の中間のような言語である。 |
| 11 | 125 CbC におけるコードセグメントはC言語における関数に、関数呼び出しが末尾のみである制約を加えようなものである。 |
| 19 | 126 コードセグメントどうしの接続は goto によって表される(Code\ref{src:simpleCs})。 |
| 11 | 127 |
| 19 | 128 \begin{lstlisting}[label=src:simpleCs, caption=code]%コードセグメントの接続例 (10加算して2倍する)] |
| 21 | 129 __code addTen(int a) { |
| 130 int b = a+10; | |
| 131 goto twice(b); | |
| 19 | 132 } |
| 133 | |
| 134 __code twice(int x) { | |
| 135 int y = 2*x; | |
| 136 goto showValue(y); | |
| 137 } | |
| 138 \end{lstlisting} | |
| 11 | 139 |
| 21 | 140 CbCにおけるコードセグメントは、C言語の関数宣言の返り値の型の部分に \verb/__code/ を記述して定義する。 |
| 141 コードセグメント内部には変数の宣言やif文による分岐といったC言語の文法を用いて処理を記述する。 | |
| 142 次のコードセグメントへ接続する場合は \verb/goto/ を用いて接続先を指定する。 | |
| 143 Code\ref{src:simpleCs}の例では、2つのコードセグメント \verb/addTen/ と \verb/twice/を定義している。 | |
| 144 \verb/addTen/では int の値を受けとり、10加算して \verb/twice/ を実行する。 | |
| 145 \verb/twice/では受けとったintの値を2倍して \verb/showValue/ を実行する。 | |
| 146 | |
| 147 また、CbCにおけるデータセグメントはC言語における構造体と共用体を用いたデータ構造である。 | |
| 148 各コードセグメントで必要な値を構造体で定義し、それらの共用体としてデータセグメントを定義する(Code\ref{src:simpleDs})。 | |
| 149 | |
| 150 \begin{lstlisting}[label=src:simpleDs, caption=data]%データセグメントの例 (10加算して2倍する)] | |
| 151 | |
| 152 union Data { | |
| 153 struct Count { | |
| 154 int x; | |
| 155 } count; | |
| 156 struct Port { | |
| 157 unsigned int port; | |
| 158 } port; | |
| 159 }; | |
| 160 \end{lstlisting} | |
| 11 | 161 |
| 21 | 162 Code\ref{src:simpleDs}ではデータセグメントとして int を持つ count と unsigned int を持つ port の2つを定義している。 |
| 163 コードセグメントに\verb/goto/する際に利用するデータセグメントを指定することで、データセグメント内部の値で処理が行なえる。 | |
| 164 | |
| 165 \begin{lstlisting}[label=src:stub, caption=stub]%データセグメントの利用例 (countの値を2倍する)] | |
| 166 | |
| 167 __code addTen(union Data* ds, int a) { | |
| 168 int b = a+10; | |
| 169 goto twice_stub(ds); | |
| 170 } | |
| 171 | |
| 172 __code twice_stub(union Data* ds) { | |
| 173 goto twice(ds->count.x); | |
| 174 } | |
| 175 | |
| 176 __code twice(int x) { | |
| 177 int y = 2*x; | |
| 178 goto showValue(y); | |
| 179 } | |
| 180 \end{lstlisting} | |
| 181 | |
| 182 Code\ref{src:stub}では \verb/twice/ の際に2倍する値は count の値であることを \verb/twice_stub/ で指定している。 | |
| 183 CbC におけるメタコードセグメントはCode\ref{src:stub}や goto する際に必ず通るコードセグメント(Code\ref{src:meta}の \verb/meta/)のように表現される。 | |
| 19 | 184 |
| 185 \begin{lstlisting}[label=src:meta, caption=meta ] %メタコードセグメントを用いて接続した例] | |
| 186 | |
| 21 | 187 struct Context { |
| 188 union Data *data; | |
| 189 /* メタ計算に必要なデータ */ | |
| 190 }; | |
| 191 | |
| 19 | 192 __code meta(struct Context* context, |
| 193 enum Code next) { | |
| 11 | 194 |
| 19 | 195 /* 接続時に行なうメタ計算を記述 */ |
| 196 switch (next) { | |
| 197 case AddTen: | |
| 198 /* 特定のコードセグメントへのメタ計算 */ | |
| 21 | 199 goto addTen_stub(context); |
| 19 | 200 case Twice: |
| 21 | 201 goto twice_stub(context); |
| 19 | 202 } |
| 203 } | |
| 204 | |
| 21 | 205 __code addTen(struct Context* context, int a) { |
| 206 x = x+10; | |
| 19 | 207 goto meta(context, Twice); |
| 208 } | |
| 209 | |
| 21 | 210 __code twice(struct Context* context, int x) { |
| 211 x = x*2; | |
| 19 | 212 goto meta(context, ShowValue); |
| 21 | 213 } |
| 19 | 214 \end{lstlisting} |
| 215 | |
| 21 | 216 メタコードセグメントの切り替えは \verb/meta/ を変更することで実現できる。 |
| 217 また、メタデータセグメントに相当する \verb/Context/ はデータセグメントをフィールドに持つ構造体として表現できる。 | |
| 11 | 218 |
| 14 | 219 CbC におけるメタ計算の例にメモリ管理がある。 |
| 220 メモリの確保やポインタ演算をメタコードセグメントのみで行なうことで、コードセグメント側ではメモリに由来するエラーを排除することができる。 | |
| 11 | 221 また、メタ計算を切り替えることでメモリの管理方法も切り替えることができるため、不要な領域の開放するよう拡張することも容易である。 |
| 222 | |
| 9 | 223 \section{メタ計算を用いたデータ構造の性質の検証} |
| 14 | 224 CbC で記述されさデータ構造と、データ構造に対する処理の性質を実際に検証する。 |
|
17
84f71cc1764a
Add bibliographies
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
15
diff
changeset
|
225 検証の対象として、当研究室で CbC を用いて開発している Gears OS \cite{gears-os}における非破壊赤黒木を用いる。 |
| 13 | 226 赤黒木とは木構造を持ったデータ構造であり、各ノードに赤と黒の色を割り当て、その色を用いて木の高さのバランスを取る。 |
| 227 また、非破壊であるため木にデータを挿入、削除した際に過去の木は変更されない。 | |
| 228 非破壊赤黒木に求められる性質には、挿入したデータを参照できること、削除できること、値の更新ができること、操作を行なった後の木はバランスしていること、などが存在する。 | |
| 14 | 229 本論文では任意の順番で木に要素を挿入しても木がバランスしていることを検証する。 |
| 230 | |
| 231 まず、検証を行なうために満たすべき仕様を定義する。 | |
| 232 仕様はデータ構造が常に満たすべき論理式として表現し、CbC のコードで記述する。 | |
| 20 | 233 検証する仕様として、木を根から辿った際に最も長い経路は最も短い経路の高々2倍に収まることを CbC で定義する(Code\ref{src:specification})。 |
| 19 | 234 |
| 235 \begin{lstlisting}[label=src:specification, caption=s]% 木の高さの仕様記述] | |
| 236 | |
| 237 if (akashaInfo.maxHeight > | |
| 238 2*akashaInfo.minHeight) { | |
| 239 goto meta(context, ShowTrace); | |
| 240 } | |
| 241 | |
| 242 \end{lstlisting} | |
| 243 | |
| 14 | 244 定義した仕様に対し、挿入する値と順番の全ての組み合わせに対して確認していく。 |
| 245 また、仕様を満たさない反例が存在する場合はその具体的な組み合わせの値を出力する。 | |
| 13 | 246 |
| 14 | 247 当研究室で開発している検証用メタ計算ライブラリ akasha と、C言語の有限モデルチェッカ cbmc を用いてこの仕様を検証した。 |
| 248 akasha では検証用の仕様をメタコードセグメントに定義する。 | |
| 249 検証に必要な木の状態の保持や挿入順番の数え上げといった状態の保持はメタデータセグメントが行なう。 | |
|
17
84f71cc1764a
Add bibliographies
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
15
diff
changeset
|
250 akasha を用いて要素数13個までは任意の順で挿入を行なっても仕様が満たされることを検証した。 |
| 14 | 251 また、赤黒木の処理に恣意的にバグを追加した際には反例をきちんとと返した。 |
| 252 | |
| 21 | 253 CbCは C とほぼ同様の構文を持つため、単純な置換でC言語に変換することができる。 |
| 14 | 254 CbCで記述された赤黒木のコードを置換でC言語に変換し、cbmcで検証する。 |
| 255 cbmc における仕様は bool を返すコードとして記述するため、akashaと同じ仕様定義を用いることができる。 | |
| 256 任意の順番での挿入の検証にはcbmcの機能に存在する非決定的な入力を用いた。 | |
| 257 しかし、cbmcで検証できる範囲内では赤黒木の仕様を検証することはできなかった。 | |
| 258 有限モデルチェッカでは探索する状態空間を有限の数で指定し、それを越える範囲は探索しない。 | |
| 259 cbmcで実行可能な最大の状態空間まで探索しても、バグを含んだ赤黒木に対する反例を得ることはできなかった。 | |
| 13 | 260 |
| 9 | 261 \section{まとめと今後の課題} |
| 15 | 262 コードセグメントとデータセグメントを用いたプログラミング手法を用いる言語CbCで記述したプログラムに対する仕様の検証を行なうことができた。 |
| 263 メタ計算として検証を行なうことで、実際に動作するプログラムを全く変更することなくプログラムを検証した。 | |
| 264 | |
| 265 今後の課題として、検証できる範囲の拡大や効率化、値の抽象化などがある。 | |
| 266 本論文では入力の組み合わせを全探索するため、過去に探索した形状の木に対しても探索を行なっていた。 | |
| 267 木の形状を抽象化することで探索範囲を抑えて高速に検証ができると思われる。 | |
| 268 また、抽象度を上げることで有限回でなく無限回の操作も扱いたい。 | |
| 269 さらに、検証の際に証明を併用することで抽象化や状態数の削減が行なえると考えている。 | |
| 9 | 270 |
| 271 \begin{thebibliography}{9} | |
| 272 | |
|
17
84f71cc1764a
Add bibliographies
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
15
diff
changeset
|
273 \bibitem{cbc-clang} 徳森海斗, 河野真治: Continuation based CのLLVM/clang 3.5上の実装について, 情報処理学会システムソフトウェアとオペレーティング・システム研究会 (OS) (2014) |
|
84f71cc1764a
Add bibliographies
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
15
diff
changeset
|
274 \bibitem{gears-os} 伊波立樹, 東恩納琢偉, 河野真治: Code Gear、 Data Gear に基づく OS のプロトタイプ, 情報処理学会システムソフトウェアとオペレーティング・システム研究会 (OS) (2016) |
| 9 | 275 |
| 276 \end{thebibliography} | |
| 277 | |
| 20 | 278 \begin{biography} |
| 279 \profile{n}{比嘉健太}{2015年琉球大学工学部情報工学科卒業。2015年琉球大学大学院理工学研究科情報工学専攻入学。} | |
| 12 | 280 % TODO: update |
| 20 | 281 \profile{n}{河野真治}{1960年生．1982年情報処理大学理学部情報科学科卒業． |
| 9 | 282 1984年同大学大学院修士課程修了．1987年同博士課程修了．理学博士．1987年情報処 |
| 283 理大学助手．1992年架空大学助教授．1997年同大教授．オンライン出版の研究 | |
| 284 に従事．2010年情報処理記念賞受賞．電子情報通信学会，IEEE，IEEE-CS，ACM | |
| 285 各会員．} | |
| 286 \end{biography} | |
| 287 | |
| 288 | |
| 289 | |
| 290 \end{document} |