Mercurial > hg > Papers > 2018 > nozomi-master

comparison paper/akasha.tex @ 94:2bc816f4af27

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Thu, 09 Feb 2017 18:58:53 +0900
parents c407b7403548
children ebe838b83ada
comparison
equal deleted inserted replaced
93:16dc3337a5a9 94:2bc816f4af27
201 201
202 \begin{figure}[htbp] 202 \begin{figure}[htbp]
203 \begin{center} 203 \begin{center}
204 \includegraphics[width=300pt]{fig/akashaPut.pdf} 204 \includegraphics[width=300pt]{fig/akashaPut.pdf}
205 \caption{put を利用するプログラムのメタを上書きする} 205 \caption{put を利用するプログラムのメタを上書きする}
206 \label{fig:akahsaPut} 206 \label{fig:akashaPut}
207 \end{center} 207 \end{center}
208 \end{figure} 208 \end{figure}
209 209
210 \verb/meta/ はリスト\ref{src:rbtree-insert-case-2}の \verb/insertCase2/ のように軽量継続を行なう際に CodeSegment 名と DataSegment を指定するものである。 210 \verb/meta/ はリスト\ref{src:rbtree-insert-case-2}の \verb/insertCase2/ のように軽量継続を行なう際に CodeSegment 名と DataSegment を指定するものである。
211 検証を行なわない通常の \verb/meta/ の実装は CodeSegment 名から対応する実体への軽量継続である(リスト\ref{src:meta})。 211 検証を行なわない通常の \verb/meta/ の実装は CodeSegment 名から対応する実体への軽量継続であった(リスト\ref{src:default-meta})。
212 212
213 \lstinputlisting[label=src:meta, caption=通常の CodeSegment の軽量継続] {src/meta.c} 213 \lstinputlisting[label=src:default-meta, caption=通常の CodeSegment の軽量継続] {src/meta.c}
214 214
215 これを、検証を行なうように変更することで \verb/insertCase2/ といった赤黒木の実装のコードを修正することなく検証を行なうことができる。 215 これを、検証を行なうように変更することで \verb/insertCase2/ といった赤黒木の実装のコードを修正することなく検証を行なうことができる。
216 検証を行ないながら軽量継続する \verb/meta/ はリスト\ref{src:akasha-meta}のように定義される。 216 検証を行ないながら軽量継続する \verb/meta/ はリスト\ref{src:akasha-meta}のように定義される。
217 実際の検証部分は \verb/PutAndGoToNextDepth/ の後に行なわれるため、直接は記述されていない。 217 実際の検証部分は \verb/PutAndGoToNextDepth/ の後に行なわれるため、直接は記述されていない。
218 この \verb/meta/ が行なうのは検証用にメモリの管理である。 218 この \verb/meta/ が行なうのは検証用にメモリの管理である。
225 % }}} 225 % }}}
226 226
227 % {{{ モデル検査器 CBMC との比較 227 % {{{ モデル検査器 CBMC との比較
228 228
229 \section{モデル検査器 CBMC との比較} 229 \section{モデル検査器 CBMC との比較}
230 akasha の比較対象として、 C言語の有限モデルチェッカ CBMC\cite{cite:cbmc} を用いて赤黒木を検証した。 230 akasha の比較対象として、 C言語の有限モデルチェッカ CBMC\cite{cbmc} を用いて赤黒木を検証した。
231 CBMC は ANSI-C を記号実行し、仕様の否定となるような実行パターンが無いかを検証するツールである。 231 CBMC は ANSI-C を記号実行し、仕様の否定となるような実行パターンが無いかを検証するツールである。
232 232
233 比較のために全く同じ赤黒木のソースコードを用いたいが、CbCの構文は厳密にはCとは異なるために変換が必要である。 233 比較のために全く同じ赤黒木のソースコードを用いたいが、CbCの構文は厳密にはCとは異なるために変換が必要である。
234 具体的には、\verb/__code/ を \verb/void/ に、 \verb/goto/ を \verb/return/ に置換することで機械的にC言語に変換できる。 234 具体的には、\verb/__code/ を \verb/void/ に、 \verb/goto/ を \verb/return/ に置換することで機械的にC言語に変換できる。
235 235