# HG changeset patch
# User tobaru
# Date 1581587688 -32400
# Node ID 455e756bfe1a79fe6d2b023b1851547ed8b3d08b
# Parent  fe7b1222efd87222ddbe7490adf8be353327b568
add Quote

diff -r fe7b1222efd8 -r 455e756bfe1a paper/GearsOS.tex
--- a/paper/GearsOS.tex	Wed Feb 12 17:05:12 2020 +0900
+++ b/paper/GearsOS.tex	Thu Feb 13 18:54:48 2020 +0900
@@ -1,6 +1,7 @@
 \chapter{CbC による Geas OS の開発}
   信頼性の保証と並列実行のサポートを目的として、 本研究室では CbC というプログラミング言語を開発してきた。
- さらにその CbC を使って Gears OS を開発している。
+LLVM\cite{llvm} 上で実装された CbC と GCC\cite{gcc} 上で実装された CbC が存在する。
+ さらにその CbC を使って Gears OSを開発している。
 従来の OS が行うメモリ管理並列実行は Meta レベル(kernel space)で処理される。
 ノーマルレベルからメタレベルの記述ができる GearsOS を開発している。
 
diff -r fe7b1222efd8 -r 455e756bfe1a paper/Xv6.tex
--- a/paper/Xv6.tex	Wed Feb 12 17:05:12 2020 +0900
+++ b/paper/Xv6.tex	Thu Feb 13 18:54:48 2020 +0900
@@ -1,5 +1,5 @@
-\chapter{Xv6}
- Xv6 とは、マサチューセッツ工科大の大学院生向け講義の教材として使うために、UNIX V6 という OS を ANSI-C(規格化されたC言語) に書き換え、x86 に移植した Xv6 OS である。
+\chapter{x.v6}
+ x.v6 とは、マサチューセッツ工科大の大学院生向け講義の教材として使うために、UNIX V6 という OS を ANSI-C(規格化されたC言語) に書き換え、x86 に移植した Xv6 OS である。
 
 
 
@@ -20,7 +20,7 @@
 \ref{syscall_list} 
  に示す。
 
-\begin{lstlisting}[frame=lrbt,label=syscall_list,caption={\footnotesize xv6 のシステムコールのリスト}]
+\begin{lstlisting}[frame=lrbt,label=syscall_list,caption={\footnotesize x.v6 のシステムコールのリスト\cite{mitsuki-master}}]
 static int (*syscalls[])(void) = {
         [SYS_fork]    =sys_fork,
         [SYS_exit]    =sys_exit,
diff -r fe7b1222efd8 -r 455e756bfe1a paper/master_paper.pdf
Binary file paper/master_paper.pdf has changed
diff -r fe7b1222efd8 -r 455e756bfe1a paper/master_paper.synctex.gz
Binary file paper/master_paper.synctex.gz has changed
diff -r fe7b1222efd8 -r 455e756bfe1a paper/memory_manage.tex
--- a/paper/memory_manage.tex	Wed Feb 12 17:05:12 2020 +0900
+++ b/paper/memory_manage.tex	Thu Feb 13 18:54:48 2020 +0900
@@ -12,7 +12,7 @@
 メタレベルの計算と呼ぶ。それ以外の処理をノーマルレベルの計算と呼ぶ。
 
 
- 本研究室ではノーマルレベルとメタレベルの記述を行える CbC というプログラミング言語を開発してきた。
+ 本研究室ではノーマルレベルとメタレベルの記述を行える CbC\cite{cbc} というプログラミング言語を開発してきた。
 CbC は Code Gear という基本的な処理の単位と Data Gear というデータの単位を用いる。
 細かい処理に対してノーマルレベルとメタレベルの Code Gear を記述し、その間を関数型プログラミング言語のように goto によって継続する。
 そのため、状態遷移を基本に記述することができる。
@@ -23,13 +23,13 @@
 % Agda は Haure Logic という検証手法を扱うことができる。
 % Haure Logic は事前条件を使ってある関数を実行して事後条件を満たすことを確認する検証手法であり、継続に事前条件と事後条件を持たせることのできる CbC と相性がいい。
 
- CbC を使って 信頼性の保証と拡張性を持たせる Gears OS の開発を行なっている。
+ CbC を使って 信頼性の保証と拡張性を持たせる Gears OS\cite{gears} の開発を行なっている。
 本論文では、
 % 資源管理を行える CbC で軽量なハードウェアでも動かせるように Arm のバイナリを出力する 
-Xv6 という OS を参考にした Geas OS の書き換えの説明を行う。
+x.v6\cite{xv6} という OS を参考にした Geas OS の書き換えの説明を行う。
 OS の信頼性の基本であるメモリ管理部分を書き換えることで信頼性を保証したい。
 具体的にはPage のバリデーションチェックによる不正なデータの変更やサンドボックスによるエクセプションを飛ばすなどが挙げられる。
-また、Gears OS のメタレベルとノーマルレベルでは書き換えなどを防ぐために見えるデータに違いが生じ、Code Gear と Meta Code Gear の記述も煩雑になる。それを解消するために、インターフェースによるモジュール化を導入した。
+また、Gears OS のメタレベルとノーマルレベルでは書き換えなどを防ぐために見えるデータに違いが生じ、Code Gear と Meta Code Gear の記述も煩雑になる。それを解消するために、インターフェースによるモジュール化を導入\cite{mitsuki-master}した。
 % インターフェースは Agda に対応するようになっている。これにより Code Gear、Data Gearんの Agda による証明が可能になるように Geas OS の構築を行った。
 インターフェースを使うことで検証や機能の入れ替えによる拡張が可能となることを目的する。