Mercurial > hg > Papers > 2022 > pine-thesis

changeset 9:48187f47422f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix typo
author Takato Matsuoka <t.matsuoka@cr.ie.u-ryukyu.ac.jp>
date Sun, 30 Jan 2022 16:17:20 +0900
parents 06592642eedc
children 884ba6158dd6
files paper/text/gears.tex paper/text/introduction.tex paper/thesis.pdf
diffstat 3 files changed, 4 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/paper/text/gears.tex	Sun Jan 30 16:03:45 2022 +0900
+++ b/paper/text/gears.tex	Sun Jan 30 16:17:20 2022 +0900
@@ -1,18 +1,18 @@
 \chapter{GearsOS}
 GearsOSは本研究室で開発しているCbCを用いて信頼性と拡張性の両立を目指したOS\cite{GearsOS}である。CbCと同様にCodeGearとDataGearを基本単位として実行し、ノーマルレベルの計算とメタレベルの計算の分離により信頼性を担保している。
 
-GearsOSは様々な役割を持つCodeGearとDataGearで構成されている。本章では構成の中心となっているMetaDataGearや、モジュール化の仕組みとして導入されているInterfaceなどについて説明を行う。
+GearsOSは様々な役割を持つCodeGearとDataGearで構成されている。本章では構成の中心となっているMetaDataGearや、モジュール化の仕組みとして導入されているInterfaceについて説明する。
 
 \section{Context}
 ContextとはGearsOSの計算に必要なCodeGearやDataGearを持つMetaDataGearであり、従来のOSにおけるプロセスやスレッドに対応する。Contextは使用可能なCodeGearとDataGearのリストや、TaskQueueへのポインタ、DataGearを格納するためのメモリ空間などを持っている。ソースコード\ref{src:def_context}がContextの定義である。
 
 \lstinputlisting[label=src:def_context, caption=Contextの定義]{src/context.h}
 
-ソースコード\ref{src:def_context}6行目のcodeがCodeGearを格納するための配列である。code配列へアクセスするためのindexは、ソースコード\ref{src:def_enumCode}で定義されるenumを用いる。このenumはGearsOSで用いるCodeGearを全て列挙しており、コンパイル時に一意な番号へと変換される。この番号と配列へ格納されるCodeGearのポインタが対応しているため、特定のCodeGearの取り出しは対応した番号をindexに指定することで実現する。
+ソースコード\ref{src:def_context}の6行目のcodeがCodeGearを格納するための配列である。code配列へアクセスするためのindexは、ソースコード\ref{src:def_enumCode}で定義されるenumを用いる。このenumはGearsOSで用いるCodeGearを全て列挙しており、コンパイル時に一意な番号へと変換される。この番号と配列へ格納されるCodeGearのポインタが対応しているため、特定のCodeGearの取り出しは対応した番号をindexに指定することで実現する。
 
 \lstinputlisting[label=src:def_enumCode, caption=CodeGearのenum]{src/enumCode.h}
 
-ソースコード\ref{src:def_context}7行目のdataがDataGearを格納するための配列である。data配列はunion Data型であり、これは共用体によって定義されている。ソースコード\ref{src:def_unionData}にunion Dataの定義を示す。
+ソースコード\ref{src:def_context}の7行目のdataがDataGearを格納するための配列である。data配列はunion Data型であり、これは共用体によって定義されている。ソースコード\ref{src:def_unionData}にunion Dataの定義を示す。
 union Data 共用体の中にAtomicやCPUWorkerなどのDataGearを構造体として定義を行っている。これは通常のC言語においては、struct Atomicとstruct CPUWorkerは当然別の型として判別される。しかしGearsOSのContextにおいてはAtomicもCPUWorkerもDataGearとして等しく扱う必要がある。そのため共用体を用いて汎用的なDataGear型であるunion Data型を定義することで任意のDataGearを一律に扱うことができる。
 
 \lstinputlisting[label=src:def_unionData, caption=union Dataの定義]{src/unionData.h}
--- a/paper/text/introduction.tex	Sun Jan 30 16:03:45 2022 +0900
+++ b/paper/text/introduction.tex	Sun Jan 30 16:17:20 2022 +0900
@@ -8,7 +8,7 @@
 仕様を満たしているかどうかを検査することでプログラムの信頼性を保証する。
 
 本研究室では定理証明やモデル検査を用いて信頼性の保証を行うGearsOSの開発を行っている。
-GearsOSはContinuation Based C(CbC)を用いて記述したOSで、CbCは本研究室で開発している言語で、CodeGearというプログラム単位で記述・遷移するC言語の下位言語である。
+GearsOSはContinuation Based C(CbC)を用いて記述したOSである。CbCは本研究室で開発している言語で、CodeGearというプログラム単位で記述・遷移するC言語の下位言語である。
 CodeGear間の遷移は通常の関数呼び出しではなく、goto文によって行われるため、呼び出し元へ戻らない。
 そのためプログラムの記述をそのまま状態遷移として落とし込むことができ、これにより定理証明やモデル検査が可能である。
 
Binary file paper/thesis.pdf has changed