# HG changeset patch # User atton # Date 1486529452 -32400 # Node ID a9ed6a6dc1f22b65b914548dff89a90aa197637f # Parent a3a9d56f71ec9231ffcc90f02cbab480720d05aa Add chapter akasha diff -r a3a9d56f71ec -r a9ed6a6dc1f2 paper/akasha.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/akasha.tex Wed Feb 08 13:50:52 2017 +0900 @@ -0,0 +1,206 @@ +\chapter{メタ計算ライブラリ akasha における検証} +\label{chapter:akasha} +第~\ref{chapter:cbc}章では Continuation based C 言語の概要と、CbC で記述された GearsOS について述べた。 +GearsOS の持つメタ計算として、モデル検査的なアプローチで CodeGear の仕様を検証していく。 + +% {{{ モデル検査 +\section{モデル検査} +モデル検査とは、ソフトウェアの全ての状態において仕様が満たされるかを確認するものである。 +このモデル検査を行なうソフトウェアをモデル検査器と呼ぶ。 +モデルは検査器は、仕様の定義と確認ができる。 +加えて、仕様を満たさない場合にはソフトウェアがどのような状態であったか反例を返す。 + +モデル検査器には Spin\cite{spin} やCBMC\cite{cbmc} などが存在する。 + +Spin は Promela と呼ばれる言語でモデルを記述し、その中に論理式として仕様を記述する。 +論理式は assert でモデルの内部に埋め込まれ、並列に実行してもその仕様が満たされるかをチェックする。 +また、Promela で記述されたモデルからC言語を生成することができる。 +しかし、Promela で記述されたモデルは元のC言語とはかなり異なる構文をしており、ユーザが記述する難易度が高い。 + +そこで、モデルを個別に記述せずに実装そのものを検査するアプローチがある。 +例えばモデル検査器 CBMC は C言語を直接検証できる。 +CBMC でも仕様は論理式で記述され、 assert と組み合わせる。 +C 言語の実行は通常の実行とは異なり、記号実行という形で実行される。 +プログラム上の変数は記号として処理され、\verb/a < b/ といった条件式により分岐が行なわれたのなら、その条件を持つ場合の経路、持たない場合の経路、と分岐していくのである。 + +GearsOS におけるモデル検査的なアプローチはCBMC のように実装言語をそのまま検証できるようにしたい。 +そのために、assert を利用した仕様の定義と、その検査、必要なら反例を提出するようなメタ計算を定義する。 +このメタ計算をメタ計算ライブラリ akasha として実装した。 + +この章では、メタ計算ライブラリ akasha を用いて GearsOS のデータ構造を検証していく。 +% }}} + +% {{{ GearsOS における非破壊赤黒木 +\section{GearsOS における非破壊赤黒木} +現状の GearsOS に実装されているメタ計算として、非破壊赤黒木が存在する。 +非破壊赤黒木はユーザがデータを保存する際に利用することを想定している。 +メタ計算として定義することで、ノーマルレベルからは木のバランスを考慮せず木への操作が行なえる。 + +なお、赤黒木とは二分探索木の一種であり、木のバランスを取るための情報として各ノードは赤か黒の色を持っている。 + +二分探索木の条件は以下である。 + +\begin{itemize} + \item 左の子孫の値は親の値より小さい + \item 右の子孫の値は親の値より大きい +\end{itemize} + +加えて、赤黒木が持つ具体的な条件は以下のものである。 + +\begin{itemize} + \item 各ノードは赤か黒の色を持つ。 + \item ルートノードの色は黒である。 + \item 葉ノードの色は黒である。 + \item 赤ノードは2つの黒ノードを子として持つ(よって赤ノードが続くことは無い)。 + \item ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定である。 +\end{itemize} + + +数値を要素に持つ赤黒木の例を図\ref{fig:rbtree}に示す。 +条件に示されている通り、ルートノードは黒であり、赤ノードは連続していない。 +加えて各最下位ノードへの経路に含まれる黒ノードの個数は全て2である。 + +\begin{figure}[htbp] + \begin{center} + \includegraphics[scale=0.5]{fig/rbtree.pdf} + \caption{赤黒木の例} + \label{fig:rbtree} + \end{center} +\end{figure} + +赤黒木の持つ条件を言い変えるのなら、「木をルートから辿った際に最も長い経路は最も短い経路の高々二倍に収まる」とも言える。 +この言い換えは「赤が続くことはない」という条件と「ルートから最下位への経路の黒ノードはどの最下位ノードでも同じ」であることから導ける。 +具体的には、最短経路は「黒のみの経路」であり、最長経路は「黒と赤が交互に続く経路」となる。 +この条件を言い変えた性質を仕様とし、検証していく。 + +GearsOS で実装されている赤黒木は特に非破壊赤黒木であり、一度構築した木構造は破壊される操作ごとに新しい木構造が生成される。 +非破壊の性質を付与した理由として、並列実行時のデータの保存がある。 +同じ赤黒木をロックせずに同時に更新した場合、ノードの値は実行順に依存したり、競合したりする。 +しかし、ロックを行なって更新した場合は同じ木に対する処理に待ち合わせが発生し、全体の並列度が下がる。 +この問題に対し GearsOS では、各スレッドは処理を行なう際には非破壊の木を利用することで並列度は保ち、値の更新が発生する時のみ木をアトミックな操作で置き換えることで競合を回避する。 +具体的には木の操作を行なった後はルートのノードを元に CAS で置き換え、失敗した時は木を読み込み直して処理を再実行する。 +CAS(Check and Set) とは、アトミックに値を置き換える操作であり、使う際は更新前の値と更新後の値を渡す。 +CAS で渡された更新前の値が、保存している値と同じであれば競合していないために値の更新に成功し、異なる場合は他に書き込みがあったことを示すために値の更新が失敗する操作のことである。 + +非破壊赤黒木の実装の基本的な戦略は、変更したいノードへのルートノードからの経路を全て複製し、変更後に新たなルートノードとする。 +この際に変更が行なわれていない部分は変更前の木と共有する(図\ref{fig:non-destructive-rbtree})。 +これは一度構築された木構造は破壊されないという非破壊の性質を用いたメモリ使用量の最適化である。 + +\begin{figure}[htbp] + \begin{center} + \includegraphics[scale=0.5]{fig/non-destructive-rbtree} + \caption{非破壊赤黒木の編集} + \label{fig:non-destructive-rbtree} + \end{center} +\end{figure} + +CbC を用いて赤黒木を実装する際の問題として、関数の呼び出しスタックが存在しないことがある。 +C における実装では関数の再帰呼び出しによって木が辿るが、それが行なえない。 +経路を辿るためには、ノードに親への参照を持たせるか、挿入や削除の際に辿った経路を記憶する必要がある。 +ノードが親への参照を持つ非破壊木構造は共通部分の共有が行なえないため、経路を記憶する方法を使う。 +経路の記憶にはスタックを用い、スタックは Meta DataSegment に保持する。 + +赤黒木を格納する DataSegment と Meta DataSegment の定義をリスト\ref{src:rbtree-context}に示す。 +経路の記憶に用いるスタックは Meta DataSegment である Context 内部の \verb/node_stack/ である。 +DataSegment は各ノード情報を持つ \verb/Node/構造体と、赤黒木を格納する \verb/Tree/構造体、挿入などで操作中の一時的な木を格納する \verb/Traverse/共用体などがある。 + +\lstinputlisting[label=src:rbtree-context, caption=赤黒木の DataSegment と Meta DataSegment] {src/rbtreeContext.h} + +Meta DataSegment を初期化する Meta CodeSegment initLLRBContext をリスト\ref{src:init-rbtree-context}に示す。 +この Meta CodeSegment ではメモリ領域の確保、CodeSegment 名と CodeSegment の実体の対応表の作成などを行なう。 +メモリ領域はプログラムの起動時に一定数のメモリを確保し、ヒープとして \verb/heap/ フィールドに保持させる。 +CodeSegment 名と CodeSegment の実体との対応は、enum で定義された CodeSegment 名の添字へと CodeSegment の関数ポインタを代入することにより持つ。 +例えば \verb/Put/ の実体は \verb/put_stub/ である。 +他にも DataSegment の初期化(リスト\ref{src:init-rbtree-context} 34-48)とスタックの初期化(リスト\ref{src:init-rbtree-context} 50-51)を行なう。 + +\lstinputlisting[label=src:init-rbtree-context, caption=赤黒木の Meta DataSegment の初期化を行なう Meta CodeSegment ] {src/initLLRBContext.c} + +実際の赤黒木の実装に用いられている Meta CodeSegment の一例をリスト\ref{src:rbtree-insert-case-2}に示す。 +Meta CodeSegment \verb/insertCase2/ は要素を挿入した場合に呼ばれる Meta CodeSegment の一つであり、親ノードの色によって処理を変える。 +まず、色を確認するために経路を記憶しているスタックから親の情報を取り出す。 +親の色が黒ならば処理を終了し、次の CodeSegment へと軽量継続する(リスト\ref{src:rbtree-insert-case-2} 5-8)。 +親の色が赤であるならばさらに処理を続行して \verb/InsertCase3/ へと軽量継続する。 +ここで、経路情報を再現するためにスタックへと親を再代入してから軽量継続を行なっている。 +なお、Meta CodeSegment でも Context から DataSegment を展開する処理は stub によって行なわれる(リスト\ref{src:rbtree-insert-case-2} 14-16)。 + +\lstinputlisting[label=src:rbtree-insert-case-2, caption=赤黒木の実装に用いられている Meta CodeSegment例] {src/insertCase2.c} + +% }}} + +% {{{ メタ計算ライブラリ akasha を用いた赤黒木の実装の検証 + +\section{メタ計算ライブラリ akasha を用いた赤黒木の実装の検証} +赤黒木の仕様の定義とその確認を CbC で行なっていく。 +仕様には赤黒木の利用方法などによっていくつかのものが考えられる。 +赤黒木に対する操作の仕様と、その操作によって保証されるべき赤黒木の状態を示すと以下のようになる。 + +\begin{itemize} + \item 挿入したデータは参照できること + \item 削除したデータは参照できないこと + \item 値を更新した後は更新された値が参照されること + \item 操作を行なった後の木はバランスしていること +\end{itemize} + +今回はバランスに関する仕様を確認する。 +操作を挿入に限定し、どのような順番で要素を挿入しても木がバランスすることを検証する。 +検証には当研究室で開発しているメタ計算ライブラリ akasha を用いる。 + +akasha では仕様は常に成り立つべき CbC の条件式として定義される。 +具体的には Meta CodeSegment に定義した assert が仕様に相当する。 +仕様の例として「木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる」という式を定義する(リスト\ref{src:assert})。 + +\lstinputlisting[label=src:assert, caption=木の高さに関する仕様記述] {src/assert.c} + +リスト\ref{src:assert} で定義した仕様がプログラムの持つ全ての状態に成り立つかを確認する。 +また、成り立たない場合には仕様に反する状態を反例として提出する。 + +まずは最も単純な検証として要素数を有限に固定し、その挿入順番を数え上げる。 +最初に、検証の対象となる赤黒木と、検証に必要な DataSegment を含む Meta DataSegment を定義する(リスト\ref{src:akasha-context})。 +これが akasha のレベルで利用する Meta DataSegment である。 +赤黒木自体はユーザから見るとメタレベル計算であるが、今回はその実装の検証するため、赤黒木がノーマルレベルとなる。 +よって akasha はメタメタレベルの計算とも考えられる。 + +% TODO: meta meta の図 + +akasha が使う DataSegment は データの挿入順を数え上げるためには使う環状リスト \verb/Iterator/ とその要素 \verb/IterElem/、検証に使う情報を保持する \verb/AkashaInfo/、木をなぞる際に使う \verb/AkashaNode/ がある。 + +\lstinputlisting[label=src:akasha-context, caption=検証を行なうための Meta DataSegment] {src/akashaContext.h} + +挿入順番の数え上げには環状リストを用いた深さ優先探索を用いる。 +最初に検証する要素を全て持つ環状リストを作成し、木に挿入した要素を除きながら環状リストを複製していく。 +環状リストが空になった時が組み合わせを一つ列挙し終えた状態となる。 +列挙し終えた後、前の深さの環状リストを再現してリストの先頭を進めることで異なる組み合わせを列挙する。 + +仕様には木の高さが含まれるので、高さを取得する Meta CodeSegment が必要となる。 +リスト\ref{src:get-min-height}に木の最も低い経路の長さを取得する Meta CodeSegment を示す。 + +木を辿るためのスタックに相当する \verb/AkshaNode/を用いて経路を保持しつつ、高さを確認している。 +スタックが空であれば全てのノードを確認したので次の CodeSegment へと軽量継続を行なう。 +空でなければ今辿っているノードが葉であるか確認し、葉ならば高さを更新して次のノードを確認するため自身へと軽量継続する。 +葉でなければ高さを1増やして左右の子をスタックに積み、自身へと軽量継続を行なう。 + +\lstinputlisting[label=src:get-min-height, caption=木の最も短かい経路の長さを確認する Meta CodeSegment] {src/getMinHeight.c} + +同様に最も高い高さを取得し、仕様であるリスト\ref{src:assert}の assert を挿入の度に実行する。 +assert は CodeSegment の結合を行なうメタ計算である \verb/meta/ を上書きすることにより実現する。 + +% TODO: 図 + +\verb/meta/ はリスト\ref{src:rbtree-insert-case-2}の \verb/insertCase2/ のように軽量継続を行なう際に CodeSegment 名と DataSegment を指定するものである。 +検証を行なわない通常の \verb/meta/ の実装は CodeSegment 名から対応する実体への軽量継続である(リスト\ref{src:meta})。 + +\lstinputlisting[label=src:meta, caption=通常の CodeSegment の軽量継続] {src/meta.c} + +これを、検証を行なうように変更することで \verb/insertCase2/ といった赤黒木の実装のコードを修正することなく検証を行なうことができる。 +検証を行ないながら軽量継続する \verb/meta/ はリスト\ref{src:akasha-meta}のように定義される。 +実際の検証部分は \verb/PutAndGoToNextDepth/ の後に行なわれるため、直接は記述されていない。 +この \verb/meta/ が行なうのは検証用にメモリの管理である。 +状態の数え上げを行なう際に状態を保存したり、元の状態に戻す処理が行なわれる。 +このメタ計算を用いた検証では、要素数13個までの任意の順で挿入の際に仕様が満たされることを確認できた。 +また、赤黒木の処理内部に恣意的なバグを追加した際には反例を返した。 + +\lstinputlisting[label=src:akasha-meta, caption=検証を行なう CodeSegment の軽量継続] {src/akashaMeta.c} + +% }}} + +\section{モデル検査器 CBMC との比較} diff -r a3a9d56f71ec -r a9ed6a6dc1f2 paper/atton-master.pdf Binary file paper/atton-master.pdf has changed diff -r a3a9d56f71ec -r a9ed6a6dc1f2 paper/atton-master.tex --- a/paper/atton-master.tex Mon Feb 06 20:23:42 2017 +0900 +++ b/paper/atton-master.tex Wed Feb 08 13:50:52 2017 +0900 @@ -6,7 +6,6 @@ % あと syntax を最新に合わせて動かしてくれ % type system に名前を付ける? % 先の展望を書くべきだな -% gears and monad % delta monad % 副査名修正 % csComp, push-pop, exec-comp の解説 @@ -15,6 +14,7 @@ % ポンチ絵を増やして良い(meta とかの上書き) % stub を生成するスクリプトを作ってるって書いて良い % スローガンを書きたい +% ソースで省略しているところはそう書く \documentclass[a4j,12pt]{jreport} @@ -121,12 +121,13 @@ \mainmatter %chapters -\input{introduction.tex} +%\input{introduction.tex} \input{cbc.tex} -\input{type.tex} -\input{agda.tex} -\input{cbc-type.tex} -\input{summary.tex} +\input{akasha.tex} +%\input{type.tex} +%\input{agda.tex} +%\input{cbc-type.tex} +%\input{summary.tex} %謝辞 \addcontentsline{toc}{chapter}{謝辞} diff -r a3a9d56f71ec -r a9ed6a6dc1f2 paper/cbc.tex --- a/paper/cbc.tex Mon Feb 06 20:23:42 2017 +0900 +++ b/paper/cbc.tex Wed Feb 08 13:50:52 2017 +0900 @@ -101,25 +101,30 @@ % {{{ Continuation based C におけるメタ計算の例: GearsOS \section{Continuation based C におけるメタ計算の例: GearsOS} -CbC におけるメタ計算は軽量継続を行なう際に Meta CodeSegment を挟むことで実現できる。 CbC を用いてメタ計算を実現した例として、GearsOS\cite{weko_142109_1}が存在する。 -GearsOS とはマルチコアCPUやGPU環境での動作を対象としたOSであり、現在OSの設計と並列処理部分の実装が行なわれている。 -GearsOS におけるメタ計算はMonadによって形式化されている\cite{Moggi:1991:NCM:116981.116984}。 -現在存在するメタ計算としてメモリの確保と割り当て、並列に書き込むことが可能な Synchronized Queue、データの保存に用いる非破壊赤黒木がある。 +GearsOS は並列に、信頼性高く動作することを目標としたOS であり、 マルチコアCPUやGPU環境での動作を対象としている。 +現在OSの設計と並列処理部分の実装が行なわれている。 +GearsOS におけるメタ計算はMonad\cite{Moggi:1991:NCM:116981.116984}を用いている。 %TODO: kkb さんの修論 +現在実装済みのメタ計算はメモリの管理、並列に書き込むことが可能な Synchronized Queue、データの保存用の非破壊赤黒木がある。 GearsOS では CodeSegment と DataSegment はそれぞれ CodeGear と DataGear と呼ばれている。 マルチコアCPU環境では CodeGear と CodeSegment は同一だが、GPU 環境では CodeGear には OpenCL~\cite{opencl}/CUDA~\cite{cuda} における kernel も含まれる。 -kernel とは GPU で実行される関数のことであり、GPU上のメモリに配置されたデータ群に対して並列に実行されるものである。 -通常 GPU でデータの処理を行なう場合はデータの転送、転送終了を同期で確認、 kernel 実行、kernel の終了を同期で確認する、という手順が必要である。 -CPU/GPU での処理をメタ計算で行なうことにより、ノーマルレベルでは CodeGear が実行されるデバイスや DataGear の位置を意識する必要が無いというメリットがある。 +kernel とは GPU で実行される関数のことであり、GPU上のメモリに配置されたデータ群に対して並列に実行される。 +通常 GPU でデータの処理を行なう場合は -GearsOS においては軽量継続の呼び出し部分もメタ計算として実現されている。 -ある CodeGear から次の CodeGear へと継続する際には、次に実行される CodeGear の名前を指定する。 -その名前を Meta CodeGear が解釈し、対応する CodeGear へと処理を引き渡す。 -これは従来の OS の Dynamic Loading Libary や Command の呼び出しに相当する。 -CodeGear と名前の対応は Meta DataGear に格納されており、従来の OS の Process や Thread に相当する。 +\begin{itemize} + \item データをメインメモリから GPUのメモリへ転送 + \item 転送終了を同期で確認 + \item kernel 起動(GPUメモリ上のデータに対して並列に処理) + \item 処理終了を同期で確認 + \item 計算結果であるデータを GPU のメモリからメインメモリへ転送 + \item 転送終了を同期で確認 +\end{itemize} -具体的には Meta DataGear には以下のようなものが格納される。 +といった手順が必要であり、ユーザは処理したいデータの位置などを意識しながらプログラミングする必要がある。 +GearsOS では CPU/GPU での処理をメタ計算としてユーザから隠すことにより、 CodeGear が実行されるデバイスや DataGear の位置を意識する必要がなくなる。 + +GearsOS で利用する Meta DataGear には以下のものが含まれる。 \begin{itemize} \item DataGear の型情報 @@ -130,9 +135,12 @@ 実際の GearsOS におけるメモリ管理を含むメタ計算用の Meta DataGear の定義例をリスト\ref{src:context}に示す。 Meta DataGear は Context という名前の構造体で定義されている。 +通常レベルの DataGear も構造体で定義されているが、メタ計算側から見た DataGear はそれぞれの構造体の共用体となっており、一様に扱える。 \lstinputlisting[label=src:context, caption=GearsOS における Meta DataGearの定義例] {src/context.h} +リスト~\ref{src:context}のソースコードは以下のように対応している。 + \begin{itemize} \item DataGear の型情報 @@ -162,164 +170,33 @@ 取り出す必要がある DataGear は enum を用いて定義し(リスト\ref{src:context} 11-14行)、 CodeGear を実行する際に data フィールドから取り出す。 \end{itemize} -なお、この Context から DataGear を取り出す Meta CodeSegment を stub と呼ぶ。 -stub の例をリスト\ref{src:stub}に示す。 -stub は Context が持つ DataGear のポインタ data に対して enum を用いてアクセスしている。 -現在、この stub は全ての CodeGear に対してユーザが1つずつ定義する必要がある。 -この作業は非常に煩雑であり、CodeGear の定義から生成するスクリプトを用いて定義の簡易化を行なっているが、コンパイラ側でのサポートは入っていない。 -この stub を型情報から自動生成するために Continuation based C における型システムを定義する必要がある。 - -\lstinputlisting[label=src:stub, caption=GearsOS における stub Meta CodeSegment] {src/stub.cbc} - -% }}} - -% {{{ GearsOS における非破壊赤黒木 - -\section{GearsOS における非破壊赤黒木} - -現状の GearsOS に実装されているメタ計算として、非破壊赤黒木が存在する。 -メタ計算として定義することにより、ノーマルレベルからは木のバランスを必要なく要素の挿入と探索、削除が行なえる。 -赤黒木とは二分探索木の一種であり、木の各ノードが赤と黒の色を持っている。 -木に対して要素の挿入や削除を行なった際、その色を用いて木のバランスを保つ。 - -二分探索木の条件は以下である。 - -\begin{itemize} - \item 左の子孫の値は親の値より小さい - \item 右の子孫の値は親の値より大きい -\end{itemize} - -加えて、赤黒木が持つ具体的な条件は以下のものである。 - -\begin{itemize} - \item 各ノードは赤か黒の色を持つ。 - \item ルートノードの色は黒である。 - \item 葉ノードの色は黒である。 - \item 赤ノードは2つの黒ノードを子として持つ(よって赤ノードが続くことは無い)。 - \item ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定である。 -\end{itemize} - - -数値を要素に持つ赤黒木の例を図\ref{fig:rbtree}に示す。 -ルートノードは黒であり、赤ノードは連続していない。 -加えて各最下位ノードへの経路に含まれる黒ノードの個数は全て2である。 - -\begin{figure}[htbp] - \begin{center} - \includegraphics[scale=0.5]{fig/rbtree.pdf} - \caption{赤黒木の例} - \label{fig:rbtree} - \end{center} -\end{figure} - -これらの条件より、木をルートから辿った際に最も長い経路は最も短い経路の高々二倍に収まる。 - -\newpage % for layout - -GearsOS で実装されている赤黒木は特に非破壊赤黒木であり、一度構築した木構造は破壊される操作ごとに新しい木構造が生成される。 -非破壊赤黒木の実装の基本的な戦略は、変更したいノードへのルートノードからの経路を全て複製し、変更後に新たなルートノードとする。 -この際に変更が行なわれていない部分は変更前の木と共有する(図\ref{fig:non-destructive-rbtree})。 -これは一度構築された木構造は破壊されないという非破壊の性質を用いたメモリ使用量の最適化である。 - -\begin{figure}[htbp] - \begin{center} - \includegraphics[scale=0.5]{fig/non-destructive-rbtree} - \caption{非破壊赤黒木の編集} - \label{fig:non-destructive-rbtree} - \end{center} -\end{figure} - -CbC を用いて赤黒木を実装する際の問題として、関数の呼び出しスタックが存在しないため、関数の再帰呼び出しによって木が辿れないことがある。 -経路を辿るためにはノードに親への参照を持たせるか、挿入・削除時に辿った経路を記憶する必要がある。 -ノードが親への参照を持つ非破壊木構造は共通部分の共有が行なえないため、辿った経路を記憶する方法を使う。 -経路の記憶にはスタックを用い、スタックは Meta DataSegment に保持させる。 +Meta CodeGear は定義された Meta DataGear を処理する CodeGear である。 +メモリ管理や並列処理の待ち合わせといった処理はこのメタレベルにしか表れない。 -赤黒木を格納する DataSegment と Meta DataSegment の定義をリスト\ref{src:rbtree-context}に示す。 -経路の記憶に用いるスタックは Meta DataSegment である Context 内部の \verb/node_stack/ である。 -DataSegment は各ノード情報を持つ \verb/Node/構造体と、赤黒木を格納する \verb/Tree/構造体、挿入などで操作中の一時的な木を格納する \verb/Traverse/共用体などがある。 - -\lstinputlisting[label=src:rbtree-context, caption=赤黒木の DataSegment と Meta DataSegment] {src/rbtreeContext.h} - -Meta DataSegment を初期化する Meta CodeSegment initLLRBContext をリスト\ref{src:init-rbtree-context}に示す。 -この Meta CodeSegment ではメモリ領域の確保、CodeSegment 名と CodeSegment の実体の対応表の作成などを行なう。 -メモリ領域はプログラムの起動時に一定数のメモリを確保し、ヒープとして \verb/heap/ フィールドに保持させる。 -CodeSegment 名と CodeSegment の実体との対応は、enum で定義された CodeSegment 名の添字へと CodeSegment の関数ポインタを代入することにより持つ。 -例えば \verb/Put/ の実体は \verb/put_stub/ である。 -他にも DataSegment の初期化(リスト\ref{src:init-rbtree-context} 34-48)とスタックの初期化(リスト\ref{src:init-rbtree-context} 50-51)を行なう。 - -\lstinputlisting[label=src:init-rbtree-context, caption=赤黒木の Meta DataSegment の初期化を行なう Meta CodeSegment ] {src/initLLRBContext.c} - -実際の赤黒木の実装に用いられている Meta CodeSegment の一例をリスト\ref{src:rbtree-insert-case-2}に示す。 -Meta CodeSegment \verb/insertCase2/ は要素を挿入した場合に呼ばれる Meta CodeSegment の一つであり、親ノードの色によって処理を変える。 -まず、色を確認するために経路を記憶しているスタックから親の情報を取り出す。 -親の色が黒ならば処理を終了し、次の CodeSegment へと軽量継続する(リスト\ref{src:rbtree-insert-case-2} 5-8)。 -親の色が赤であるならばさらに処理を続行して \verb/InsertCase3/ へと軽量継続する。 -ここで、経路情報を再現するためにスタックへと親を再代入してから軽量継続を行なっている。 -なお、Meta CodeSegment でも Context から DataSegment を展開する処理は stub によって行なわれる(リスト\ref{src:rbtree-insert-case-2} 14-16)。 - -\lstinputlisting[label=src:rbtree-insert-case-2, caption=赤黒木の実装に用いられている Meta CodeSegment例] {src/insertCase2.c} - -% }}} - -% {{{ メタ計算ライブラリ akasha を用いた赤黒木の実装の検証 - -\section{メタ計算ライブラリ akasha を用いた赤黒木の実装の検証} -GearsOS の赤黒木の仕様の定義とその確認を CbC で行なっていく。 -赤黒木には以下の性質が求められる。 - -\begin{itemize} - \item 挿入したデータは参照できること - \item 削除したデータは参照できないこと - \item 値を更新した後は更新された値が参照されること - \item 操作を行なった後の木はバランスしていること -\end{itemize} - -今回はバランスに関する仕様を確認する。 -操作を挿入に限定し、木にどのような順番で要素を挿入しても木がバランスすることを検証する。 -検証には当研究室で開発しているメタ計算ライブラリ akasha を用いる。 -akasha では仕様は常に成り立つべき CbC の条件式として定義される。 -具体的には Meta CodeSegment に定義した assert が仕様に相当する。 -仕様の例として、木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる、という木がバランスしている際に成り立つ式を定義する(リスト\ref{src:assert})。 - -\lstinputlisting[label=src:assert, caption=木の高さに関する仕様記述] {src/assert.c} - -リスト\ref{src:assert} で定義した仕様が常に成り立つか、全ての挿入順番を列挙しながら確認していく。 -まずは最も単純な有限の個数の任意の順の数え上げに対して検証していく。 -最初に検証の対象となる赤黒木と検証に必要な DataSegment を含む Meta DataSegment を定義する(リスト\ref{src:akasha-context})。 -DataSegment は データの挿入順を数え上げるためには使う環状リスト \verb/Iterator/ とその要素 \verb/IterElem/、検証に使う情報を保持する \verb/AkashaInfo/、木をなぞる際に使う \verb/AkashaNode/ がある。 - -\lstinputlisting[label=src:akasha-context, caption=検証を行なうための Meta DataSegment] {src/akashaContext.h} - -挿入順番の数え上げには環状リストを用いた深さ優先探索を用いる。 -最初に検証する要素を全て持つ環状リストを作成し、木に挿入した要素を除きながら環状リストを複製していく。 -環状リストが空になった時が組み合わせを一つ列挙し終えた状態となる。 -列挙し終えた後、前の深さの環状リストを再現してリストの先頭を進めることで異なる組み合わせを列挙する。 - -仕様には木の高さが含まれるので、高さを取得する Meta CodeSegment が必要となる。 -リスト\ref{src:get-min-height}に木の最も低い経路の長さを取得する Meta CodeSegment を示す。 - -木を辿るためのスタックに相当する \verb/AkshaNode/を用いて経路を保持しつつ、高さを確認している。 -スタックが空であれば全てのノードを確認したので次の CodeSegment へと軽量継続を行なう。 -空でなければ今辿っているノードが葉であるか確認し、葉ならば高さを更新して次のノードを確認するため自身へと軽量継続する。 -葉でなければ高さを1増やして左右の子をスタックに積み、自身へと軽量継続を行なう。 - -\lstinputlisting[label=src:get-min-height, caption=木の最も短かい経路の長さを確認する Meta CodeSegment] {src/getMinHeight.c} - -同様に最も高い高さを取得し、仕様であるリスト\ref{src:assert}の assert を挿入の度に実行する。 -assert は CodeSegment の結合を行なうメタ計算である \verb/meta/ を上書きすることにより実現する。 -\verb/meta/ はリスト\ref{src:rbtree-insert-case-2}の \verb/insertCase2/ のように軽量継続を行なう際に CodeSegment 名と DataSegment を指定するものである。 -検証を行なわない通常の \verb/meta/ の実装は CodeSegment 名から対応する実体への軽量継続である(リスト\ref{src:meta})。 +GearsOS においては軽量継続もメタ計算として実現されている。 +とある CodeGear から次の CodeGear へと軽量継続する際には、次に実行される CodeGear の名前を指定する。 +その名前を Meta CodeGear が解釈し、対応する CodeGear へと処理を引き渡す(リスト~\ref{src:meta}の \verb/meta/)。 \lstinputlisting[label=src:meta, caption=通常の CodeSegment の軽量継続] {src/meta.c} -これを、検証を行なうように変更することで \verb/insertCase2/ といった赤黒木の実装のコードを修正することなく検証を行なうことができる。 -検証を行ないながら軽量継続する \verb/meta/ はリスト\ref{src:akasha-meta}のように定義される。 -実際の検証部分は \verb/PutAndGoToNextDepth/ の後に行なわれるため、直接は記述されていない。 -この \verb/meta/ が行なうのは検証用にメモリの管理である。 -状態の数え上げを行なう際に状態を保存したり、元の状態に戻す処理が行なわれる。 -このメタ計算を用いた検証では、要素数13個までの任意の順で挿入の際に仕様が満たされることを確認できた。 -また、赤黒木の処理内部に恣意的なバグを追加した際には反例を返した。 +CodeGear と名前の対応は Meta DataGear に格納されており、従来の OS の Process や Thread に相当する。 +名前の対応を動的に切り替えたり、Thread ごとに切り替えることにより、通常レベルのプログラムを変更せず実行を上書きできる。 +これは従来の OS の Dynamic Loading Libary や Command の呼び出しに相当する。 + +また、通常レベルの CodeGear から Meta DataGear を操作できてしまうと、ユーザがメタレベル操作を自由に記述できてしまい、メタ計算を分離した意味が無くなってしまう。 +これを防ぐために、CodeGear を実行する際は Meta DataGear から必要な DataGear だけを渡す。 +このように、 Meta DataGear から DataGear を取り出す Meta CodeGear を stub と呼ぶ。 +stub の例をリスト\ref{src:stub}に示す。 +\lstinputlisting[label=src:stub, caption=GearsOS における stub Meta CodeSegment] {src/stub.cbc} -\lstinputlisting[label=src:akasha-meta, caption=検証を行なう CodeSegment の軽量継続] {src/akashaMeta.c} +stub は Context が持つ DataGear のポインタ data に対して enum を用いてアクセスしている。 +なお、現在はメタレベルの計算とノーマルレベルの分離はコンパイラ側がサポートしていないため、引数に Meta DataGear である Context が渡されているが、本来はノーマルレベルではアクセスできない。 +% また、stub は全ての CodeGear に対してユーザが1つずつ定義する必要があるため、 CodeGear の定義が煩雑になっている。 +% レベルの分離と stub の自動生成を行なうスクリプトも存在しているが、コンパイラ側のサポートはまだ行なわれていない。 +% 型情報を用いたコンパイル時 stub 生成や、軽量継続時の型チェックを行なうために本研究では CbC の型システムを定義する。 + +また、GearsOS におけるメタ計算として CodeGear のモデル検査がある。 +通常レベルの CodeGear を変更することなく、その仕様を検証するものである。 +個々の CodeGear の仕様を検証することにより、より信頼性の高いOSを目指す。 % }}}