--- a/paper/GearsOS.tex	Sun Feb 09 15:29:56 2020 +0900
+++ b/paper/GearsOS.tex	Sun Feb 09 18:20:37 2020 +0900
@@ -35,6 +35,7 @@
 メタレベルの変換は Perl スクリプトによる cmake で実装している。
 Gears OS での Meta Code Gear は Code Gear の直前、 直後に挿入され、メタ計算を実行する。
 それぞれの Code Gear, Meta Code Gear の継続には入力される Data Gear(Input Data Gear) と出力されるData Gear(Output Data Gear)が存在する。
+Meta Code Gear は自動生成だけではなく記述することも可能である。そうすることでメタ計算を記述することができるようになったり、goto による継続先を変更することで Geas OS の機能を置き換えることができる。
 Code Gear 間の継続はノーマルレベルでは 図 \ref{fig:codegear} のように見えるが、メタレベルでの Code Gear は図 \ref{fig:meta_cg_dg} の下のように継続を行っている。
 
 
@@ -49,31 +50,42 @@
 
 \section{Context}
  Gears OS の Context は Meta Data Gear であり、接続可能な Code Gear と Data Gear のリスト、 Data Gear を確保するメモリ空間などを持っている。
-従来のスレッドやプロセスに対応する。Gears OS では Code Gear と Data Gear への接続を Context を通して行う。Context が持つ Data Gear のメモリ空間は事前に確保され、Data Gear のメモリ確保の際に heap の値をずらしてメモリを割り当てる。
-% パルスさん3.1
+Gears OS は 必要な Code Gear、 Data Gear を参照したい場合、Context を経由する必要がある。
+しかし、Context をノーマルレベルの計算から直接扱うと書き換えられるリスクが生じる。
+そこで Context から必要なデータを取り出して Code Gear に接続する Meta Code Gear を定義して、間接的に Data Gear にアクセスする。
+この Meta Code Gear を stub Code Gear と呼ぶ。
+stub Code Gear は Code Gear ごとに生成され、生成元の Code Gear の直後に goto で継続される。
 
 
-ノーマルレベルの Code Gaer から Meta Data Gear である Context を直接参照してしまうと、ユーザーがメタ計算をノーマルレベルで自由に記述できてしまい、メタ計算を分離した意味がなくなってしまう。
-この問題を防ぐため、Context から必要な Data Gear のみをノーマルレベルの Code Gear に渡す処理を行なっている。
+Context と stub Code Gear の関係を 図 \ref{fig:context} に示す。
+Code Gear は Context が持つ Data Gear へのポインタを持っており、Context 内のその Data Gear にアクセスする。
 
 
- Meta Code Gear は使用される全ての Code Gear ごとに記述する必要がある。しかし、全ての Code Gear に対して記述すると膨大な記述量になる。そのため、Interface を実装した Code Gear の Meta Code Gear は Perl スクリプトで自動生成する。
-
-
-Meta Code Gear はユーザーが記述することも可能である。そうすることでメタ計算を記述することができるようになったり、goto による継続先を変更することで Geas OS の機能を置き換えることができる。
+ \begin{figure}[ht]
+ \begin{center}
+  \includegraphics[width=160mm]{./fig/Context_ref}
+ \end{center}
+ \caption{Context が持つ Data Gear へのアクセス\cite{mitsuki-master}}
+ \label{fig:context}
+\end{figure}
 
 
- 第5章で扱うメモリ管理部分である vm の Context を ソースコード \ref{contexth} に示す。
 
-\lstinputlisting[label=contexth, caption={\footnotesize 生成された Context}]{./src/context.h}
+
 
-% code は全ての Code Gear を列挙した enum と関数ポインタの組みで表現される。(ソースコード \ref{contexth} 55行目~68行目)
-Code Gear の名前は enum で定義され、コンパイル後には整数で変換される。
-Code Gear に接続する際は enum で定義された番号を指定する。
-これによってメタ計算時に接続する Code Gear を切り替えることができる。
+%  第5章で扱うメモリ管理部分である vm の Context を ソースコード \ref{contexth} に示す。
+
+% \lstinputlisting[label=contexth, caption={\footnotesize 生成された Context}]{./src/context.h}
 
 
-Data Gear のメモリ空間は事前に領域を確保した後、必要に応じて領域を割り当てることで実現する。
-実際に Allocation する際は ソースコード \ref{contexth} 9行目で定義した heap を Data Gear のサイズ分増やすことで実現する。
+% ソースコード載せて説明
+% code は全ての Code Gear を列挙した enum と関数ポインタの組みで表現される。(ソースコード \ref{contexth} 55行目~68行目)
+% Code Gear の名前は enum で定義され、コンパイル後には整数で変換される。
+% Code Gear に接続する際は enum で定義された番号を指定する。
+% これによってメタ計算時に接続する Code Gear を切り替えることができる。
 
 
+% Data Gear のメモリ空間は事前に領域を確保した後、必要に応じて領域を割り当てることで実現する。
+% 実際に Allocation する際は ソースコード \ref{contexth} 9行目で定義した heap を Data Gear のサイズ分増やすことで実現する。
+
+

--- a/paper/cbc_interface.tex	Sun Feb 09 15:29:56 2020 +0900
+++ b/paper/cbc_interface.tex	Sun Feb 09 18:20:37 2020 +0900
@@ -164,6 +164,22 @@
 vm\_impl.cbc の Code Gear であるloaduvmvm\_impl から goto で loaduvm\_ptesize\_checkvm\_impl に遷移する。
 vm.c での最初の if 文までの処理を 1つの Code Gear として loaduvm\_ptesize\_checkvm\_impl に記述する。(3行目~11行目)
 
+
+\section{vm の Context}
+メモリ変換の処理で生成される Context の説明をする。
+code は全ての Code Gear を列挙した enum と関数ポインタの組みで表現される。(ソースコード \ref{contexth} 55行目~68行目)
+Code Gear の名前は enum で定義され、コンパイル後には整数で変換される。
+Code Gear に接続する際は enum で定義された番号を指定する。
+これによってメタ計算時に接続する Code Gear を切り替えることができる。
+
+
+Data Gear のメモリ空間は事前に領域を確保した後、必要に応じて領域を割り当てることで実現する。
+実際に Allocation する際は ソースコード \ref{contexth} の9行目で定義した heap を Data Gear のサイズ分増やすことで実現する。
+
+
+\lstinputlisting[label=contexth, caption={\footnotesize 生成された Context}]{./src/context.h}
+
+
 \section{CbC のループ処理}
  
 CbC では goto での状態遷移によって実装するので loop は if 文を使って実装する。

Binary file paper/fig/Context_ref.graffle has changed

Binary file paper/fig/Context_ref.pdf has changed

Binary file paper/master_paper.pdf has changed

Binary file paper/master_paper.synctex.gz has changed

--- a/paper/master_paper.tex	Sun Feb 09 15:29:56 2020 +0900
+++ b/paper/master_paper.tex	Sun Feb 09 18:20:37 2020 +0900
@@ -103,7 +103,7 @@
 \input{summary.tex}
 
 
-% 
+
 % %謝辞
 \addcontentsline{toc}{chapter}{謝辞}
 \input{thanks.tex}

--- a/paper/memory_manage.tex	Sun Feb 09 15:29:56 2020 +0900
+++ b/paper/memory_manage.tex	Sun Feb 09 18:20:37 2020 +0900
@@ -3,35 +3,35 @@
 実際にパスワードなしで root にアクセスできるバグや、コンピュータの日付の設定を変更するとコンピュータ自体が壊れるバグが発生した。
 
 
- OS 自体に信頼性が求められるが、複雑な機能が多く、短期間のアップデートが必要な OS では、全てのコードに対して検証を行うのは困難である。
-CPU やメモリなどの資源管理は基本的には OS が行なっているため、ユーザーが信頼性を保証こともできない。
+ OS 自体に信頼性が求められるが、複雑な機能が多く、全てのコードに対して検証を行うのは困難である。
+CPU やメモリなどの資源管理は基本的には OS が行なっている。
 これは資源管理が複雑な上、アクセスされたり書き換えられることを防ぐためだと考えられる。
-OS による資源管理によってユーザーは資源を気にすることなくコンピュータを扱うことができる。
 
 
- このように OS には資源管理やシステムコールされた後の処理などユーザーが記述するプログラム以外の部分が存在する。
-その処理をメタレベルの計算、ユーザーが記述する部分をノーマルレベルの計算と呼ぶ。
+ このように OS には資源管理やカーネルの処理などの部分が存在し、
+メタレベルの計算と呼ぶ。それ以外の処理をノーマルレベルの計算と呼ぶ。
 
 
  本研究室ではノーマルレベルとメタレベルの記述を行える CbC というプログラミング言語を開発してきた。
 CbC は Code Gear という基本的な処理の単位と Data Gear というデータの単位を用いる。
-細かい処理に対してノーマルレベルとメタレベルの Code Gear を記述し、その間を関数型プログラミング言語のように goto によって継続する。そのため、状態遷移モデルに落とし込むことができる。
+細かい処理に対してノーマルレベルとメタレベルの Code Gear を記述し、その間を関数型プログラミング言語のように goto によって継続する。
+そのため、状態遷移を基本に記述することができる。
 Code Gear に対して入力の Data Gear と出力の Data Gear が存在し、入力に対して期待される出力がされてるか検査することで信頼性を保証する。
 
 
-モデル検査には定理証明支援系である Agda を用いる。
-Agda は Haure Logic という検証手法を扱うことができる。
-Haure Logic は事前条件を使ってある関数を実行して事後条件を満たすことを確認する検証手法であり、継続に事前条件と事後条件を持たせることのできる CbC と相性がいい。
-
+% モデル検査には定理証明支援系である Agda を用いる。
+% Agda は Haure Logic という検証手法を扱うことができる。
+% Haure Logic は事前条件を使ってある関数を実行して事後条件を満たすことを確認する検証手法であり、継続に事前条件と事後条件を持たせることのできる CbC と相性がいい。
 
  CbC を使って 信頼性の保証と拡張性を持たせる Gears OS の開発を行なっている。
 本論文では、
 % 資源管理を行える CbC で軽量なハードウェアでも動かせるように Arm のバイナリを出力する 
 Xv6 という OS を参考にした Geas OS の書き換えの説明を行う。
-OS の信頼性の基本であるメモリ管理部分を書き換えることで Page のバリデーションチェックによる不正なデータの変更やサンドボックスによるエクセプションをが可能となる。
+OS の信頼性の基本であるメモリ管理部分を書き換えることで信頼性を保証したい。
+具体的にはPage のバリデーションチェックによる不正なデータの変更やサンドボックスによるエクセプションを飛ばすなどが挙げられる。
 また、Gears OS のメタレベルとノーマルレベルでは書き換えなどを防ぐために見えるデータに違いが生じ、Code Gear と Meta Code Gear の記述も煩雑になる。それを解消するために、インターフェースによるモジュール化を導入した。
 % インターフェースは Agda に対応するようになっている。これにより Code Gear、Data Gearんの Agda による証明が可能になるように Geas OS の構築を行った。
-インターフェースを使うことで機能の入れ替えによる拡張性や Agda による証明が可能となることを目的する。
+インターフェースを使うことで検証や機能の入れ替えによる拡張が可能となることを目的する。
 
 % 既存の Gears OS でのメモリ管理では単に Page Table Entry をコピーする Fork を実装
 % しているが、 さらに資源管理を行える CbC で軽量なハードウェアでも動かせるように Arm のバイナリを出力する Xv6 を参考に GearsOS にメモリ管理を行う API を考察する。

--- a/paper/reference.bib	Sun Feb 09 15:29:56 2020 +0900
+++ b/paper/reference.bib	Sun Feb 09 18:20:37 2020 +0900
@@ -1,3 +1,19 @@
+@mastersthesis{
+    mitsuki-master,
+    author = "宮城 光希",
+    title  = "継続を基本とした言語による OS のモジュール化",
+    school = "琉球大学 大学院理工学研究科 情報工学専攻",
+    year   = "2019"
+}
+
+@mastersthesis{
+    parusu-master,
+    author = "伊波 立樹",
+    title  = "Gears OS の並列処理",
+    school = "琉球大学 大学院理工学研究科 情報工学専攻",
+    year   = "2018"
+}
+
 @article{
     cbc,
     author = "Kaito TOKKMORI and Shinji KONO",

--- a/paper/summary.tex	Sun Feb 09 15:29:56 2020 +0900
+++ b/paper/summary.tex	Sun Feb 09 18:20:37 2020 +0900
@@ -1,5 +1,4 @@
 \chapter{まとめ}
-\section{今後の書き換え方針}
 OS 内部で CbCインターフェースを扱えるようになった。
 また、CMake を使った Linux 上で Arm のバイナリを吐けるように Cross Compile を行えるようになった。
 今後 Xv6 全体の CbC による書き換えを行なっていく。

--- a/paper/thanks.tex	Sun Feb 09 15:29:56 2020 +0900
+++ b/paper/thanks.tex	Sun Feb 09 18:20:37 2020 +0900
@@ -1,4 +1,5 @@
 \chapter*{謝辞}
+ 本研究と論文作成にあたり、ご多忙にも関わらず終始懇切なるご指導とご教授を賜わりました河野 真治准教授に心より感謝致します。また、先行研究として関わってくれた先輩方、共に研究を行い支えてくれた並列信頼研のメンバーに感謝いたします。最後に、理工学研究科情報工学専攻の学友、並びに家族に深く感謝いたします。
 
 \begin{flushright}
     2020年 3月 \\ 桃原 優