# HG changeset patch # User atton # Date 1485159570 -32400 # Node ID 243d8dc4a2922558e1503881c8a9cc9a086ef042 # Parent 5510bb043a7494d0e12c1f27d8eb16691b038c21 Add akasha description diff -r 5510bb043a74 -r 243d8dc4a292 paper/cbc.tex --- a/paper/cbc.tex Mon Jan 23 15:42:08 2017 +0900 +++ b/paper/cbc.tex Mon Jan 23 17:19:30 2017 +0900 @@ -172,7 +172,10 @@ % }}} -\section{メタ計算ライブラリ akasha を用いた赤黒木の実装の検証} +% {{{ GearsOS における非破壊赤黒木 + +\section{GearsOS における非破壊赤黒木} + 現状の GearsOS に実装されているメタ計算として、非破壊赤黒木が存在する。 メタ計算として定義することにより、ノーマルレベルからは木のバランスを必要なく要素の挿入と探索、削除が行なえる。 赤黒木とは二分探索木の一種であり、木の各ノードが赤と黒の色を持っている。 @@ -255,8 +258,52 @@ \lstinputlisting[label=src:rbtree-insert-case-2, caption=赤黒木の実装に用いられている Meta CodeSegment例] {src/insertCase2.c} +% }}} -% TODO: akasha context case x の解説くらい -% TODO: akasha context の初期化 -% TODO: verification の assert +\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 を挿入の度に実行する。 + + +% TODO: meta の定義 % TODO: akasha の結果 diff -r 5510bb043a74 -r 243d8dc4a292 paper/src/akashaContext.h --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/akashaContext.h Mon Jan 23 17:19:30 2017 +0900 @@ -0,0 +1,31 @@ +// Data Segment +union Data { + struct Tree { /* ... */ } tree; + struct Node { /* ... */ } node; + + /* for verification */ + struct IterElem { + unsigned int val; + struct IterElem* next; + } iterElem; + struct Iterator { + struct Tree* tree; + struct Iterator* previousDepth; + struct IterElem* head; + struct IterElem* last; + unsigned int iteratedValue; + unsigned long iteratedPointDataNum; + void* iteratedPointHeap; + } iterator; + struct AkashaInfo { + unsigned int minHeight; + unsigned int maxHeight; + struct AkashaNode* akashaNode; + } akashaInfo; + struct AkashaNode { + unsigned int height; + struct Node* node; + struct AkashaNode* nextAkashaNode; + } akashaNode; +}; + diff -r 5510bb043a74 -r 243d8dc4a292 paper/src/assert.c --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/assert.c Mon Jan 23 17:19:30 2017 +0900 @@ -0,0 +1,4 @@ +void verifySpecification(struct Context* context, struct Tree* tree) { + assert(!(maxHeight(tree->root, 1) > 2*minHeight(tree->root, 1))); + return meta(context, EnumerateInputs); +} diff -r 5510bb043a74 -r 243d8dc4a292 paper/src/getMinHeight.c --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/getMinHeight.c Mon Jan 23 17:19:30 2017 +0900 @@ -0,0 +1,51 @@ +__code getMinHeight_stub(struct Context* context) { + goto getMinHeight(context, &context->data[Allocate]->allocate, &context->data[AkashaInfo]->akashaInfo); +} + +__code getMinHeight(struct Context* context, struct Allocate* allocate, struct AkashaInfo* akashaInfo) { + const struct AkashaNode* akashaNode = akashaInfo->akashaNode; + + if (akashaNode == NULL) { + allocate->size = sizeof(struct AkashaNode); + allocator(context); + akashaInfo->akashaNode = (struct AkashaNode*)context->data[context->dataNum]; + + akashaInfo->akashaNode->height = 1; + akashaInfo->akashaNode->node = context->data[Tree]->tree.root; + + goto getMaxHeight_stub(context); + } + + const struct Node* node = akashaInfo->akashaNode->node; + if (node->left == NULL && node->right == NULL) { + if (akashaInfo->minHeight > akashaNode->height) { + akashaInfo->minHeight = akashaNode->height; + akashaInfo->akashaNode = akashaNode->nextAkashaNode; + goto getMinHeight_stub(context); + } + } + + akashaInfo->akashaNode = akashaInfo->akashaNode->nextAkashaNode; + + if (node->left != NULL) { + allocate->size = sizeof(struct AkashaNode); + allocator(context); + struct AkashaNode* left = (struct AkashaNode*)context->data[context->dataNum]; + left->height = akashaNode->height+1; + left->node = node->left; + left->nextAkashaNode = akashaInfo->akashaNode; + akashaInfo->akashaNode = left; + } + + if (node->right != NULL) { + allocate->size = sizeof(struct AkashaNode); + allocator(context); + struct AkashaNode* right = (struct AkashaNode*)context->data[context->dataNum]; + right->height = akashaNode->height+1; + right->node = node->right; + right->nextAkashaNode = akashaInfo->akashaNode; + akashaInfo->akashaNode = right; + } + + goto getMinHeight_stub(context); +}