Mercurial > hg > Papers > 2022 > pine-thesis

changeset 12:538bcf79ca64

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Takato Matsuoka <t.matsuoka@cr.ie.u-ryukyu.ac.jp>
date Mon, 31 Jan 2022 18:18:54 +0900
parents 49d3390d757e
children ae09749b0890
files paper/ie-thesis.sty paper/text/Jabstract.tex paper/text/cbc.tex paper/text/existingDebugger.tex paper/text/gears.tex paper/text/gearsdebugger.tex paper/text/introduction.tex paper/text/reference.tex paper/thesis.pdf
diffstat 9 files changed, 16 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/paper/ie-thesis.sty	Mon Jan 31 02:52:18 2022 +0900
+++ b/paper/ie-thesis.sty	Mon Jan 31 18:18:54 2022 +0900
@@ -50,7 +50,7 @@
 		%\begingroup
 		\renewcommand{\arraystretch}{1.5}
 		\begin{tabular}{c}
-			\textbf{\Large \number\year 年度 卒業論文}\\
+			\textbf{\Large \number2021年度 卒業論文}\\
 			\textbf{\Large Bachelor's Thesis}\\
 		\end{tabular}\\
 		\vspace{3zw}
--- a/paper/text/Jabstract.tex	Mon Jan 31 02:52:18 2022 +0900
+++ b/paper/text/Jabstract.tex	Mon Jan 31 18:18:54 2022 +0900
@@ -7,4 +7,5 @@
 スタックを持たないためにスタックトレースが使えないなどの特性を持つ。
 これらの特性により既存デバッガを用いたデバッグが難しく、エラー・バグの特定が難しいという問題を抱えている。
 
+
 本研究ではGearsOS特化のデバッガを開発することでエラー・バグの発見および修正のコストを下げるとともにさらなるGearsOSの信頼性の向上を目指す。
--- a/paper/text/cbc.tex	Mon Jan 31 02:52:18 2022 +0900
+++ b/paper/text/cbc.tex	Mon Jan 31 18:18:54 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_llvm, cbc_kono}とは、本研究室で開発している軽量継続を導入したC言語の下位言語である。軽量継続とはSchemeのcall/ccなどの環境を持つ継続とは異なり、スタックが無く環境を持たない継続である。そのためcall/ccよりも軽量であることから軽量継続と呼ばれる。
 
 \section{CodeGear}
 CbCは従来のプログラミング言語における関数ではなくCodeGearという単位でプログラムを記述する。プログラムの遷移はCodeGearからCodeGearへの遷移によって実現され、軽量継続であるgoto文を用いて行われる。
@@ -28,6 +28,7 @@
 
 ノーマルレベルから見るとCodeGearが直接InputDataGearからデータを受け取り、プログラム実行、その後OutputDataGearにデータを書き込んでいるように見えるが、実際にはCodeGear実行の前にMetaCodeGearが実行され、MetaCodeGearを経由してDataGearとデータの受け渡しを行っている。メタレベルの計算をMetaCodeGearが行うことで、ノーマルレベルの計算とメタレベルの計算の分離を実現している。MetaCodeGear、MetaDataGearを含めたCodeGearの遷移を図\ref{figs:MetaCodeGear_flow}に示す。
 
+
 \begin{figure}[htbp]
   \begin{center}
    \includegraphics[width=13cm]{./figs/meta-cg-dg.pdf}
--- a/paper/text/existingDebugger.tex	Mon Jan 31 02:52:18 2022 +0900
+++ b/paper/text/existingDebugger.tex	Mon Jan 31 18:18:54 2022 +0900
@@ -3,7 +3,7 @@
 既存デバッガとしてはGDB\cite{gdb}やLLDB\cite{lldb}などがあり、これらの既存デバッガの持つ代表的な機能として以下が挙げられる。
  
  \section{ステップ実行}
- プログラムを1ステップずつ実行させる機能である。これによりプログラムの動作を1つずつ確認することができる。ステップ実行には種類がありステップイン、ステップオーバー、ステップアウトなどがある。
+ プログラムを1ステップずつ実行させる機能である。これによりプログラムの動作を1命令ずつ確認することができる。ステップ実行には種類がありステップイン、ステップオーバー、ステップアウトなどがある。
  
  \section{変数の値の確認}
  現在の状態における変数の確認ができる機能である。変数だけでなく、構造体やクラスなどの値を確認することもできる。これを用いて任意の状態における変数の値を確認することで、プログラマーが意図した処理が正常に実行されているかどうかを確かめることができる。
@@ -11,8 +11,10 @@
  \section{ソースコードの表示}
  プログラムをステップ実行する際にどの行を実行しているかを表示する。
  
+ 
  \section{ブレークポイント}
  ブレークポイントはプログラムの任意の行や関数を指定することでその箇所でプログラムの実行を一時停止する機能である。ブレークポイントを設定して、変数の値の確認など行うことで変数に正しい値が格納されているかどうかなどを確かめることができる。
  
+ 
  \section{スタックトレース}
  スタックトレースとはプログラムの実行手順を確認できる機能で、関数がどのように呼び出されているのかを確認できる。これを使うことでプログラムの実行順を追いやすくなりデバッグ作業を行う上で重要な機能である。
\ No newline at end of file
--- a/paper/text/gears.tex	Mon Jan 31 02:52:18 2022 +0900
+++ b/paper/text/gears.tex	Mon Jan 31 18:18:54 2022 +0900
@@ -1,5 +1,5 @@
 \chapter{GearsOS}
-GearsOSは本研究室で開発しているCbCを用いて信頼性と拡張性の両立を目指したOS\cite{GearsOS}である。CbCと同様にCodeGearとDataGearを基本単位として実行し、ノーマルレベルの計算とメタレベルの計算の分離により信頼性を担保している。
+GearsOSは本研究室で開発しているCbCを用いて信頼性と拡張性の両立を目指したOS\cite{GearsOS, parusuMaster, anaguraMaster}である。CbCと同様にCodeGearとDataGearを基本単位として実行し、ノーマルレベルの計算とメタレベルの計算の分離により信頼性を担保している。
 
 GearsOSは様々な役割を持つCodeGearとDataGearで構成されている。本章では構成の中心となっているMetaDataGearや、モジュール化の仕組みとして導入されているInterfaceについて説明する。
 
@@ -40,7 +40,7 @@
 \begin{figure}[htbp]
   \begin{center}
    \includegraphics[width=12cm]{./figs/transpiler.png}
-   \caption{MetaCodeGearを含めたCodeGearの遷移}
+   \caption{トランスパイラによるCbCファイルの生成}
    \label{figs:transpiler}
    \end{center}
 \end{figure}
--- a/paper/text/gearsdebugger.tex	Mon Jan 31 02:52:18 2022 +0900
+++ b/paper/text/gearsdebugger.tex	Mon Jan 31 18:18:54 2022 +0900
@@ -18,6 +18,7 @@
 \subsection{DataGearの表示}
 CbCのデータ単位であり、GearsOSの基本単位であるDataGearの表示が可能となった。
 表示する際にはprint DataGearを意味するpdコマンドを入力する。また複数存在するDataGearの指定に対応するため、オプションでDataGear名を指定することで特定のDataGearの表示が出来る。表示の際には全てのDataGearの参照ができるcontextを経由して参照を行う。実際にDPPMCで使用されるDataGearであるPhilsの表示結果をソースコード\ref{src:pd_example}に示す。
+ソースコード\ref{src:pd_example}の1行目でプロンプトにpdコマンドを入力することでPhilsの持つDataGear Addressやnextなどのメンバの値が表示される。
 
 \lstinputlisting[label=src:pd_example, caption=pdコマンドを用いたPhilsの表示結果]{src/pd_example.txt}
 
@@ -49,4 +50,6 @@
 \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	Mon Jan 31 02:52:18 2022 +0900
+++ b/paper/text/introduction.tex	Mon Jan 31 18:18:54 2022 +0900
@@ -13,7 +13,7 @@
 そのためプログラムの記述をそのまま状態遷移として落とし込むことができ、これにより定理証明やモデル検査が容易になる。
 
 GearsOSは定理証明やモデル検査により信頼性の保証を行っているが、
-これらの定理証明やモデル検査自体を自分がどう証明したのかを確かめたり、GearsOS上の例題のデバッグしたいということがある。
+これらの定理証明やモデル検査自体を自分がどう証明したのかを確かめたり、GearsOS上の例題をデバッグしたいということがある。
 現状このような場合にはGDB\cite{gdb}やLLDB\cite{lldb}などの既存のデバッガを用いて変数の値の確認や、
 スタックトレースによる関数呼び出しの確認を行うことでデバッグを行っている。
 しかし、GearsOSは変数の格納方法が複雑なため煩雑な記述を行わなければならない特性や、
--- a/paper/text/reference.tex	Mon Jan 31 02:52:18 2022 +0900
+++ b/paper/text/reference.tex	Mon Jan 31 18:18:54 2022 +0900
@@ -2,12 +2,14 @@
 \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_llvm} 並列信頼研究室. Cbc. http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC\_ llvm/. Accessed: 2021-01-31.
 \bibitem{cbc_kono} 河野真治. 継続を持つ c の下位言語によるシステム記述. 日本ソフトウェア科学会第 17 回大会, 2000.
 \bibitem{GearsOS} 河野真治, 伊波立樹, 東恩納琢偉. Code gear、data gear に基づく os のプロトタイ プ. 情報処理学会システムソフトウェアとオペレーティング・システム研究会 (OS), May 2016.
+\bibitem{parusuMaster} 伊波 立樹. Gears OSの並列処理. 琉球大学大学院理工学研究科情報工学専攻修士論文, March 2018.
+\bibitem{anaguraMaster} 清水隆博. GearsOSのメタ計算. 琉球大学大学院理工学研究科情報工学専攻修士論文, March 2021.
 \bibitem{transpiler} 清水隆博. GearsOSのメタ計算. 琉球大学大学院理工学研究科情報工学専攻修士論文, pp.68, March 2021.
 \bibitem{generate_stub} 清水隆博. GearsOSのメタ計算. 琉球大学大学院理工学研究科情報工学専攻修士論文, pp.32, March 2021.
 \bibitem{ikkunMaster} 東恩納琢偉. GearsOS におけるモデル検査を実現する手法について. 琉球大学大学院理工学研究科情報工学専攻修士論文, March2021.
 \bibitem{meta.pm} 清水隆博. GearsOSのメタ計算. 琉球大学大学院理工学研究科情報工学専攻修士論文, pp.77, March 2021.
-\bibitem{parusuMaster} 伊波 立樹. Gears OSの並列処理. 琉球大学大学院理工学研究科情報工学専攻修士論文, March 2018.
 
 \end{thebibliography}
Binary file paper/thesis.pdf has changed