Mercurial > hg > Papers > 2019 > menikon-sigos
changeset 10:7b4fed4aefb1
add figures
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 08 May 2019 18:23:07 +0900 |
| parents | 44c5e4cacaae |
| children | 31f3ff793b58 |
| files | Paper/fig/Interface.graffle Paper/fig/Interface.pdf Paper/fig/Interface.xbb Paper/fig/state.graffle Paper/fig/state.pdf Paper/fig/state.xbb Paper/fig/xv6.graffle Paper/fig/xv6.pdf Paper/fig/xv6.xbb Paper/sigos.pdf Paper/sigos.tex Paper/src/Stack.cbc Paper/src/console.c Paper/src/console.cbc Paper/src/consoleinit.c Paper/src/fileread.c Paper/src/fileread.cbc Paper/src/readi.c Paper/src/readi.cbc Paper/src/stackimpl.cbc Paper/xv6.pdf |
| diffstat | 21 files changed, 713 insertions(+), 8 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/fig/Interface.xbb Wed May 08 18:23:07 2019 +0900 @@ -0,0 +1,8 @@ +%%Title: fig/Interface.pdf +%%Creator: extractbb 20160307 +%%BoundingBox: 0 0 288 421 +%%HiResBoundingBox: 0.000000 0.000000 288.000000 421.000000 +%%PDFVersion: 1.4 +%%Pages: 1 +%%CreationDate: Thu Feb 7 14:56:37 2019 +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/fig/state.xbb Wed May 08 18:23:07 2019 +0900 @@ -0,0 +1,8 @@ +%%Title: fig/state.pdf +%%Creator: extractbb 20160307 +%%BoundingBox: 0 0 1142 453 +%%HiResBoundingBox: 0.000000 0.000000 1142.000000 453.000000 +%%PDFVersion: 1.3 +%%Pages: 1 +%%CreationDate: Mon Feb 11 20:08:25 2019 +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/fig/xv6.xbb Wed May 08 18:23:07 2019 +0900 @@ -0,0 +1,8 @@ +%%Title: fig/xv6.pdf +%%Creator: extractbb 20160307 +%%BoundingBox: 0 0 656 695 +%%HiResBoundingBox: 0.000000 0.000000 656.000000 695.000000 +%%PDFVersion: 1.4 +%%Pages: 1 +%%CreationDate: Sun Feb 10 12:31:31 2019 +
--- a/Paper/sigos.tex Wed May 08 17:38:26 2019 +0900 +++ b/Paper/sigos.tex Wed May 08 18:23:07 2019 +0900 @@ -5,6 +5,7 @@ \usepackage{listings} \usepackage{caption} + \def\Underline{\setbox0\hbox\bgroup\let\\\endUnderline} \def\endUnderline{\vphantom{y}\egroup\smash{\underline{\box0}}\\} \def\|{\verb|} @@ -63,7 +64,7 @@ 現代の OS では拡張性と信頼性を両立させることが要求されている。 信頼性をノーマルレベルの計算に対して保証し、拡張性をメタレベルの計算で実現することを目標に Gears OS を設計中である。 -Gears OS は Continuation based C (CbC) によってアプリケーションと OS そのものを記述する。 +Gears OS は Continuation based C (CbC)\cite{cbc} によってアプリケーションと OS そのものを記述する。 OS の下ではプログラムの記述は通常の処理の他に、メモリ管理、スレッドの待ち合わせやネットワークの管理、 エラーハンドリング等の記述しなければならない処理が存在する。 これらの計算をメタ計算と呼ぶ。 @@ -102,21 +103,405 @@ \label{fig:cbc} \end{figure} -現在CbCはCコンパイラであるGCC\cite{cbc-gcc}及びLLVM\cite{cbc-llvm}をバックエンドとしたclang +現在CbCはCコンパイラであるGCC\cite{gcc}及びLLVM\cite{llvm}をバックエンドとしたclang % MicroCコンパイラ 上で実装されている。今回 xv6 のkernelの部分をこの CbC を 用いて書き換える。 +\section{Gears におけるメタ計算} +プログラムを記述する際、ノーマルレベルの処理の他に、メモリ管理、スレッド管理、CPU や GPU の資源管理等、記述しなければならない処理 +が存在する。 +これらの計算をメタ計算と呼ぶ。 +Code Gear、Data Gear にはそれぞれメタレベルの単位である Meta Code Gear、Meta Data Gear が存在し、 +これらを用いてメタ計算を実現する。 + +Gears OS には Context と呼ばれる全ての Code Gear、Data Gear のリストを持つ Meta Data Gear が存在する。 +Gears OS ではこの Context を常に持ち歩いているが、これはノーマルレベルでは見えることはない。 + +ノーマルレベルの処理とメタレベルを含む処理は同じ動作を行う。 +しかしメタレベルの計算を含むプログラムとノーマルレベルでは、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}。 +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 のプログラミングスタイルは、従来の関数呼出を中心としたものとはかなり異なる。 + + + +\section{Interface} +Interface は Gears OS のモジュール化の仕組みである。 +%java のインターフェースの話を入れる モジュール化 +Interface は呼び出しの引数になる Data Gear の集合であり、そこで呼び出される Code Gear のエントリである。 +呼び出される Code Gear の引数となる Data Gear はここで全て定義される。 +Interface を定義することで複数の実装を持つことができる。 +図 \ref{fig:Interface} は Stack の Interface とその実装を表したものである。 + +\begin{figure}[ht] + \begin{center} + \includegraphics[width=60mm]{fig/Interface.pdf} + \end{center} + \caption{Stack の Interface とその実装} + \label{fig:Interface} +\end{figure} + +Data Gear は、ノーマルレベルとメタレベルで見え方が異なる。 +ノーマルレベルの Code Gear では Data Gear の引数に見える。 +しかし、メタレベルでは Data Gear は Context が持つ構造体である。 +この見え方の違いを Meta Code Gear である stub Code Gear によって調整する必要がある。 + +また、CbC は関数呼び出しと異なり、goto による継続で遷移を行う。 +このため CbC の継続にはスタックフレームがなく引数を格納する場所がない。 + +Context は初期化の際に引数格納用の Data Gear の領域を確保する。 +Code Gear が継続する際にはこの領域に引数の Data Gear を格納する。 +この領域に確保された Data Gear へのアクセスは Interface の情報から行われる。 + +ソースコード\ref{pushStack} は、pushSingleLinkedStack のソースコードである。 +ノーマルレベルの Code Gear では Stack の push の操作は、 +push するデータと次の継続先の Code Gear という引数の集合のように見える。 +しかしメタレベルでは Context が持つ構造体である。 + +stub Code Gear では Context が確保した 引数格納用の領域に格納した Data Gear を取り出している。 +Interface を導入することでノーマルレベルとメタレベルのズレの調整を解決した。 + +\begin{lstlisting}[frame=lrbt,label=pushStack,caption={pushSingleLinkedStack}] +__code stackTest1(struct Stack* stack) { + Node* node = new Node(); + node->color = Red; + goto stack->push(node, stackTest2); +} + +__code pushSingleLinkedStack_stub(struct Context* context) { + SingleLinkedStack* stack = (SingleLinkedStack*)context->data[D_Stack]->Stack.stack->Stack.stack; + Data* data = context->data[D_Stack]->Stack.data; + num Code next = context->data[D_Stack]->Stack.next; + goto pushSingleLinkedStack(context, stack, data, next); +} + +__code pushSingleLinkedStack(struct SingleLinkedStack* stack, union Data* data, __code next(...)) { + Element* element = new Element(); + element->next = stack->top; + element->data = data; + stack->top = element; + goto next(...); +} +\end{lstlisting} + +ソースコード\ref{interface}は Stack の Interface である。 +typedef struct Stack で Interface を定義する。 +Impl には実装の型が入る。 +ソースコード\ref{interface}、2〜4行目のunion Data で定義されてるものは、 +Interface の API で用いる全ての Data Gear である。 +Interface の全ての API で用いる全ての Data Gear は Interface で定義される。 +ソースコード\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 を通す必要があるが、 +Interface を記述することでデータ構造の API と Data Gear を結びつけることが出来る。 +これによりノーマルレベルとメタレベルの分離が可能となった。 + +ソースコード\ref{implement}は Stack の実装の例である。 +createImpl は実装の初期化を行う関数である。 +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 しているが、 +stack\verb|->|pop には Code Gear の番号が入っているため実装した Code Gear へと継続する。 +このため、ソースコード \ref{Gears_code} では 6行目の popSingleLinkedStack へと継続している。 + +\lstinputlisting[label=implement, caption=SingleLinkedStackの実装]{./src/stackimpl.cbc} + +\begin{lstlisting}[frame=lrbt,label=SingleLinkedStack,caption={SingleLinkedStack のデータ構造}] + struct SingleLinkedStack { + struct Element* top; + } SingleLinkedStack; + + struct Element { + union Data* data; + struct Element* next; + } Element; +\end{lstlisting} + + +\section{xv6 の CbC への書き換え} +xv6 は 2006 年に MIT のオペレーティングシステムコースで教育用の目的として開発されたオペレーティングシステムである。 +xv6 はプロセス、仮想メモリ、カーネルとユーザの分離、割り込み、 +ファイルシステムなどの基本的な Unix の構造を持つにも関わらず、 +シンプルで学習しやすい。 + +CbC は 継続を中心とした言語であるため状態遷移モデルに落とし込むことができる。 +xv6 を CbC で書き換えることにより、OS の機能の保証が可能となる。 + +また、ハードウェア上でのメタレベルの計算や並列実行を行いたい。 +このため、xv6 を ARM\cite{arm} プロセッサを搭載したシングルボードコンピュータである Raspberry pi 用に移植した xv6-rpi を用いて実装する。 + +xv6 全体を CbC で書き換えるためには Interface を用いてモジュール化する必要がある。 +xv6 をモジュール化し、CbC で書き換えることができれば、Gears OS の機能を置き換えることもできる。 +図 \ref{fig:xv6Interface} は xv6 の構成図となる。 + +\begin{figure}[htp] + \begin{center} + \includegraphics[width=80mm]{fig/xv6.pdf} + \end{center} + \caption{モジュール化した xv6 の構成} + \label{fig:xv6Interface} +\end{figure} + +xv6 はカーネルと呼ばれる形式をとっている。 +カーネルは OS にとって中核となるプログラムである。 +xv6 ではカーネルとユーザープログラムは分離されており、カーネルはプログラムにプロセス管理、メモリ管理、I/O やファイルの管理などのサービスを提供する。 +ユーザープログラムがカーネルのサービスを呼び出す場合、システムコールを用いてユーザー空間からカーネル空間へ入りサービスを実行する。 +カーネルは CPU のハードウェア保護機構を使用して、ユーザー空間で実行されているプロセスが自身のメモリのみアクセスできるように保護している。 +ユーザープログラムがシステムコールを呼び出すと、ハードウェアが特権レベルを上げ、カーネルのプログラムが実行される。 +この特権レベルを持つプロセッサの状態をカーネルモード、特権のない状態をユーザーモードという。 + +ユーザープログラムがカーネルの提供するサービスを呼び出す際にはシステムコールを用いる。 +ユーザープログラムがシステムコールを呼び出すと、トラップが発生する。 +トラップが発生すると、ユーザープログラムは中断され、カーネルに切り替わり処理を行う。 +ソースコード \ref{syscall_list} は xv6 のシステムコールのリストである。 + +\begin{lstlisting}[frame=lrbt,label=syscall_list,caption={\footnotesize xv6 のシステムコールのリスト}] +static int (*syscalls[])(void) = { + [SYS_fork] =sys_fork, + [SYS_exit] =sys_exit, + [SYS_wait] =sys_wait, + [SYS_pipe] =sys_pipe, + [SYS_read] =sys_read, + [SYS_kill] =sys_kill, + [SYS_exec] =sys_exec, + [SYS_fstat] =sys_fstat, + [SYS_chdir] =sys_chdir, + [SYS_dup] =sys_dup, + [SYS_getpid] =sys_getpid, + [SYS_sbrk] =sys_sbrk, + [SYS_sleep] =sys_sleep, + [SYS_uptime] =sys_uptime, + [SYS_open] =sys_open, + [SYS_write] =sys_write, + [SYS_mknod] =sys_mknod, + [SYS_unlink] =sys_unlink, + [SYS_link] =sys_link, + [SYS_mkdir] =sys_mkdir, + [SYS_close] =sys_close, +}; +\end{lstlisting} + +プロセスとは、カーネルが実行するプログラムの単位である。 +xv6 のプロセスは、ユーザー空間メモリとカーネル用のプロセスの状態を持つ空間で構成されている。 +プロセスは独立しており、他のプロセスからメモリを破壊されたりすることはない。 +また、独立していることでカーネルそのものを破壊することもない。 +各プロセスの状態は struct proc によって管理されている。 +プロセスは fork システムコールによって新たに生成される。 +fork は新しく、親プロセスと呼ばれる呼び出し側と同じメモリ内容の、子プロセスと呼ばれるプロセスを生成する。 +fork システムコールは、親プロセスであれば子プロセスのID、子プロセスであれば 0 を返す。 +親プロセスと子プロセスは最初は同じ内容を持っているが、それぞれ異なるメモリ、レジスタで実行されているため、片方のメモリ内容を変更してももう片方に影響はない。 +exit システムコールはプロセスの停止を行い、メモリを解放する。 +wait システムコールは終了した子プロセスのIDを返す。子プロセスが終了するまで待つ。 +exec システムコールは呼び出し元のプロセスのメモリをファイルシステムのファイルのメモリイメージと置き換え実行する。 +ファイルには命令、データなどの配置が指定されたフォーマット通りになっていなければならない。 +xv6 は ELF と呼ばれるフォーマットを扱う。 + +ファイルディスクリプタは、カーネルが管理するプロセスが読み書きを行うオブジェクトを表す整数値である。 +プロセスは、ファイル、ディレクトリ、デバイスを開く、または既存のディスクリプタを複製することによって、 +ファイルディスクリプタを取得する。 +xv6 はプロセス毎にファイルディスクリプタのテーブルを持っている。 +ファイルディスクリプタは普通、0 が標準入力、1 が標準出力、2 がエラー出力として使われる。 +ファイルディスクリプタのテーブルのエントリを変更することで入出力先を変更することができる。 +1 の標準出力を close し、ファイルを open することでプログラムはファイルに出力することになる。 +ファイルディスクリプタはファイルがどのように接続するか隠すことでファイルへの入出力を容易にしている。 + +xv6 のファイルシステムはバイト配列であるデータファイルとデータファイルおよび他のディレクトリの参照を含むディレクトリを提供する。 +ディレクトリは root と呼ばれる特別なディレクトリから始まるツリーを形成している。 +絶対パスである "/dir1/dir2/file1" というパスは root ディレクトリ内の dir1 という名前のディレクトリ内の dir2 という名前のディレクトリ内の file というデータファイルを指す。 +相対パスである "dir2/file2" のようなパスは、現在のディレクトリ内の dir2 という名前のディレクトリ内の file というデータファイルを指す。 + +\section{xv6-rpi の CbC 対応} + +オリジナルの xv6 は x86 アーキテクチャで実装されたものだが、xv6-rpi は Raspberry Pi 用に実装されたものである。 + +Raspberry Pi は ARM\cite{arm} プロセッサを搭載したシングルボードコンピュータである。 +教育用のコンピューターとして開発されたもので、低価格であり、小型であるため使い勝手が良い。 +ストレージにハードディスクや SSD を使用するのではなく、SD カードを用いる。 +HDMI 出力や USB ポートも備えており、開発に最適である。 + +Raspberry Pi には Raspberry Pi 3、Raspberry Pi 2、Raspberry Pi 1、Raspberry Pi Zero といったバージョンが存在する。 + +xv6-rpi を CbC で書き換えるために、 +GCC 上で実装した CbC コンパイラを ARM 向けに build し xv6-rpi をコンパイルした。 +これにより、 xv6-rpi を CbC で書き換えることができるようになった。 + +\section{CbC によるシステムコールの書き換え} +CbC によるシステムコールの書き換えは、従来の xv6 のシステムコールの形から、 +大きく崩すことなく可能である。 +CbC は Code Gear 間の遷移は goto による継続で行われるため、 +状態遷移ベースでのプログラムに適している。 +xv6 を CbC で書き換えることにより、OS のプログラムを状態遷移モデルに落とし込むことができる。 +これにより状態遷移系のモデル検査が可能となる。 +図 \ref{fig:state} は CbC 書き換えによる read システムコールの遷移図である。 + +\begin{figure}[ht] + \begin{center} + \includegraphics[width=80mm]{fig/state.pdf} + \end{center} + \caption{read システムコールの遷移図} + \label{fig:state} +\end{figure} + +ソースコード \ref{syscall} は syscall() におけるシステムコールの呼び出しを行うコードである。 +システムコールはソースコード \ref{syscall_list} の関数のリストの番号から呼び出される。 +CbC でも同様に num で指定された番号の cbccodes のリストの Code Gear へ goto する。 +ソースコード \ref{syscall} 6行目でトラップフレームからシステムコールの番号を取得する。 +通常のシステムコールであればソースコード \ref{syscall} 13行目からの分岐へ入るが、 +cbc システムコールであれば ソースコード \ref{syscall} 8行目へ入り、goto によって遷移する。 +引数に持つ cbc\_ret は 継続した先でトラップに戻ってくるための Code Gear である。 + + +\begin{lstlisting}[frame=lrbt,label=syscall,caption={\footnotesize syscall()}] +void syscall(void) +{ + int num; + int ret; + + num = proc->tf->r0; + + if((num >= NELEM(syscalls)) && (num <= NELEM(cbccodes)) && cbccodes[num]) { + proc->cbc_arg.cbc_console_arg.num = num; + goto (cbccodes[num])(cbc_ret); + } + + if((num > 0) && (num <= NELEM(syscalls)) && syscalls[num]) { + ret = syscalls[num](); + + // in ARM, parameters to main (argc, argv) are passed in r0 and r1 + // do not set the return value if it is SYS_exec (the user program + // anyway does not expect us to return anything). + if (num != SYS_exec) { + proc->tf->r0 = ret; + } + } else { + cprintf("%d %s: unknown sys call %d\n", proc->pid, proc->name, num); + proc->tf->r0 = -1; + } +} +\end{lstlisting} + +ソースコード \ref{cbc_read} は、 +read システムコールであるソースコード \ref{sys_read} を CbC で書き換えたコードである。 +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)){ + struct file *f; + int n; + char *p; + + if(argfd(0, 0, &f) < 0 || argint(2, &n) < 0 || argptr(1, &p, n) < 0) { + goto next(-1); + } + goto cbc_fileread(f, p, n, next); +} +\end{lstlisting} + +\begin{lstlisting}[frame=lrbt,label=sys_read,caption={\footnotesize read システムコール}] +int sys_read(void) +{ + struct file *f; + int n; + char *p; + + if(argfd(0, 0, &f) < 0 || argint(2, &n) < 0 || argptr(1, &p, n) < 0) { + return -1; + } + + return fileread(f, p, n); +} +\end{lstlisting} +ソースコード \ref{cbcfileread} は、ソースコード \ref{fileread} を CbC で書き換えたコードである。 +継続で Code Gear 間を遷移するため関数呼び出しとは違い元の関数には戻ってこない。 +このため、書き換えの際には ソースコード \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} を書き換えたコードである。 +CbC では cbc\_devsw を定義しておりソースコード \ref{cbcreadi} 11行目で次の Code Gear へと継続する。 +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 へ継続する際、戻るべき継続先を一緒に送ることで、 +sleep から consoleread に戻ってくることができる。 + +\lstinputlisting[label=cbc_consoleread, caption=consoleread の CbC 書き換えの例]{./src/console.cbc} +\lstinputlisting[label=consoleread, caption=書き換え前の consoleread]{./src/console.c} + +CbC による書き換えにより、状態遷移ベースへと書き換えることができた。 +現在はシステムコールの書き換えのみであるが、カーネル全体を書き換えることで、 +カーネルを状態遷移モデルに落とし込むことができる。 \section{結論} -\subsection{現状} +本論文では 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 は関数より細かく分割されてるためメタ計算を柔軟に記述できる。 +Gears OS は Code Gear と Input/Output Data Gear の組を Task とし、並列実行を行う。 -\subsection{今後} -\subsection{} +Code Gear と Data Gear は Interface と呼ばれるまとまりとして記述される。 +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 を直接扱うことはセキュリティ上好ましくない。 +このため Context から必要なデータを取り出して Code Gear に接続する Meta Code Gear である stub Code Gear を定義した。 +stub Code Gear は Code Gear 毎に記述され、Code Gear 間の遷移の前に挿入される。 -\begin{thebibliography}{9} -\bibitem{latex} 宮城光希: \textbf{継続を基本とした言語によるOSのモジュール化}. 琉球大学理工学研究科修士論文、2019 +これらのメタ計算の記述は煩雑であるため Perl スクリプトによる自動生成を行なった。 +これにより Gears OS のコードの煩雑さは改善され、ユーザーレベルではメタを意識する必要がなくなった。 + +ハードウェア上での Gears OS の実装を実現させるために Raspberry Pi 上での実装を考察した。 +比較的シンプルな OS である xv6 を CbC に書き換えることにした。 + +xv6 を CbC で書き換えることによって、実行可能な CbC プログラムで記述された OS がそのまま、 +状態遷移モデルによるモデル検査、Agda による定理証明が可能となる。 -\end{thebibliography} +今後の課題は、 +現在は xv6 のシステムコールの一部のみの書き換えと、設計のみしか行っていないので、カーネル全ての書き換えと、 +Gears OS の TaskManager の置き換えを行い、Gears OS の機能を xv6 に組み込む必要がある。 +また、xv6-rpi は QEMU のみの動作でしか確認してないため、実機上での動作が可能なように実装する必要がある。 + +\bibliographystyle{ipsjunsrt} +\bibliography{reference} +% \begin{thebibliography}{9} +% \bibitem{latex} 宮城光希: \textbf{継続を基本とした言語によるOSのモジュール化}. 琉球大学理工学研究科修士論文、2019 +% \end{thebibliography} + \end{document}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/Stack.cbc Wed May 08 18:23:07 2019 +0900 @@ -0,0 +1,14 @@ +typedef struct Stack<Impl>{ + union Data* stack; + union Data* data; + union Data* data1; + __code whenEmpty(...); + __code clear(Impl* stack,__code next(...)); + __code push(Impl* stack,union Data* data, __code next(...)); + __code pop(Impl* stack, __code next(union Data*, ...)); + __code pop2(Impl* stack, __code next(union Data*, union Data*, ...)); + __code isEmpty(Impl* stack, __code next(...), __code whenEmpty(...)); + __code get(Impl* stack, __code next(union Data*, ...)); + __code get2(Impl* stack, __code next(union Data*, union Data*, ...)); + __code next(...); +} Stack;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/console.c Wed May 08 18:23:07 2019 +0900 @@ -0,0 +1,47 @@ +int consoleread (struct inode *ip, char *dst, int n) +{ + uint target; + int c; + + iunlock(ip); + + target = n; + acquire(&input.lock); + + while (n > 0) { + while (input.r == input.w) { + if (proc->killed) { + release(&input.lock); + ilock(ip); + return -1; + } + + sleep(&input.r, &input.lock); + } + + c = input.buf[input.r++ % INPUT_BUF]; + + if (c == C('D')) { // EOF + if (n < target) { + // Save ^D for next time, to make sure + // caller gets a 0-byte result. + input.r--; + } + + break; + } + + *dst++ = c; + --n; + + if (c == '\n') { + break; + } + } + + release(&input.lock); + ilock(ip); + + return target - n; +} +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/console.cbc Wed May 08 18:23:07 2019 +0900 @@ -0,0 +1,79 @@ +__code cbc_consoleread2 () +{ + struct inode *ip = proc->cbc_arg.cbc_console_arg.ip; + __code(*next)(int ret) = proc->cbc_arg.cbc_console_arg.next; + if (input.r == input.w) { + if (proc->killed) { + release(&input.lock); + ilock(ip); + goto next(-1); + } + goto cbc_sleep(&input.r, &input.lock, cbc_consoleread2); + } + goto cbc_consoleread1(); +} + +__code cbc_consoleread1 () +{ + int cont = 1; + int n = proc->cbc_arg.cbc_console_arg.n; + int target = proc->cbc_arg.cbc_console_arg.target; + char* dst = proc->cbc_arg.cbc_console_arg.dst; + struct inode *ip = proc->cbc_arg.cbc_console_arg.ip; + __code(*next)(int ret) = proc->cbc_arg.cbc_console_arg.next; + + int c = input.buf[input.r++ % INPUT_BUF]; + + if (c == C('D')) { // EOF + if (n < target) { + // Save ^D for next time, to make sure + // caller gets a 0-byte result. + input.r--; + } + cont = 0; + } + + *dst++ = c; + --n; + + if (c == '\n') { + cont = 0; + } + + if (cont == 1) { + if (n > 0) { + proc->cbc_arg.cbc_console_arg.n = n; + proc->cbc_arg.cbc_console_arg.target = target; + proc->cbc_arg.cbc_console_arg.dst = dst; + proc->cbc_arg.cbc_console_arg.ip = ip; + proc->cbc_arg.cbc_console_arg.next = next; + goto cbc_sleep(&input.r, &input.lock, cbc_consoleread2); + } + } + + release(&input.lock); + ilock(ip); + + goto next(target - n); +} + +__code cbc_consoleread (struct inode *ip, char *dst, int n, __code(*next)(int ret)) +{ + uint target; + + iunlock(ip); + + target = n; + acquire(&input.lock); + + if (n > 0) { + proc->cbc_arg.cbc_console_arg.n = n; + proc->cbc_arg.cbc_console_arg.target = target; + proc->cbc_arg.cbc_console_arg.dst = dst; + proc->cbc_arg.cbc_console_arg.ip = ip; + proc->cbc_arg.cbc_console_arg.next = next; + goto cbc_consoleread2(); + } + goto cbc_consoleread1(); +} +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/consoleinit.c Wed May 08 18:23:07 2019 +0900 @@ -0,0 +1,13 @@ +void consoleinit (void) +{ + initlock(&cons.lock, "console"); + initlock(&input.lock, "input"); + + devsw[CONSOLE].write = consolewrite; + devsw[CONSOLE].read = consoleread; + cbc_devsw[CONSOLE].write = cbc_consolewrite; + cbc_devsw[CONSOLE].read = cbc_consoleread; + + cons.locking = 1; +} +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/fileread.c Wed May 08 18:23:07 2019 +0900 @@ -0,0 +1,26 @@ +int fileread (struct file *f, char *addr, int n) +{ + int r; + + if (f->readable == 0) { + return -1; + } + + if (f->type == FD_PIPE) { + return piperead(f->pipe, addr, n); + } + + if (f->type == FD_INODE) { + ilock(f->ip); + + if ((r = readi(f->ip, addr, f->off, n)) > 0) { + f->off += r; + } + + iunlock(f->ip); + + return r; + } + + panic("fileread"); +}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/fileread.cbc Wed May 08 18:23:07 2019 +0900 @@ -0,0 +1,30 @@ +__code cbc_fileread1 (int r) +{ + struct file *f = proc->cbc_arg.cbc_console_arg.f; + __code (*next)(int ret) = cbc_ret; + if (r > 0) + f->off += r; + iunlock(f->ip); + goto next(r); +} + +__code cbc_fileread (struct file *f, char *addr, int n, __code (*next)(int ret)) +{ + if (f->readable == 0) { + goto next(-1); + } + + if (f->type == FD_PIPE) { + goto cbc_piperead(f->pipe, addr, n, next); + goto next(-1); + } + + if (f->type == FD_INODE) { + ilock(f->ip); + proc->cbc_arg.cbc_console_arg.f = f; + goto cbc_readi(f->ip, addr, f->off, n, cbc_fileread1); + } + + goto cbc_panic("fileread"); +} +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/readi.c Wed May 08 18:23:07 2019 +0900 @@ -0,0 +1,30 @@ +int readi (struct inode *ip, char *dst, uint off, uint n) +{ + uint tot, m; + struct buf *bp; + + if (ip->type == T_DEV) { + if (ip->major < 0 || ip->major >= NDEV || !devsw[ip->major].read) { + return -1; + } + + return devsw[ip->major].read(ip, dst, n); + } + + if (off > ip->size || off + n < off) { + return -1; + } + + if (off + n > ip->size) { + n = ip->size - off; + } + + for (tot = 0; tot < n; tot += m, off += m, dst += m) { + bp = bread(ip->dev, bmap(ip, off / BSIZE)); + m = min(n - tot, BSIZE - off%BSIZE); + memmove(dst, bp->data + off % BSIZE, m); + brelse(bp); + } + + return n; +}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/readi.cbc Wed May 08 18:23:07 2019 +0900 @@ -0,0 +1,30 @@ +__code cbc_readi (struct inode *ip, char *dst, uint off, uint n, __code (*next)(int ret)) +{ + uint tot, m; + struct buf *bp; + + if (ip->type == T_DEV) { + if (ip->major < 0 || ip->major >= NDEV || !cbc_devsw[ip->major].read) { + goto next(-1); + } + + goto cbc_devsw[ip->major].read(ip, dst, n, next); + } + + if (off > ip->size || off + n < off) { + goto next(-1); + } + + if (off + n > ip->size) { + n = ip->size - off; + } + + for (tot = 0; tot < n; tot += m, off += m, dst += m) { + bp = bread(ip->dev, bmap(ip, off / BSIZE)); + m = min(n - tot, BSIZE - off%BSIZE); + memmove(dst, bp->data + off % BSIZE, m); + brelse(bp); + } + + goto next(n); +}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/stackimpl.cbc Wed May 08 18:23:07 2019 +0900 @@ -0,0 +1,27 @@ +Stack* createSingleLinkedStack(struct Context* context) { + struct Stack* stack = new Stack(); + struct SingleLinkedStack* singleLinkedStack = new SingleLinkedStack(); + stack->stack = (union Data*)singleLinkedStack; + singleLinkedStack->top = NULL; + stack->push = C_pushSingleLinkedStack; + stack->pop = C_popSingleLinkedStack; + stack->pop2 = C_pop2SingleLinkedStack; + stack->get = C_getSingleLinkedStack; + stack->get2 = C_get2SingleLinkedStack; + stack->isEmpty = C_isEmptySingleLinkedStack; + stack->clear = C_clearSingleLinkedStack; + return stack; +} + +__code clearSingleLinkedStack(struct SingleLinkedStack* stack,__code next(...)) { + stack->top = NULL; + goto next(...); +} + +__code pushSingleLinkedStack(struct SingleLinkedStack* stack,union Data* data, __code next(...)) { + Element* element = new Element(); + element->next = stack->top; + element->data = data; + stack->top = element; + goto next(...); +}