Mercurial > hg > Papers > 2020 > ikkun-sigos

--- a/paper/ikkun-sigos.tex	Thu May 28 09:45:25 2020 +0900
+++ b/paper/ikkun-sigos.tex	Mon Feb 01 15:21:35 2021 +0900
@@ -91,42 +91,79 @@
 信頼性を保証する一つの方法は、プログラムの可能な実行を数え上げて要求仕様を満たしているかどうかを調べるモデル検査である。
 本論文では、Gears OS上のアプリケーション、さらに Gears OSそのものをGears OS上でモデル検査することに関して考察する。

-CbC (Continuation based C)はCの機能を持ち、goto 文で遷移する codeGearという単位を持っている。通常の関数呼び出しと異なり、stackや環境を
-隠して持つことがなく、計算の状態は codeGear の入力ですべて決まる。codeGearの入力は dataGearと呼ばれる構造体だが、これには
+\begin{figure}[tb]
+    \begin{center}
+        \includegraphics[width=80mm]{pic/input-outputDataSegment.pdf}
+    \end{center}
+    \caption{codeGear と DataGear}
+    \label{fig:code-datagear}
+\end{figure}
+
+CbC (Continuation based C)はCの機能を持ち、goto 文で遷移する codeGearという単位を持っている。
+Cの関数の型が\verb+__code+ であるような構文で定義することができる。
+つまり、codeGearはdataGearを通して、次のcodeGearに  goto で接続される(図\ref{fig:code-datagear})。
+
+例えば、Dinign Philosopher の例題で右のforkを取るところは以下のように書ける。
+ここでは \verb+cas+ (check and set)と busy wait で書いてある。
+通常の関数呼び出しと異なり、stackや環境を
+隠して持つことがなく、計算の状態は codeGear の入力ですべて決まる。
+
+{\footnotesize
+\begin{verbatim}
+  __code pickup_rfork(PhilsPtr self,__code __next(...))
+  {
+      if (cas(self->right_fork->owner, self) == self) {
+        goto self->think(self, next);
+      } else {
+        goto self->pickup_rfork(self, next);
+      }
+  }
+\end{verbatim}
+}
+
+codeGearの入力は dataGearと呼ばれる構造体だが、これには
 ノーマルレベルのdataGearとメタレベルのdataGearの階層がある。メタレベルには計算を実行するCPUやメモリ、計算に関与するすべてのノーマルレベルの
 dataGearを格納する context などがある。context は通常のOSのプロセスに相当する。

 メタレベルから見ると、codeGearの入力は context ただ一つであり、そこから必要なノーマルレベルのdataGearを取り出して、ノーマルレベルのcodeGaerを
 呼び出す。この取り出しは stub と呼ばれる meta codeGear によって行われる。
+<<<<<<< working copy
+これは通常の関数呼び出しのABI(引数とレジスタやスタック上の関係を決めたバイナリインターフェース)に相当する。
+=======
 Codeは codeGear では codeGear における goto の遷移と引数を渡す例題である。
 Codeは stub codeGear は codeGear の接続の間に挟まれる Meta Code Gear である。ノーマルレベルのcodeGear から MetadataGear である Context を直接参照してしまうと、ユーザーがメタ計算をノーマルレベルで自由に記述できてしまい、メタ計算を分離した意味がなくなってしまう。stub Code Gear はこの問題を防ぐため、Context から必要なdataGaerのみをノーマルレベルに和刺す処理を行なっている。
+>>>>>>> merge rev

-\begin{lstlisting}[frame=lrbt,label=src:cbc_example,caption=CodeGearandgoto]
-__code cg0(int a, int b) {
-     goto cg1(a+b);
- }
-
- __code cg1(int c) {
-     goto cg2(c);
-}
-\end{lstlisting}
+<<<<<<< working copy
+遷移は次のcodeGearに移動するだけだが、その前に出力するdataGearをcontextに書き出す必要がある。
+これは通常の関数呼び出しのreturnの処理に相当する。
+以下はメタレベルから見た codeGear である。
+goto 先は meta という meta codeGaer であり、そこで必要なメタ計算が行われる。ここに任意のメタ計算を置くことができる。
+この場合の引数は context と行き先を表す番号だけである。
+
+このようにノーマルレベルから context を見ることはできず、メタ計算レベルではノーマルレベルの引数の詳細を気にしないで
+処理を行うことができるようになっている。ノーマルレベルとメタレベルは、必要ならばCPUのsystem mode と user mode の状態を変えても良い。

-\begin{lstlisting}[frame=lrbt,caption=metacodeGearstub]
-  __code popSingleLinkedStack_stub(struct
-  Context* context) {
-    SingleLinkedStack* stack = (
-    SingleLinkedStack*)context->data[
-      D_Stack]->Stack.stack->Stack.stack;
-    enum Code next = context->data[
-      D_Stack]->
-    Stack.next;
-    Data** O_data = &context->data[
-      D_Stack]->
-    Stack.data;
-    goto popSingleLinkedStack(context,
-    stack,next, O_data);
-    }
-\end{lstlisting}
+{\footnotesize
+\begin{verbatim}
+   __code pickup_rfork_stub(ContextPtr cbc_context)
+   {
+      PhisPtr self = GearRef(cbc_context,D_Phisoloper);
+      PhisPtr next = GearRef(cbc_context,D_next);
+      goto  pickup_rfork(ContextPtr cbc_context, self,next);
+   }
+
+    __code pickup_rfork(PhilsPtr self,
+       __code __next(ContextPtr cbc_context));
+   {
+     if (cas(self->right_fork->owner, self) == self) {
+          goto meta(context,C_phil_think);
+     } else {
+         goto meta(context,C_pickup_rfork);
+     }
+   }
+\end{verbatim}
+}

 ここでcodeGearの実行はOSの中での基本単位である必要がある。つまり、codeGearは並行処理などにより割り込まれることなく、codeGearで記述された通りに実行される必要がある。これは一般的には保証されない。他のcodeGearが共有された dataGearに競合的に書き込んだり、割り込みにより処理が中断したりする。しかし、Gears OS が codeGear が正しく実行さることを保証する。つまり、Gears OS はそのように実装されているとする。
 プログラムの非決定的な実行は入力あるいは並列実行の非決定性から生じる。後者は並列実行される codeGear の順列並び替えになる。従って、これらの並び替えを生成し、その時に生じる context の状態をすべて数え上げれればモデル検査を実装できることになる。
@@ -180,7 +217,7 @@

 \section{既存のモデル検査手法}
 モデル検査の方法としてよく利用される物として、SPIN と java path finder(以下JVM)というツールがある。\\
-SPIN は Promela という仕様記述言語で記述する事でC言語の検証器を生成する事で、コンパイルまたは実行時に検証する事ができる。チャネルを使っての通信や並列動作する有限オートマトンのモデル検査が可能である。\\
+SPIN は Promela という仕様記述言語で記述する事でC言語の検証器を生成する事で、コンパイルまたは実行時に検証する事ができる。チャネルを使っての通信や並列動作する有限オートマトンのモデル検査が可能である。
 SPIN では以下の性質を検査する事ができる。
 \begin{itemize}
 \item アサーション
@@ -200,29 +237,23 @@


 \section{Continuation based C}
-GearsOS は Continuation based C (以下CbC) という言語を用いて拡張性と信頼性を両立させることを目的として本研究室で開発されている。CbC はC言語と似た構文を持つ言語であるが、CodeSegment と DataSegment を用いるプログラミングスタイルを提案している。CodeSegmentは処理の単位である。CodeSegument は値を入力として受け取り処理を行ったあと出力を行う、また他の CodeSegment を接続していくことによりプログラムを構築していく。DataSegment は CodeSegment が扱うデータの単位であり、処理に必要なデータが全て入っている。DataSegmen は Input DataSegment と呼ばれ、出力はOutput DataSegment と呼ばれる。CodeSegment A と CodeSegment B を接続したとき、A の Output DataSegment は B の入力 Input DataSegment となる。
-\begin{figure}[tb]
-    \begin{center}
-        \includegraphics[width=80mm]{./pic/input-outputDataSegment.pdf}
-    \end{center}
-    \caption{CodeSegment と DataSegment}
-    \label{code-datasegment}
-\end{figure}
+GearsOS は Continuation based C (以下CbC) という言語を用いて拡張性と信頼性を両立させることを目的として本研究室で開発されている。CbC はC言語と似た構文を持つ言語であるが、codeGear と DataGear を用いるプログラミングスタイルを提案している。codeGearは処理の単位である。codeSegument は値を入力として受け取り処理を行ったあと出力を行う、また他の codeGear を接続していくことによりプログラムを構築していく。DataGear は codeGear が扱うデータの単位であり、処理に必要なデータが全て入っている。DataSegmen は Input DataGear と呼ばれ、出力はOutput DataGear と呼ばれる。codeGear A と codeGear B を接続したとき、A の Output DataGear は B の入力 Input DataGear となる。

-CodeSegment の接続処理はメタ計算として定義されており、実装や環境によって切り替えを行なうことができる。検証を行なうメタ計算を定義することにより、CodeSegment の定義を検証用に変更せずプログラムの検証を行なう。\\
-CbC における接続は goto を用いて行われる。got は関数呼び出しのような環境変数を持たず goto の直後に遷移先を記述することで、遷移先に接続される。これを軽量継続と言い、遷移元の処理に囚われず、遷移先を自由に変更する事が可能でり 遷移元の code gear の goto 先以外に変更する事なく、処理の間にメタレベルの計算を挿入する事が可能である。CbC における遷移記述はそのまま状態遷移記述にすることができる。\ref{fig:meta_Gear}\\
+codeGear の接続処理はメタ計算として定義されており、実装や環境によって切り替えを行なうことができる。検証を行なうメタ計算を定義することにより、codeGear の定義を検証用に変更せずプログラムの検証を行なう。
+CbC における接続は goto を用いて行われる。got は関数呼び出しのような環境変数を持たず goto の直後に遷移先を記述することで、遷移先に接続される。これを軽量継続と言い、遷移元の処理に囚われず、遷移先を自由に変更する事が可能でり 遷移元の code gear の goto 先以外に変更する事なく、処理の間にメタレベルの計算を挿入する事が可能である。CbC における遷移記述はそのまま状態遷移記述にすることができる(図\ref{fig:meta_Gear})。

 \begin{figure}[tb]
     \begin{center}
-        \includegraphics[width=90mm]{./pic/meta_gear.pdf}
+        \includegraphics[width=90mm]{pic/meta_gear.pdf}
     \end{center}
     \caption{Gears OS のメタ計算}
-    \label{meta_Gear}
+    \label{fig:meta_Gear}
 \end{figure}

-GearsOS では CodeSegment と DataSegment はそれぞれ CodeGear と DataGear と呼ばれている。マルチコアCPU環境では CodeGaer と CodeSegment は同一だが、、GPU環境では CodeGear にはOpenCL/CUDA における kernel も含まれる。kernelとはGPUで実行される関数のことである。\
+GearsOS では codeGear と DataGear はそれぞれ codeGear と DataGear と呼ばれている。マルチコアCPU環境では codeGaer と codeGear は同一だが、、GPU環境では codeGear にはOpenCL/CUDA における kernel も含まれる。kernelとはGPUで実行される関数のことである。

 \section{DPP}
+
 検証用のサンプルプログラムとしてDining Philosohers Ploblem (以下DPP)を用いる。これは資源共有問題の１つで、次のような内容である。\ref{varargnext3}

 5人の哲学者が円卓についており、各々スパゲッティーの皿が目の前に用意されている。スパゲッィーはとても絡まっているので食べるには2本のフォークを使わないと食べれない。しかしフォークはお皿の間に一本ずつおいてあるので、円卓にフォークが5本しか用意されていない。\figref{fig}哲学者は思索と食事を交互に繰り返している。空腹を覚えると、左右のオークを手に取ろうと試み、2本のフォークを取ることに成功するとしばし食事をし、しばらくするとフォークを置いて思索に戻る。隣の哲学者が食事中でフォークが手に取れない場合は、そのままフォークが置かれるのを待つ。
@@ -250,7 +281,7 @@

 \begin{figure}[tb]
     \begin{center}
-        \includegraphics[width=70mm]{./pic/dpp_image.pdf}
+        \includegraphics[width=70mm]{pic/dpp_image.pdf}
     \end{center}
     \caption{Dining Philosohers Ploblem}
     \label{DPP_imag}
@@ -261,10 +292,12 @@

 タブロー法は実行可能な状態の組み合わせを深さ優先探索で調べ、木構造で保存する方法である。この時、同じ状態の組み合わせがあれば共有することで状態を抽象化する事で、状態数が増えすぎる事を抑える。

- \section{GearsOSを用いたモデル検査}
-DPP は哲学者5人が同時に行動するので、5つのスレッドで同時に処理することで状態を生成する事ができる。まず Gears OS の並列構文の par goto が用いることでマルチスレッド処理の実装を行う。 par goto は引数として、data gaer と実行後に継続する\|__exit|を渡す。par goto で生成された Task は\|__exit| に継続する事で終了する。これによりGears OS は複数スレッドでの実行を行う事が可能である。
-また Gears OS には　Synchronized Queue というマルチスレッドでのデータの一貫性を保証する事ができる Queue があり、これを使い5つのフォークの状態を管理する。
-Syncrhonized Queueは CAS(Check and Set)を用いて実装されており、値の比較、更新をアトミックに行う命令である。CASを使う際は更新前の値と更新後の値を渡し、渡された更新前の値を実際に保存されているメモリ番地の値と比較し、同じデータ今日がないため、データの更新に成功する。異なる場合は他の書き込みがあったとみなされ、値の更新に失敗し、もう一度 CAS を行う。
+\section{GearsOSを用いたモデル検査}
+DPP は哲学者5人が同時に行動するので、5つのスレッドで同時に処理することで状態を生成する事ができる。まず Gears OS の並列構文の par goto が用いることでマルチスレッド処理の実装を行う。 par goto は引数として、data gaer と実行後に継続する\verb+__exit+を渡す。par goto で生成された Task は\verb|__exit| に継続する事で終了する。これによりGears OS は複数スレッドでの実行を行う事が可能である。
+%また Gears OS には　Synchronied Queue というマルチスレッドでのデータの一貫性を保証する事ができる Queue があり、これを使い5つのフォークの状態を管理する。
+%Syncrhonized Queueは CAS(Check and Set)を用いて実装されており、値の比較、更新をアトミックに行う命令である。
+5つのフォークの状態はCASで管理する。
+CASを使う際は更新前の値と更新後の値を渡し、渡された更新前の値を実際に保存されているメモリ番地の値と比較し、同じデータがないため、データの更新に成功する。異なる場合は他の書き込みがあったとみなされ、値の更新に失敗し、もう一度 CAS を行う。
 5スレッドで行われる処理の状態は以下の6通りで、think のあとPickup Right fork に戻ってくる。
 \begin{itemize}
 \item Pickup Right fork
@@ -279,11 +312,51 @@
 DPPの状態遷移は6つの状態を繰り返すため、同じ状態が出た場合には終了させなければならない。そこでstate DBを用いて同じ状態を検索することで終了判定をだす。

 \begin{figure}[tb]
-        \includegraphics[width=90mm]{./pic/model_checking.pdf}
+    \begin{center}
+        \includegraphics[width=90mm]{pic/model_checking.pdf}
+    \end{center}
     \caption{DPP chacking}
     \label{DPP_chacking}
 \end{figure}

+この実行は Single thread に行われるが、interator を使って並行実行しても良い。
+
+必要な時相論理的な仕様は codeGear にコンパイルすることができるので、それを同時に走らせることによりチェックできる。
+これは SPIN の LTL の仕様記述と同じことになる。このようにモデル検査を codeGear と dataGear 上に実現することができる。
+
+
+メモリ領域の登録には
+\verb+add_mamory_area(ContextPtr cbc_contex+ \verb+,void *addrss,long length)+ のようなAPIを用いる。
+状態の格納は、mera codeGear で行われるので、customize が可能である。この段階で対称性の利用や状態の抽象化を行うことができる。
+
+\section{OS自体のモデル検査}
+
+Gears OS 自体も codeGear/dataGear で書かれているので、この枠組みの中で検証することが可能であると思われる。
+しかし、いくつかの問題がある。
+
+OSの場合はほとんどがmeta levelの記述なので、それを emulation する必要がある。メモリやCPUは問題ないが TLB などは工夫が必要になる。
+CPUの状態、例えばキャッシュなども emulation する場合には、codeGear の大きさをメモリアクセスレベルまで小さくする必要がある。
+つまり、見つけたいバグを知っていれば検証は可能だが、起きる可能性のある未知のメタ計算に関しては何も教えてくれない。
+
+モデル検査は膨大な状態空間を探索する必要があり、OS込みのモデル検査となると厳しいと予想される。
+しかし、OS特定部分を調べるのに巨大なアプリケーションは必要ないと思われる。普通のテストの代わりにモデル検査を使うような感じになる。
+
+OSを含むモデル検査はデバイスドライバの開発などに向いていると考えられる。この場合は、デバイス自体の仕様が codeGear/dataGear
+で書かれている必要がある。
+
+Gears OS は Unix 上のApplicationとして実現されているものと、x.v6 の書き換えとして実現するものとの二種類がある。
+後者の開発にモデル検査が使えると良い。
+
+\section{まとめ}
+
+Gears OS でのモデル検査の実装方法について考察した。DPPの検証自体は前に書かれたことがある\cite{}。
+この時のmemory tree と state DB を使うことも可能だが、これ自体はCで書かれている。
+これも codeGear で書く方が望ましい。
+
+
+まず、DPPを動かすとこから始めて、OS自体を検証する方向に研究を進めていきたい。
+
+
 \nocite{*}
 \bibliographystyle{ipsjunsrt}
 \bibliography{ikkun.bib}