Mercurial > hg > Papers > 2020 > ikkun-sigos

Binary file paper/ikkun-sigos.pdf has changed
--- a/paper/ikkun-sigos.tex	Thu May 07 23:29:52 2020 +0900
+++ b/paper/ikkun-sigos.tex	Mon May 18 20:10:53 2020 +0900
@@ -14,6 +14,28 @@
 \usepackage[dvips,dvipdfmx]{graphicx}
 \usepackage{latexsym}
 \usepackage{listings}
+\lstset{
+  language=C,
+  tabsize=2,
+  frame=single,
+  basicstyle={\tt\footnotesize}, %
+  identifierstyle={\footnotesize}, %
+  commentstyle={\footnotesize\itshape}, %
+  keywordstyle={\footnotesize\ttfamily}, %
+  ndkeywordstyle={\footnotesize\ttfamily}, %
+  stringstyle={\footnotesize\ttfamily},
+  breaklines=true,
+  captionpos=b,
+  columns=[l]{fullflexible}, %
+  xrightmargin=0zw, %
+  xleftmargin=1zw, %
+  aboveskip=1zw,
+  numberstyle={\scriptsize}, %
+  stepnumber=1,
+  numbersep=0.5zw, %
+  lineskip=-0.5ex,
+}
+ \usepackage{caption}
 \def\Underline{\setbox0\hbox\bgroup\let\\\endUnderline}
 \def\endUnderline{\vphantom{y}\egroup\smash{\underline{\box0}}\\}
 \def\|{\verb|}
@@ -22,7 +44,7 @@
 %\setcounter{巻数}{59}%vol59=2018
 %\setcounter{号数}{10}
 %\setcounter{page}{1}
-
+\renewcommand{\lstlistingname}{Code}

 \begin{document}

@@ -76,19 +98,20 @@

 メタレベルから見ると、codeGearの入力は context ただ一つであり、そこから必要なノーマルレベルのdataGearを取り出して、ノーマルレベルのcodeGaerを
 呼び出す。この取り出しは stub と呼ばれる meta codeGear によって行われる。
-Code\ref{varargnext}は codeGear では codeGear における goto の遷移と引数を渡す例題である。
-Code\ref{varargnext2}は stub codeGear は codeGear の接続の間に挟まれる Meta Code Gear である。ノーマルレベルのcodeGear から MetadataGear である Context を直接参照してしまうと、ユーザーがメタ計算をノーマルレベルで自由に記述できてしまい、メタ計算を分離した意味がなくなってしまう。stub Code Gear はこの問題を防ぐため、Context から必要なdataGaerのみをノーマルレベルに和刺す処理を行なっている。
-\begin{lstlisting}[label=varargnext,frame=lrbt,caption={codeGear goto}]
-__code cg0(int a, int b) {
-    goto cg1(a+b);
-}
+Codeは codeGear では codeGear における goto の遷移と引数を渡す例題である。
+Codeは stub codeGear は codeGear の接続の間に挟まれる Meta Code Gear である。ノーマルレベルのcodeGear から MetadataGear である Context を直接参照してしまうと、ユーザーがメタ計算をノーマルレベルで自由に記述できてしまい、メタ計算を分離した意味がなくなってしまう。stub Code Gear はこの問題を防ぐため、Context から必要なdataGaerのみをノーマルレベルに和刺す処理を行なっている。

-__code cg1(int c) {
-    goto cg2(c);
-  }
-\end{lstlisting}
+\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}

-\begin{lstlisting}[label=varargnext2,frame=lrbt,caption={meta codeGear stub}]
+\begin{lstlisting}[frame=lrbt,caption=metacodeGearstub]
   __code popSingleLinkedStack_stub(struct
   Context* context) {
     SingleLinkedStack* stack = (
@@ -105,12 +128,8 @@
     }
 \end{lstlisting}

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

 ただし、context の状態は有限状態になるとは限らないし、有限になるとしても巨大になることがある。しかし、OSやアプリケーションのテストだと
 考えると、それらの動作の振る舞いを調べるのに十分な状態があれば良い。一つの方法は context の状態をなんらかの方法で抽象化することである。
@@ -204,15 +223,18 @@
 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本ずつフォークを持って場合はデッドロックしていることになる。プロセスの並列実行はスケジューラによって制御することで実現する。\\
+検証用のサンプルプログラムとしてDining Philosohers Ploblem (以下DPP)を用いる。これは資源共有問題の１つで、次のような内容である。\ref{varargnext3}
+
+5人の哲学者が円卓についており、各々スパゲッティーの皿が目の前に用意されている。スパゲッィーはとても絡まっているので食べるには2本のフォークを使わないと食べれない。しかしフォークはお皿の間に一本ずつおいてあるので、円卓にフォークが5本しか用意されていない。\figref{fig}哲学者は思索と食事を交互に繰り返している。空腹を覚えると、左右のオークを手に取ろうと試み、2本のフォークを取ることに成功するとしばし食事をし、しばらくするとフォークを置いて思索に戻る。隣の哲学者が食事中でフォークが手に取れない場合は、そのままフォークが置かれるのを待つ。
+
+各哲学者を１つのプロセスとすると、この問題では5個のプロセスが並列に動くことになり、全員が1本ずつフォークを持って場合はデッドロックしていることになる。プロセスの並列実行はスケジューラによって制御することで実現する。
+
 以下はDPPにおける左側のフォークを取るプログラムである。
 最初に左のフォークを持たれているかどうかを確認し、いなければ自分を持ち主に登録する。
 その後 next に次に遷移する自分の状態を入れ scheduler に遷移することによって scheduler を通して次の状態に遷移する。このときscheduler からメタ計算を挟むことによって状態をMemoryTree に入れる事ができる。
 左のフォークの持ち主がいた場合は飢餓状態を登録し scheduler に遷移する事で待機状態を維持する。
-\begin{lstlisting}[frame=lrbt,label=src:cbc_example,caption={DPP}]

+\begin{lstlisting}[label=varargnext3,frame=lrbt,label=src:cbc_example,caption={DPP}]
   code pickup_lfork(PhilsPtr self,
   TaskPtr current_task)
 {
@@ -257,9 +279,7 @@
 DPPの状態遷移は6つの状態を繰り返すため、同じ状態が出た場合には終了させなければならない。そこでstate DBを用いて同じ状態を検索することで終了判定をだす。

 \begin{figure}[tb]
-    \begin{center}
         \includegraphics[width=90mm]{./pic/model_checking.pdf}
-    \end{center}
     \caption{DPP chacking}
     \label{DPP_chacking}
 \end{figure}
--- a/paper/ikkun.bib	Thu May 07 23:29:52 2020 +0900
+++ b/paper/ikkun.bib	Mon May 18 20:10:53 2020 +0900
@@ -1,41 +1,46 @@
 @article{
-    gears,
+    pargoto,
     author = "河野 真治 and 伊波 立樹 and  東恩納 琢偉",
-    title = "Code Gear、Data Gear に基づく OS のプロトタイプ",
-    journal = "情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)",
+    title = {Code Gear、Data Gear に基づく OS のプロトタイプ},
+    journal = {情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)},
     month = "May",
-    year = 2016}
+    year = 2016
+}
+
 @article{
-    gears,
+    gearsOS2,
     author = "宮城　光希 and 桃原　優 and  河野真治",
-    title = "Code Gear と Data Gear を持つ Gears OS の設計",
-    journal = "第59回プログラミング・シンポジウム)",
+    title = {Code Gear と Data Gear を持つ Gears OS の設計},
+    journal = {第59回プログラミング・シンポジウム},
     month = "Jan",
-    year = 2018}
+    year = 2018
+    }
 @article{
-    gears,
-    author = "小久保翔平 and 伊波立樹 and 河野真治"
-    title = "Monad に基づくメタ計算を基本とする Gears OS の設計"
-    journal = 情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)
+    GearsOS,
+    author = "小久保翔平 and 伊波立樹 and 河野真治",
+    title = {Monad に基づくメタ計算を基本とする Gears OS の設計},
+    journal = {情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)},
     month = "May",
-    year = 2015}
+    year = 2015
+    }
 @article{
-    gears,
-    author = "下地篤樹 and 河野真治"
-    title = "タブロー法を用いたContinuation based C プログラムの検証"
-    journal = 日本ソフトウェア科学会第23回大会,
-    year = 2006}
+    tauble,
+    author = "下地篤樹 and 河野真治",
+    title = {タブロー法を用いたContinuation based C プログラムの検証},
+    journal = {日本ソフトウェア科学会第23回大会},
+    year = 2006
+    }
 @article{
-    gears,
-    author = "河野真治"
-    title = "継続を持つCの下位言語によるシステム記述"
-    journal = 日本ソフトウェア科学会第17回大会
-    year = 2000}
+    CbC,
+    author = "河野真治",
+    title = {継続を持つCの下位言語によるシステム記述},
+    journal = {日本ソフトウェア科学会第17回大会},
+    year = 2000
+    }
 @article{
-    gears,
-    author = "比嘉 薫 and 河野真治"
-    title = "タブロー法の負荷分散について"
-    journal = 日本ソフトウェア科学会第18回論文集
-    year = 2001}
-
-
+    tauble2,
+    author = "比嘉 薫 and 河野真治",
+    title = {タブロー法の負荷分散について},
+    journal = {日本ソフトウェア科学会第18回論文集},
+    year = 2001
+    }
\ No newline at end of file