Mercurial > hg > Papers > 2020 > ikkun-sigos

Binary file paper/ikkun-sigos.pdf has changed
--- a/paper/ikkun-sigos.tex	Thu May 07 19:55:59 2020 +0900
+++ b/paper/ikkun-sigos.tex	Thu May 07 22:00:44 2020 +0900
@@ -69,40 +69,73 @@
 信頼性を保証する一つの方法は、プログラムの可能な実行を数え上げて要求仕様を満たしているかどうかを調べるモデル検査である。
 本論文では、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 によって行われる。
-
-\begin{lstlisting}[frame=lrbt,label=src:cbc_example,caption={}]
-__code cg0(int a, int b) {
-    goto cg1(a+b);
-}
+これは通常の関数呼び出しのABI(引数とレジスタやスタック上の関係を決めたバイナリインターフェース)に相当する。

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

-\begin{lstlisting}[frame=lrbt,label=src:cbc_example,caption={codeGearのstub と goto}]
-  __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}
-    メタレベルのでのcodeGaerのstub と goto meta
+{\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に競合的に書き込んだり、割り込みにより処理が
@@ -160,7 +193,7 @@

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


 \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)を用いる。これは資源共有問題の１つで、次のような内容である。\\
-5人の哲学者が円卓についており、各々スパゲッティーの皿が目の前に用意されている。スパゲッィーはとても絡まっているので食べるには2本のフォークを使わないと食べれない。しかしフォークはお皿の間に一本ずつおいてあるので、円卓にフォークが5本しか用意されていない。\figref{fig}哲学者は思索と食事を交互に繰り返している。空腹を覚えると、左右のオークを手に取ろうと試み、2本のフォークを取ることに成功するとしばし食事をし、しばらくするとフォークを置いて思索に戻る。隣の哲学者が食事中でフォークが手に取れない場合は、そのままフォークが置かれるのを待つ。\\
-各哲学者を１つのプロセスとすると、この問題では5個のプロセスが並列に動くことになり、全員が1本ずつフォークを持って場合はデッドロックしていることになる。プロセスの並列実行はスケジューラによって制御することで実現する。\\
-
-\begin{lstlisting}[frame=lrbt,label=src:cbc_example,caption={DPP}]
+検証用のサンプルプログラムとしてDining Philosohers Ploblem (以下DPP)を用いる。これは資源共有問題の１つで、次のような内容である。
+5人の哲学者が円卓についており、各々スパゲッティーの皿が目の前に用意されている。スパゲッィーはとても絡まっているので食べるには2本のフォークを使わないと食べれない。しかしフォークはお皿の間に一本ずつおいてあるので、円卓にフォークが5本しか用意されていない。\figref{DPP_imag}哲学者は思索と食事を交互に繰り返している。空腹を覚えると、左右のオークを手に取ろうと試み、2本のフォークを取ることに成功するとしばし食事をし、しばらくするとフォークを置いて思索に戻る。隣の哲学者が食事中でフォークが手に取れない場合は、そのままフォークが置かれるのを待つ。
+各哲学者を1つのプロセスとすると、この問題では5個のプロセスが並列に動くことになり、全員が1本ずつフォークを持って場合はデッドロックしていることになる。プロセスの並列実行はスケジューラによって制御することで実現する。

-  code pickup_lfork(PhilsPtr self,
-  TaskPtr current_task)
-{
-    if (self->left_fork->owner == NULL) {
-        self->left_fork->owner = self;
-        self->next = pickup_rfork;
-        goto scheduler(self, current_task);
-    } else {
-        self->next = hungry1;
-        goto scheduler(self, current_task);
-}
-\end{lstlisting}

 \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}
@@ -236,7 +248,7 @@
 タブロー法は実行可能な状態の組み合わせを深さ優先探索で調べ、木構造で保存する方法である。この時、同じ状態の組み合わせがあれば共有することで状態を抽象化する事で、状態数が増えすぎる事を抑える。

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

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