|
9
|
1 \documentclass[submit,PRO]{ipsj}
|
|
|
2 \usepackage{PROpresentation}
|
|
|
3 \PROheadtitle{y-n-(x): 情報処理学会プログラミング研究会 発表資料 Y年m月d日}
|
|
|
4
|
|
|
5 \usepackage{graphicx}
|
|
|
6 \usepackage{latexsym}
|
|
|
7
|
|
|
8 \def\Underline{\setbox0\hbox\bgroup\let\\\endUnderline}
|
|
|
9 \def\endUnderline{\vphantom{y}\egroup\smash{\underline{\box0}}\\}
|
|
|
10 \def\|{\verb|}
|
|
|
11
|
|
|
12 \setcounter{巻数}{57}
|
|
|
13 \setcounter{号数}{1}
|
|
|
14 \setcounter{page}{1}
|
|
|
15
|
|
|
16
|
|
|
17 \受付{2015}{3}{4}
|
|
|
18 %\再受付{2015}{7}{16} %省略可能
|
|
|
19 %\再再受付{2015}{7}{20} %省略可能
|
|
|
20 \採録{2015}{8}{1}
|
|
|
21
|
|
|
22
|
|
|
23
|
|
|
24
|
|
|
25 \begin{document}
|
|
|
26
|
|
|
27
|
|
|
28 \title{Continuation based C を用いたプログラムの検証手法}
|
|
|
29 \etitle{Verification method of programs using Continuation based C}
|
|
|
30
|
|
|
31 \affiliate{RUnivIe}{琉球大学 大学院 理工学研究科 情報工学専攻\\
|
|
|
32 Infomation Engineering Course Graduate School of Engineering and Science University of the Ryukyus}
|
|
|
33 \affiliate{RUniv}{琉球大学\\
|
|
|
34 University of the Ryukyus}
|
|
|
35
|
|
|
36
|
|
|
37 \author{比嘉 健太}{Yasutaka HIGA}{RUnivIe}[atton@cr.ie.u-ryukyu.ac.jp]
|
|
|
38 \author{河野 真治}{Shinji KONO}{RUniv}[kono@ie.u-ryukyu.ac.jp]
|
|
|
39
|
|
|
40 \begin{abstract}
|
|
12
|
41 % TODO: update
|
|
9
|
42 Continuation based C 言語によって記述されたプログラムのデータ構造の性質を検証する手法を提案する。
|
|
|
43 Continuation based C とは当研究室が提案している Code Segment, Data Segment という単位でプログラムを記述する言語である。
|
|
|
44 Code Segment とは処理の単位であり、データの単位である Data Segment を入力と出力に持つ。
|
|
|
45 プログラム全体は Code Segment どうしの接続により表現され、あるCode Segment の出力は接続された次の Code Segment の入力となる。
|
|
|
46 また、メモリ管理やエラーの処理など、本来中心に行ないたい処理と異なる処理はメタ計算として分離し、Meta Code Segment, Meta Data Segment として記述する。
|
|
|
47 Code Segment の接続処理を Meta Code Segment として表現し、接続部分に検証を含めることで 元の Code Segment を変更することなくプログラムの検証を行なう。
|
|
|
48 本論文では Continuatoin based C によって記述された赤黒木や Synchronized Queue といったデータ構造の性質を検証する。
|
|
|
49 \end{abstract}
|
|
|
50
|
|
|
51
|
|
|
52 \begin{jkeyword}
|
|
|
53 プログラミング言語, 検証, 赤黒木
|
|
|
54 \end{jkeyword}
|
|
|
55
|
|
|
56 \begin{eabstract}
|
|
12
|
57 % TODO: update
|
|
9
|
58 We propose a verification method for programs using Continuation based C language.
|
|
|
59 Our laboratory develops Continuation based C language which supports programming unit called Code Segment, Data Segment.
|
|
|
60 Code segments are calculation units which have input/output data segments that data unit.
|
|
|
61 Programs are represented by connections among with code segments and code segments.
|
|
|
62 The output data segment of some code segment is converted to the input data segment of connected one.
|
|
|
63 We introduce meta computations which split main computations and complicated computations such as memory control, error handling and more.
|
|
|
64 Meta computations represented to meta code segment and meta data segment, which saves main computations.
|
|
|
65 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.
|
|
|
66 \end{eabstract}
|
|
|
67
|
|
|
68 \begin{ekeyword}
|
|
|
69 Programming Language, Verification, Red-Black Tree
|
|
|
70 \end{ekeyword}
|
|
|
71
|
|
|
72 \maketitle
|
|
|
73
|
|
|
74 \section{コードセグメントとデータセグメント}
|
|
10
|
75 本研究は実際に動作するプログラムの信頼性を保証することを目的とする。
|
|
|
76 プログラムの信頼性とは、定められた環境下においてプログラムの動作が必ず仕様を満たすことである。
|
|
|
77 プログラムが仕様を満たすことを保証する手法として、プログラムの性質を証明する手法やプログラムの状態を全て数えあげるモデルチェッカなどが存在する。 % TODO ref
|
|
|
78 しかし、証明では実際に動作するコードでなく証明用にコードを書き直したり、モデルチェッカでは高速化のために抽象化した記号実行によって性質が検証されるなど、実際に動作するコードとの乖離が発生してしまう。
|
|
|
79
|
|
|
80 実際に動作するコードを検証しやすいよう、本研究室ではコードセグメントとデータセグメントを用いるプログラミングスタイルを提案している。 % TODO ref?
|
|
|
81 コードセグメントとは処理の単位であり、ループを含まない単純な処理のみを行なう。
|
|
|
82 プログラムはコードセグメントどうしを組み合わせることにより構築される。
|
|
|
83 組み合わせる際のコードセグメント間における値の受け渡しにはデータセグメントを用いる。
|
|
|
84 データセグメントとはデータの単位である。
|
|
|
85 なお、接続されたコードセグメントには依存関係が発生するが、依存関係が無いコードセグメントは並列に実行することが可能である。
|
|
|
86
|
|
|
87 % TODO cs/ds の図
|
|
|
88
|
|
|
89 ここで、コードセグメントどうしの接続処理について考える。
|
|
|
90 処理を表すコードセグメントの接続も処理であるため、コードセグメントで表現できる。
|
|
|
91 このように、計算を実現するための計算をメタ計算と呼び、メタ計算を行なうコードセグメントをメタコードセグメントと呼ぶ。
|
|
|
92 メタコードセグメントはコードセグメント間に存在する処理と考えることもできる。
|
|
|
93 また、メタ計算に必要なデータはメタデータセグメントに格納する。
|
|
|
94 プログラムの性質を検証する機能をメタ計算として提供することで、ユーザが書いたコードセグメントを変更することなく、メタコードセグメントを切り替えるだけでプログラムの信頼性を上げることができる。
|
|
|
95
|
|
9
|
96 \section{Continuation based C}
|
|
11
|
97 コードセグメントとデータセグメントを用いたプログラミングスタイルで記述言語に Continuation based C 言語が存在する。 % TODO ref
|
|
|
98 Continuation based C (以下 CbC)はOSや組込みシステムなどの記述を行なうことを目標に作られた、アセンブラとC言語の中間のような言語である。 % TODO 要出典
|
|
|
99 CbC におけるコードセグメントはC言語における関数に、関数呼び出しが末尾のみである制約を加えようなものである。
|
|
|
100 コードセグメントどうしの接続は goto によって表される。
|
|
|
101
|
|
|
102 % TODO: かんたんな goto program
|
|
|
103
|
|
|
104 また、データセグメントは構造体と共用体を用いたデータ構造を用いる。
|
|
|
105
|
|
|
106 CbC におけるメタコードセグメントは goto する際に必ず通るコードセグメント(以下の例では \verb/meta/ がそれにあたる)として表現される。
|
|
|
107
|
|
|
108 % TODO: meta を使った program
|
|
|
109 メタコードセグメントの切り替えは \verb/meta/ の切り替えで表現できる。
|
|
|
110 メタデータセグメントはデータセグメントをフィールドに持つ構造体として表現できる。
|
|
|
111
|
|
14
|
112 CbC におけるメタ計算の例にメモリ管理がある。
|
|
|
113 メモリの確保やポインタ演算をメタコードセグメントのみで行なうことで、コードセグメント側ではメモリに由来するエラーを排除することができる。
|
|
11
|
114 また、メタ計算を切り替えることでメモリの管理方法も切り替えることができるため、不要な領域の開放するよう拡張することも容易である。
|
|
|
115
|
|
9
|
116 \section{メタ計算を用いたデータ構造の性質の検証}
|
|
14
|
117 CbC で記述されさデータ構造と、データ構造に対する処理の性質を実際に検証する。
|
|
13
|
118 検証の対象として、当研究室で CbC を用いて開発している Gears OS における非破壊赤黒木を用いる。
|
|
|
119 赤黒木とは木構造を持ったデータ構造であり、各ノードに赤と黒の色を割り当て、その色を用いて木の高さのバランスを取る。
|
|
|
120 また、非破壊であるため木にデータを挿入、削除した際に過去の木は変更されない。
|
|
|
121 非破壊赤黒木に求められる性質には、挿入したデータを参照できること、削除できること、値の更新ができること、操作を行なった後の木はバランスしていること、などが存在する。
|
|
14
|
122 本論文では任意の順番で木に要素を挿入しても木がバランスしていることを検証する。
|
|
|
123
|
|
|
124 まず、検証を行なうために満たすべき仕様を定義する。
|
|
|
125 仕様はデータ構造が常に満たすべき論理式として表現し、CbC のコードで記述する。
|
|
|
126 検証する仕様として、木を根から辿った際に最も長い経路は最も短い経路の高々2倍に収まることを CbC で定義する。
|
|
|
127 % TODO code
|
|
|
128 定義した仕様に対し、挿入する値と順番の全ての組み合わせに対して確認していく。
|
|
|
129 また、仕様を満たさない反例が存在する場合はその具体的な組み合わせの値を出力する。
|
|
13
|
130
|
|
14
|
131 当研究室で開発している検証用メタ計算ライブラリ akasha と、C言語の有限モデルチェッカ cbmc を用いてこの仕様を検証した。
|
|
|
132 akasha では検証用の仕様をメタコードセグメントに定義する。
|
|
|
133 検証に必要な木の状態の保持や挿入順番の数え上げといった状態の保持はメタデータセグメントが行なう。
|
|
|
134 akasha を用いて要素数12個までは任意の順で挿入を行なっても仕様が満たされることを検証した。 % todo: だっけか
|
|
|
135 また、赤黒木の処理に恣意的にバグを追加した際には反例をきちんとと返した。
|
|
|
136
|
|
|
137 CbCは C とほぼ同じ構文を持つため、単純な置換でC言語に変換することができる。
|
|
|
138 CbCで記述された赤黒木のコードを置換でC言語に変換し、cbmcで検証する。
|
|
|
139 cbmc における仕様は bool を返すコードとして記述するため、akashaと同じ仕様定義を用いることができる。
|
|
|
140 任意の順番での挿入の検証にはcbmcの機能に存在する非決定的な入力を用いた。
|
|
|
141 しかし、cbmcで検証できる範囲内では赤黒木の仕様を検証することはできなかった。
|
|
|
142 有限モデルチェッカでは探索する状態空間を有限の数で指定し、それを越える範囲は探索しない。
|
|
|
143 cbmcで実行可能な最大の状態空間まで探索しても、バグを含んだ赤黒木に対する反例を得ることはできなかった。
|
|
13
|
144
|
|
9
|
145 \section{まとめと今後の課題}
|
|
14
|
146 % unbounded にする
|
|
|
147 % 状態の抽象化
|
|
|
148 % 証明を使った空間削減
|
|
9
|
149
|
|
|
150 \begin{thebibliography}{9}
|
|
|
151 \bibitem{okumura}
|
|
|
152 奥村晴彦：改訂第5版 \LaTeXe 美文書作成入門，
|
|
|
153 技術評論社(2010).
|
|
|
154
|
|
|
155 \bibitem{companion}
|
|
|
156 Goossens, M., Mittelbach, F. and Samarin, A.: {\it The LaTeX Companion},
|
|
|
157 Addison Wesley, Reading, Massachusetts (1993).
|
|
|
158
|
|
|
159 \bibitem{book1}
|
|
|
160 木下是雄：
|
|
|
161 理科系の作文技術，
|
|
|
162 中公新書(1981).
|
|
|
163
|
|
|
164 \bibitem{book2}
|
|
|
165 Strunk, W.J. and White, E.B.: {\it The Elements of Style, Forth Edition},
|
|
|
166 Longman (2000).
|
|
|
167
|
|
|
168 \bibitem{book3}
|
|
|
169 Blake, G. and Bly, R.W.: {\it The Elements of Technical Writing},
|
|
|
170 Longman (1993).
|
|
|
171
|
|
|
172 \bibitem{book4}
|
|
|
173 Higham, N.J.:
|
|
|
174 {\it Handbook of Writing for the Mathematical Sciences},
|
|
|
175 SIAM (1998).
|
|
|
176
|
|
|
177 \bibitem{webpage1}
|
|
|
178 情報処理学会論文誌ジャーナル編集委員会：
|
|
|
179 投稿者マニュアル(オンライン)，
|
|
|
180 \urlj{http://www.ipsj.or.jp/journal/ submit/manual/j\_manual.html}%
|
|
|
181 \refdatej{2007-04-05}.
|
|
|
182
|
|
|
183 \bibitem{webpage2}
|
|
|
184 情報処理学会論文誌ジャーナル編集委員会：
|
|
|
185 べからず集(オンライン)，
|
|
|
186 \urlj{http://www.ipsj.or.jp/journal/\\ manual/bekarazu.html}%
|
|
|
187 \refdatej{2011-09-15}.
|
|
|
188
|
|
|
189 \end{thebibliography}
|
|
|
190
|
|
12
|
191 % TODO: update
|
|
9
|
192 \begin{biography}
|
|
|
193 \profile{m,E}{情報 太郎}{1970年生．1992年情報処理大学理学部情報科学科卒業．
|
|
|
194 1994年同大学大学院修士課程修了．同年情報処理学会入社．オンライン出版の研究
|
|
|
195 に従事．電子情報通信学会，IEEE，ACM 各会員．}
|
|
|
196 %
|
|
|
197 \profile{n}{処理 花子}{1960年生．1982年情報処理大学理学部情報科学科卒業．
|
|
|
198 1984年同大学大学院修士課程修了．1987年同博士課程修了．理学博士．1987年情報処
|
|
|
199 理大学助手．1992年架空大学助教授．1997年同大教授．オンライン出版の研究
|
|
|
200 に従事．2010年情報処理記念賞受賞．電子情報通信学会，IEEE，IEEE-CS，ACM
|
|
|
201 各会員．}
|
|
|
202 %
|
|
|
203 \profile{h,L}{学会 次郎}{1950年生．1974年架空大学大学院修士課程修了．
|
|
|
204 1987年同博士課程修了．工学博士．1977年架空大学助手．1992年情報処理大学助
|
|
|
205 教授．1987年同大教授．2000年から情報処理学会顧問．オンライン出版の研究
|
|
|
206 に従事．2010年情報処理記念賞受賞．情報処理学会理事．電子情報通信学会，
|
|
|
207 IEEE，IEEE-CS，ACM 各会員．}
|
|
|
208 \end{biography}
|
|
|
209
|
|
|
210
|
|
|
211
|
|
|
212 \end{document}
|
