--- a/paper/evaluation.tex	Tue Feb 12 07:20:51 2019 +0900
+++ b/paper/evaluation.tex	Tue Feb 12 08:05:32 2019 +0900
@@ -75,4 +75,40 @@
 また、stub Code Gear は Code Gear 毎に挿入されるため、               
 これが自動生成されることによってソースコードの記述量が大幅に減少した。
 
+\section{xv6 の CbC 書き換えのための環境構築}
+xv6-rpi の CbC 書き換えを行うために、ARM 用のクロスコンパイラを build する必要があった。
+しかし、LLVM 上で実装した CbC では上手くいかなかったため、GCC 上で実装した CbC を用いることにした。
+GCC 上で実装した CbC は更新が止まっていたため、現在の GCC へのアップデート作業を行なった。
 
+これにより、GCC 上で実装された CbC が、最新の環境で動作するようになり、
+ARM 用のクロスコンパイラの build も可能となった。
+
+\section{xv6 の CbC 書き換え}
+
+CbC は Code Gear 間の遷移は goto による継続で行われるため、
+状態遷移ベースでのプログラムに適している。
+xv6 を CbC で書き換えることにより、実行可能な OS のプログラムを状態遷移モデルに落とし込むことができる。
+これにより状態遷移系のモデル検査が可能となる。
+
+xv6 のシステムコールを CbC によって書き換えることで、
+元の C のソースコードからの大きな変更をすることなしに、
+図 \ref{fig:state} のように状態遷移ベースの実行可能なプログラムへと落とし込むことができた。
+
+\begin{figure}[ht]
+ \begin{center}
+  \includegraphics[width=150mm]{fig/state.pdf}
+ \end{center}
+ \caption{read システムコールの遷移図}
+ \label{fig:state}
+\end{figure}
+
+また、CbC は C 言語との互換があるため、システムコールのみ CbC へと書き換えるといったことも可能であるため、
+信頼性を保証したい機能のみを CbC で記述することもできる。
+
+さらに、CbC は Agda に変換できるように設計されているため CbC で記述された実行可能なプログラムが、
+そのまま Agda による定理証明が可能となる。
+
+これらのため、CbC で記述された実行可能な OS そのものがモデル検査と定理証明が可能となり、
+OS の信頼性が保証できる。
+
+

--- a/paper/generate_code.tex	Tue Feb 12 07:20:51 2019 +0900
+++ b/paper/generate_code.tex	Tue Feb 12 08:05:32 2019 +0900
@@ -64,6 +64,7 @@
 生成された stub  Code Gear は、
 継続先の Code Gear が引数で指定した Input Data Gear、Output Data Gear を Context から参照している。
 Gearef は Context から Data Gear を参照するためのマクロである。
+ソースコード\ref{macro} 1行目が Gearef マクロの定義である。
 ソースコード\ref{noref} はマクロを用いなかった場合の pop stack の stub Code Gear である。
 Context には Allocation 等で生成した Data Gear へのポインタが格納されている。
 Code Gear が Context にアクセスする際、
@@ -74,10 +75,14 @@
 
 GearImpl マクロは Interface の型に包まれた Data Gear から
 実装の Data Gear を取り出すためのマクロである。
+ソースコード\ref{macro} 2行目が GearImpl マクロの定義である。
 実装の Data Gear を取り出す際も、ポインタでの記述が複雑になってしまうため 同様に GearImpl を定義した。
 GearImpl は Context と Interface の型、実装の Data Gear 名を指定することで参照する。
 
-% 変換前のコードも入れる
+\begin{lstlisting}[frame=lrbt,label=macro,caption={Gearef、GearImpl}]
+#define Gearef(context, t) (&(context)->data[D_##t]->t)
+#define GearImpl(context, intf, name) (Gearef(context, intf)->name->intf.name)
+\end{lstlisting}
 
 \begin{lstlisting}[frame=lrbt,label=noref,caption={マクロを用いない stub Code Gear}]
 __code popSingleLinkedStack_stub(struct Context* context) {

Binary file paper/master_paper.pdf has changed