# HG changeset patch
# User mir3636
# Date 1549879496 -32400
# Node ID d3ed28a7964fa9f350aef392b4a80c5ef90fd723
# Parent  de8210a1f8e471cb27949919df3151bd28a8f5fd
update

diff -r de8210a1f8e4 -r d3ed28a7964f paper/introduction.tex
--- a/paper/introduction.tex	Mon Feb 11 17:10:33 2019 +0900
+++ b/paper/introduction.tex	Mon Feb 11 19:04:56 2019 +0900
@@ -55,17 +55,15 @@
 これらを用いて、検証された Gears OS\cite{gears} を構築したい。
 図\ref{fig:MetaGear}。
 
-本論文では、Gears OS の要素である Code Gear、Data Gear、そして、Meta Code Gear 、Meta Data Gear の構成を示す。これらは、CbC に変換されて実行される。
-Gears OS は、Task Scheduler を CPU や GPU 毎に持ち、一つの Task に対応する Context という Meta Data Gear を使用しながら計算を実行する。
-
 Meta Gear を入れかえることにより、ノーマルレベルの Gear をモデル検査することができるようにしたい。
 ノーマルレベルでの Code Gear と Data Gear は継続を基本とした関数型プログラミング的な記述に対応する。
 この記述を定理証明支援系である Agda を用いて直接に証明できるようにしたい。
 Gears OS の記述はそのまま Agda に落ちる。
 Code Gear、Data Gear を用いた言語である CbC で記述することによって検証された OS を実装することができる。
 
-従来の研究でメタ計算を用いる場合は、関数型言語では Monad を用いる\cite{moggi-monad}。これは Hakell では実行時の環境を記述する構文として使われている。
-OS の研究では、メタ計算の記述に型つきアセンブラ(Typed Assembler)を用いることがある\cite{Yang:2010:SLI:1806596.1806610}。Python や Haskell による記述をノーマルレベルとして
+従来の研究でメタ計算を用いる場合は、関数型言語では 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}。
 
@@ -74,12 +72,9 @@
 CbC はスタック上に隠された環境を持たないので、メタレベルで使用する資源を明確にできるという利点がある。
 ただし、Gear のプログラミングスタイルは、従来の関数呼出を中心としたものとはかなり異なる。
 
-
-また、本研究では Gears の記述をモジュール化するために Interface を導入した。
-さらに並列処理の記述用にpar goto 構文を導入する。
+Gears の記述をモジュール化するために Interface を導入した。
 これらの機能は Agda \cite{agda} 上で継続を用いた関数型プログラムに対応するようになっている。\cite{agda-ryokka}
-これにより Code Gear、Data Gear の Agda による証明が可能となり、
-モデル検査を入れられるように Gears OS の構築を行った。 
+これにより Code Gear、Data Gear の Agda による証明が可能となるように Gears OS の構築を行った。 
 
 \begin{figure}[ht]
  \begin{center}
@@ -89,9 +84,9 @@
  \label{fig:MetaGear}
 \end{figure}
 
-本研究では Gears OS のモジュール化の仕組みである Interface を用いた Gears OS の構築を行った。
+本論文では、Gears OS の要素である Code Gear、Data Gear、そして、Meta Code Gear 、Meta Data Gear の構成を示す。
+また、OS の信頼性を保証するため、xv6 \cite{xv6} の CbC による書き換えについて考察する。
+xv6 は OS の基本的な機能を持っているにも関わらず、Linux などに比べてシンプルであり、
+CbC に書き換えることによって状態遷移ベースのプログラミングが可能となり、
+実行可能なプログラムがそのままモデル検査が可能で、Agda による証明が可能な OS となることを目的とする。
 
-また、ハードウェア上でメタレベルの処理、および並列実行を可能とするために、Raspberry Pi\cite{rpi} 上での Gears OS の実装についての考察を行う。
-ここでは、Linax 等に比べてシンプルである xv6 の機能の一部を Gears OS に置き換えることで実現させる。
-xv6 は UNIX V6 を x86 へ再実装したものであるが、ここでは Raspberry pi 用に移植した xv6-rpi\cite{xv6rpi} を用いて実装した。
-
diff -r de8210a1f8e4 -r d3ed28a7964f paper/master_paper.pdf
Binary file paper/master_paper.pdf has changed
diff -r de8210a1f8e4 -r d3ed28a7964f paper/src/fileread.c
--- a/paper/src/fileread.c	Mon Feb 11 17:10:33 2019 +0900
+++ b/paper/src/fileread.c	Mon Feb 11 19:04:56 2019 +0900
@@ -1,46 +1,15 @@
-__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);
-}
+int fileread (struct file *f, char *addr, int n)
+{
+    int 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);
 
@@ -55,4 +24,3 @@
 
     panic("fileread");
 }
-
diff -r de8210a1f8e4 -r d3ed28a7964f paper/src/readi.c
--- a/paper/src/readi.c	Mon Feb 11 17:10:33 2019 +0900
+++ b/paper/src/readi.c	Mon Feb 11 19:04:56 2019 +0900
@@ -1,36 +1,3 @@
-__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;
diff -r de8210a1f8e4 -r d3ed28a7964f paper/xv6.tex
--- a/paper/xv6.tex	Mon Feb 11 17:10:33 2019 +0900
+++ b/paper/xv6.tex	Mon Feb 11 19:04:56 2019 +0900
@@ -8,7 +8,7 @@
 xv6 を CbC で書き換えることにより、OS の機能の保証が可能となる。
 
 また、ハードウェア上でのメタレベルの計算や並列実行を行いたい。
-このため、xv6\cite{xv6} を ARM\cite{arm} プロセッサを搭載したシングルボードコンピュータである Raspberry pi 用に移植した xv6-rpi を用いて実装する。
+このため、xv6 を ARM\cite{arm} プロセッサを搭載したシングルボードコンピュータである Raspberry pi 用に移植した xv6-rpi を用いて実装する。
 
 \section{xv6 のモジュール化}
 
@@ -109,17 +109,27 @@
 
 \section{システムコールの書き換え}
 ソースコード \ref{syscall} は syscall() におけるシステムコールの呼び出しを行うコードである。
-システムコールはソースコード \ref{syscall_list} の関数のリストから呼び出される。
+システムコールはソースコード \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]();
 
@@ -129,13 +139,19 @@
         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{sys_read} は CbC で書き換えた read システムコールである。
-Code Gear であるため関数呼び出しではなく goto による継続となる。
+ソースコード \ref{cbc_read} は、
+read システムコールであるソースコード \ref{sys_read} を CbC で書き換えたコードである。
+CbC は C の関数を呼び出すことも出来るため、書き換えたい部分だけを書き換えることができる。
+Code Gear であるため、ソースコード \ref{cbc_read} 7、9行目のように関数呼び出しではなく goto による継続となる。
 
-\begin{lstlisting}[frame=lrbt,label=sys_read,caption={\footnotesize read システムコール}]
+\begin{lstlisting}[frame=lrbt,label=sys_read,caption={\footnotesize cbc\_read システムコール}]
 __code cbc_read(__code (*next)(int ret)){
     struct file *f;
     int n;
@@ -146,7 +162,9 @@
     }
     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;
@@ -162,14 +180,16 @@
 \end{lstlisting}
 
 継続で Code Gear 間を遷移するため関数呼び出しとは違い元の関数には戻ってこない。
-このため、書き換えの際には ソースコード \ref{fileread} のように分割する必要がある。
+このため、書き換えの際には ソースコード \ref{cbcfileread} のように分割する必要がある。
 プロセスの状態を持つ struct proc は大域変数であるため Code Gear を用いるために必要なパラメーターを cbc\_arg として持たせることにした。
 継続を行う際には必要なパラメーターをここに格納する。
 
-\lstinputlisting[label=fileread, caption=fileread の CbC 書き換えの例]{./src/fileread.c}
+\lstinputlisting[label=cbcfileread, caption=fileread の CbC 書き換えの例]{./src/fileread.cbc}
+\lstinputlisting[label=fileread, caption=書き換え前の fileread]{./src/fileread.c}
 
-CbC では cbc\_devsw を定義しておりソースコード \ref{readi} 11行目で次の Code Gear へと継続する。
+CbC では cbc\_devsw を定義しておりソースコード \ref{cbcreadi} 11行目で次の Code Gear へと継続する。
 
+\lstinputlisting[label=cbcreadi, caption=readi の CbC 書き換えの例]{./src/readi.cbc}
 \lstinputlisting[label=readi, caption=readi の CbC 書き換えの例]{./src/readi.c}
 
 ソースコード \ref{consoleread} 11、50、行目 では sleep へ継続する際、戻るべき継続先を一緒に送ることで、