--- a/paper/text/Eabstract.tex	Sat Jan 22 15:00:30 2022 +0900
+++ b/paper/text/Eabstract.tex	Sat Jan 29 20:27:16 2022 +0900
@@ -1,1 +1,10 @@
-ここには英語で要旨を記述する．日本語で記述される卒業論文であってもこの項目を省略することはできない．分量規定はないが，日本語用紙と比較して極端に少ないことがないようにする．
\ No newline at end of file
+Errors and bugs are inevitable in programming, 
+and it is important to find and fix them.
+A debugger is a tool that supports the detection of errors and bugs. 
+By using a debugger, you can check the value of variables and check function calls with stack traces.
+
+In this laboratory, we are developing GearsOS, which is an OS with both reliability and scalability using Continuation Based C (CbC).
+The debugger is also used in the development of GearsOS to find errors and bugs.
+However, GearsOS has some characteristics such as a complicated method of storing variables and the inability to use stack tracing.
+
+This research aims to develop a GearsOS-specific debugger to reduce the cost of finding and fixing errors and bugs, and to further improve the reliability of GearsOS.

--- a/paper/text/Jabstract.tex	Sat Jan 22 15:00:30 2022 +0900
+++ b/paper/text/Jabstract.tex	Sat Jan 29 20:27:16 2022 +0900
@@ -1,1 +1,11 @@
-ここには日本語要旨を記述する．分量の目安は全角300文字以上1ページ以内程度である．本文が英語の場合であっても日本語要旨を記述するものとする．
+プログラミングにおいてエラー・バグは付き物であり、その発見・修正が重要である。
+エラー・バグの発見を支援するツールとしてデバッガがある。デバッガを使うことで変数の値の確認や、
+スタックトレースによる関数呼び出しの確認を行うことでエラー・バグの発見を行う。
+
+本研究室では、Continuation Based C(CbC)を用いて信頼性と拡張性を両立させたOSであるGearsOSの開発を行っている。
+GearsOSの開発においてもエラー・バグの発見のためにデバッガを用いてデバッグを行っている。
+しかし、GearsOSは変数の格納方法が複雑なため煩雑な記述を行わなければならない特性や、
+スタックを持たないためにスタックトレースが使えないなどの特性を持つ。
+これらの特性により既存デバッガを用いたデバッグが難しく、エラー・バグの特定が難しいという問題を抱えている。
+
+本研究ではGearsOS特化のデバッガを開発することでエラー・バグの発見および修正のコストを下げるとともにさらなるGearsOSの信頼性の向上を目指す。

--- a/paper/text/cbc.tex	Sat Jan 22 15:00:30 2022 +0900
+++ b/paper/text/cbc.tex	Sat Jan 29 20:27:16 2022 +0900
@@ -1,5 +1,5 @@
 \chapter{Continuation Based C}
-Continuation Based C(以下CbC)\cite{cbc_kono}とは、本研究室で開発している軽量継続を導入したC言語の下位言語である。軽量継続とはSchemeのcall/ccなどの環境を持つ継続とは異なり、スタックが無く環境を持たない継続である。そのためcall/ccよりも軽量であることから軽量継続と呼ばれる。
+Continuation Based C(CbC)\cite{cbc_kono}とは、本研究室で開発している軽量継続を導入したC言語の下位言語である。軽量継続とはSchemeのcall/ccなどの環境を持つ継続とは異なり、スタックが無く環境を持たない継続である。そのためcall/ccよりも軽量であることから軽量継続と呼ばれる。
 
 \section{CodeGear}
 CbCは従来のプログラミング言語における関数ではなくCodeGearという単位でプログラムを記述する。プログラムの遷移はCodeGearからCodeGearへの遷移によって実現され、軽量継続であるgoto文を用いて行われる。

--- a/paper/text/gears.tex	Sat Jan 22 15:00:30 2022 +0900
+++ b/paper/text/gears.tex	Sat Jan 29 20:27:16 2022 +0900
@@ -1,11 +1,8 @@
 \chapter{GearsOS}
 GearsOSは本研究室で開発しているCbCを用いて信頼性と拡張性の両立を目指したOS\cite{GearsOS}である。CbCと同様にCodeGearとDataGearを基本単位として実行し、ノーマルレベルの計算とメタレベルの計算の分離により信頼性を担保している。
 
-\section{GearsOSの構成・アーキテクチャ}
 GearsOSは様々な役割を持つCodeGearとDataGearで構成されている。本章では構成の中心となっているMetaDataGearや、モジュール化の仕組みとして導入されているInterfaceなどについて説明を行う。
 
-TODO: Gearsの構成図を書いて貼る
-
 \section{Context}
 ContextとはGearsOSの計算に必要なCodeGearやDataGearを持つMetaDataGearであり、従来のOSにおけるプロセスやスレッドに対応する。Contextは使用可能なCodeGearとDataGearのリストや、TaskQueueへのポインタ、DataGearを格納するためのメモリ空間などを持っている。ソースコード\ref{src:def_context}がContextの定義である。
 

--- a/paper/text/gearsdebugger.tex	Sat Jan 22 15:00:30 2022 +0900
+++ b/paper/text/gearsdebugger.tex	Sat Jan 29 20:27:16 2022 +0900
@@ -1,8 +1,6 @@
 \chapter{GearsDebugger}
 本研究では、GearsOSに特化したデバッガとしてGearsDebuggerの開発を行った。本章ではGearsDebuggerの持つ機能や仕組みについて記述する。
 
-TODO: Gearsの場合、前章の既存デバッガを使うにあたってどういう問題があるのかを提起する。
-
 \section{GearsDebuggerの持つ機能}
 GearsDebuggerの持つ機能として以下が挙げられる。
 
@@ -41,17 +39,11 @@
 
 2つ目の違いとしては、DebugTaskManagerはメモリ状態を保存するためのDBであるstateDBの情報を持つ。
 
-\section{debugMeta}
+\section{debugMeta} \label{debugMeta}
 \ref{DebugWorker}でDebugWorker内にdebugMetaを作成したが、そのdebugMetaの行う処理について記述していく。
-debugMetaはデバッグ処理におけるユーザーインプット部分を担うMetaCodeGearである。GearsDebuggerは1つのCodeGearの実行後にDataGearの表示などデバッグ情報を見たい。そのため、各CodeGearの呼び出し後にdebugMetaを呼び出すことでユーザーに入力を促す。これによって各CodeGear実行後にデバッグを行うことができる。各CodeGearの呼び出し後にdebugMetaを呼び出す方法については、meta.pm\cite{meta.pm}というGearsOSのビルドシステムのAPIを用いている。通常はCodeGear実行後、次のCodeGearのStubCodeGearへと遷移するが、meta.pmを使うことでCodeGear実行後の遷移先を特定のMetaCodeGearへと変更することができる。ソースコード\ref{src:meta.pm}にmeta.pmを示す。ソースコード\ref{src:meta.pm}の7行目にqr/HelloImpl/と正規表現がある。トランスパイラはこの正規表現にマッチしたCodeGearのgoto先を切り替えている。例でいうと、HelloImplという文字列を含むCodeGearがあった場合、ソースコード\ref{src:meta.pm} 13行目のサブルーチンgeneratedebugMetaを呼び出し、goto先をdebugMetaへと切り替えている。
+debugMetaはデバッグ処理におけるユーザーインプット部分を担うMetaCodeGearである。GearsDebuggerは1つのCodeGearの実行後にDataGearの表示などデバッグ情報を見たい。そのため、各CodeGearの呼び出し後にdebugMetaを呼び出すことでユーザーに入力を促す。これによって各CodeGear実行後にデバッグを行うことができる。
+
+\section{meta.pm}
+\ref{debugMeta}にて各CodeGearの呼び出し後にdebugMetaを呼び出すと説明したが、その呼び出し方法としてmeta.pm\cite{meta.pm}というGearsOSのビルドシステムのAPIを用いている。通常はCodeGear実行後、次のCodeGearのStubCodeGearへと遷移するが、meta.pmを使うことでCodeGear実行後の遷移先を特定のMetaCodeGearへと変更することができる。ソースコード\ref{src:meta.pm}にmeta.pmを示す。ソースコード\ref{src:meta.pm}の7行目にqr/HelloImpl/と正規表現がある。トランスパイラはこの正規表現にマッチしたCodeGearのgoto先を切り替えている。例でいうと、HelloImplという文字列を含むCodeGearがあった場合、ソースコード\ref{src:meta.pm} 13行目のサブルーチンgeneratedebugMetaを呼び出し、goto先をdebugMetaへと切り替えている。
 
 \lstinputlisting[label=src:meta.pm, caption=meta.pm]{src/meta.pm}
-
-
-
-
-
-
-
-
-

--- a/paper/text/introduction.tex	Sat Jan 22 15:00:30 2022 +0900
+++ b/paper/text/introduction.tex	Sat Jan 29 20:27:16 2022 +0900
@@ -1,10 +1,23 @@
-\chapter{序論}
-本章は，標準として「背景と目的」および「論文の構成」の2節で構成される．分量の規定はないが，2節合わせて2$\sim $3ページ程度が標準的である．
+\chapter{GearsOSにおけるデバッグ}
+
+OSはCPUの割り当てやスケジュール、記憶容量へのアクセスなどアプリケーションが動作する上で土台となる重要なソフトウェアである。
+そのためOSの信頼性は高く保証されている必要がある。
+信頼性を保証する方法として形式検証が挙げられる。
+形式検証には定理証明とモデル検査があり、定理証明はAgda\cite{agda}などの定理証明支援系を用いて数学的にプログラムの信頼性を保証する。
+モデル検査はプログラムが特定の状態から遷移しうる全ての状態を数え上げ、
+仕様を満たしているかどうかを検査することでプログラムの信頼性を保証する。
 
-\section{背景と目的}
-この節には，研究の背景と目的を記述する．研究の社会的もしくは学術的な意義を明らかにするものとする．
+本研究室では定理証明やモデル検査を用いて信頼性の保証を行うGearsOSの開発を行っている。
+GearsOSはContinuation Based C(CbC)を用いて記述したOSで、CbCは本研究室で開発している言語で、CodeGearというプログラム単位で記述・遷移するC言語の下位言語である。
+CodeGear間の遷移は通常の関数呼び出しではなく、goto文によって行われるため、呼び出し元へ戻らない。
+そのためプログラムの記述をそのまま状態遷移として落とし込むことができ、これにより定理証明やモデル検査が可能である。
 
-\section{論文の構成}
-この節では，卒業論文の全体構成を述べる．論文の構成は研究分野によって異なるので，指導教員と調整すると良い．その上で，卒業論文の内容に従って以下の例のように論文の構成を記述しなさい．この記述形式でないといけないということではないので，各自で適切に調整しなさい．
+GearsOSは定理証明やモデル検査により信頼性の保証を行っているが、
+これらの定理証明やモデル検査自体を自分がどう証明したのかを確かめたり、GearsOS上の例題のデバッグしたいということがある。
+現状このような場合にはGDB\cite{gdb}やLLDB\cite{lldb}などの既存のデバッガを用いて変数の値の確認や、
+スタックトレースによる関数呼び出しの確認を行うことでデバッグを行っている。
+しかし、GearsOSは変数の格納方法が複雑なため煩雑な記述を行わなければならない特性や、
+スタックを持たないためにスタックトレースが使えないなどの特性を持つ。これらの特性によりプログラムの遷移の流れや、
+変数の値の変化など既存デバッガを用いたデバッグが難しいという問題がある。
 
-本論文は以下の章で構成される．第1章の○○(○○に章タイトルを記述する)に続き，第2章の関連研究では△△△について述べる．第3章では，□□□について本論文で新たに提案する手法について述べる．第4章では，提案手法での植物形態の三次元再構成精度検証実験について述べるとともに，既存の研究結果との比較考察を述べる．最後に，第5章で本論文のまとめと今後の展望について述べる．
+本研究ではGearsOS特化のデバッガを開発することでエラー・バグの発見および修正のコストを下げるとともにさらなるGearsOSの信頼性の向上を目指す。

--- a/paper/text/reference.tex	Sat Jan 22 15:00:30 2022 +0900
+++ b/paper/text/reference.tex	Sat Jan 29 20:27:16 2022 +0900
@@ -1,10 +1,11 @@
 \begin{thebibliography}{99}
+\bibitem{agda} Ulf Norell. Dependently typed programming in agda. pp. 1\\UTF{2013}2, 2009
 \bibitem{gdb} https://www.gnu.org/software/gdb/
 \bibitem{lldb} https://lldb.llvm.org/
+\bibitem{cbc_kono} 河野真治. 継続を持つ c の下位言語によるシステム記述. 日本ソフトウェア科学会第 17 回大会, 2000.
 \bibitem{ikkunMaster} 東恩納琢偉. GearsOS におけるモデル検査を実現する手法について. 琉球大学大学院理工学研究科情報工学専攻修士論文, March2021.
 \bibitem{stateDB} 東恩納琢偉. GearsOS におけるモデル検査を実現する手法について. 琉球大学大学院理工学研究科情報工学専攻修士論文, pp.13, March2021.
 \bibitem{GearsDebugger} 東恩納琢偉. GearsOS におけるモデル検査を実現する手法について. 琉球大学大学院理工学研究科情報工学専攻修士論文, pp26-27, March 2021.
-\bibitem{cbc_kono} 河野真治. 継続を持つ c の下位言語によるシステム記述. 日本ソフトウェア科学会第 17 回大会, 2000.
 \bibitem{GearsOS} 河野真治, 伊波立樹, 東恩納琢偉. Code gear、data gear に基づく os のプロトタイ プ. 情報処理学会システムソフトウェアとオペレーティング・システム研究会 (OS), May 2016.
 \bibitem{cmake} https://cmake.org/
 \bibitem{parusuMaster} 伊波 立樹. Gears OSの並列処理. 琉球大学大学院理工学研究科情報工学専攻修士論文, March 2018.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/text/summary.tex	Sat Jan 29 20:27:16 2022 +0900
@@ -0,0 +1,20 @@
+\chapter{結論}
+本研究では、GearsOSに特化したデバッガの作成を行った。CodeGear単位で遷移を行うGearsOSのデバッグを行うために、CodeGear単位でプログラムを一時停止させ、デバッグコマンドを入力することでDataGearの値を見ることが可能となった。また、デバッグ用のWorkerとTaskManagerを作成し、通常のWorkerとTaskManagerと変更することで、様々な例題を対象としてDataGearの値を確認することが可能となった。
+
+\section{今後の課題}
+今後の課題としてデバッガ呼び出し手順の煩雑さが挙げられる。現状でデバッガを呼び出すには通常のWorkerとTaskManagerからデバッグ用のWorker、TaskManagerへの入れ替えや、meta.pmの記述・配置、debugMetaのプロトタイプ宣言の記述を行い、再ビルドを行う必要がある。
+WorkerやTaskManagerに関しては、通常のWorkerやTaskManagerをデバッグ用に拡張させ、例題実行時にオプションとしてデバッグオプションを指定することで振る舞いを通常の振る舞いからデバッグ用へと分岐させることが可能だと考えられる。またmeta.pmやdebugMetaに関してはGearsOSのビルドシステムであるgenerate\_stub.plやgenerate\_context.pl側でデバッグオプションの有無により継続を先を変更することが出来れば、通常の例題を再ビルドさせることなく、オプションの有無によって通常実行とデバッグ実行を切り替えられると考える。
+
+\begin{comment}
+\begin{itemize}
+	\item Worker, TaskManagerの入れ替え
+	\item meta.pmの配置
+	\item debugMetaのプロトタイプ宣言
+\end{itemize}
+\begin{itemize}
+     \item デバッガ呼び出し時の煩雑さ
+      \item トレース機能の実装
+      \item 再実行機能
+\end{itemize}
+\end{comment}
+

Binary file paper/thesis.pdf has changed

--- a/paper/thesis.tex	Sat Jan 22 15:00:30 2022 +0900
+++ b/paper/thesis.tex	Sat Jan 29 20:27:16 2022 +0900
@@ -59,8 +59,8 @@
 % 図目次，図がある場合のみ
 \listoffigures
 
-% 表も軸，表がある場合のみ
-\listoftables
+% 表目次，表がある場合のみ
+%\listoftables
 
 % pagecounter settings
 \setcounter{page}{0}	%Don't remove.
@@ -81,9 +81,10 @@
 
 \include{./text/gearsdebugger}
 
-\chapter{まとめと今後の展望}
+\include{./text/summary}
 
 \chapter*{謝辞}
+本研究の遂行、本論文の作成にあたり、御多忙にも関わらず終始懇切なる御指導と御教授を賜わりました河野真治准教授に心より感謝致します。そして、 共に研究を行い暖かな気遣いと励ましをもって支えてくれた並列信頼研究室の全てのメンバーに感謝致します。 最後に、有意義な時間を共に過ごした知能情報コースの学友、並びに物心両面で支えてくれた家族に深く感謝致します。
 
 % reference
 \include{./text/reference}