Mercurial > hg > Papers > 2018 > nozomi-master

comparison paper/akasha.tex @ 100:ebe838b83ada

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Self review
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Sun, 12 Feb 2017 11:52:20 +0900
parents 2bc816f4af27
children
comparison
equal deleted inserted replaced
99:a891d7551bbf 100:ebe838b83ada
5 5
6 % {{{ モデル検査 6 % {{{ モデル検査
7 \section{モデル検査} 7 \section{モデル検査}
8 モデル検査とは、ソフトウェアの全ての状態において仕様が満たされるかを確認するものである。 8 モデル検査とは、ソフトウェアの全ての状態において仕様が満たされるかを確認するものである。
9 このモデル検査を行なうソフトウェアをモデル検査器と呼ぶ。 9 このモデル検査を行なうソフトウェアをモデル検査器と呼ぶ。
10 モデルは検査器は、仕様の定義と確認ができる。 10 モデルは検査器は、仕様の定義とその検証ができる。
11 加えて、仕様を満たさない場合にはソフトウェアがどのような状態であったか反例を返す。 11 加えて、仕様を満たさない場合にはソフトウェアがどのような状態であったか反例を返す。
12 12
13 モデル検査器には Spin\cite{spin} やCBMC\cite{cbmc} などが存在する。 13 モデル検査器には Spin\cite{spin} やCBMC\cite{cbmc} などが存在する。
14 14
15 Spin は Promela と呼ばれる言語でモデルを記述し、その中に論理式として仕様を記述する。 15 Spin は Promela と呼ばれる言語でモデルを記述し、その中に論理式として仕様を記述する。
80 この問題に対し GearsOS では、各スレッドは処理を行なう際には非破壊の木を利用することで並列度は保ち、値の更新が発生する時のみ木をアトミックな操作で置き換えることで競合を回避する。 80 この問題に対し GearsOS では、各スレッドは処理を行なう際には非破壊の木を利用することで並列度は保ち、値の更新が発生する時のみ木をアトミックな操作で置き換えることで競合を回避する。
81 具体的には木の操作を行なった後はルートのノードを元に CAS で置き換え、失敗した時は木を読み込み直して処理を再実行する。 81 具体的には木の操作を行なった後はルートのノードを元に CAS で置き換え、失敗した時は木を読み込み直して処理を再実行する。
82 CAS(Check and Set) とは、アトミックに値を置き換える操作であり、使う際は更新前の値と更新後の値を渡す。 82 CAS(Check and Set) とは、アトミックに値を置き換える操作であり、使う際は更新前の値と更新後の値を渡す。
83 CAS で渡された更新前の値が、保存している値と同じであれば競合していないために値の更新に成功し、異なる場合は他に書き込みがあったことを示すために値の更新が失敗する操作のことである。 83 CAS で渡された更新前の値が、保存している値と同じであれば競合していないために値の更新に成功し、異なる場合は他に書き込みがあったことを示すために値の更新が失敗する操作のことである。
84 84
85 非破壊赤黒木の実装の基本的な戦略は、変更したいノードへのルートノードからの経路を全て複製し、変更後に新たなルートノードとする。 85 非破壊赤黒木の実装の基本的な戦略は、変更したいノードへのルートノードからの経路を全て複製し、変更後に新たなルートノードとすることである。
86 この際に変更が行なわれていない部分は変更前の木と共有する(図\ref{fig:non-destructive-rbtree})。 86 この際に変更されていない部分は変更前の木と共有する(図\ref{fig:non-destructive-rbtree})。
87 これは一度構築された木構造は破壊されないという非破壊の性質を用いたメモリ使用量の最適化である。 87 これは一度構築された木構造は破壊されないという非破壊の性質を用いたメモリ使用量の最適化である。
88 88
89 \begin{figure}[htbp] 89 \begin{figure}[htbp]
90 \begin{center} 90 \begin{center}
91 \includegraphics[scale=0.5]{fig/non-destructive-rbtree} 91 \includegraphics[scale=0.5]{fig/non-destructive-rbtree}
143 143
144 今回はバランスに関する仕様を確認する。 144 今回はバランスに関する仕様を確認する。
145 操作を挿入に限定し、どのような順番で要素を挿入しても木がバランスすることを検証する。 145 操作を挿入に限定し、どのような順番で要素を挿入しても木がバランスすることを検証する。
146 検証には当研究室で開発しているメタ計算ライブラリ akasha を用いる。 146 検証には当研究室で開発しているメタ計算ライブラリ akasha を用いる。
147 147
148 akasha では仕様は常に成り立つべき CbC の条件式として定義される。 148 akasha では仕様は常に成り立つべき CbC の条件式として定義する。
149 具体的には Meta CodeSegment に定義した assert が仕様に相当する。 149 具体的には Meta CodeSegment に定義した assert が仕様に相当する。
150 仕様の例として「木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる」という式を定義する(リスト\ref{src:assert})。 150 仕様の例として「木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる」という式を定義する(リスト\ref{src:assert})。
151 151
152 \lstinputlisting[label=src:assert, caption=木の高さに関する仕様記述] {src/assert.c} 152 \lstinputlisting[label=src:assert, caption=木の高さに関する仕様記述] {src/assert.c}
153 153