Binary file main1.pdf has changed

--- a/main1.tex	Tue Apr 27 15:52:47 2021 +0900
+++ b/main1.tex	Tue Apr 27 18:16:56 2021 +0900
@@ -4,6 +4,7 @@
 \usepackage{fontspec}
 \usepackage{graphicx}
 \usepackage{float}
+\usepackage{listings}
 \restylefloat{figue}
 \pagestyle{empty}
 

--- a/model.ind	Tue Apr 27 15:52:47 2021 +0900
+++ b/model.ind	Tue Apr 27 18:16:56 2021 +0900
@@ -51,7 +51,7 @@
 \begin{tabular}{c}
 \begin{minipage}{0.50\hsize}
 \begin{center}
-\includegraphics[width=70mm]{images/graphEF.pdf}
+\includegraphics[width=40mm]{images/graphEF.pdf}
 \caption{ある枝でいつか真になる EF}
 \label{fig:EF}
 \end{center}
@@ -59,7 +59,7 @@
 
 \begin{minipage}{0.50\hsize}
 \begin{center}
-\includegraphics[width=70mm]{images/graphAF.pdf}
+\includegraphics[width=40mm]{images/graphAF.pdf}
 \caption{すべての枝でいつか真になる AF}
 \label{fig:AF}
 \end{center}
@@ -73,7 +73,7 @@
 \begin{tabular}{c}
 \begin{minipage}{0.50\hsize}
 \begin{center}
-\includegraphics[width=70mm]{images/graphEG.pdf}
+\includegraphics[width=40mm]{images/graphEG.pdf}
 \caption{ある枝でいつも真になる EG}
 \label{fig:EG}
 \end{center}
@@ -81,7 +81,7 @@
 
 \begin{minipage}{0.50\hsize}
 \begin{center}
-\includegraphics[width=70mm]{images/graphAG.pdf}
+\includegraphics[width=40mm]{images/graphAG.pdf}
 \caption{すべての枝でいつも真になる AG}
 \label{fig:AG}
 \end{center}
@@ -130,13 +130,13 @@
 Cの関数の型が\verb+__code+ であるような構文で定義することができる。
 つまり、codeGearはdataGearを通して、次のcodeGearに goto で接続される(図\ref{fig:code-datagear})。
 
-\begin{figure}[tb]
+\begin{figure*}[tb]
 \begin{center}
 \includegraphics[width=140mm]{fig/input-outputDataSegment.pdf}
 \end{center}
 \caption{codeGear と DataGear}
 \label{fig:code-datagear}
-\end{figure}
+\end{figure*}
 
 
 例えば、ソースコード3.1は DiningPhilosohersPloblem(以下DPP) の例題で右のforkを取るという処理を行っているは以下のように書ける。
@@ -144,7 +144,7 @@
 通常の関数呼び出しと異なり、stackや環境を
 隠して持つことがなく、計算の状態は codeGear の入力ですべて決まる。
 
-\lstinputlisting[caption=pickUrforkp, label=pickUprfork]{src/PhilsImpl.cbc}
+\lstinputlisting[caption=pickUrforkp, label=pickUprfork, basicstyle=\footnotesize ]{src/PhilsImpl.cbc}
 
 メタ計算 と stub
 codeGear の入力は dataGear と呼ばれる構造体だが、これにはノーマルレベルの dataGear とメタレベルの dataGear の階層がある。メタレベルには計算を実行する CPU やメモリ、計算に関与するすべてのノーマルレベルの dataGear を格納する context などがある。context は通常の OS のプロセスに相当する。
@@ -158,31 +158,31 @@
 ソースコード3.2は DPP における 右のフォークを持ち上げる例題の stub\cite{gearsOS2} である pickup\_rfork\_stub と、その stub meta に goto する ノーマルレベルのものになる。
 このようにノーマルレベルの CodeGear からメタレベルに遷移する際には goto meta で引数を渡すだけで、メタレベルの計算は隠されている。
 
-\lstinputlisting[caption=pickuprfork, label=pickuprfork]{src/pickup_rfork.cbc}
+\lstinputlisting[caption=pickuprfork, label=pickuprfork, basicstyle=\footnotesize ]{src/pickup_rfork.cbc}
 
-\begin{figure}[tb]
+\begin{figure*}[tb]
 \begin{center}
-\includegraphics[width=150mm]{fig/meta_gear.pdf}
+\includegraphics[width=140mm]{fig/meta_gear.pdf}
 \end{center}
 \caption{Gears OS のメタ計算}
 \label{fig:meta_Gear}
-\end{figure}
+\end{figure*}
 
 メタレベルから見ると、codeGearの入力は context ただ一つであり、そこから必要なノーマルレベルのdataGearを取り出して、ノーマルレベルのcodeGaerを呼び出す。この取り出しは stub と呼ばれる meta codeGear によって行われる。(図\ref{fig:Context_ref})
 これは通常の関数呼び出しのABI(引数とレジスタやスタック上の関係を決めたバイナリインターフェース)に相当する。
 \newpage
- stub codeGear は codeGear の接続の間に挟まれる Meta Code Gear である。ノーマルレベルのcodeGear から MetadataGear である Context を直接参照してしまうと、ユーザーがメタ計算をノーマルレベルで自由に記述できてしまい、メタ計算を分離した意味がなくなってしまう。stub Code Gear はこの問題を防ぐため、Context から必要なdataGaerのみをノーマルレベルに和刺す処理を行なっている。
+stub codeGear は codeGear の接続の間に挟まれる Meta Code Gear である。ノーマルレベルのcodeGear から MetadataGear である Context を直接参照してしまうと、ユーザーがメタ計算をノーマルレベルで自由に記述できてしまい、メタ計算を分離した意味がなくなってしまう。stub Code Gear はこの問題を防ぐため、Context から必要なdataGaerのみをノーマルレベルに和刺す処理を行なっている。
 
- このようにノーマルレベルの Code Gear からは context を見ることはできず、メタ計算レベルではノーマルレベルの引数の詳細を気にしないで
+このようにノーマルレベルの Code Gear からは context を見ることはできず、メタ計算レベルではノーマルレベルの引数の詳細を気にしないで
 処理を行うことができるようになっている。ノーマルレベルとメタレベルは、必要ならばCPUのsystem mode と user mode の状態を変えても良い。
 
-\begin{figure}[tb]
+\begin{figure*}[tb]
 \begin{center}
 \includegraphics[width=140mm]{fig/Context_ref.pdf}
 \end{center}
 \caption{Contexが持つDataGaerへのアクセス}
 \label{fig:Context_ref}
-\end{figure}
+\end{figure*}
 
 \clearpage
 
@@ -237,7 +237,7 @@
 
 と考えられる。
 
---Dining Philosophers Problem の例題
+--Dining Philosophers 
 
 モデル検査の検証用のサンプルプログラムとしてDining Philosohers Ploblem (以下DPP)を用いる。これは資源共有問題の１つで、次のような内容である。
 
@@ -250,15 +250,7 @@
 その後 next に次に遷移する自分の状態を入れ scheduler に遷移することによって scheduler を通して次の状態に遷移する。このときscheduler からメタ計算を挟むことによって状態をMemoryTree に入れる事ができる。
 左のフォークの持ち主がいた場合は飢餓状態を登録し scheduler に遷移する事で待機状態を維持する。
 
-\lstinputlisting[caption=pickuplfork, label=pickuplfork]{src/pickup_lfork.cbc}
-
-\begin{figure}[tb]
-\begin{center}
-\includegraphics[width=140mm]{fig/dpp_image.pdf}
-\end{center}
-\caption{Dining Philosohers Ploblem image}
-\label{DPP_image}
-\end{figure}
+\lstinputlisting[caption=pickuplfork, label=pickuplfork, basicstyle=\footnotesize ]{src/pickup_lfork.cbc}
 
 
 --Gears OS を用いた DPP 
@@ -325,27 +317,27 @@
 その後11行目で受け取った文字列を goto 先にランダムに、配置しており。
 16行目では文字列を受け取った文字列に遷移する前に mcMeta を挟むようにしている。 
 
-\lstinputlisting[caption=meta.pm, label=meta.pm]{src/meta.pm}
+\lstinputlisting[caption=meta.pm, label=meta.pm, basicstyle=\footnotesize ]{src/meta.pm}
     
 --導出木の作り方
 
-\lstinputlisting[caption=putdown\_lfork, label=putdownlfork]{src/putdown_lfork.cbc}
+\lstinputlisting[caption=putdown\_lfork, label=putdownlfork, basicstyle=\footnotesize ]{src/putdown_lfork.cbc}
 ソースコード5.5 は DPP の例題のもので、Philospher の Leftfork を置く部分である。フォークは各 Philosher 間で共有されるデータのため、競合が起きないように CAS を行う必要がある。
 このソースコードは以下のソースコード5.6に変換される。
 Gearef はContext から Data Gaer を参照するマクロになっている。
 goto 先がmcMeta になっている。
 
-\lstinputlisting[caption=putdownlforkImpl, label=putdownlforkImpl]{src/putdown_lforkImpl.cbc}
+\lstinputlisting[caption=putdownlforkImpl, label=putdownlforkImpl, basicstyle=\footnotesize ]{src/putdown_lforkImpl.cbc}
 
 Gears OS のノーマルレベルの code は変換されるが、mcMeta は \_\_ncode と記述されており、これは meta として扱い変換しない意味である。
 9行目にある mctiにタスクを渡している。
 
-\lstinputlisting[caption=mcMeta, label=mcMeta]{src/mcMeta.cbc}
+\lstinputlisting[caption=mcMeta, label=mcMeta, basicstyle=\footnotesize,multicols=2 ]{src/mcMeta.cbc}
 
 --モデル検査のフラグの管理
 
 ソースコード4.3 の mcDPP.h はモデル検査で使われるフラグの宣言をしている。
-\lstinputlisting[caption=mcDPP.h, label=mcDPP.h]{src/mcDPP.h}
+\lstinputlisting[caption=mcDPP.h, label=mcDPP.h, basicstyle=\footnotesize ]{src/mcDPP.h}
 しかし今回の DPP の例題においては t\_eating と f\_F\_eating のフラグしか使用してしいない。
 DPPの例題は食事とそれ以外の状態を循環しているため t\_eating フラグの「食事中」と f\_F\_eating フラグの「いつか食事にする」という２つの状態で表すことが可能となる。
 
@@ -359,11 +351,11 @@
 フラグは now と next を見比べながら update する。すべての状態は 今のcontext にのっているが、過去は add\_memory\_rangeで記録されたものあるいはフラグしか見れないようになっている。
  
 ソースコード4.4 のmcDPP.cbc ではフラグの比較によるモデル検査を行っている。
-\lstinputlisting[caption=mcDPP.cbc, label=mcDPP.cbc]{src/mcDPP.cbc}
+\lstinputlisting[caption=mcDPP.cbc, label=mcDPP.cbc, basicstyle=\footnotesize ]{src/mcDPP.cbc}
  
-最初に今のフラグと次のフラグを取得し、次にphils-\>self が 1 である場合はreturn でぬける。
+最初に今のフラグと次のフラグを取得し、次に\verb|phils->self| が 1 である場合はreturn でぬける。
 12行目では 次と今のフラグがet\_ating または t\_F\_eatingであればt\_F\_eating;
-15行目では直前のフラグと今のフラグ、または直前のフラグと次のフラグが違っているとchangeに1が入り、動き続け、そうでなければ18行目で今のフラグとt\_F\_eatingを比較し、あっている場合にはnot<>eating となり、終了する。
+15行目では直前のフラグと今のフラグ、または直前のフラグと次のフラグが違っているとchangeに1が入り、動き続け、そうでなければ18行目で今のフラグとt\_F\_eatingを比較し、あっている場合には\verb+not<>eating+ となり、終了する。
 
 --実行結果
 
@@ -375,34 +367,32 @@
 その次の5つの値が各スレッドの状態を示している。
 flag 0 の後の部分がstateDBによって同じ状態のものを探しハッシュ値で抽象化している部分となり、最後にこの処理を行っていたスレッド番号となっている。
 
-\begin{itembox}[1]{モデル検査の実行結果を一部抜粋}
-\begin{verbatim}
-not <> eating
-00000000 01000000 02000000 03000000 04000000 
-01000000 01000000 01000000 01000000 01000000
-flag 0 0x7fb22255e090 -> 0x7fb22255e090 hash 5feba6a0 iter 5
+モデル検査の実行結果を一部抜粋
 
-not <> eating
-00000000 01000000 02000000 03000000 04000000 
-01000000 01000000 01000000 01000000 01000000
-flag 0 0x7fb22255e090 -> 0x7fb22255e090 hash 5feba6a0 iter 4
+    not <> eating
+    00000000 01000000 02000000 03000000 04000000 
+    01000000 01000000 01000000 01000000 01000000
+    flag 0 0x7fb22255e090 -> 0x7fb22255e090 hash 5feba6a0 iter 5
+
+    not <> eating
+    00000000 01000000 02000000 03000000 04000000 
+    01000000 01000000 01000000 01000000 01000000
+    flag 0 0x7fb22255e090 -> 0x7fb22255e090 hash 5feba6a0 iter 4
 
-not <> eating
-00000000 01000000 02000000 03000000 04000000 
-01000000 01000000 01000000 01000000 01000000
-flag 0 0x7fb22255e090 -> 0x7fb22255e090 hash 5feba6a0 iter 3
+    not <> eating
+    00000000 01000000 02000000 03000000 04000000 
+    01000000 01000000 01000000 01000000 01000000
+    flag 0 0x7fb22255e090 -> 0x7fb22255e090 hash 5feba6a0 iter 3
 
-not <> eating
-00000000 01000000 02000000 03000000 04000000 
-01000000 01000000 01000000 01000000 01000000
-flag 0 0x7fb22255e090 -> 0x7fb22255e090 hash 5feba6a0 iter 2
+    not <> eating
+    00000000 01000000 02000000 03000000 04000000 
+    01000000 01000000 01000000 01000000 01000000
+    flag 0 0x7fb22255e090 -> 0x7fb22255e090 hash 5feba6a0 iter 2
 
-not <> eating
-00000000 01000000 02000000 03000000 04000000 
-01000000 01000000 01000000 01000000 01000000
-flag 0 0x7fb22255e090 -> 0x7fb22255e090 hash 5feba6a0 iter 1
-\end{verbatim}
-\end{itembox}
+    not <> eating
+    00000000 01000000 02000000 03000000 04000000 
+    01000000 01000000 01000000 01000000 01000000
+    flag 0 0x7fb22255e090 -> 0x7fb22255e090 hash 5feba6a0 iter 1
 
 --評価