Mercurial > hg > Papers > 2022 > ikki-master

changeset 13:9991e90cff65

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tweak
author ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
date Mon, 31 Jan 2022 21:27:24 +0900
parents 2c54886cebef
children 0a4cafd954b9
files Paper/chapter/0-introduction.tex Paper/chapter/2-CbC.tex Paper/chapter/3-GearsOS.tex Paper/chapter/4-Christie.tex Paper/chapter/5-Implementation.tex Paper/chapter/6-Evaluation.tex Paper/chapter/conclusion.tex Paper/chapter/thanks.tex Paper/master_paper.pdf Paper/reference.bib
diffstat 10 files changed, 196 insertions(+), 31 deletions(-) [+]
line wrap: on
line diff
--- a/Paper/chapter/0-introduction.tex	Sun Jan 30 04:52:30 2022 +0900
+++ b/Paper/chapter/0-introduction.tex	Mon Jan 31 21:27:24 2022 +0900
@@ -13,10 +13,10 @@
 
 また、当研究室では信頼性の保証と拡張性の高さを目指したOSプロジェクトである、GearsOSの開発を行なっている。
 GearsOSはテストコードでなく、AgdaやCoqなどの型式手法に含まれる定理証明支援系やモデル検査を用い、
-実施にOSとして動作するコードそのもののを検証することで信頼性の補償を目指している。
+実施にOSとして動作するコードそのものを検証することで信頼性の補償を目指している。
 また、GeasOSはノーマルレベルとメタレベルを分離して記述するContinuation based C(CbC)にて記述される。
 ノーマルレベルとはユーザが行いたい計算をさし、メタレベルとはノーマルレベルの計算を行うための計算をさす。
-ノーメルレベルのプログラムのメタレベルに対して自由に差し替えを行うことにより、
+ノーマルレベルのプログラムのメタレベルに対して自由に差し替えを行うことにより、
 コードの整合性の検証やプログラムのデバッグを行えるような作りとなっている。
 
 現状においてGearsOSは言語フレームワークとして実装されており、
@@ -25,7 +25,7 @@
 GearsOSのファイルシステムは既存のOSが持つファイルシステムの問題点の解決や
 従来ではアプリケーションが担っているバックアップを始めとした機能を搭載したファイルシステムの構成を目指して開発を行いたいと考えた。
 問題点の解決の一部として、既存のファイルシステムとは異なりファイルシステムをデータベースとして構成したい。
-レコードでファイルデータを取り扱うことによりファイルの更新や操作を簡潔に行い、加えてFileSystemのAPIを総括してトランザクションとしたい。
+レコードでファイルデータを取り扱うことによりファイルの更新や操作を簡潔に行い、またFileSystemのAPIを総括してトランザクションとしたい。
 加えて、データのバックアップについてもOSに搭載したい。
 従来のようにバックアップデータをユーザが管理するのではなく、OSが管理をすることによりバックアップデータ自体の紛失を防ぎたい。
 
--- a/Paper/chapter/2-CbC.tex	Sun Jan 30 04:52:30 2022 +0900
+++ b/Paper/chapter/2-CbC.tex	Mon Jan 31 21:27:24 2022 +0900
@@ -42,7 +42,7 @@
 今回のソースコードでは、
 mainから二つのint型のDataGearの入力と共にCG1へgotoで遷移、
 続いてCG2へCG1での処理結果をDataGearとして引き渡し遷移、
-最後にexitをするという流れとなる。
+最後にexitをするという流れとなる。 
 
 \lstinputlisting[label=src:cbc_sample, caption=CbCの例題]{src/CbC_sample.cbc}
 
--- a/Paper/chapter/3-GearsOS.tex	Sun Jan 30 04:52:30 2022 +0900
+++ b/Paper/chapter/3-GearsOS.tex	Mon Jan 31 21:27:24 2022 +0900
@@ -18,9 +18,9 @@
 
 \lstinputlisting[label=src:Queue.h, caption=Queueのインターフェース]{src/Queue.h}
 
-GearsOSにおけるInterfaceは、ヘッダファイルへプログラム内で使われるCodeGearとそのCodeGearに入出力されるDataGearを記述する。
-5から10行目にはAPIとなるCodeGearが宣言されている。
-また、2, 3行目のunion Data型の変数はAPIのCodeGearで使用されるDataGearである。
+GearsOSにおけるInterfaceはヘッダファイルに対して記述を行い、APIとして用いたいCodeGearとそのCodeGearに入出力されるDataGearを記述する。
+5から10行目はCodeGearの宣言である。
+また、2, 3行目のunion Data型の変数はAPIのCodeGearで使用されるDataGearを記述する。
 
 コード内のCodeGearの第1引数はImpl*型の変数となっており、Interfaceを引き継いだImplementのポインタとなる。
 これはCbCはスタックを持たず、複数のCodeGear間をまたいで必要な情報はDataGearとして持ち運ぶ必要があるため、
@@ -56,14 +56,14 @@
 \lstinputlisting[label=src:SynchronizedQueue.h, caption=Queue.hの実装となるSynchronizedQueue.h]{src/SynchronizedQueue.h}
 
 \section{GearsOSのプログラム例}
-GearsOSのプログラムの一例として先述したソースコード\ref{src:Queue.h}、\ref{src:SynchronizedQueue.h}の実装となる
+GearsOSのプログラムの一例として先述したソースコード\ref{src:Queue.h}、\ref{src:SynchronizedQueue.h}をInterface,Imlementとして継承した
 SynchronizedQueue.cbcの一部分をソースコード\ref{src:SynchronizedQueue.cbc}に示す。
 GearsOSにはImplementが記述されたヘッダファイルから、cbcファイルの雛形を自動生成するimpl2cbc.plが導入されている。
 雛形には7行目のQueue*を返すcreateSychronizedQueueとその中の処理、
 加えて22行目のputSynchronizedQueueのようなInterfaceのヘッダファイル内で記述されたCodeGearが用意されている。
 
 プログラム内で呼び出したいInterfaceは2,3行目のような記述が必要となる。
-7から20行目に記述されているcreateSynchronizedQueueはQueueインターフェースをSynchronizedQueueで実装する際のコンストラクタであると言える。
+7から20行目に記述されているcreateSynchronizedQueueはQueueインターフェースをSynchronizedQueueで実装する際のコンストラクタである。
 関数呼び出しで実装されており、返り値はInterfaceのポインタである。
 
 コンストラクタ内の記述を解説すると、8,9行目にてQueueとSynchronizedQueueのアロケーションを行い、
@@ -72,15 +72,14 @@
 コンパイル時に後述のContextが持つDataGearのヒープ領域のアロケーションを行うマクロへ置き換えられる。
 10から13行目の記述では初期はImplementの型定義ファイルに記述された変数の宣言が行われている。
 当然プログラマは、宣言した変数に任意の状態が設定されるように変更することができる。
-13行目ではatomic型のinterfaceをAtomicReference型で実装を行っている。
+13行目ではatomic型のinterfaceをAtomicReference型で呼び出している。
 15から18行目はInterfaceの定義にて記述されたAPIとcbcプログラム内のCodeGearの紐付けを行っている。
-現状では必ずC\texttt{\_} + API名 + Impl名;と記述する必要がある。
 
 \lstinputlisting[label=src:SynchronizedQueue.cbc, caption=SynchronizedQueue.cbcの記述の一部]{src/SynchronizedQueue.cbc}
 
 22行目から38行目はInterfaceで宣言されたputAPIの実装部分である。
 Interfaceで宣言されたAPIと対応するCodeGearは.cbcファイル上ではAPI名 + Impl名で宣言する必要がある。
-コンストラクタ内13行目にてatopmiReferenceの実装を行っているが、atomicInterfaceへのポインタは最終的に返り値のqueueポインタが保持するため、
+コンストラクタ内13行目にてatopmiReferenceの呼び出しを行っているが、atomicInterfaceへのポインタは最終的に返り値のqueueが保持しているため、
 atomicInterfaceで定義されたAPIのCodeGearへ遷移することができるようになる。
 現状のGearsOSでは一度、Interfaceのポインタ型をプログラム内で宣言し、コンストラクタで生成した実装のポインタを代入、
 そしてgoto文を用いて遷移するという冗長な記述が必要となっているため、トランスコンパイラにより改善するといった手段が考えられる。
@@ -96,7 +95,7 @@
 メタレベルでは全てのCodeGearは必ずContextをDataGearとして呼び出す仕組みとなっている。
 そのためContextはGear概念で言うとMetaDataGearに相当する。
 
-図\ref{fig:context}にCodeGearが遷移する際のContextに対するDataGearの書き込みまたは呼び出しの形を示す。
+図\ref{fig:context}にCodeGearが遷移する際のContextに対するDataGearの書き込みまたは呼び出しを示す。
 CodeGearが遷移する際にOutputDataGearをContextに対して書き込みを行う。
 続いて遷移先のstubCodeGearがContextから遷移先CodeGearが必要とするInputDataGer
 と出力する必要があるOutputDataGearを参照する。
@@ -107,7 +106,7 @@
 Contextをユーザーが任意の操作することはノーマルレベルとメタレベルの分離した意味が無くなってしまうためである。
 Contextに対するDataGearの操作はstubCodeGearのみならずCodeGear内でも行われるが、それらの記述はトランスコンパイラの自動生成により行われる。
 先述のnew演算子がその一例として挙げられる。
-もしnew演算子でなく、Contextが保持するDataGearに対してAllocate操作が行えてしまうと、
+もしnew演算子でなく、直にContextの操作が行えてしまうと、
 並行に動作している他のUser Contextの中身を書き換えるなどプログラム処理に支障が出るような不正な改ざんが行えてしまう。
 
 \begin{figure}[tb]
@@ -123,13 +122,13 @@
 また実行されているGPUやCPUごとにもContextが必要となり、これをCPU Contextと呼ぶ。
 加えてOSとしてUser ContextやCPU Contextを含めた、全体を管理するためのContextも必要となる。
 これはKernel ContextやKContextと呼ばれている。
-これらのContextは特に、GearsOSに実装されているpar gotoと呼ばれる並列処理用の構文の内部構成などのメタレベルのプログラミングの際に強く意識されている。
+これらのContextは特に、GearsOSに実装されているpar gotoと呼ばれる並列処理用の構文の内部構成などのメタレベルのプログラミングの際に強く意識する必要がある。
 GearsOSではKernelContextが複数のUser ContextとCPU Contextを管理し、
 ノーマルレベルのプログラムに応じてWorkerに対してTaskを割り振ることで分散処理の機構が実現されている。
 
-\section{トランスコンパイル後のCbCプログラム}
+\section{トランスコンパイル後の実行プログラム}
 先にも述べたように、GearsOS上で記述するプログラムは拡張子が.cbcとなるcbcファイルへ記述を行う。
-しかし、実際の動作ファイルはcbcをPerlスクリプトによりトランスコンパイルによりstubCodeGearなどのメタレベルの処理やマクロの書き換えが追加された、
+しかし、実際の動作ファイルはcbcをPerlスクリプトによりトランスコンパイルによりstubCodeGearなどのメタレベルの処理やマクロの書き換えがされた、
 拡張子.cファイルとなる。
 ソースコード\ref{src:SynchronizedQueue.c}にSynchronizedQueue.cbc(ソースコード\ref{src:SynchronizedQueue.cbc})をトランスコンパイルした結果出力された
 SyncheonizedQueue.cの一部である。
@@ -146,7 +145,7 @@
 54行目ではGearImplマクロを用いてInterfaceの実装型のポインタをContextから呼び出す。
 55, 56行目に記述されているGearefマクロはcontextのInterface内で宣言されているDataGearを参照するマクロである。
 55行目の場合、QueueInterface内で宣言されているDataGearであるdataを呼び出している。
-56行目では共用体で取り扱われているnextCodeGearを呼び出す。
+56行目では共用体として取り扱われているnextCodeGearを呼び出す。
 CodeGear本体に必要なinputDataGearをimplで呼び出してから本体のCodeGearへ遷移する。
 
 本体のCodeGearでは、ノーマルレベルでの操作を禁止したいContextに対する操作が追記される。
--- a/Paper/chapter/4-Christie.tex	Sun Jan 30 04:52:30 2022 +0900
+++ b/Paper/chapter/4-Christie.tex	Mon Jan 31 21:27:24 2022 +0900
@@ -40,7 +40,8 @@
 \end{figure}
 
 \section{LocalDGMとRemoteDGM}
-DataGearManagerはLocalDGMとRemoteDGMの二種類が存在する。
+図DataGearManagerはLocalDGMとRemoteDGMの二種類が存在する。
+\ref{fig:RDGM}にDataGearManagerによる通信の関係性を示す。
 LocalDGMは所有しているCodeGearManager自身に対応するDGMである。
 LocalDGMにput操作を行うことで自身の持つkeyに対してDataGearを送ることができる。
 
@@ -49,8 +50,8 @@
 RemoteDGMにput操作すると対応したCGMが持つLocalDGMへDataGearをputすることができる。
 図\ref{fig:gearsRelation}に示す。
 
-ChristieのノードどおしのやりとりはこのRemoteDGMを介して行われる。
-つまりRemoteDGMを作成することはノードどおしの接続を行うことにあたる。
+ChristieのノードどうしのやりとりはこのRemoteDGMを介して行われる。
+つまりRemoteDGMを作成することはノードどうしの接続を行うことにあたる。
 また、RemoteDGMは単方向の通信にあたるため、複数のノードを双方向で通信させたい場合は双方に相手のRemoteDGMを作る必要がある。
 
 
@@ -59,7 +60,7 @@
         \includegraphics[width=150mm]{./images/Remote_DataGearManager.pdf}
     \end{center}
     \caption{RemoteDGMを介したノード接続}
-    \label{fig:gearsRelation}
+    \label{fig:RDGM}
 \end{figure}
 
 
@@ -77,7 +78,7 @@
 DataGearの呼び出しはTake操作が基本となる。
 Peek操作は特定のDGを参照し続けたい場合に用いるが、Peekアノテーションを単独で用いる場合、
 処理次第では無限ループが生じてしまう場合があるため気をつける必要がある。
-
+DataGearはCodeGearMangerが持つLocalなDataGearManagerに対して参照を行う。
 
 
 \section{Christieのプログラミング例}
--- a/Paper/chapter/5-Implementation.tex	Sun Jan 30 04:52:30 2022 +0900
+++ b/Paper/chapter/5-Implementation.tex	Mon Jan 31 21:27:24 2022 +0900
@@ -208,7 +208,7 @@
 
 
 \section{ディレクトリシステム}
-本研究と並行する形で又吉雄斗によるGearsFileSystemのディレクトリ構造の構築が行われている。[論文No.]
+本研究と並行する形で又吉雄斗によるGearsFileSystemのディレクトリ構造の構築が行われている\cite{mata-thesis}。
 GearsFSのディレクトリシステムはUnixOSのディレクトリシステムのinodeの仕組みを用いて再現することを試みている。
 通常のUnixのディレクトリシステムと異なる点として、ディレクトリを赤黒木(RedBlackTree)を用いて構成する。
 
--- a/Paper/chapter/6-Evaluation.tex	Sun Jan 30 04:52:30 2022 +0900
+++ b/Paper/chapter/6-Evaluation.tex	Mon Jan 31 21:27:24 2022 +0900
@@ -52,15 +52,16 @@
 Taskを処理したWorkerを解放せるための\texttt{\_\_}exitをnext\texttt{\_}codeとして指定したい。
 しかし、下記のコードではトランスコンパイルの時点でエラーを起こし、プログラムのコンパイルが行えない。
 
-6行目は別の並列プログラムtwiceでのpar gotoの記述である。異なる点として遷移先のCodeGearがInterfaceを継承したクラスに記述されたものでなく、
-そのCodeGear内で利用されるクラスをInputDataGearとして指定していることにある。
-この記述の場合、\texttt{\_\_}exitは問題なく動作することができるが、GearsOSに実装されたQueueやTreeといった多くのプログラムはInterfaceを継承したクラスとして実装されている。
+6行目は別の並列プログラムtwiceでのpar gotoの記述である。異なる点として遷移先のCodeGearがなんらかのInterfaceの呼び出されたプログラムの中に記述されたものでなく、
+そのCodeGear内で利用されるInterfaceをInputDataGearとして指定していることにある。
+この記述の場合、\texttt{\_\_}exitは問題なく動作することができるが、GearsOSに実装されたQueueやTreeといった多くのプログラムはInterfaceを継承した上で実装されている。
 そのため従来のプログラムをTaskとして利用することが難しくなっている。
 
 加えてトランスコンパイラのバグも確認されている。
-クラス内部へ記述されたCodeGearへのpar gotoはInputCodeGearが存在する場合、
+Interfaceを継承したプログラム内部へ記述されたCodeGearへのpar gotoはInputCodeGearが存在する場合、
 ソースコード\ref{src:misspar}の15, 33行目のInterfaceのGET\texttt{\_}METAが生成されなくなってしまう。
-
+そのため現状、Interface内CodeGearの分散処理は行うことができるが、InputDataGearがそのInterface自身とnext\texttt{\_}code以外のInputCodeGearが参照できない、
+加えて\texttt{\_\_}exitが機能しないという問題が存在する。
 
 \lstinputlisting[label=src:mainDist, caption=takeCodeGearから遷移されるstubCodeGear]{src/mainDist.cbc}
 
--- a/Paper/chapter/conclusion.tex	Sun Jan 30 04:52:30 2022 +0900
+++ b/Paper/chapter/conclusion.tex	Mon Jan 31 21:27:24 2022 +0900
@@ -3,6 +3,7 @@
 GearsOSにおけるファイルは競合的なアクセスを許した大域的な資源であり、
 ファイルは分散フレームワークChristieのDataGearManagerに相当する。
 ファイル内のデータは任意の構造体によるレコード単位に分割されており、ファイルを読み込む場合、レコードを順番にTakeで呼び出せば良い。
+ファイルのデータとなるレコードはプログラマが任意の形の構造体で形成することができ、ファイルの種類によって実装を適切なものに構成することができる。
 
 ファイルの共有による通信はRemoteDataGearManagerによるploxyに対して操作することで行われる。
 そのため、GearsOSでのファイルはファイルそのものであると同時に分散処理の通信とも見ることができる。
@@ -12,6 +13,12 @@
 そのため、変更の履歴はOSが参照できる形で残されており、定期的なバックアップや履歴データの削除などの機能を作成することで
 アプリケーションに頼らず、OSがバックアップを担当することができる。
 
+加えてファイルシステムの構築をしながら、GearsOS自体の改善点や利用の検証を行った。
+現状のGearsOSはノーマルレベルとメタレベルの分離という目的を達成してはいるものの、
+関数スタックを持たない軽量継続という記述の独自な特性や記述の難易度、トランスコンパイラによるバグなどにより
+プログラマが慣れ親しみ問題を解決しながらプログラムが記述できるようになるまで時間がかかってしまう。
+GearsOSは現在際実装の検討が行われており、トランスコンパイラによるメタレベルの記述を他の手段を用いるといった検証が行われている。
+
 
 \section{今後の課題}
 ファイルの通信接続はChristieのTopologyManagerの機能を用いるが、詳細な設計は現時点で行えていない。
--- a/Paper/chapter/thanks.tex	Sun Jan 30 04:52:30 2022 +0900
+++ b/Paper/chapter/thanks.tex	Mon Jan 31 21:27:24 2022 +0900
@@ -1,9 +1,9 @@
 \chapter*{謝辞}
-\addcontentsline{toc}{chapter}{謝辞}
+\addcontentsline{toc}{chapter}{謝辞}  
 本研究の遂行、本論文の執筆にあたり、丁寧な御指導と御教授を賜りました河野真治准教授に心より感謝いたします。
 ご多忙の中にも関わらず、研究の引き継ぎと御教授を頂きました卒業生である清水隆博さん、赤堀貴一さんに感謝いたします。
 加えて、共に研究の遂行を行ってくれた又吉雄斗さんを始めとして、共に研究に励み心の支えとなってくださった並列信頼研の所属学生に感謝いたします。
-最後に、理工学研究科情報工学専攻の学友、教員方と職員、並びに生活と心の支えをくださった家族に深く感謝いたします。
+最後に、理工学研究科情報工学専攻の教員方、職員方と学友、並びに生活と心の支えをくださった家族に深く感謝いたします。
 
 \begin{flushright}
     2022年 3月 \\ 一木貴裕
Binary file Paper/master_paper.pdf has changed
--- a/Paper/reference.bib	Sun Jan 30 04:52:30 2022 +0900
+++ b/Paper/reference.bib	Mon Jan 31 21:27:24 2022 +0900
@@ -62,6 +62,42 @@
  keywords = {isabelle/hol, l4, microkernel, sel4},
 }
 
+@article{Klein:2010:SFV:1743546.1743574,
+ author = {Klein, Gerwin and Andronick, June and Elphinstone, Kevin and Heiser, Gernot and Cock, David and Derrin, Philip and Elkaduwe, Dhammika and Engelhardt, Kai and Kolanski, Rafal and Norrish, Michael and Sewell, Thomas and Tuch, Harvey and Winwood, Simon},
+ title = {seL4: Formal Verification of an Operating-system Kernel},
+ journal = {Commun. ACM},
+ issue_date = {June 2010},
+ volume = {53},
+ number = {6},
+ month = jun,
+ year = {2010},
+ issn = {0001-0782},
+ pages = {107--115},
+ numpages = {9},
+ url = {http://doi.acm.org/10.1145/1743546.1743574},
+ doi = {10.1145/1743546.1743574},
+ acmid = {1743574},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+}
+
+@inproceedings{Nelson:2017:HPV:3132747.3132748,
+ author = {Nelson, Luke and Sigurbjarnarson, Helgi and Zhang, Kaiyuan and Johnson, Dylan and Bornholt, James and Torlak, Emina and Wang, Xi},
+ title = {Hyperkernel: Push-Button Verification of an OS Kernel},
+ booktitle = {Proceedings of the 26th Symposium on Operating Systems Principles},
+ series = {SOSP '17},
+ year = {2017},
+ isbn = {978-1-4503-5085-3},
+ location = {Shanghai, China},
+ pages = {252--269},
+ numpages = {18},
+ url = {http://doi.acm.org/10.1145/3132747.3132748},
+ doi = {10.1145/3132747.3132748},
+ acmid = {3132748},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+}
+
 @inproceedings{Sigurbjarnarson:2016:PVF:3026877.3026879,
  author = {Sigurbjarnarson, Helgi and Bornholt, James and Torlak, Emina and Wang, Xi},
  title = {Push-button Verification of File Systems via Crash Refinement},
@@ -77,3 +113,124 @@
  publisher = {USENIX Association},
  address = {Berkeley, CA, USA},
 }
+
+@inproceedings{OSBook,
+ author = {Andrew S. Tanenbaum},
+ booktitle = {Modern Operating Systems Fourth Edition},
+ series = {OSDI'15},
+ year = {2015},
+ isbn = {978-0-13-359162-0},
+ location = {Hervert BOS Vrije Universiteit Amsterdam, The Netherlands},
+ pages = {265-332},
+ numpages = {67},
+}
+
+
+@misc{hg:cbcgcc,
+    title = {CbC\_gcc},
+    author = {並列信頼研究室},
+    organization = "琉球大学",
+    howpublished = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC_gcc/}},
+    note = {Accessed: 2021-01-31},
+}
+
+@misc{hg:gears,
+    title = {GearsOS},
+    author = {並列信頼研究室},
+    organization = "琉球大学",
+    howpublished = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/Gears/Gears/}},
+    note = {Accessed: 2021-01-31},
+}
+
+@misc{hg:Christie,
+    title = {Christie},
+    author = {並列信頼研究室},
+    organization = "琉球大学",
+    howpublished = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/Database/Christie/}},
+    note = {Accessed: 2021-01-31},
+}
+
+
+@article{
+    gears,
+    author = "河野 真治 and 伊波 立樹 and  東恩納 琢偉",
+    title = "Code Gear、Data Gear に基づく OS のプロトタイプ",
+    journal = "情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)",
+    month = "May",
+    year = 2016
+}
+
+@article{
+    anatofz,
+    author = "清水 隆博 and 河野真治",
+    title = "GearsOSのメタ計算",
+    journal = "琉球大学理工学研究科修士論文",
+    month = "Merch",
+    year = 2020
+}
+
+@article{
+    koki,
+    author = "宮城 光輝 and 河野真治",
+    title = "継続を基本とした言語による OS のモジュール化",
+    journal = "琉球大学理工学研究科修士論文",
+    month = "Merch",
+    year = 2018
+}
+
+@article{
+    tokumori,
+    author = "徳森 海斗 and 河野真治",
+    title = "LLVM Clang 上の Continuation based C コンパイラ の改良",
+    journal = "琉球大学理工学研究科修士論文",
+    month = "Merch",
+    year = 2016
+}
+
+
+@article{
+    mata-thesis,
+    author = "又吉 雄斗 and  河野　真治",
+    title = "GearsOS における inode を用いた File system の設計",
+    journal = "琉球大学工学部知能情報コース卒業論文",
+    month = "Merch",
+    year = 2022
+}
+
+
+@article{
+    pop,
+    author = "照屋 のぞみ and  河野　真治",
+    title = "分散フレームワークChristieの設計",
+    journal = "琉球大学理工学研究科修士論文",
+    month = "Merch",
+    year = 2018
+}
+
+@article{
+    Alice,
+    author = "赤嶺 一樹 and  河野　真治",
+    title = "分散ネットワークフレームワークAlice の 提案と実装",
+    journal = "琉球大学理工学研究科修士論文",
+    month = "Merch",
+    year = 2012
+}
+
+@article{
+    BlockChain,
+    author = "赤堀 貴一 and  河野　真治",
+    title = "Christieによるブロックチェーンの実装",
+    journal = "琉球大学工学部情報工学科卒業論文",
+    month = "Merch",
+    year = 2019
+}
+
+@manual{man:socket,
+  author = "{man-page of SOCKET}",
+  title ="{\url{https://linuxjm.osdn.jp/html/LDP_man-pages/man2/socket.2.html}}",
+}
+
+@manual{man:getaddrinfo,
+  author = "{man-page of GETADDRINFO}",
+  title ="{\url{https://linuxjm.osdn.jp/html/LDP_man-pages/man3/getaddrinfo.3.html}}",
+}