changeset 4:e94e544fce5c

...
author matac42 <matac@cr.ie.u-ryukyu.ac.jp>
date Sat, 15 Jan 2022 16:50:14 +0900
parents ff22de05cde1
children 47c5e331d020
files .hgignore paper/figs/meta-cg-dg.pdf paper/figs/wordCountStates.pdf paper/src/hello.cbc paper/text/Eabstract.tex paper/text/Jabstract.tex paper/text/chapter2.tex paper/text/introduction.tex paper/text/reference.tex paper/thesis.bib paper/thesis.pdf paper/thesis.tex
diffstat 12 files changed, 198 insertions(+), 47 deletions(-) [+]
line wrap: on
line diff
--- a/.hgignore	Wed Jan 05 20:22:26 2022 +0900
+++ b/.hgignore	Sat Jan 15 16:50:14 2022 +0900
@@ -295,4 +295,7 @@
 # glossaries
 *.glstex
 
+# latex vscode generate file
+__latexindent*
+
 # End of https://www.toptal.com/developers/gitignore/api/tex
\ No newline at end of file
Binary file paper/figs/meta-cg-dg.pdf has changed
Binary file paper/figs/wordCountStates.pdf has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/hello.cbc	Sat Jan 15 16:50:14 2022 +0900
@@ -0,0 +1,18 @@
+__code add1(int in_n) {
+    int out_n = n + 1;
+    goto add2(out_n);
+}
+
+__code add2(int in_n) {
+    int out_n = n + 2;
+    goto end(out_n);
+}
+
+__code end(int in_n) {
+    printf("%d", n);
+}
+
+int main(int argc, char *arcv[]) {
+    int n = 1;
+    goto add1(n);
+}
\ No newline at end of file
--- a/paper/text/Eabstract.tex	Wed Jan 05 20:22:26 2022 +0900
+++ b/paper/text/Eabstract.tex	Sat Jan 15 16:50:14 2022 +0900
@@ -1,1 +1,7 @@
-ここには英語で要旨を記述する.日本語で記述される卒業論文であってもこの項目を省略することはできない.分量規定はないが,日本語用紙と比較して極端に少ないことがないようにする.
\ No newline at end of file
+Ensuring the reliability of applications is an important issue for ensuring the reliability of information systems and operations that use computers. In order to guarantee the reliability of applications, it is necessary to improve the reliability of the underlying operating system. Theorem proving and model checking are the methods to guarantee the reliability.
+
+In our laboratory, we are developing GearsOS for the purpose of guaranteeing reliability by theorem proving and model checking. GearsOS is written in Continuation Based C (CbC), which can separate normal-level and meta-level processing, and has the programming concept of Gear. GearsOS is written in Continuation Based C (CbC), which can separate normal-level and meta-level processing.
+
+There are currently unimplemented features in GearsOS, one of which is the file system. We would like to implement a file system for GearsOS that can guarantee reliability through model checking.
+
+In this paper, we first introduce the basic concept of the file system construction of GearsOS, and then describe the concrete construction method of the file system of GearsOS.
\ No newline at end of file
--- a/paper/text/Jabstract.tex	Wed Jan 05 20:22:26 2022 +0900
+++ b/paper/text/Jabstract.tex	Sat Jan 15 16:50:14 2022 +0900
@@ -1,1 +1,16 @@
-ここには日本語要旨を記述する.分量の目安は全角300文字以上1ページ以内程度である.本文が英語の場合であっても日本語要旨を記述するものとする.
+アプリケーションの信頼性を保証することは
+情報システムやコンピュータを用いる業務の信頼性の保障につながる重要な課題である.
+アプリケーションの信頼性を保証するために,基盤となるOSの信頼性を高める必要がある.
+信頼性を保証するための手法として定理証明やモデル検査が挙げられる.
+
+当研究室では,定理証明やモデル検査による信頼性の保証を目的としたGearsOSを開発している.
+GearsOSはノーマルレベル,メタレベルの処理を切り分けることができる
+Continuation Based C(CbC)で記述されており,Gearというプログラミング概念を持つ.
+CbCでメタレベルの処理を切り出したものに対して定理証明やモデル検査を行うことで
+信頼性を保証する\cite{modelcheck}.
+
+GearsOSには現在未実装の機能があり,その一つにファイルシステムが挙げられる.
+信頼性をモデル検査を通して保証することができるGearsOSのファイルシステムを実装したい.
+
+本論文では,まずGearsOSのファイルシステム構築に関する基礎概念の紹介をし,
+その後GearsOSのファイルシステムの具体的な構築方法について述べる.
\ No newline at end of file
--- a/paper/text/chapter2.tex	Wed Jan 05 20:22:26 2022 +0900
+++ b/paper/text/chapter2.tex	Sat Jan 15 16:50:14 2022 +0900
@@ -1,14 +1,69 @@
 \chapter{Continuation based C}
+Continuation based C(CbC)\cite{cbcllvm,cbc}とはCの下位言語である.
+function callの代わりにgotoによる継続を用いる.
+CbCのプログラムはCodeGearと呼ばれる処理の単位で記述し,ノーマルレベルとメタレベルの処理を切り分けることが可能である.
+
 \section{CodeGearとDataGear}
+CbCでは関数の代わりにCodeGearという単位でプログラミングを行う.
+CodeGearは\emph{\_\_code}という記述で宣言することができる.
+データの単位にはDataGearと呼ばれる変数データを用いる.
+DataGearを入力として受け取り,別のDataGearに書き込み出力することができる.
+特に入力のDataGearをInput DataGear,出力のDataGearをOutput DataGearと呼ぶ.
+gotoで次のCodeGearに遷移することができ,その際Output DataGearを次のCodeGearのInput DataGearとして渡すことができる.
+
 \section{ノーマルレベルとメタレベル}
-\section{継続性}
+図\ref{fig:meta-cgdg}はCodeGearの遷移とMetaCodeGearの関係を表している.
+ノーマルレベルで見るとCodeGearがDataGearを受け取り,
+処理後,DataGearを次のCodeGearに渡すという動作をしているように見える.
+実際にはデータの整合性の確認や資源管理などのメタレベルの処理が存在し,
+それらの計算はMetaCodeGearで行われる.
+その際,MetaCodeGearに渡されるDataGearのことは特にMetaDataGearと呼ばれる.
+CodeGearの前に実行されるMetaCodeGearは特にstubCodeGearと呼ばれ,
+メタレベルを含めるとstubCodeGearとCodeGearを交互に実行する形で遷移していく.
+\begin{figure}[h]
+  \begin{center}
+      \includegraphics[width=100mm]{figs/meta-cg-dg.pdf}
+  \end{center}
+      \caption{CodeGearとMetaCodeGearの関係}
+  \label{fig:meta-cgdg}
+\end{figure}
+
+\section{継続}
+CodeGearから次のCodeGearに遷移していく一連の動作を継続と呼ぶ.
+CbCの継続はfunction callをせずにgotoによるjmpで行われる.
+function callによる継続と異なり,jmpによる継続はstackなどの環境を保存しないことから軽量である.
+そのことからCbCにおける継続を特に軽量継続と呼ぶ.
+
+\section{CbCの記述例}
+CbCのプログラム例をソースコード\ref{src:cbc}に示す.まずmain関数においてadd1 CodeGearへgotoを行う.
+その際add1へInput DataGearとしてnを渡す.
+add1は処理の最後にadd2 CodeGearへgotoを行う.
+その際Output DataGear out\_nをadd2のInput DataGearとして渡す.
+このようにCbCではCodeGearのOutput DataGearを次のCodeGearのInput DataGearとして渡すことを繰り返すことで処理を進める.
+
+\lstinputlisting[caption=CbCのプログラム例,label=src:cbc]{src/hello.cbc}
+
 
 \chapter{GearsOS}
+GearsOS\cite{gears,gearsos,cr}は 信頼性と拡張性の両立を目的として,開発されている.
+Gearという概念があり,実行の単位をCodeGear,データの単位をDataGearと呼ぶ.
+軽量継続を基本とし,stackを持たない代わりに全てをContext経由で実行する.
+ノーマルレベルとメタレベルの処理を切り分けることができ,同様にGearの概念を持つCbC(Continuation based C)で記述されている.
+GearsOSは現在開発途上であり,OSとして動作するために今後実装しなければならない機能がいくつか残っている.
 \section{信頼性の保証}
 \section{stub}
 \section{context}
 
 \chapter{Christie}
+Christieは当研究室で開発を行っているJavaで記述された分散フレームワークである.
+CodeGear,DataGear,CodeGearManager,DataGearManagerなどのCbCと似ているが別物のGearという概念を持つ.
+CodeGearはクラスやスレッドに相当する.DataGearは変数データに相当し,Javaのアノテーションを用いて記述される.
+CodeGearManagerはいわゆるノードに相当し,CodeGear,DataGear,DataGearManagerを管理する.
+複数のCodeGearManager同士が配線され,DataGearを送信し合うことで分散処理を実現している.
+DataGearManagerはDataGearを管理しているもので変数プールに相当する.
+GearsOSではDataGearManagerの仕組みをファイルシステムとして用いたい.
+さらに,ChristieにはTopologyを形成するためのTopologyManagerがある.
+TopologyManagerはCodeGearManagerを任意の形のTopologyに接続する機能を持っている.
 \section{Gearの概念}
 \section{DataGearManager}
 \section{topology manager}
@@ -30,6 +85,12 @@
 \section{logによるバージョン管理}
 
 \chapter{WordCount}
+WordCount例題\cite{file}はGearsOSのファイルシステムを構築する際に用いてる例題である.
+指定したファイルの文字数や行数,ファイルの内の文字列を出力する.
+図\ref{fig:WCStates}はWordCount例題の処理の流れを示している.
+大きく分けて,指定したファイルをFile構造体としてopenするFileOpenスレッド,
+File構造体を受け取り文字数と行数をcountUpするWordCountスレッドの二つのCodeGearで記述することができる.
+ファイル内の文字列を行ごとにCountUpに送信し,EOFを受け取ったらループを抜けfinishに移行する.
 \section{API}
 \section{GearBox的な処理}
 
--- a/paper/text/introduction.tex	Wed Jan 05 20:22:26 2022 +0900
+++ b/paper/text/introduction.tex	Sat Jan 15 16:50:14 2022 +0900
@@ -1,1 +1,4 @@
-\chapter{GearsOSにおけるFileSystem}
\ No newline at end of file
+\chapter{GearsOSにおけるFileSystem}
+FileSystemはOSにおける重要な機能の一つである.
+しかしながら,GearsOSは開発途上でFileSystemは未実装であるため,実装する必要がある.
+実装はUnixにおけるFileSystemと比較・検討しながら進める.
\ No newline at end of file
--- a/paper/text/reference.tex	Wed Jan 05 20:22:26 2022 +0900
+++ b/paper/text/reference.tex	Sat Jan 15 16:50:14 2022 +0900
@@ -1,41 +0,0 @@
-\begin{thebibliography}{99}
-\bibitem{ref-related-work}
-論文の読み方・書き方, 金森 由博, \url{http://kanamori.cs.tsukuba.ac.jp/docs/how_to_read_and_write_papers.html}, 2021/09/28.
-
-\bibitem{ref-jsps} 
-研究者のみなさまへ~責任ある研究活動を目指して~, 国立研究開発法人科学技術振興機構, \url{https://www.jst.go.jp/researchintegrity/shiryo/pamph_for_researcher.pdf}, 2020. 
-
-\bibitem{ref-ieice} 
-和文論文誌投稿のしおり, 電子情報通信学会, \url{https://www.ieice.org/jpn/shiori/iss_2.html#2.6}, 2021/09/28.
-
-\bibitem{ref-ipsj} 
-論文誌ジャーナル原稿執筆案内, 情報処理学会, \url{https://www.ipsj.or.jp/journal/submit/ronbun_j_prms.html}, 2021/09/28.
-
-\bibitem{ref-journal} 
-著者名, ``論文タイトル,'' 雑誌名, vol, no, page, year.
-
-\bibitem{ref-journal-ex} 
-國田 樹, 遠藤聡志, ``学術論文の出典記載例,'' 知能情報学会誌, vol. 3, no. 2, pp.8-13, 2021.
-
-\bibitem{ref-book}
-著者名, ``書籍タイトル,'' (編集者名), 出版社名, 発行都市名, 発行年.
-
-\bibitem{ref-book-ex}
-國田樹, ``著書の出典記載例,'' 知能情報出版, 沖縄, 2021.
-
-\bibitem{ref-proceedings}
-著者名, ``論文タイトル,'' 学会名もしくは会議名, no.論文番号, ページ, 開催都市名, 開催国名, year. 
-
-\bibitem{ref-proceedings-ex}
-國田樹, 遠藤聡志, ``学会論文の出典記載例'' 第2回知能情報国際会議, no.2-1234, pp.1-8, Okinawa, Japan, 2021. 
-
-\bibitem{ref-web}
-著者名(サイト管理者と同一の場合は省略可), Webページタイトル, サイト管理者名等, URL(url命令を使用すること), 参照年月日.  
-
-\bibitem{ref-report1}
-見延庄太郎,理系のためのレポート・論文完全ナビ,講談社, 2016.
-
-\bibitem{ref-report2}
-福地健太郎,理工系のためのよい文章の書き方,翔泳社, 2019.
-
-\end{thebibliography}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/thesis.bib	Sat Jan 15 16:50:14 2022 +0900
@@ -0,0 +1,55 @@
+@misc{gearsos,
+  title        = {GearsOS},
+  author       = {並列信頼研究室},
+  organization = {琉球大学},
+  howpublished = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/Gears/Gears/}}
+}
+
+@misc{cbcllvm,
+  title        = {CbC},
+  author       = {並列信頼研究室},
+  organization = {琉球大学},
+  howpublished = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC\_llvm/}}
+}
+
+@article{cbc,
+  author  = {河野 真治},
+  title   = {継続を持つCの下位言語によるシステム記述},
+  journal = {日本ソフトウェア科学会第17回大会論文集},
+  month   = {September},
+  year    = 2000
+}
+
+@article{cr,
+  author      = {伊波 立樹},
+  title       = {GearsOSの並列処理},
+  institution = {琉球大学工学部情報工学科, 琉球大学大学院理工学研究科情報工学専攻, 琉球大学工学部情報工学科},
+  journal     = {修士 (工学) 学位論文},
+  month       = {March},
+  year        = 2018
+}
+
+@article{gears,
+  author      = {清水隆博},
+  title       = {GearsOSのメタ計算},
+  institution = {琉球大学工学部情報工学科, 琉球大学大学院理工学研究科情報工学専攻, 琉球大学工学部情報工学科},
+  journal     = {修士 (工学) 学位論文},
+  month       = {March},
+  year        = 2021
+}
+
+@article{file,
+  author  = {一木 貴裕, 河野 真治(琉球大学)},
+  title   = {GearsOSの分散ファイルシステムの設計},
+  journal = {情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)},
+  month   = {May},
+  year    = 2021
+}
+
+@article{modelcheck,
+  author  = {東恩納 琢偉,奥田 光希,河野 真治(琉球大学)},
+  title   = {Gears OSでモデル検査を実現する手法について},
+  journal = {情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)},
+  month   = {May},
+  year    = 2020
+}
\ No newline at end of file
Binary file paper/thesis.pdf has changed
--- a/paper/thesis.tex	Wed Jan 05 20:22:26 2022 +0900
+++ b/paper/thesis.tex	Sat Jan 15 16:50:14 2022 +0900
@@ -1,7 +1,8 @@
 \documentclass[title,12pt]{jsreport}
 \usepackage{ie-thesis}
+\usepackage{listings}
 
-\jtitle{GearsOSにおけるFileSystemの設計}
+\jtitle{GearsOSにおけるinodeを用いたFileSystemの設計}
 \title{Designing a FileSystem in GearsOS}
 
 \affiliation{琉球大学工学部工学科知能情報コース}
@@ -12,6 +13,32 @@
 %\Jabstract{\include{./text/Jabstract}}
 \Jabstract{\input{./text/Jabstract.tex}}
 \Eabstract{\input{./text/Eabstract.tex}}
+
+\lstset{
+  frame=single,
+  keepspaces=true,
+  stringstyle={\ttfamily},
+  commentstyle={\ttfamily},
+  identifierstyle={\ttfamily},
+  keywordstyle={\ttfamily},
+  basicstyle={\ttfamily},
+  breaklines=true,
+  xleftmargin=0zw,
+  xrightmargin=0zw,
+  framerule=.2pt,
+  columns=[l]{fullflexible},
+  numbers=left,
+  stepnumber=1,
+  numberstyle={\scriptsize},
+  numbersep=1em,
+  language={},
+  tabsize=4,
+  lineskip=-0.5zw,
+  escapechar={@, $},
+}
+
+\renewcommand{\lstlistingname}{ソースコード}
+\renewcommand{\lstlistlistingname}{ソースコード目次}
    
 \begin{document}
 \maketitle %Don't remove.
@@ -25,6 +52,9 @@
 % 表も軸,表がある場合のみ
 \listoftables
 
+% ソースコード目次
+\lstlistoflistings
+
 % pagecounter settings
 \setcounter{page}{0}	%Don't remove.
 
@@ -41,7 +71,8 @@
 \chapter*{謝辞}
 
 % reference
-\include{./text/reference}
+\bibliography{thesis}
+\bibliographystyle{junsrt}
 
 %付録がある場合のみ
 %\appendix