Mercurial > hg > Papers > 2019 > menikon-sigos
changeset 13:a107505931f7
fix
| author | e165723 <e165723@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 09 May 2019 15:21:02 +0900 |
| parents | f27751983554 |
| children | 1473a66fe4e6 |
| files | Paper/sigos.pdf Paper/sigos.tex |
| diffstat | 2 files changed, 106 insertions(+), 106 deletions(-) [+] |
line wrap: on
line diff
--- a/Paper/sigos.tex Wed May 08 20:23:56 2019 +0900 +++ b/Paper/sigos.tex Thu May 09 15:21:02 2019 +0900 @@ -51,7 +51,7 @@ \author{河野真治}{Shinji KONO}{IPSJ} \begin{abstract} -xv6 は MIT で教育用の目的で開発されたオペレーティングシステムで基本的な Unix の構造を持っている。当研究室で開発している Continuation based C (CbC) は継続を中心とした言語で、用いることにより検証しやすくなる。xv6 を CbC で書き換えることで、 オペレーティングシステムの基本的な機能に対する検証を行うために書き換えを行う。 +xv6 は MIT で教育用の目的で開発されたオペレーティングシステムで基本的な Unix の構造を持っている。当研究室で開発している Continuation based C (CbC) は継続を中心とした言語で、 用いることにより検証しやすくなる。xv6 を CbC で書き換えることで、 オペレーティングシステムの基本的な機能に対する検証を行うために書き換えを行う。 \end{abstract} @@ -62,35 +62,35 @@ \section{はじめに} 現代の OS では拡張性と信頼性を両立させることが要求されている。 -信頼性をノーマルレベルの計算に対して保証し、拡張性をメタレベルの計算で実現することを目標に Gears OS を設計中である。 +信頼性をノーマルレベルの計算に対して保証し、 拡張性をメタレベルの計算で実現することを目標に Gears OS を設計中である。 Gears OS は Continuation based C (CbC)\cite{cbc} によってアプリケーションと OS そのものを記述する。 -OS の下ではプログラムの記述は通常の処理の他に、メモリ管理、スレッドの待ち合わせやネットワークの管理、 +OS の下ではプログラムの記述は通常の処理の他に、 メモリ管理、 スレッドの待ち合わせやネットワークの管理、 エラーハンドリング等の記述しなければならない処理が存在する。 これらの計算をメタ計算と呼ぶ。 -メタ計算を通常の計算から切り離して記述するために、Code Gear、Data Gear という単位を提案している。 +メタ計算を通常の計算から切り離して記述するために、 Code Gear、 Data Gear という単位を提案している。 CbC はこの Code Gear と Data Gear の単位でプログラムを記述する。 -OS は時代とともに複雑さが増し、OS の信頼性を保証することは難しい。 -そこで、基本的な OS の機能を揃えたシンプルな OS である xv6 を CbC で書き換え、OS の機能を保証する。 +OS は時代とともに複雑さが増し、 OS の信頼性を保証することは難しい。 +そこで、 基本的な OS の機能を揃えたシンプルな OS である xv6 を CbC で書き換え、 OS の機能を保証する。 Code Gear は goto による継続で処理を表すことができる。 -これにより、状態遷移による OS の記述が可能となり、複雑な OS のモデル検査を可能とする。 -また、CbC は 定理証明支援系 Agda に置き換えることができるように構築されている。 +これにより、 状態遷移による OS の記述が可能となり、 複雑な OS のモデル検査を可能とする。 +また、 CbC は 定理証明支援系 Agda に置き換えることができるように構築されている。 これらを用いて OS の信頼性を保証したい。 -CbC でシステムやアプリケーションを記述するためには、Code Gear と Data Gear を柔軟に再利用する必要があり、 +CbC でシステムやアプリケーションを記述するためには、 Code Gear と Data Gear を柔軟に再利用する必要があり、 機能を接続するAPIと実装の分離が可能であることが望ましい。 -Gears OS の信頼性を保証するために、形式化されたモジュールシステムを提供する必要がある。 +Gears OS の信頼性を保証するために、 形式化されたモジュールシステムを提供する必要がある。 -本論文では、Interface を用いたモジュールシステムの説明と、 +本論文では、 Interface を用いたモジュールシステムの説明と、 xv6 の CbC 書き換えについての考察を行う。 \section{Continuation based C} CbC は処理を Code Gear という単位を用いて記述するプログラミ ング言語である。 Code Gear 間では軽量継続 (goto 文) による -遷移を行うので、継続前の Code Gear に戻 ることはない。この記述方法は +遷移を行うので、 継続前の Code Gear に戻 ることはない。この記述方法は 図1のように状態 遷移ベースのプログラミングに適している。 @@ -107,41 +107,41 @@ 上で実装されている。今回 xv6 のkernelの部分をこの CbC を 用いて書き換える。 \section{Gears におけるメタ計算} -プログラムを記述する際、ノーマルレベルの処理の他に、メモリ管理、スレッド管理、CPU や GPU の資源管理等、記述しなければならない処理 +プログラムを記述する際、 ノーマルレベルの処理の他に、 メモリ管理、 スレッド管理、 CPU や GPU の資源管理等、 記述しなければならない処理 が存在する。 これらの計算をメタ計算と呼ぶ。 -Code Gear、Data Gear にはそれぞれメタレベルの単位である Meta Code Gear、Meta Data Gear が存在し、 +Code Gear、 Data Gear にはそれぞれメタレベルの単位である Meta Code Gear、 Meta Data Gear が存在し、 これらを用いてメタ計算を実現する。 -Gears OS には Context と呼ばれる全ての Code Gear、Data Gear のリストを持つ Meta Data Gear が存在する。 -Gears OS ではこの Context を常に持ち歩いているが、これはノーマルレベルでは見えることはない。 +Gears OS には Context と呼ばれる全ての Code Gear、 Data Gear のリストを持つ Meta Data Gear が存在する。 +Gears OS ではこの Context を常に持ち歩いているが、 これはノーマルレベルでは見えることはない。 ノーマルレベルの処理とメタレベルを含む処理は同じ動作を行う。 -しかしメタレベルの計算を含むプログラムとノーマルレベルでは、Data Gear の扱いなどでギャップがある。 -ノーマルレベルでは Code Gear は Data Gear を引数の集合として引き渡しているが、 -メタレベルでは Context に格納されており、ここを参照することで Data Gear を扱っている。 +しかしメタレベルの計算を含むプログラムとノーマルレベルでは、 Data Gear の扱いなどでギャップがある。 +ノーマルレベルでは Code Gear は Data Gear を引数の集合として引き渡しているが、 +メタレベルでは Context に格納されており、 ここを参照することで Data Gear を扱っている。 このギャップを解消するためにメタレベルでは stub Code Gear と呼ばれる Context から Data Gear の参照を行う Meta Code Gear が Code Gear 継続前に挿入されこれを解決する。 -従来の研究でメタ計算を用いる場合は、関数型言語では Monad を用いる\cite{moggi-monad}。これは Haskell では実行時の環境を記述する構文として使われている。 -OS の研究では、メタ計算の記述に型つきアセンブラ(Typed Assembler)を用いることがある\cite{Yang:2010:SLI:1806596.1806610}。 +従来の研究でメタ計算を用いる場合は、 関数型言語では Monad を用いる\cite{moggi-monad}。これは Haskell では実行時の環境を記述する構文として使われている。 +OS の研究では、 メタ計算の記述に型つきアセンブラ(Typed Assembler)を用いることがある\cite{Yang:2010:SLI:1806596.1806610}。 Python や Haskell による記述をノーマルレベルとして 採用した OS の検証の研究もある\cite{Klein:2009:SFV:1629575.1629596,Chen:2015:UCH:2815400.2815402}。 SMIT などのモデル検査を OS の検証に用いた例もある\cite{Sigurbjarnarson:2016:PVF:3026877.3026879}。 -本研究で用いる Meta Gear は制限された Monad に相当し、型つきアセンブラよりは大きな表現単位を提供する。 -Haskell などの関数型プログラミング言語では実行環境が複雑であり、実行時の資源使用を明確にすることができない。 -CbC はスタック上に隠された環境を持たないので、メタレベルで使用する資源を明確にできるという利点がある。 -ただし、Gear のプログラミングスタイルは、従来の関数呼出を中心としたものとはかなり異なる。 +本研究で用いる Meta Gear は制限された Monad に相当し、 型つきアセンブラよりは大きな表現単位を提供する。 +Haskell などの関数型プログラミング言語では実行環境が複雑であり、 実行時の資源使用を明確にすることができない。 +CbC はスタック上に隠された環境を持たないので、 メタレベルで使用する資源を明確にできるという利点がある。 +ただし、 Gear のプログラミングスタイルは、 従来の関数呼出を中心としたものとはかなり異なる。 \section{Interface} Interface は Gears OS のモジュール化の仕組みである。 %java のインターフェースの話を入れる モジュール化 -Interface は呼び出しの引数になる Data Gear の集合であり、そこで呼び出される Code Gear のエントリである。 +Interface は呼び出しの引数になる Data Gear の集合であり、 そこで呼び出される Code Gear のエントリである。 呼び出される Code Gear の引数となる Data Gear はここで全て定義される。 Interface を定義することで複数の実装を持つことができる。 図 \ref{fig:Interface} は Stack の Interface とその実装を表したものである。 @@ -154,20 +154,20 @@ \label{fig:Interface} \end{figure} -Data Gear は、ノーマルレベルとメタレベルで見え方が異なる。 +Data Gear は、 ノーマルレベルとメタレベルで見え方が異なる。 ノーマルレベルの Code Gear では Data Gear の引数に見える。 -しかし、メタレベルでは Data Gear は Context が持つ構造体である。 +しかし、 メタレベルでは Data Gear は Context が持つ構造体である。 この見え方の違いを Meta Code Gear である stub Code Gear によって調整する必要がある。 -また、CbC は関数呼び出しと異なり、goto による継続で遷移を行う。 +また、 CbC は関数呼び出しと異なり、 goto による継続で遷移を行う。 このため CbC の継続にはスタックフレームがなく引数を格納する場所がない。 Context は初期化の際に引数格納用の Data Gear の領域を確保する。 Code Gear が継続する際にはこの領域に引数の Data Gear を格納する。 この領域に確保された Data Gear へのアクセスは Interface の情報から行われる。 -ソースコード\ref{pushStack} は、pushSingleLinkedStack のソースコードである。 -ノーマルレベルの Code Gear では Stack の push の操作は、 +ソースコード\ref{pushStack} は、 pushSingleLinkedStack のソースコードである。 +ノーマルレベルの Code Gear では Stack の push の操作は、 push するデータと次の継続先の Code Gear という引数の集合のように見える。 しかしメタレベルでは Context が持つ構造体である。 @@ -200,30 +200,30 @@ ソースコード\ref{interface}は Stack の Interface である。 typedef struct Stack で Interface を定義する。 Impl には実装の型が入る。 -ソースコード\ref{interface}、2〜4行目のunion Data で定義されてるものは、 +ソースコード\ref{interface}、 2〜4行目のunion Data で定義されてるものは、 Interface の API で用いる全ての Data Gear である。 Interface の全ての API で用いる全ての Data Gear は Interface で定義される。 -ソースコード\ref{interface}、5〜13行目の \_\_code で記述されているものは、 +ソースコード\ref{interface}、 5〜13行目の \_\_code で記述されているものは、 Interface の API である。 ここでは Stack のAPI である push や pop などの Code Gear となっている。 \lstinputlisting[label=interface, caption=StackのInterface]{./src/Stack.cbc} -通常 Code Gear、Data Gear に参照するためには Context を通す必要があるが、 +通常 Code Gear、 Data Gear に参照するためには Context を通す必要があるが、 Interface を記述することでデータ構造の API と Data Gear を結びつけることが出来る。 これによりノーマルレベルとメタレベルの分離が可能となった。 ソースコード\ref{implement}は Stack の実装の例である。 createImpl は実装の初期化を行う関数である。 -Interface の実装を呼び出す際、この関数を呼び出すことで ソースコード\ref{pushStack} 4 行目のように実装の操作を呼び出せるようになる。 +Interface の実装を呼び出す際、 この関数を呼び出すことで ソースコード\ref{pushStack} 4 行目のように実装の操作を呼び出せるようになる。 ソースコード\ref{implement} 2 行目は操作する Stack のデータ構造の確保をしている。 SingleLinkedStack のデータ構造は ソースコード \ref{SingleLinkedStack} である。 ソースコード\ref{implement} 6〜12行目で実装の Code Gear に代入しているものは Context が持つ enum で定義された Code Gear の番号である。 -%ソースコード \ref{Gears_code} 3行目で stack\verb|->|pop へと goto しているが、 +%ソースコード \ref{Gears_code} 3行目で stack\verb|->|pop へと goto しているが、 %stack\verb|->|pop には Code Gear の番号が入っているため実装した Code Gear へと継続する。 -%このため、ソースコード \ref{Gears_code} では 6行目の popSingleLinkedStack へと継続している。 +%このため、 ソースコード \ref{Gears_code} では 6行目の popSingleLinkedStack へと継続している。 \lstinputlisting[label=implement, caption=SingleLinkedStackの実装]{./src/stackimpl.cbc} @@ -241,18 +241,18 @@ \section{xv6 の CbC への書き換え} xv6 は 2006 年に MIT のオペレーティングシステムコースで教育用の目的として開発されたオペレーティングシステムである。 -xv6 はプロセス、仮想メモリ、カーネルとユーザの分離、割り込み、 -ファイルシステムなどの基本的な Unix の構造を持つにも関わらず、 +xv6 はプロセス、 仮想メモリ、 カーネルとユーザの分離、 割り込み、 +ファイルシステムなどの基本的な Unix の構造を持つにも関わらず、 シンプルで学習しやすい。 CbC は 継続を中心とした言語であるため状態遷移モデルに落とし込むことができる。 -xv6 を CbC で書き換えることにより、OS の機能の保証が可能となる。 +xv6 を CbC で書き換えることにより、 OS の機能の保証が可能となる。 -また、ハードウェア上でのメタレベルの計算や並列実行を行いたい。 -このため、xv6 を ARM\cite{arm} プロセッサを搭載したシングルボードコンピュータである Raspberry pi 用に移植した xv6-rpi を用いて実装する。 +また、 ハードウェア上でのメタレベルの計算や並列実行を行いたい。 +このため、 xv6 を ARM\cite{arm} プロセッサを搭載したシングルボードコンピュータである Raspberry pi 用に移植した xv6-rpi を用いて実装する。 xv6 全体を CbC で書き換えるためには Interface を用いてモジュール化する必要がある。 -xv6 をモジュール化し、CbC で書き換えることができれば、Gears OS の機能を置き換えることもできる。 +xv6 をモジュール化し、 CbC で書き換えることができれば、 Gears OS の機能を置き換えることもできる。 図 \ref{fig:xv6Interface} は xv6 の構成図となる。 \begin{figure}[htp] @@ -265,15 +265,15 @@ xv6 はカーネルと呼ばれる形式をとっている。 カーネルは OS にとって中核となるプログラムである。 -xv6 ではカーネルとユーザープログラムは分離されており、カーネルはプログラムにプロセス管理、メモリ管理、I/O やファイルの管理などのサービスを提供する。 -ユーザープログラムがカーネルのサービスを呼び出す場合、システムコールを用いてユーザー空間からカーネル空間へ入りサービスを実行する。 -カーネルは CPU のハードウェア保護機構を使用して、ユーザー空間で実行されているプロセスが自身のメモリのみアクセスできるように保護している。 -ユーザープログラムがシステムコールを呼び出すと、ハードウェアが特権レベルを上げ、カーネルのプログラムが実行される。 -この特権レベルを持つプロセッサの状態をカーネルモード、特権のない状態をユーザーモードという。 +xv6 ではカーネルとユーザープログラムは分離されており、 カーネルはプログラムにプロセス管理、 メモリ管理、 I/O やファイルの管理などのサービスを提供する。 +ユーザープログラムがカーネルのサービスを呼び出す場合、 システムコールを用いてユーザー空間からカーネル空間へ入りサービスを実行する。 +カーネルは CPU のハードウェア保護機構を使用して、 ユーザー空間で実行されているプロセスが自身のメモリのみアクセスできるように保護している。 +ユーザープログラムがシステムコールを呼び出すと、 ハードウェアが特権レベルを上げ、 カーネルのプログラムが実行される。 +この特権レベルを持つプロセッサの状態をカーネルモード、 特権のない状態をユーザーモードという。 ユーザープログラムがカーネルの提供するサービスを呼び出す際にはシステムコールを用いる。 -ユーザープログラムがシステムコールを呼び出すと、トラップが発生する。 -トラップが発生すると、ユーザープログラムは中断され、カーネルに切り替わり処理を行う。 +ユーザープログラムがシステムコールを呼び出すと、 トラップが発生する。 +トラップが発生すると、 ユーザープログラムは中断され、 カーネルに切り替わり処理を行う。 ソースコード \ref{syscall_list} は xv6 のシステムコールのリストである。 \begin{lstlisting}[frame=lrbt,label=syscall_list,caption={\footnotesize xv6 のシステムコールのリスト}] @@ -302,56 +302,56 @@ }; \end{lstlisting} -プロセスとは、カーネルが実行するプログラムの単位である。 -xv6 のプロセスは、ユーザー空間メモリとカーネル用のプロセスの状態を持つ空間で構成されている。 -プロセスは独立しており、他のプロセスからメモリを破壊されたりすることはない。 -また、独立していることでカーネルそのものを破壊することもない。 +プロセスとは、 カーネルが実行するプログラムの単位である。 +xv6 のプロセスは、 ユーザー空間メモリとカーネル用のプロセスの状態を持つ空間で構成されている。 +プロセスは独立しており、 他のプロセスからメモリを破壊されたりすることはない。 +また、 独立していることでカーネルそのものを破壊することもない。 各プロセスの状態は struct proc によって管理されている。 プロセスは fork システムコールによって新たに生成される。 -fork は新しく、親プロセスと呼ばれる呼び出し側と同じメモリ内容の、子プロセスと呼ばれるプロセスを生成する。 -fork システムコールは、親プロセスであれば子プロセスのID、子プロセスであれば 0 を返す。 -親プロセスと子プロセスは最初は同じ内容を持っているが、それぞれ異なるメモリ、レジスタで実行されているため、片方のメモリ内容を変更してももう片方に影響はない。 -exit システムコールはプロセスの停止を行い、メモリを解放する。 +fork は新しく、 親プロセスと呼ばれる呼び出し側と同じメモリ内容の、 子プロセスと呼ばれるプロセスを生成する。 +fork システムコールは、 親プロセスであれば子プロセスのID、 子プロセスであれば 0 を返す。 +親プロセスと子プロセスは最初は同じ内容を持っているが、 それぞれ異なるメモリ、 レジスタで実行されているため、 片方のメモリ内容を変更してももう片方に影響はない。 +exit システムコールはプロセスの停止を行い、 メモリを解放する。 wait システムコールは終了した子プロセスのIDを返す。子プロセスが終了するまで待つ。 exec システムコールは呼び出し元のプロセスのメモリをファイルシステムのファイルのメモリイメージと置き換え実行する。 -ファイルには命令、データなどの配置が指定されたフォーマット通りになっていなければならない。 +ファイルには命令、 データなどの配置が指定されたフォーマット通りになっていなければならない。 xv6 は ELF と呼ばれるフォーマットを扱う。 -ファイルディスクリプタは、カーネルが管理するプロセスが読み書きを行うオブジェクトを表す整数値である。 -プロセスは、ファイル、ディレクトリ、デバイスを開く、または既存のディスクリプタを複製することによって、 +ファイルディスクリプタは、 カーネルが管理するプロセスが読み書きを行うオブジェクトを表す整数値である。 +プロセスは、 ファイル、 ディレクトリ、 デバイスを開く、 または既存のディスクリプタを複製することによって、 ファイルディスクリプタを取得する。 xv6 はプロセス毎にファイルディスクリプタのテーブルを持っている。 -ファイルディスクリプタは普通、0 が標準入力、1 が標準出力、2 がエラー出力として使われる。 +ファイルディスクリプタは普通、 0 が標準入力、 1 が標準出力、 2 がエラー出力として使われる。 ファイルディスクリプタのテーブルのエントリを変更することで入出力先を変更することができる。 -1 の標準出力を close し、ファイルを open することでプログラムはファイルに出力することになる。 +1 の標準出力を close し、 ファイルを open することでプログラムはファイルに出力することになる。 ファイルディスクリプタはファイルがどのように接続するか隠すことでファイルへの入出力を容易にしている。 xv6 のファイルシステムはバイト配列であるデータファイルとデータファイルおよび他のディレクトリの参照を含むディレクトリを提供する。 ディレクトリは root と呼ばれる特別なディレクトリから始まるツリーを形成している。 絶対パスである "/dir1/dir2/file1" というパスは root ディレクトリ内の dir1 という名前のディレクトリ内の dir2 という名前のディレクトリ内の file というデータファイルを指す。 -相対パスである "dir2/file2" のようなパスは、現在のディレクトリ内の dir2 という名前のディレクトリ内の file というデータファイルを指す。 +相対パスである "dir2/file2" のようなパスは、 現在のディレクトリ内の dir2 という名前のディレクトリ内の file というデータファイルを指す。 \section{xv6-rpi の CbC 対応} -オリジナルの xv6 は x86 アーキテクチャで実装されたものだが、xv6-rpi は Raspberry Pi 用に実装されたものである。 +オリジナルの xv6 は x86 アーキテクチャで実装されたものだが、 xv6-rpi は Raspberry Pi 用に実装されたものである。 Raspberry Pi は ARM\cite{arm} プロセッサを搭載したシングルボードコンピュータである。 -教育用のコンピューターとして開発されたもので、低価格であり、小型であるため使い勝手が良い。 -ストレージにハードディスクや SSD を使用するのではなく、SD カードを用いる。 -HDMI 出力や USB ポートも備えており、開発に最適である。 +教育用のコンピューターとして開発されたもので、 低価格であり、 小型であるため使い勝手が良い。 +ストレージにハードディスクや SSD を使用するのではなく、 SD カードを用いる。 +HDMI 出力や USB ポートも備えており、 開発に最適である。 -Raspberry Pi には Raspberry Pi 3、Raspberry Pi 2、Raspberry Pi 1、Raspberry Pi Zero といったバージョンが存在する。 +Raspberry Pi には Raspberry Pi 3、 Raspberry Pi 2、 Raspberry Pi 1、 Raspberry Pi Zero といったバージョンが存在する。 -xv6-rpi を CbC で書き換えるために、 +xv6-rpi を CbC で書き換えるために、 GCC 上で実装した CbC コンパイラを ARM 向けに build し xv6-rpi をコンパイルした。 これにより、 xv6-rpi を CbC で書き換えることができるようになった。 \section{CbC によるシステムコールの書き換え} -CbC によるシステムコールの書き換えは、従来の xv6 のシステムコールの形から、 +CbC によるシステムコールの書き換えは、 従来の xv6 のシステムコールの形から、 大きく崩すことなく可能である。 -CbC は Code Gear 間の遷移は goto による継続で行われるため、 +CbC は Code Gear 間の遷移は goto による継続で行われるため、 状態遷移ベースでのプログラムに適している。 -xv6 を CbC で書き換えることにより、OS のプログラムを状態遷移モデルに落とし込むことができる。 +xv6 を CbC で書き換えることにより、 OS のプログラムを状態遷移モデルに落とし込むことができる。 これにより状態遷移系のモデル検査が可能となる。 図 \ref{fig:state} は CbC 書き換えによる read システムコールの遷移図である。 @@ -367,8 +367,8 @@ システムコールはソースコード \ref{syscall_list} の関数のリストの番号から呼び出される。 CbC でも同様に num で指定された番号の cbccodes のリストの Code Gear へ goto する。 ソースコード \ref{syscall} 6行目でトラップフレームからシステムコールの番号を取得する。 -通常のシステムコールであればソースコード \ref{syscall} 13行目からの分岐へ入るが、 -cbc システムコールであれば ソースコード \ref{syscall} 8行目へ入り、goto によって遷移する。 +通常のシステムコールであればソースコード \ref{syscall} 13行目からの分岐へ入るが、 +cbc システムコールであれば ソースコード \ref{syscall} 8行目へ入り、 goto によって遷移する。 引数に持つ cbc\_ret は 継続した先でトラップに戻ってくるための Code Gear である。 @@ -401,10 +401,10 @@ } \end{lstlisting} -ソースコード \ref{cbc_read} は、 +ソースコード \ref{cbc_read} は、 read システムコールであるソースコード \ref{sys_read} を CbC で書き換えたコードである。 -CbC は C の関数を呼び出すことも出来るため、書き換えたい部分だけを書き換えることができる。 -Code Gear であるため、ソースコード \ref{cbc_read} 7、9行目のように関数呼び出しではなく goto による継続となる。 +CbC は C の関数を呼び出すことも出来るため、 書き換えたい部分だけを書き換えることができる。 +Code Gear であるため、 ソースコード \ref{cbc_read} 7、 9行目のように関数呼び出しではなく goto による継続となる。 \begin{lstlisting}[frame=lrbt,label=cbc_read,caption={\footnotesize cbc\_read システムコール}] __code cbc_read(__code (*next)(int ret)){ @@ -433,74 +433,74 @@ return fileread(f, p, n); } \end{lstlisting} -ソースコード \ref{cbcfileread} は、ソースコード \ref{fileread} を CbC で書き換えたコードである。 +ソースコード \ref{cbcfileread} は、 ソースコード \ref{fileread} を CbC で書き換えたコードである。 継続で Code Gear 間を遷移するため関数呼び出しとは違い元の関数には戻ってこない。 -このため、書き換えの際には ソースコード \ref{cbcfileread} のように分割する必要がある。 +このため、 書き換えの際には ソースコード \ref{cbcfileread} のように分割する必要がある。 プロセスの状態を持つ struct proc は大域変数であるため Code Gear を用いるために必要なパラメーターを cbc\_arg として持たせることにした。 継続を行う際には必要なパラメーターをここに格納する。 \lstinputlisting[label=cbcfileread, caption=fileread の CbC 書き換えの例]{./src/fileread.cbc} \lstinputlisting[label=fileread, caption=書き換え前の fileread]{./src/fileread.c} -ソースコード \ref{cbcreadi} は、ソースコード \ref{readi} を書き換えたコードである。 +ソースコード \ref{cbcreadi} は、 ソースコード \ref{readi} を書き換えたコードである。 CbC では cbc\_devsw を定義しておりソースコード \ref{cbcreadi} 11行目で次の Code Gear へと継続する。 -cbc\_devsw はソースコード \ref{consoleinit}で初期化されており、cbc\_consoleread へと継続する。 +cbc\_devsw はソースコード \ref{consoleinit}で初期化されており、 cbc\_consoleread へと継続する。 \lstinputlisting[label=cbcreadi, caption=readi の CbC 書き換えの例]{./src/readi.cbc} \lstinputlisting[label=readi, caption=書き換え前の readi]{./src/readi.c} \lstinputlisting[label=consoleinit, caption=consoleinit]{./src/consoleinit.c} -ソースコード \ref{cbc_consoleread} の cbc\_consoleread は、ソースコード \ref{consoleread} を書き換えたものである。 -ソースコード \ref{cbc_consoleread} 11、50、行目 では sleep へ継続する際、戻るべき継続先を一緒に送ることで、 +ソースコード \ref{cbc_consoleread} の cbc\_consoleread は、 ソースコード \ref{consoleread} を書き換えたものである。 +ソースコード \ref{cbc_consoleread} 11、 50、 行目 では sleep へ継続する際、 戻るべき継続先を一緒に送ることで、 sleep から consoleread に戻ってくることができる。 \lstinputlisting[label=cbc_consoleread, caption=consoleread の CbC 書き換えの例]{./src/console.cbc} \lstinputlisting[label=consoleread, caption=書き換え前の consoleread]{./src/console.c} -CbC による書き換えにより、状態遷移ベースへと書き換えることができた。 -現在はシステムコールの書き換えのみであるが、カーネル全体を書き換えることで、 +CbC による書き換えにより、 状態遷移ベースへと書き換えることができた。 +現在はシステムコールの書き換えのみであるが、 カーネル全体を書き換えることで、 カーネルを状態遷移モデルに落とし込むことができる。 \section{結論} -本論文では Gears OS のプロトタイプの設計と実装、メタ計算である Context と stub の生成を行う Perl スクリプトの記述を行った。 -さらに Raspberry Pi 上での Gears OS 実装の考察、xv6 の機能の一部を CbC で書き換えを行った。 +本論文では Gears OS のプロトタイプの設計と実装、 メタ計算である Context と stub の生成を行う Perl スクリプトの記述を行った。 +さらに Raspberry Pi 上での Gears OS 実装の考察、 xv6 の機能の一部を CbC で書き換えを行った。 -Code Gear 、Data Gear を処理とデータの単位として用いて Gears OS を設計した。 -Code Gear、Data Gear にはメタ計算を記述するための Meta Code Gear、Meta Data Gear が存在する。 -メタ計算を Meta Code Gear、によって行うことでメタ計算を階層化して行うことができる。 +Code Gear 、 Data Gear を処理とデータの単位として用いて Gears OS を設計した。 +Code Gear、 Data Gear にはメタ計算を記述するための Meta Code Gear、 Meta Data Gear が存在する。 +メタ計算を Meta Code Gear、 によって行うことでメタ計算を階層化して行うことができる。 Code Gear は関数より細かく分割されてるためメタ計算を柔軟に記述できる。 -Gears OS は Code Gear と Input/Output Data Gear の組を Task とし、並列実行を行う。 +Gears OS は Code Gear と Input/Output Data Gear の組を Task とし、 並列実行を行う。 Code Gear と Data Gear は Interface と呼ばれるまとまりとして記述される。 -Interface は使用される Data Gear の定義と、それに対する操作を行う Code Gear の集合である。 -Interface は複数の実装をもち、Meta Data Gear として定義される。 -従来の関数呼び出しでは引数をスタック上に構成し、関数の実装アドレスを Call するが、 -Gears OS では引数は Context 上に用意された Interface の Data Gear に格納され、操作に対応する Code Gear に goto する。 +Interface は使用される Data Gear の定義と、 それに対する操作を行う Code Gear の集合である。 +Interface は複数の実装をもち、 Meta Data Gear として定義される。 +従来の関数呼び出しでは引数をスタック上に構成し、 関数の実装アドレスを Call するが、 +Gears OS では引数は Context 上に用意された Interface の Data Gear に格納され、 操作に対応する Code Gear に goto する。 -Context は使用する Code Gear、Data Gear をすべて格納している Meta Data Gear である。 +Context は使用する Code Gear、 Data Gear をすべて格納している Meta Data Gear である。 通常の計算から Context を直接扱うことはセキュリティ上好ましくない。 このため Context から必要なデータを取り出して Code Gear に接続する Meta Code Gear である stub Code Gear を定義した。 -stub Code Gear は Code Gear 毎に記述され、Code Gear 間の遷移の前に挿入される。 +stub Code Gear は Code Gear 毎に記述され、 Code Gear 間の遷移の前に挿入される。 これらのメタ計算の記述は煩雑であるため Perl スクリプトによる自動生成を行なった。 -これにより Gears OS のコードの煩雑さは改善され、ユーザーレベルではメタを意識する必要がなくなった。 +これにより Gears OS のコードの煩雑さは改善され、 ユーザーレベルではメタを意識する必要がなくなった。 ハードウェア上での Gears OS の実装を実現させるために Raspberry Pi 上での実装を考察した。 比較的シンプルな OS である xv6 を CbC に書き換えることにした。 -xv6 を CbC で書き換えることによって、実行可能な CbC プログラムで記述された OS がそのまま、 -状態遷移モデルによるモデル検査、Agda による定理証明が可能となる。 +xv6 を CbC で書き換えることによって、 実行可能な CbC プログラムで記述された OS がそのまま、 +状態遷移モデルによるモデル検査、 Agda による定理証明が可能となる。 -今後の課題は、 -現在は xv6 のシステムコールの一部のみの書き換えと、設計のみしか行っていないので、カーネル全ての書き換えと、 -Gears OS の TaskManager の置き換えを行い、Gears OS の機能を xv6 に組み込む必要がある。 -また、xv6-rpi は QEMU のみの動作でしか確認してないため、実機上での動作が可能なように実装する必要がある。 +今後の課題は、 +現在は xv6 のシステムコールの一部のみの書き換えと、 設計のみしか行っていないので、 カーネル全ての書き換えと、 +Gears OS の TaskManager の置き換えを行い、 Gears OS の機能を xv6 に組み込む必要がある。 +また、 xv6-rpi は QEMU のみの動作でしか確認してないため、 実機上での動作が可能なように実装する必要がある。 \nocite{*} \bibliographystyle{ipsjunsrt} \bibliography{reference} % \begin{thebibliography}{9} -% \bibitem{latex} 宮城光希: \textbf{継続を基本とした言語によるOSのモジュール化}. 琉球大学理工学研究科修士論文、2019 +% \bibitem{latex} 宮城光希: \textbf{継続を基本とした言語によるOSのモジュール化}. 琉球大学理工学研究科修士論文、 2019 % \end{thebibliography} \end{document}