Binary file paper/fig/xv6.graffle has changed

Binary file paper/fig/xv6.pdf has changed

--- /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
+

Binary file paper/master_paper.pdf has changed

--- /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;
+}
+

--- 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 の信頼性が保証できる。
+