# HG changeset patch # User mir3636 # Date 1549841335 -32400 # Node ID 675cd2c69450d756e1a8c43b42b0b7a0f551e7f2 # Parent 3003930e44359b846681851cd014c48d029cf6ef add diff -r 3003930e4435 -r 675cd2c69450 paper/abstract.tex --- a/paper/abstract.tex Sun Feb 10 12:38:09 2019 +0900 +++ b/paper/abstract.tex Mon Feb 11 08:28:55 2019 +0900 @@ -10,16 +10,20 @@ メタ計算を通常の計算から切り離して記述するために、Code Gear、Data Gear という単位を提案している。 CbC はこの Code Gear と Data Gear の単位でプログラムを記述する。 -システムやアプリケーションを記述するためにCode Gear と Data Gear を柔軟に再利用する必要がある。 +OS は時代とともに複雑さが増し、OS の信頼性を保証することは難しい。 +そこで、基本的な OS の機能を揃えたシンプルな OS である xv6 を CbC で書き換え、OS の機能を保証する。 + +Code Gear は goto による継続で処理を表すことができる。 +これにより、状態遷移による OS の記述が可能となり、複雑な OS のモデル検査を可能とする。 +また、CbC は 定理証明支援系 Agda に置き換えることができるように構築されている。 +これらを用いて OS の信頼性を保証したい。 + +CbC でシステムやアプリケーションを記述するためには、Code Gear と Data Gear を柔軟に再利用する必要がある。 このときに機能を接続するAPIと実装の分離が可能であることが望ましい。 Gears OS の信頼性を保証するために、形式化されたモジュールシステムを提供する必要がある。 本論文では、Interface を用いたモジュールシステムの説明と、 -ハードウェア上でメタレベルの処理、および並列実行を可能とするために、 -Raspberry Pi 上での Gears OS の実装についての考察も行う。 - -ハードウェア上でのメタレベルの計算や並列実行を行うために、基本的な OS の機能を揃えたうえ、 -シンプルである xv6 を Gears OS に置き換えることによって実現させる。 +xv6 の CbC 書き換えについての考察を行う。 \chapter*{Abstract} %英語論文 diff -r 3003930e4435 -r 675cd2c69450 paper/fig/xv6_2.graffle Binary file paper/fig/xv6_2.graffle has changed diff -r 3003930e4435 -r 675cd2c69450 paper/master_paper.pdf Binary file paper/master_paper.pdf has changed diff -r 3003930e4435 -r 675cd2c69450 paper/src/fileread.c --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/fileread.c Mon Feb 11 08:28:55 2019 +0900 @@ -0,0 +1,58 @@ +__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"); +} + +// Read from file f. +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"); +} + diff -r 3003930e4435 -r 675cd2c69450 paper/src/readi.c --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/readi.c Mon Feb 11 08:28:55 2019 +0900 @@ -0,0 +1,63 @@ +__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); +} + +//PAGEBREAK! +// Read data from inode. +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; +} diff -r 3003930e4435 -r 675cd2c69450 paper/xv6.tex --- a/paper/xv6.tex Sun Feb 10 12:38:09 2019 +0900 +++ b/paper/xv6.tex Mon Feb 11 08:28:55 2019 +0900 @@ -2,7 +2,7 @@ Gears OS をハードウェア上で実装するために、ARM\cite{arm} プロセッサを搭載したシングルボードコンピュータである Raspberry Pi 上で Gears OS 実装したい。 ハードウェア上でのメタレベルの計算や並列実行を行うために、Linax 等に比べてシンプルである xv6 の機能の一部を Gears OS に置き換えることで実現させる。 xv6 は UNIX V6 を x86 へ再実装したものであるが、 -ここでは xv6 を Raspberry pi 用に移植した xv6-rpi を用いて実装する。 +ここでは xv6\cite{xv6} を Raspberry pi 用に移植した xv6-rpi を用いて実装する。 Xv6 は 2006 年に MIT のオペレーティングシステムコースで教育用の目的として開発されたオペレーティングシステムである。 Xv6 はプロセス、仮想メモリ、カーネルとユーザの分離、割り込み、ファイルシステムなどの基本的な Unix の構造を持つにも関わらず、 @@ -157,133 +157,12 @@ プロセスの状態を持つ struct proc は大域変数であるため Code Gear を用いるために必要なパラメーターを cbc\_arg として持たせることにした。 継続を行う際には必要なパラメーターをここに格納する。 -\begin{lstlisting}[frame=lrbt,label=fileread,caption={\footnotesize fileread の CbC 書き換えの例}] -__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"); -} - -// Read from file f. -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"); -} -\end{lstlisting} +\lstinputlisting[label=fileread, caption=fileread の CbC 書き換えの例]{./src/fileread.c} -\begin{lstlisting}[frame=lrbt,label=fileread,caption={\footnotesize readi の CbC 書き換えの例}] -__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); -} +ソースコード \ref{readi} では、cbc\_devsw を -//PAGEBREAK! -// Read data from inode. -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; -} -\end{lstlisting} - -\lstinputlisting[label=TaskManager, caption=consoleread の CbC 書き換えの例]{./src/console.c} +\lstinputlisting[label=readi, caption=readi の CbC 書き換えの例]{./src/readi.c} +\lstinputlisting[label=consoleread, caption=consoleread の CbC 書き換えの例]{./src/console.c} xv6 のシステムコールの関数を CbC で書き換え、QEMU 上で動作させることができた。