Mercurial > hg > Papers > 2018 > nozomi-master
annotate paper/cbc.tex @ 74:e9ff08a232f7
Add references
| author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 06 Feb 2017 16:13:14 +0900 |
| parents | 45d3ac176bf5 |
| children | a9ed6a6dc1f2 |
| rev | line source |
|---|---|
| 12 | 1 \chapter{Continuation based C} |
| 22 | 2 \label{chapter:cbc} |
| 12 | 3 |
| 4 Continuation based C (CbC)は当研究室で開発しているプログラミング言語であり、OSや組み込みソフトウェアの開発を主な対象としている。 | |
| 13 | 5 CbC は C言語の下位の言語であり、構文はほぼC言語と同じものを持つが、よりアセンブラに近い形でプログラムを記述する。 |
| 12 | 6 CbC は CodeSegment と呼ばれる単位で処理を定義し、それらを組み合わせることにでプログラム全体を構成する。 |
| 7 データの単位は DataSegment と呼ばれる単位で定義し、それら CodeSegment によって変更していくことでプログラムの実行となる。 | |
| 8 CbC の処理系には llvm/clang による実装\cite{110009766999} と gcc\cite{weko_82695_1}による実装などが存在する。 | |
| 9 | |
| 13 | 10 % {{{ section: CodeSegment と DataSegment |
| 12 | 11 |
| 12 \section{CodeSegment と DataSegment} | |
| 13 本研究室では検証を行ないやすいプログラムの単位として CodeSegment と DataSegment を用いるプラグラミングスタイルを提案している。 | |
| 14 | |
| 15 CodeSegment は処理の単位である。 | |
| 16 入力を受け取り、それに対して処理を行なった後を出力を行なう。 | |
| 17 また、CodeSegment は他の CodeSegment と組み合わせることが可能である。 | |
| 18 あるCodeSegment A を CodeSegment B に接続した場合、 A の出力は B の入力となる。 | |
| 19 | |
| 20 % TODO: figure (cs A . cs B) | |
| 21 | |
| 22 DataSegment は CodeSegment が扱うデータの単位であり、処理に必要なデータが全て入っている。 | |
| 23 CodeSegment の入力となる DataSegment は Input DataSegment と呼ばれ、出力は Output DataSegment と呼ばれる。 | |
| 24 CodeSegment A と CodeSegment B を接続した時、A の Output DataSegment は B の入力 Input DataSegment となる。 | |
| 25 | |
| 26 % TODO: figure (cs A --(ds)--> cs B) | |
| 27 | |
| 13 | 28 % }}} |
| 12 | 29 |
| 15 | 30 % {{{ Continuation based C における CodeSegment と DataSegment |
| 31 | |
| 12 | 32 \section{Continuation based C における CodeSegment と DataSegment} |
|
14
6bf2e0196a1e
Add goto.cbc and goto.pdf
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
33 最も基本的な CbC のソースコードをリスト\ref{src:goto}に、ソースコードが実行される流れを図\ref{fig:goto}に示す。 |
| 13 | 34 Continuation based C における CodeSegment は返り値を持たない関数として表現される。 |
| 35 CodeSegment を定義するためには、C言語の関数を定義する構文の返り値の型部分に \verb/__code/ キーワードを指定する。 | |
| 36 Input DataSegment は関数の引数として定義される。 | |
| 37 次の CodeSegment へ処理を移す際には \verb/goto/ キーワードの後に CodeSegment 名と Input DataSegment を指定する。 | |
|
14
6bf2e0196a1e
Add goto.cbc and goto.pdf
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
38 処理の移動を軽量継続と呼び、リスト\ref{src:goto}内の \verb/goto cs1(a+b);/ がこれにあたる。 |
|
6bf2e0196a1e
Add goto.cbc and goto.pdf
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
39 この時の \verb/(a+b)/ が次の CodeSegment である cs1 の Input DataSegment となる cs0 の Output DataSegment である。 |
|
6bf2e0196a1e
Add goto.cbc and goto.pdf
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
40 |
|
6bf2e0196a1e
Add goto.cbc and goto.pdf
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
41 \lstinputlisting[label=src:goto, caption=CodeSegment の軽量継続] {src/goto.cbc} |
| 12 | 42 |
|
14
6bf2e0196a1e
Add goto.cbc and goto.pdf
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
43 \begin{figure}[htbp] |
|
6bf2e0196a1e
Add goto.cbc and goto.pdf
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
44 \begin{center} |
|
6bf2e0196a1e
Add goto.cbc and goto.pdf
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
45 \includegraphics[scale=1.0]{fig/goto.pdf} |
|
6bf2e0196a1e
Add goto.cbc and goto.pdf
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
46 \caption{CodeSegment の軽量継続} |
|
6bf2e0196a1e
Add goto.cbc and goto.pdf
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
47 \label{fig:goto} |
|
6bf2e0196a1e
Add goto.cbc and goto.pdf
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
48 \end{center} |
|
6bf2e0196a1e
Add goto.cbc and goto.pdf
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
49 \end{figure} |
| 13 | 50 |
| 51 % TODO: scheme ref? | |
| 52 Scheme などの call/cc といった継続はトップレベルから現在までの位置を環境として保持する。 | |
| 53 通常環境とは関数の呼び出しスタックの状態である。 | |
| 54 CbC の軽量継続は呼び出し元の情報を持たないため、スタックを破棄しながら処理を続けていく。 | |
|
14
6bf2e0196a1e
Add goto.cbc and goto.pdf
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
13
diff
changeset
|
55 よって、リスト\ref{src:goto} のプログラムでは cs0 から cs1 へと継続した後にcs0 へ戻ることはできない。 |
| 13 | 56 |
| 15 | 57 もう少し複雑な CbC のソースコードをリスト\ref{src:factrial}に、実行される流れを図\ref{fig:factrial}に示す。 |
| 58 このソースコードは整数の階乗を求めるプログラムである。 | |
| 59 CodeSegment factorial0 では自分自身への再帰的な継続を用いて階乗を計算している。 | |
| 60 軽量継続時には関数呼び出しのスタックは存在しないが、計算中の値を DataSegment で持つことで再帰を含むループ処理も行なうことができる。 | |
| 61 | |
| 62 \lstinputlisting[label=src:factrial, caption=階乗を求める CbC プログラム] {src/factrial.cbc} | |
| 13 | 63 |
| 15 | 64 \begin{figure}[htbp] |
| 65 \begin{center} | |
| 66 \includegraphics[scale=0.8]{fig/factorial.pdf} | |
| 67 \caption{階乗を求める CbC プログラム} | |
| 68 \label{fig:factrial} | |
| 69 \end{center} | |
| 70 \end{figure} | |
| 12 | 71 |
| 15 | 72 % }}} |
| 12 | 73 |
| 16 | 74 % {{{ MetaCodeSegment と MetaDataSegment |
| 75 | |
| 12 | 76 \section{MetaCodeSegment と MetaDataSegment} |
| 16 | 77 プログラムを記述する際、本来行ないたい計算の他にも記述しなければならない部分が存在する。 |
| 78 メモリの管理やネットワーク処理、エラーハンドリングや並列処理などがこれにあたり、本来行ないたい計算と区別してメタ計算と呼ぶ。 | |
| 79 プログラムを動作させるためにメタ計算部分は必須であり、しばしば本来の処理よりも複雑度が高い。 | |
| 80 | |
| 81 CodeSegment を用いたプログラミングスタイルでは計算とメタ計算を分離して記述する。 | |
| 82 分離した計算は階層構造を持ち、本来行ないたい処理をノーマルレベルとし、メタ計算はメタレベルとしてノーマルレベルよりも上の存在に位置する。 | |
| 83 複雑なメタ計算部分をライブラリやOS側が提供することで、ユーザはノーマルレベルの計算の記述に集中することができる。 | |
| 84 また、ノーマルレベルのプログラムに必要なメタ計算を追加することで、並列処理やネットワーク処理などを含むプログラムに拡張できる。 | |
| 85 さらに、ノーマルレベルからはメタレベルは隠蔽されているため、メタ計算の実装を切り替えることも可能である。 | |
| 86 例えば、並列処理のメタ計算用いたプログラムを作成する際、CPUで並列処理を行なうメタ計算とGPUで並列処理メタ計算を環境に応じて作成することができる。 | |
| 87 | |
| 88 なお、メタ計算を行なう CodeSegment は Meta CodeSegment と呼び、メタ計算に必要な DataSegment は Meta DataSegment と呼ぶ。 | |
| 89 Meta CodeSegment は CodeSegment の前後にメタ計算を挟むことで実現され、Meta DataSegment は DataSegment を含む上位の DataSegment として実現できる。 | |
| 90 よって、メタ計算は通常の計算を覆うように計算を拡張するものだと考えられる(図\ref{fig:meta})。 | |
| 91 | |
| 92 \begin{figure}[htbp] | |
| 93 \begin{center} | |
| 94 \includegraphics[scale=1.0]{fig/meta.pdf} | |
| 95 \caption{Meta CodeSegment と Meta DataSegment} | |
| 96 \label{fig:meta} | |
| 97 \end{center} | |
| 98 \end{figure} | |
| 99 | |
| 100 % }}} | |
| 101 | |
| 18 | 102 % {{{ Continuation based C におけるメタ計算の例: GearsOS |
| 17 | 103 \section{Continuation based C におけるメタ計算の例: GearsOS} |
| 104 CbC におけるメタ計算は軽量継続を行なう際に Meta CodeSegment を挟むことで実現できる。 | |
| 47 | 105 CbC を用いてメタ計算を実現した例として、GearsOS\cite{weko_142109_1}が存在する。 |
| 17 | 106 GearsOS とはマルチコアCPUやGPU環境での動作を対象としたOSであり、現在OSの設計と並列処理部分の実装が行なわれている。 |
| 47 | 107 GearsOS におけるメタ計算はMonadによって形式化されている\cite{Moggi:1991:NCM:116981.116984}。 |
| 17 | 108 現在存在するメタ計算としてメモリの確保と割り当て、並列に書き込むことが可能な Synchronized Queue、データの保存に用いる非破壊赤黒木がある。 |
| 12 | 109 |
| 17 | 110 GearsOS では CodeSegment と DataSegment はそれぞれ CodeGear と DataGear と呼ばれている。 |
| 74 | 111 マルチコアCPU環境では CodeGear と CodeSegment は同一だが、GPU 環境では CodeGear には OpenCL~\cite{opencl}/CUDA~\cite{cuda} における kernel も含まれる。 |
| 17 | 112 kernel とは GPU で実行される関数のことであり、GPU上のメモリに配置されたデータ群に対して並列に実行されるものである。 |
| 113 通常 GPU でデータの処理を行なう場合はデータの転送、転送終了を同期で確認、 kernel 実行、kernel の終了を同期で確認する、という手順が必要である。 | |
| 114 CPU/GPU での処理をメタ計算で行なうことにより、ノーマルレベルでは CodeGear が実行されるデバイスや DataGear の位置を意識する必要が無いというメリットがある。 | |
| 115 | |
| 18 | 116 GearsOS においては軽量継続の呼び出し部分もメタ計算として実現されている。 |
| 117 ある CodeGear から次の CodeGear へと継続する際には、次に実行される CodeGear の名前を指定する。 | |
| 118 その名前を Meta CodeGear が解釈し、対応する CodeGear へと処理を引き渡す。 | |
| 119 これは従来の OS の Dynamic Loading Libary や Command の呼び出しに相当する。 | |
| 120 CodeGear と名前の対応は Meta DataGear に格納されており、従来の OS の Process や Thread に相当する。 | |
| 121 | |
| 122 具体的には Meta DataGear には以下のようなものが格納される。 | |
| 123 | |
| 124 \begin{itemize} | |
| 125 \item DataGear の型情報 | |
| 126 \item DataGear を格納するメモリの情報 | |
| 127 \item CodeGear の名前と CodeGear の関数ポインタ との対応表 | |
| 128 \item CodeGear が参照する DataGear へのポインタ | |
| 129 \end{itemize} | |
| 130 | |
| 131 実際の GearsOS におけるメモリ管理を含むメタ計算用の Meta DataGear の定義例をリスト\ref{src:context}に示す。 | |
| 132 Meta DataGear は Context という名前の構造体で定義されている。 | |
| 133 | |
| 134 \lstinputlisting[label=src:context, caption=GearsOS における Meta DataGearの定義例] {src/context.h} | |
| 135 | |
| 136 \begin{itemize} | |
| 137 \item DataGear の型情報 | |
| 138 | |
| 139 DataGear は構造体を用いて定義する(リスト\ref{src:context} 27-46行)。 | |
| 140 Tree や Node、 Allocate 構造体が DataGear に相当する。 | |
| 141 メタ計算は任意の DataGear 扱うために全ての DataGear を扱える必要がある。 | |
| 142 全ての DataGear の共用体を定義することで、 DataGear を一律に扱うことができる(リスト\ref{src:context} 26-47行)。 | |
| 143 メモリを確保する場合はこの型情報からサイズを決定する。 | |
| 144 | |
| 145 \item DataGear を格納するメモリの情報 | |
| 146 | |
| 147 メモリ領域の管理は、事前に領域を確保した後、必要に応じてその領域を割り当てることで実現する。 | |
| 148 そのために Context は割り当て済みの領域 heap と、割り当てた DataGear の数 dataNum を持つ。 | |
| 149 | |
| 150 \item CodeGear の名前と CodeGear の関数ポインタ との対応表 | |
| 151 | |
| 152 CodeGear の名前と CodeGear の関数ポインタの対応は enum と関数ポインタによって実現されている。 | |
| 153 CodeGear の名前は enum (リスト\ref{src:context} 5-9行) で定義され、コンパイル後には整数へと変換される。 | |
| 154 プログラム全体で利用する CodeGear は code フィールドに格納されており、enum を用いてアクセスする。 | |
| 155 この対応表を動的に変更することにより、実行時に比較ルーチンなどを変更することが可能になる。 | |
| 156 | |
| 157 | |
| 158 \item CodeGear が参照する DataGear へのポインタ | |
| 159 | |
| 160 Meta CodeGear は Context を引数に取る CodeGear として定義されている。 | |
| 161 そのため、Meta CodeGear が DataGear の値を使う為には Context から DataGear を取り出す必要がある。 | |
| 162 取り出す必要がある DataGear は enum を用いて定義し(リスト\ref{src:context} 11-14行)、 CodeGear を実行する際に data フィールドから取り出す。 | |
| 163 \end{itemize} | |
| 164 | |
| 19 | 165 なお、この Context から DataGear を取り出す Meta CodeSegment を stub と呼ぶ。 |
| 166 stub の例をリスト\ref{src:stub}に示す。 | |
| 167 stub は Context が持つ DataGear のポインタ data に対して enum を用いてアクセスしている。 | |
| 168 現在、この stub は全ての CodeGear に対してユーザが1つずつ定義する必要がある。 | |
| 169 この作業は非常に煩雑であり、CodeGear の定義から生成するスクリプトを用いて定義の簡易化を行なっているが、コンパイラ側でのサポートは入っていない。 | |
| 170 この stub を型情報から自動生成するために Continuation based C における型システムを定義する必要がある。 | |
| 171 | |
| 172 \lstinputlisting[label=src:stub, caption=GearsOS における stub Meta CodeSegment] {src/stub.cbc} | |
| 173 | |
| 18 | 174 % }}} |
| 175 | |
| 27 | 176 % {{{ GearsOS における非破壊赤黒木 |
| 177 | |
| 178 \section{GearsOS における非破壊赤黒木} | |
| 179 | |
| 24 | 180 現状の GearsOS に実装されているメタ計算として、非破壊赤黒木が存在する。 |
| 181 メタ計算として定義することにより、ノーマルレベルからは木のバランスを必要なく要素の挿入と探索、削除が行なえる。 | |
| 182 赤黒木とは二分探索木の一種であり、木の各ノードが赤と黒の色を持っている。 | |
| 183 木に対して要素の挿入や削除を行なった際、その色を用いて木のバランスを保つ。 | |
| 17 | 184 |
| 24 | 185 二分探索木の条件は以下である。 |
| 186 | |
| 187 \begin{itemize} | |
| 188 \item 左の子孫の値は親の値より小さい | |
| 189 \item 右の子孫の値は親の値より大きい | |
| 190 \end{itemize} | |
| 191 | |
| 192 加えて、赤黒木が持つ具体的な条件は以下のものである。 | |
| 193 | |
| 194 \begin{itemize} | |
| 195 \item 各ノードは赤か黒の色を持つ。 | |
| 196 \item ルートノードの色は黒である。 | |
| 197 \item 葉ノードの色は黒である。 | |
| 198 \item 赤ノードは2つの黒ノードを子として持つ(よって赤ノードが続くことは無い)。 | |
| 199 \item ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定である。 | |
| 200 \end{itemize} | |
| 201 | |
| 202 | |
| 203 数値を要素に持つ赤黒木の例を図\ref{fig:rbtree}に示す。 | |
| 204 ルートノードは黒であり、赤ノードは連続していない。 | |
| 205 加えて各最下位ノードへの経路に含まれる黒ノードの個数は全て2である。 | |
| 206 | |
| 207 \begin{figure}[htbp] | |
| 208 \begin{center} | |
| 209 \includegraphics[scale=0.5]{fig/rbtree.pdf} | |
| 210 \caption{赤黒木の例} | |
| 211 \label{fig:rbtree} | |
| 212 \end{center} | |
| 213 \end{figure} | |
| 214 | |
| 215 これらの条件より、木をルートから辿った際に最も長い経路は最も短い経路の高々二倍に収まる。 | |
| 216 | |
| 25 | 217 \newpage % for layout |
| 218 | |
| 24 | 219 GearsOS で実装されている赤黒木は特に非破壊赤黒木であり、一度構築した木構造は破壊される操作ごとに新しい木構造が生成される。 |
| 220 非破壊赤黒木の実装の基本的な戦略は、変更したいノードへのルートノードからの経路を全て複製し、変更後に新たなルートノードとする。 | |
| 221 この際に変更が行なわれていない部分は変更前の木と共有する(図\ref{fig:non-destructive-rbtree})。 | |
| 222 これは一度構築された木構造は破壊されないという非破壊の性質を用いたメモリ使用量の最適化である。 | |
| 223 | |
| 25 | 224 \begin{figure}[htbp] |
| 225 \begin{center} | |
| 226 \includegraphics[scale=0.5]{fig/non-destructive-rbtree} | |
| 227 \caption{非破壊赤黒木の編集} | |
| 228 \label{fig:non-destructive-rbtree} | |
| 229 \end{center} | |
| 230 \end{figure} | |
| 26 | 231 |
| 232 CbC を用いて赤黒木を実装する際の問題として、関数の呼び出しスタックが存在しないため、関数の再帰呼び出しによって木が辿れないことがある。 | |
| 233 経路を辿るためにはノードに親への参照を持たせるか、挿入・削除時に辿った経路を記憶する必要がある。 | |
| 234 ノードが親への参照を持つ非破壊木構造は共通部分の共有が行なえないため、辿った経路を記憶する方法を使う。 | |
| 235 経路の記憶にはスタックを用い、スタックは Meta DataSegment に保持させる。 | |
| 236 | |
| 237 赤黒木を格納する DataSegment と Meta DataSegment の定義をリスト\ref{src:rbtree-context}に示す。 | |
| 238 経路の記憶に用いるスタックは Meta DataSegment である Context 内部の \verb/node_stack/ である。 | |
| 239 DataSegment は各ノード情報を持つ \verb/Node/構造体と、赤黒木を格納する \verb/Tree/構造体、挿入などで操作中の一時的な木を格納する \verb/Traverse/共用体などがある。 | |
| 240 | |
| 241 \lstinputlisting[label=src:rbtree-context, caption=赤黒木の DataSegment と Meta DataSegment] {src/rbtreeContext.h} | |
| 242 | |
| 243 Meta DataSegment を初期化する Meta CodeSegment initLLRBContext をリスト\ref{src:init-rbtree-context}に示す。 | |
| 244 この Meta CodeSegment ではメモリ領域の確保、CodeSegment 名と CodeSegment の実体の対応表の作成などを行なう。 | |
| 245 メモリ領域はプログラムの起動時に一定数のメモリを確保し、ヒープとして \verb/heap/ フィールドに保持させる。 | |
| 246 CodeSegment 名と CodeSegment の実体との対応は、enum で定義された CodeSegment 名の添字へと CodeSegment の関数ポインタを代入することにより持つ。 | |
| 247 例えば \verb/Put/ の実体は \verb/put_stub/ である。 | |
| 248 他にも DataSegment の初期化(リスト\ref{src:init-rbtree-context} 34-48)とスタックの初期化(リスト\ref{src:init-rbtree-context} 50-51)を行なう。 | |
| 249 | |
| 250 \lstinputlisting[label=src:init-rbtree-context, caption=赤黒木の Meta DataSegment の初期化を行なう Meta CodeSegment ] {src/initLLRBContext.c} | |
| 251 | |
| 252 実際の赤黒木の実装に用いられている Meta CodeSegment の一例をリスト\ref{src:rbtree-insert-case-2}に示す。 | |
| 253 Meta CodeSegment \verb/insertCase2/ は要素を挿入した場合に呼ばれる Meta CodeSegment の一つであり、親ノードの色によって処理を変える。 | |
| 254 まず、色を確認するために経路を記憶しているスタックから親の情報を取り出す。 | |
| 255 親の色が黒ならば処理を終了し、次の CodeSegment へと軽量継続する(リスト\ref{src:rbtree-insert-case-2} 5-8)。 | |
| 256 親の色が赤であるならばさらに処理を続行して \verb/InsertCase3/ へと軽量継続する。 | |
| 257 ここで、経路情報を再現するためにスタックへと親を再代入してから軽量継続を行なっている。 | |
| 258 なお、Meta CodeSegment でも Context から DataSegment を展開する処理は stub によって行なわれる(リスト\ref{src:rbtree-insert-case-2} 14-16)。 | |
| 259 | |
| 260 \lstinputlisting[label=src:rbtree-insert-case-2, caption=赤黒木の実装に用いられている Meta CodeSegment例] {src/insertCase2.c} | |
| 261 | |
| 27 | 262 % }}} |
| 26 | 263 |
| 28 | 264 % {{{ メタ計算ライブラリ akasha を用いた赤黒木の実装の検証 |
| 265 | |
| 27 | 266 \section{メタ計算ライブラリ akasha を用いた赤黒木の実装の検証} |
| 267 GearsOS の赤黒木の仕様の定義とその確認を CbC で行なっていく。 | |
| 268 赤黒木には以下の性質が求められる。 | |
| 269 | |
| 270 \begin{itemize} | |
| 271 \item 挿入したデータは参照できること | |
| 272 \item 削除したデータは参照できないこと | |
| 273 \item 値を更新した後は更新された値が参照されること | |
| 274 \item 操作を行なった後の木はバランスしていること | |
| 275 \end{itemize} | |
| 276 | |
| 277 今回はバランスに関する仕様を確認する。 | |
| 278 操作を挿入に限定し、木にどのような順番で要素を挿入しても木がバランスすることを検証する。 | |
| 279 検証には当研究室で開発しているメタ計算ライブラリ akasha を用いる。 | |
| 280 akasha では仕様は常に成り立つべき CbC の条件式として定義される。 | |
| 281 具体的には Meta CodeSegment に定義した assert が仕様に相当する。 | |
| 282 仕様の例として、木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる、という木がバランスしている際に成り立つ式を定義する(リスト\ref{src:assert})。 | |
| 283 | |
| 284 \lstinputlisting[label=src:assert, caption=木の高さに関する仕様記述] {src/assert.c} | |
| 285 | |
| 286 リスト\ref{src:assert} で定義した仕様が常に成り立つか、全ての挿入順番を列挙しながら確認していく。 | |
| 287 まずは最も単純な有限の個数の任意の順の数え上げに対して検証していく。 | |
| 288 最初に検証の対象となる赤黒木と検証に必要な DataSegment を含む Meta DataSegment を定義する(リスト\ref{src:akasha-context})。 | |
| 289 DataSegment は データの挿入順を数え上げるためには使う環状リスト \verb/Iterator/ とその要素 \verb/IterElem/、検証に使う情報を保持する \verb/AkashaInfo/、木をなぞる際に使う \verb/AkashaNode/ がある。 | |
| 290 | |
| 291 \lstinputlisting[label=src:akasha-context, caption=検証を行なうための Meta DataSegment] {src/akashaContext.h} | |
| 292 | |
| 293 挿入順番の数え上げには環状リストを用いた深さ優先探索を用いる。 | |
| 294 最初に検証する要素を全て持つ環状リストを作成し、木に挿入した要素を除きながら環状リストを複製していく。 | |
| 295 環状リストが空になった時が組み合わせを一つ列挙し終えた状態となる。 | |
| 296 列挙し終えた後、前の深さの環状リストを再現してリストの先頭を進めることで異なる組み合わせを列挙する。 | |
| 297 | |
| 298 仕様には木の高さが含まれるので、高さを取得する Meta CodeSegment が必要となる。 | |
| 299 リスト\ref{src:get-min-height}に木の最も低い経路の長さを取得する Meta CodeSegment を示す。 | |
| 300 | |
| 301 木を辿るためのスタックに相当する \verb/AkshaNode/を用いて経路を保持しつつ、高さを確認している。 | |
| 302 スタックが空であれば全てのノードを確認したので次の CodeSegment へと軽量継続を行なう。 | |
| 303 空でなければ今辿っているノードが葉であるか確認し、葉ならば高さを更新して次のノードを確認するため自身へと軽量継続する。 | |
| 304 葉でなければ高さを1増やして左右の子をスタックに積み、自身へと軽量継続を行なう。 | |
| 305 | |
| 306 \lstinputlisting[label=src:get-min-height, caption=木の最も短かい経路の長さを確認する Meta CodeSegment] {src/getMinHeight.c} | |
| 307 | |
| 308 同様に最も高い高さを取得し、仕様であるリスト\ref{src:assert}の assert を挿入の度に実行する。 | |
| 28 | 309 assert は CodeSegment の結合を行なうメタ計算である \verb/meta/ を上書きすることにより実現する。 |
| 310 \verb/meta/ はリスト\ref{src:rbtree-insert-case-2}の \verb/insertCase2/ のように軽量継続を行なう際に CodeSegment 名と DataSegment を指定するものである。 | |
| 311 検証を行なわない通常の \verb/meta/ の実装は CodeSegment 名から対応する実体への軽量継続である(リスト\ref{src:meta})。 | |
| 27 | 312 |
| 28 | 313 \lstinputlisting[label=src:meta, caption=通常の CodeSegment の軽量継続] {src/meta.c} |
| 27 | 314 |
| 28 | 315 これを、検証を行なうように変更することで \verb/insertCase2/ といった赤黒木の実装のコードを修正することなく検証を行なうことができる。 |
| 316 検証を行ないながら軽量継続する \verb/meta/ はリスト\ref{src:akasha-meta}のように定義される。 | |
| 317 実際の検証部分は \verb/PutAndGoToNextDepth/ の後に行なわれるため、直接は記述されていない。 | |
| 318 この \verb/meta/ が行なうのは検証用にメモリの管理である。 | |
| 319 状態の数え上げを行なう際に状態を保存したり、元の状態に戻す処理が行なわれる。 | |
| 320 このメタ計算を用いた検証では、要素数13個までの任意の順で挿入の際に仕様が満たされることを確認できた。 | |
| 321 また、赤黒木の処理内部に恣意的なバグを追加した際には反例を返した。 | |
| 322 | |
| 323 \lstinputlisting[label=src:akasha-meta, caption=検証を行なう CodeSegment の軽量継続] {src/akashaMeta.c} | |
| 324 | |
| 325 % }}} |