# HG changeset patch # User mir3636 # Date 1549604386 -32400 # Node ID 6b48a2c84700c6b28216e8012695b2c0d04052c0 # Parent 87515b5f186728e442f54b8050d1ec00e114b874 update diff -r 87515b5f1867 -r 6b48a2c84700 paper/fig/xv6.graffle Binary file paper/fig/xv6.graffle has changed diff -r 87515b5f1867 -r 6b48a2c84700 paper/fig/xv6.pdf Binary file paper/fig/xv6.pdf has changed diff -r 87515b5f1867 -r 6b48a2c84700 paper/fig/xv6.xbb --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/fig/xv6.xbb Fri Feb 08 14:39:46 2019 +0900 @@ -0,0 +1,8 @@ +%%Title: fig/xv6.pdf +%%Creator: extractbb 20160307 +%%BoundingBox: 0 0 745 701 +%%HiResBoundingBox: 0.000000 0.000000 745.000000 701.000000 +%%PDFVersion: 1.4 +%%Pages: 1 +%%CreationDate: Fri Feb 8 14:33:25 2019 + diff -r 87515b5f1867 -r 6b48a2c84700 paper/master_paper.pdf Binary file paper/master_paper.pdf has changed diff -r 87515b5f1867 -r 6b48a2c84700 paper/src/console.c --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/console.c Fri Feb 08 14:39:46 2019 +0900 @@ -0,0 +1,147 @@ +__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; + 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(); + } +} + +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; +} + +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; +} + diff -r 87515b5f1867 -r 6b48a2c84700 paper/xv6.tex --- a/paper/xv6.tex Fri Feb 08 05:05:15 2019 +0900 +++ b/paper/xv6.tex Fri Feb 08 14:39:46 2019 +0900 @@ -9,6 +9,12 @@ シンプルで学習しやすい。 \section{Raspberry Pi} +Raspberry Pi\cite{rpi} は ARM\cite{arm} プロセッサを搭載したシングルボードコンピュータである。 +教育用のコンピューターとして開発されたもので、低価格であり、小型であるため使い勝手が良い。 +ストレージにハードディスクや SSD を使用するのではなく、SD カードを用いる。 +HDMI 出力や USB ポートも備えており、開発に最適である。 + +Raspberry Pi には Raspberry Pi 3、Raspberry Pi 2、Raspberry Pi 1、Raspberry Pi Zero といったバージョンが存在する。 \section{xv6 の構成要素} xv6 はカーネルと呼ばれる形式をとっている。 @@ -211,12 +217,101 @@ } \end{lstlisting} +\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); +} + +//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} + + xv6 のシステムコールの関数を CbC で書き換え、QEMU 上で動作させることができた。 \section{xv6 のモジュール化} xv6 全体を CbC で書き換えるためには Interface を用いてモジュール化する必要がある。 xv6 をモジュール化し、CbC で書き換えることができれば、Gears OS の機能を置き換えることもできる。 -図 \ref{fig:xv6Interface} では Interface を用いた xv6 の構成図となる。 +図 \ref{fig:xv6Interface} は xv6 の構成図となる。 + +\begin{figure}[ht] + \begin{center} + \includegraphics[width=150mm]{fig/xv6.pdf} + \end{center} + \caption{モジュール化した xv6 の構成} + \label{fig:xv6Interface} +\end{figure} + +\section{xv6 の CbC 書き換えによる評価} +CbC は Code Gear 間の遷移は goto による継続で行われるため、 +状態遷移ベースでのプログラムに適している。 +xv6 を CbC で書き換えることにより、OS のプログラムを状態遷移モデルに落とし込むことができる。 +これにより状態遷移系のモデル検査が可能となる。 +また、CbC は Agda に変換できるように設計されているため CbC で記述された実行可能なプログラムが、 +そのまま Agda による定理証明ができる。 + +これらのため、CbC で記述された実行可能な OS そのものがモデル検査と定理証明が可能となり、 +OS の信頼性が保証できる。 +