changeset 60:1ce43db7c038

update
author anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
date Tue, 02 Feb 2021 18:47:49 +0900
parents 23d1cff7c260
children e1dbf6e648ad
files paper/chapter/01-introduction.tex paper/chapter/02-cbc.tex paper/chapter/03-gears.tex paper/chapter/04-interface.tex paper/chapter/05-perl.tex paper/chapter/06-evaluation.tex paper/chapter/conclusion.tex paper/drawio/geasflow1.drawio paper/drawio/geasflow1.pdf paper/master_paper.pdf paper/master_paper.tex
diffstat 11 files changed, 96 insertions(+), 62 deletions(-) [+]
line wrap: on
line diff
--- a/paper/chapter/01-introduction.tex	Tue Feb 02 17:18:59 2021 +0900
+++ b/paper/chapter/01-introduction.tex	Tue Feb 02 18:47:49 2021 +0900
@@ -37,6 +37,10 @@
 しかしOSの処理は膨大である。
 すべての存在可能な状態を数え上げるモデル検査では状態爆発が問題となる。
 状態を有限に制限したり抽象化を行う必要がある。
+また、モデル検査ができるモデル検査器は特定のプログラム形式でないと動かないものがある。
+例えばSpinはPromela形式でないとモデル検査ができない。
+モデル検査ができる場合も、 モデル検査したコードと実際に動くコードを同一にしたい。
+また、モデル検査をする場合としない場合の切り替えを、より手軽に行いたい。
 
 
 OSのシステムコールは、ユーザーからAPI経由で呼び出され、 いくつかの処理を行う。
@@ -65,7 +69,7 @@
 プログラムの整合性の検証はメタレベルの計算で行いたい。
 ユーザーが実装したノーマルレベルの計算に対応するメタレベルの計算を、自由にメタレベルの計算で証明したい。
 またメタレベルで検証ががすでにされたプログラムがあった場合、都度実行ユーザーの環境で検証が行われるとパフォーマンスに問題が発生する。
-この場合はメタレベルの計算を検証をするもの、しないものと切り替えられる柔軟なAPIが必要となる。
+この場合は検証を実行するメタ計算と、 検証をしないメタ計算を手軽に切り替える必要がある。
 メタレベルの計算をノーマルレベルの計算と同等にプログラミングできると、動作するコードに対して様々なアプローチが掛けられる。
 この為にはノーマルレベル、メタレベル共にプログラミングできる言語と環境が必要となる。
 
--- a/paper/chapter/02-cbc.tex	Tue Feb 02 17:18:59 2021 +0900
+++ b/paper/chapter/02-cbc.tex	Tue Feb 02 18:47:49 2021 +0900
@@ -23,14 +23,13 @@
 これは呼び出し元の関数を次のCodeGearの継続対象として設定するものである。
 これはGCCでは内部コードを生成を行う。
 LLVM/clangでは\texttt{setjmp}と\texttt{longjmp}を使い実装している。
-したがってプログラマから見ると、通常のCの関数呼び出しの返り値をCodeGearから取得する事が可能となる。
+環境付きgotoを使うと、通常のCの関数呼び出しの返り値をCodeGearから取得する事が可能となる。
 
-\section{DataGearとMetaDataGear}
+\section{DataGear}
 DataGearはCbCでのデータの単位である。
-基本はC言語の構造体そのものであるが、 DataGearの場合はデータに付随するメタ情報も取り扱う。
-これはデータ自身がどういう型を持っているかなどの情報である。
-ほかに計算を実行するCPU、 GPUの情報や、 計算に必要なすべてのDataGearの管理などの実行環境のメタデータもDataGearの形で表現される。
-このメタデータを扱うDataGearをMetaDataGearと呼ぶ。
+CbC上では構造体の形で表現される。
+各CodeGearの入力として受けるDataGearをInputDataGearと呼ぶ。
+逆に次の継続に渡すDataGearをOutputDataGearと呼ぶ。
 
 
 \section{CbCを使ったシステムコールディスパッチの例題}
@@ -56,6 +55,7 @@
 CbCでのメタ計算はCodeGear、 DataGearの単位がそのまま使用できる。
 メタ計算で使われるこれらの単位はそれぞれ、 MetaCodeGear、 MetaDataGearと呼ばれる。
 
+
 \section{MetaCodeGear}
 
 GearsOSでは、 CodeGearとDataGearを元にプログラミングを行う。
@@ -79,3 +79,7 @@
 これは図\ref{meta-cg-dg}の下段に対応する。
 
 \section{MetaDataGear}
+基本はC言語の構造体そのものであるが、 DataGearの場合はデータに付随するメタ情報も取り扱う。
+これはデータ自身がどういう型を持っているかなどの情報である。
+ほかに計算を実行するCPU、 GPUの情報や、 計算に必要なすべてのDataGearの管理などの実行環境のメタデータもDataGearの形で表現される。
+このメタデータを扱うDataGearをMetaDataGearと呼ぶ。
\ No newline at end of file
--- a/paper/chapter/03-gears.tex	Tue Feb 02 17:18:59 2021 +0900
+++ b/paper/chapter/03-gears.tex	Tue Feb 02 18:47:49 2021 +0900
@@ -7,6 +7,10 @@
 現在のGearsOSはUnixシステム上のアプリケーションとして実装されているものと、 xv6の置き換えとして実装されているもの\cite{weko_195888_1}がある。
 
 
+\section{Context}
+Contextとは従来のOSのプロセスに相当する概念である。
+GearsOSではMetaDataGearとして表現される。
+
 \section{GearsOSのビルドシステム}
 GearsOSではビルドツールにCMakeを利用している。
 ビルドフローを図\ref{fig:gearsbuild1}に示す。
@@ -22,14 +26,68 @@
 Perlスクリプトで変換されたCbCファイルなどをもとにCbCコンパイラがコンパイルを行う。
 ビルドの処理は自動化されており、 CMake経由でmakeやninjaコマンドを用いてビルドする。
 
-\begin{figure}[hp]
+\begin{figure}[h]
   \begin{center}
-   \includegraphics[width=120mm]{drawio/geasflow1.pdf}
+   \includegraphics[width=150mm]{drawio/geasflow1.pdf}
   \end{center}
   \caption{GearsOSのビルドフロー}
   \label{fig:gearsbuild1}
  \end{figure}
 
+\section{GearsOSのCbCから純粋なCbCへの変換}
+GearsOSはCbCを拡張した言語となっている。
+ただしこの拡張自体はCbCコンパイラであるgcc、 llvm/clangには搭載されていない。
+その為GearsOSの拡張部分を、等価な純粋なCbCの記述に変換する必要がある。
+現在のGearsOSでは、 CMakeによるコンパイル時にPerlで記述された\texttt{generate\_stub.pl}と\texttt{generate\_context.pl}の2種類のスクリプトで変換される。
+
+\section{generate\_stub.pl}
+generate\_stub.plは各CbCファイルごとに呼び出される。
+入力としてCbCファイルを受け取りメタ計算を含んだ形に変換し、 純粋なCbCファイルとして書き出す。
+図\ref{fig:generate_stub_pl_1}に処理の概要を示す
+
+\begin{figure}[h]
+  \begin{center}
+   \includegraphics[width=160mm]{drawio/gears_os_build_flow.pdf}
+  \end{center}
+  \caption{generate\_sub.plを使ったトランスコンパイル}
+  \label{fig:generate_stub_pl_1}
+\end{figure}
+
+\section{generate\_context.pl}
+
+
+\begin{itemize}
+  \item \texttt{generate\_stub.pl}
+  \begin{itemize}
+    \item 各CbCファイルごとに呼び出されるスクリプト
+    \item 対応するメタ計算を導入したCbCファイル(拡張子はc)に変換する
+  \end{itemize}
+  \item \texttt{generate\_context.pl}
+  \begin{itemize}
+    \item 生成したCbCファイルを解析し、使われているCodeGearを確定する
+    \item context.hを読み込み、使われているDataGearを確定する
+    \item Context関係の初期化ルーチンやCodeGear、 DataGearの番号であるenumを生成する
+    \begin{itemize}
+      \item 図\ref{fig:generate_context_1}に処理の概要を示す
+    \end{itemize}
+  \end{itemize}
+\end{itemize}
+
+これらのPerlスクリプトはプログラマが自分で動かすことはない。
+Perlスクリプトの実行手順はCMakeLists.txtに記述しており、 makeやninja-buildでのビルド時に呼び出される。(ソースコード \ref{src:cmake1})
+
+\lstinputlisting[label=src:cmake1, caption=CMakeList.txt内でのPerlの実行部分]{src/cmakefile.1.txt}
+
+\begin{figure}[h]
+  \begin{center}
+   \includegraphics[width=130mm]{drawio/old_generate_context.pdf}
+  \end{center}
+  \caption{generate\_context.plを使ったファイル生成}
+  \label{fig:generate_context_1}
+ \end{figure}
+
+
+
 \section{CbC xv6}
 CbC xv6はGearsOSのシステムを利用してxv6 OSの置き換えを目指しているプロジェクトである。\cite{cbcxv6repo}
 xv6はv6 OS\cite{lions1996lions}をx86アーキテクチャ用にMITによって実装し直されたものである。
--- a/paper/chapter/04-interface.tex	Tue Feb 02 17:18:59 2021 +0900
+++ b/paper/chapter/04-interface.tex	Tue Feb 02 18:47:49 2021 +0900
@@ -105,6 +105,7 @@
 privateCodeGearにgotoする場合、 goto元のCodeGearからは\texttt{goto meta}経由で遷移する。
 goto metaが発行されるとStub Code Gearに遷移するが、現在のシステムではInterfaceから値を取得しに行く。
 
+\section{Interfaceの実装のCbCファイルへの構文の導入}
 
 \section{GearsCbCのInterfaceの実装時の問題}
 
@@ -218,7 +219,6 @@
 このような細かな調整をする場合は、 generate\_stub.pl側での自動生成はせずに、 雛形生成されたコンストラクタを変更すれば良い。
 あくまで雛形生成スクリプトはプログラマ支援であるため、 いくつかの手動での実装は許容している。
 
-\section{Interfaceの実装のCbCファイルへの構文の導入}
 
 \section{Interfaceの引数の検知}
 
--- a/paper/chapter/05-perl.tex	Tue Feb 02 17:18:59 2021 +0900
+++ b/paper/chapter/05-perl.tex	Tue Feb 02 18:47:49 2021 +0900
@@ -22,54 +22,17 @@
 すべてのTypeScriptのコードはJavaScriptにコンパイル可能である。
 JavaScriptに静的型の機能を取り込みたい場合に使われる言語であり、 JavaScriptの上位の言語と言える。
 
-GearsOSはCbCを拡張した言語となっている。
-ただしこの拡張自体はCbCコンパイラであるgcc、 llvm/clangには搭載されていない。
-その為GearsOSの拡張部分を、等価な純粋なCbCの記述に変換する必要がある。
-現在のGearsOSでは、 CMakeによるコンパイル時にPerlで記述された\texttt{generate\_stub.pl}と\texttt{generate\_context.pl}の2種類のスクリプトで変換される。
 
-
+GearsOSはCbCにノーマルレベル、メタレベルの書き別けの機能などを追加した拡張言語であると言える。
+コンパイル時にCMakeによって呼び出される2種類のPerlスクリプトで等価な純粋なCbCに変換される。
+これらのPerlスクリプトはGearsOSのCbCから純粋なCbCへと変換している為に一種のトランスコンパイラと言える。
 
-\begin{itemize}
-  \item \texttt{generate\_stub.pl}
-  \begin{itemize}
-    \item 各CbCファイルごとに呼び出されるスクリプト
-    \item 対応するメタ計算を導入したCbCファイル(拡張子はc)に変換する
-    \begin{itemize}
-      \item 図\ref{fig:generate_stub_pl_1}に処理の概要を示す
-    \end{itemize}
-  \end{itemize}
-  \item \texttt{generate\_context.pl}
-  \begin{itemize}
-    \item 生成したCbCファイルを解析し、使われているCodeGearを確定する
-    \item context.hを読み込み、使われているDataGearを確定する
-    \item Context関係の初期化ルーチンやCodeGear、 DataGearの番号であるenumを生成する
-    \begin{itemize}
-      \item 図\ref{fig:generate_context_1}に処理の概要を示す
-    \end{itemize}
-  \end{itemize}
-\end{itemize}
-
-これらのPerlスクリプトはプログラマが自分で動かすことはない。
-Perlスクリプトの実行手順はCMakeLists.txtに記述しており、 makeやninja-buildでのビルド時に呼び出される。(ソースコード \ref{src:cmake1})
-
-\lstinputlisting[label=src:cmake1, caption=CMakeList.txt内でのPerlの実行部分]{src/cmakefile.1.txt}
-
-\begin{figure}[htp]
-  \begin{center}
-   \includegraphics[width=160mm]{drawio/gears_os_build_flow.pdf}
-  \end{center}
-  \caption{generate\_sub.plを使ったトランスコンパイル}
-  \label{fig:generate_stub_pl_1}
- \end{figure}
-
-\begin{figure}[htp]
-  \begin{center}
-   \includegraphics[width=130mm]{drawio/old_generate_context.pdf}
-  \end{center}
-  \caption{generate\_context.plを使ったファイル生成}
-  \label{fig:generate_context_1}
- \end{figure}
-
+\section{トランスコンパイラによるメタレベルのコード生成}
+トランスコンパイラはノーマルレベルで記述されたGearsOSを、メタレベルを含むCbCへと変換する役割である。
+変換時に様々なメタ情報をCbCのファイルに書き出すことが可能である。
+従来はStubの生成や、 引数の変更などを行っていたが、 さらにメタレベルのコードをトランスコンパイラで作製したい。
+トランスコンパイラ上でメタレベルのコードを作製することによって、 GearsOS上でのアプリケーションの記述が容易になり、かつメタレベルのコードを柔軟に扱うことができる。
+本研究では様々なメタレベルのコードを、トランスコンパイラで生成することを検討した。
 
 
 \section{context.hの自動生成}
@@ -117,6 +80,7 @@
 Stub Code Gearに直ちに遷移してしまう\texttt{\_\_code meta}以外のMeta CodeGearに、 特定のCodeGearの計算が終わったら遷移したい。
 このためには、特定のCodeGearの遷移先のMetaCodeGearをユーザーが定義できるAPIが必要となる。
 このAPIを実装すると、ユーザーが柔軟にメタ計算を選択することが可能となる。
+これはいわゆるリフレクション処理に該当する。
 
 GearsOSのビルドシステムのAPIとして\texttt{meta.pm}を作製した。
 これはPerlのモジュールファイルとして実装した。
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/chapter/06-evaluation.tex	Tue Feb 02 18:47:49 2021 +0900
@@ -0,0 +1,7 @@
+\chapter{評価}
+
+\section{GearsOSのビルドシステム}
+
+\section{GearsOSのトランスコンパイラ}
+
+\section{GearsOSのメタ計算}
\ No newline at end of file
--- a/paper/chapter/conclusion.tex	Tue Feb 02 17:18:59 2021 +0900
+++ b/paper/chapter/conclusion.tex	Tue Feb 02 18:47:49 2021 +0900
@@ -1,7 +1,4 @@
-\chapter{まとめ}
-\section{総括}
+\chapter{結論}
 
 \section{今後の課題}
 
-\subsection{hogehoge}
-
--- a/paper/drawio/geasflow1.drawio	Tue Feb 02 17:18:59 2021 +0900
+++ b/paper/drawio/geasflow1.drawio	Tue Feb 02 18:47:49 2021 +0900
@@ -1,1 +1,1 @@
-<mxfile host="Electron" modified="2021-01-31T08:21:50.486Z" agent="5.0 (Windows NT 10.0; Win64; x64) AppleWebKit/537.36 (KHTML, like Gecko) draw.io/14.1.8 Chrome/87.0.4280.88 Electron/11.1.1 Safari/537.36" etag="JuOyPGK8KAoW3IoDYvsS" version="14.1.8" type="device"><diagram id="V5Gp7kS3jipglgoInpt8" name="ページ1">7VhRU6MwEP41nbl70ClQqH1sq+c9nKM3vRn1MUKE2JBgCJb6629DQqHQ9jhr1XPupWW/JEuy336bhJ4zjfNzgZLoggeY9ux+kPec055tDz0PfhWw1IBr9zUQChJoyKqAGXnGBiy7ZSTA6VpHyTmVJFkHfc4Y9uUahoTgi/Vu95yuvzVBIW4BMx/RNnpNAhlp9MQeVvh3TMKofLPljXRLjMrOZiVphAK+qEHOWc+ZCs6lforzKaYqdmVc9LhvW1pXExOYyS4Dnme/ssy7Hi1H45NLJ3tm7OfjkWEnlctywTiA9RuTCxnxkDNEzyp0InjGAqy89sGq+vzgPAHQAvABS7k0ZKJMcoAiGVPTinMib2rPt8rVsWus09x4LoxlaTApljd1ozZKmdWwwirHpVLw+Yo6BxC9YrXMrYE0UMoz4eMd0SsTEokQyx393BXdIBPMYwwzhHECUyTJ0/o8kEnYcNWv4hQeDK1/QbHx+4RoZt7Usz0K053cc1hwnXzvMeNlw1Fa0DeGDhCcvGqEp1D9X2Gh3p36giSydAkz1F51n3Z2UQrKVVm0iIjEswQVAV5A7VjPEZQmWs73JFe5tpXIJywkzndT2Q69GWB7RpymOlkDYy8qrVulgKO6zkvw1ely3kORB1WJ3VElW6h6G5XYB1LJOUYihdaZjlJHmcBekahHxmUHrdwhfx4WOXCZSUoYNniAxPwSRhFZVMPjvnsoHVn9ho5s+9htK8napCTXPRClJ//3tj1U63ZU7fA9VetuVW2aIPZy1U7vpsWZMk4IxaKmWu3239jcBu6H29yG+1fZwSa+cI79TKI7GAtnfEI7F9oPQZTnfDiiRhuIamY7C8bqggWWT1GaEr+IDxKyDb/KUaMdv1p83A3hKbHOtci84YqTIhnLQ2JDR47ViLqupWZU/QbWcOT1/+BIF9uWo4LB1bL3uAn0DyS/6QWaK+V9iYt/VTsZYQ/oa1cZgnZkQ3mUhEzlEOQAVGBnohRG4F4+Ng0xCQK9ZWOYXiF9vSsmKnxFQN1Jzz1VvmCX1kvYmYF7adhpcmu3NWwPNiTpwSRsbbr4bdcw4+rc+MmU6r5QqU1Hq3viWyl103Xkc3PXKo4v5a7p6PW4A7P6XKe7V988nbPf</diagram></mxfile>
\ No newline at end of file
+<mxfile host="Electron" modified="2021-02-02T09:06:54.023Z" agent="5.0 (Windows NT 10.0; Win64; x64) AppleWebKit/537.36 (KHTML, like Gecko) draw.io/14.1.8 Chrome/87.0.4280.88 Electron/11.1.1 Safari/537.36" etag="WHRDa5VHNI_z_1e4iOA4" version="14.1.8" type="device"><diagram id="V5Gp7kS3jipglgoInpt8" name="ページ1">7VrbUtswEP2azLQPZOIr5BECpZ1pSzvpFPqo2MIWKJIry8Th6ytZchxfEowTE2j7ZO9qtZL37FldkoE1maeXDEThF+pDPDBHfjqwzgemaThjSzykZqk0jjlSioAhXxsViil6hFqZmyXIh3HJkFOKOYrKSo8SAj1e0gHG6KJsdktxedQIBLCmmHoA17XXyOeh0p6Yx4X+I0RBmI9suGPVMge5sf6SOAQ+XayprIuBNWGUcvU2TycQy+DlcVH9PmxoXU2MQcLbdHic/kgS93q8HJ+eXFnJIyHffx+5em58mX8w9MX3a5EyHtKAEoAvCu0ZownxofQ6ElJh85nSSCgNobyDnC81mCDhVKhCPse6FaaI36y9/5Kuho6WzlPtOROWuUA4W96sC2u9pFh0y6S8X8wZvV9BZwlNPW46lDFNmAe3BCvPP8ACyLfYOcpORnJtAI3KJaRzKGYoDBjEgKOHcqYBnbDByq7AVLxoWJ8Bsfb7AHCiRxqYLuYyNhEgJfDd34nMxrNbSvhRnMF3KgxEtNKiUbwF8hlAAhngMPc2Y3mL4CKHKR9GOG8TE1eDKYN60mEsCC2TaxEiDqcRyIBYiJpSTh0QR4rltyiVKfgcfB8gE9PaiohuNV3NWV20DFvLi6IEGDmvw3X658q9o2gdgqj14HalYXfSmXXSzR6iRXCd/vTtr493n7wrHtws8jTfH+l0128UiSmvUuOknBnmqAK4mqfuVMF8NYvuaWBuJLPkbHcyX0LAYtE6VXAUtFVuN9BWLGmRfCWUt+DuDHj3QZaTVwnHiECt9wG7vxK9EM+yZThy+uL1kWFViG2aQ6dObaOJ2o7TE7VP/q/B7cuB03INPn5Va7DT0xo8mU2yve88QhiyN7ra2s6rW22Pdy+zdhNeMIVewsFM9BVnEYRbV9pXAZRbrZ6HB2rcAFQ124l/Kg+CQvIwiGPkZfEBjNfVW/c+GyP4ZJFZi4/TEJ5ct+PWpEIjy6gEXdXW2tak5scdPeGo5z1OPtze2Tf5Au4l8d7Ns6csnQSRO/C+LQvlqaZCPIwCIlNI5IQowNaZZBPyAD7VDXPk+2rFhmJ6GfPVohjJ8GUBdc4Gzrn0JRZp9QnPTcBnnGyq2DZQ2LQbcrQ3BhtN59PNFCZU7hv/LqLaHYla8bOSX4qnTYeRvxu5WmmshrxrjV3dOOwfu22n5d4vhWpb0eKuqOsQ+5lozJPZQS+oajW7Ie8378QOuRFrTKgG6h/ifqqxWrSK7I6VwahcDBnj8bByYdC2NtTQrbvquTpYey/sPojDDGljJ5BeqsqX49+9yJf8vHCJt/9tEG3D2g+KVUcvDGPT1VG/J9zXi2mVmF1PuLbxhKOeMXUbMN3HATeCTI4dewxF/E0danfaDRmVvDhuuRvqsBkSYvGLvUqH4n8P1sUf</diagram></mxfile>
\ No newline at end of file
Binary file paper/drawio/geasflow1.pdf has changed
Binary file paper/master_paper.pdf has changed
--- a/paper/master_paper.tex	Tue Feb 02 17:18:59 2021 +0900
+++ b/paper/master_paper.tex	Tue Feb 02 18:47:49 2021 +0900
@@ -99,12 +99,12 @@
 \input{chapter/03-gears.tex}
 \input{chapter/04-interface.tex}
 \input{chapter/05-perl.tex}
+\input{chapter/06-evaluation.tex}
 \input{chapter/conclusion.tex}
 
 
 
 % %謝辞
-\addcontentsline{toc}{chapter}{謝辞}
 \input{chapter/thanks.tex}
 %
 %参考文献