--- 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}
 %英語論文

Binary file paper/fig/xv6_2.graffle has changed

Binary file paper/master_paper.pdf has changed

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

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

--- 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 上で動作させることができた。