Mercurial > hg > Papers > 2020 > ikkun-sigos

Binary file paper/ikkun-sigos.pdf has changed
--- a/paper/ikkun-sigos.tex	Thu May 07 18:12:10 2020 +0900
+++ b/paper/ikkun-sigos.tex	Thu May 07 19:55:10 2020 +0900
@@ -13,7 +13,7 @@

 \usepackage[dvips,dvipdfmx]{graphicx}
 \usepackage{latexsym}
-
+\usepackage{listings}
 \def\Underline{\setbox0\hbox\bgroup\let\\\endUnderline}
 \def\endUnderline{\vphantom{y}\egroup\smash{\underline{\box0}}\\}
 \def\|{\verb|}
@@ -77,8 +77,31 @@
 メタレベルから見ると、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);
+}
+
+__code cg1(int c) {
+    goto cg2(c);
+  }
+\end{lstlisting}
     ノーマルレベルのcodeGaerのgoto

+\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

 ここでcodeGearの実行はOSの中での基本単位である必要がある。つまり、codeGearは並行処理などにより割り込まれることなく、codeGearで記述された
@@ -155,7 +178,7 @@
 \item Partial Order Reduction
 \end{itemize}

-\newpage
+
 \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]
@@ -177,13 +200,28 @@
     \label{meta_Gear}
 \end{figure}

-GearsOS では CodeSegment と DataSegment はそれぞれ CodeGear と DataGear と呼ばれている。マルチコアCPU環境では CodeGaer と CodeSegment は同一だが、、GPU環境では CodeGear にはOpenCL/CUDA における kernel も含まれる。kernelとはGPUで実行される関数のことである。\\
-
+GearsOS では CodeSegment と DataSegment はそれぞれ CodeGear と DataGear と呼ばれている。マルチコアCPU環境では CodeGaer と CodeSegment は同一だが、、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}]
+
+  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}
@@ -193,7 +231,8 @@
 \end{figure}

  \section{タブロー展開と状態数の抽象化}
- 　GearsOS におけるモデル検査はタブロー展開を用いることでデッドロックを調べる。タブロー法は生成可能な状態の全てを生成する手法である。反例を探す場合は反例が見つかった時点で状態の生成を停止してもよいが、証明を行う場合は全ての状態を生成する必要がある。状態の生成は初期状態から非決定的に生成される全ての次の状態を生成することにより行われ、これを状態の展開という。証明はプログラムの状態の数に比例し、またプログラムが含む変数の数の指数状の計算量がかかる。この展開の際に仕様うも同時に展開することでプログラムに対する仕様の検証を行う事が可能である。\\
+ 　GearsOS におけるモデル検査はタブロー展開を用いることでデッドロックを調べる。タブロー法は生成可能な状態の全てを生成する手法である。反例を探す場合は反例が見つかった時点で状態の生成を停止してもよいが、証明を行う場合は全ての状態を生成する必要がある。状態の生成は初期状態から非決定的に生成される全ての次の状態を生成することにより行われ、これを状態の展開という。証明はプログラムの状態の数に比例し、またプログラムが含む変数の数の指数状の計算量がかかる。この展開の際に仕様うも同時に展開することでプログラムに対する仕様の検証を行う事が可能である。
+
 タブロー法は実行可能な状態の組み合わせを深さ優先探索で調べ、木構造で保存する方法である。この時、同じ状態の組み合わせがあれば共有することで状態を抽象化する事で、状態数が増えすぎる事を抑える。

  \section{GearsOSを用いたモデル検査}
@@ -211,9 +250,6 @@
 \end{itemize}
 この状態は goto next によって遷移する。またこの状態遷移は無限ループするのでMemoryTree に保管し、保管されている状態とはstat DB によって保管される

-
-
-
 \begin{figure}[tb]
     \begin{center}
         \includegraphics[width=90mm]{./pic/model_checking.pdf}
@@ -226,7 +262,8 @@


 \nocite{*}
-
+\bibliographystyle{ipsjunsrt}
+\bibliography{ikkun-bib}