Mercurial > hg > Papers > 2020 > anatofuz-sigos

--- a/paper/anatofuz-sigos.md	Fri May 01 13:07:45 2020 +0900
+++ b/paper/anatofuz-sigos.md	Sat May 02 11:41:36 2020 +0900
@@ -19,6 +19,7 @@
 実装用の言語と証明用の言語の両方に適した言語としてContinuation Based C(CbC)がある。
 CbCはCと互換性のあるCの下位言語であり、 状態遷移をベースとした記述に適したプログラミング言語である。
 Cとの互換性のために、 CbCのプログラムをコンパイルすることで動作可能なバイナリに変換が可能である。
+またCbCの基本文法は簡潔であるため、 Agdaなどの定理証明支援系との相互変換や、 CbC自体でのモデル検査が可能であると考えられる。
 すなわちCbCを用いて状態遷移を基本とした単位でプログラミングをすると、 形式手法で証明が可能かつ実際に動作するコードを記述できる。

 現在小さなunixであるxv6 kernelをCbCを用いて再実装している。
@@ -48,16 +49,33 @@
 現在CbCはGCC及びLLVM/clang上にそれぞれ実装されている。


-CbCの例題をCode \ref{src:cbc_example}に示す。
-
+CbCで階乗を求める例題をCode \ref{src:cbc_example}に示す。
+CbCでは関数の代わりにCodeGearという単位でプログラミングを行う。
+CodeGearはコード中では、型の代わりに`__code`で関数の様に宣言を行う。


-``` src:cbc_example, c
-__code code_gear1(struct str* st) {
-    if (st->number) {
-        goto hoge(...);
+``` src:cbc_example, Cbで階乗を求める処理
+__code factorial(struct F arg) {
+    if (arg.n<0) {
+        exit(1);
+    }
+    if (arg.n==0) {
+      goto arg.next(arg);
+    } else {
+      arg.r *= arg.n;
+      arg.n--;
+      goto factorial(arg);
     }
-    goto code_gear2(foo);
 }
+```

-```
+# xv6のファイルシステムの一部の分析
+
+xv6のファイルシステムに関する定義ファイルはfs.c中に記述されている。
+この中に出てくる関数に着目し、 この関数をさらにCodeGearに変換していくことで状態遷移単位での記述を試みた。
+
+まず関数内でif文などの分岐を持たない基本単位であるBasic Blockに着目した。
+CbCのCodeGearの粒度はCの関数とアセンブラの中間であるといえるので、 BasicBlockをCodeGearに置き換える事が可能である。
+したがって特定の関数内の処理のBasicBlockを分析し、 BasicBlockに対応したCodeGearに変換することで状態遷移系への変換を行った。
+
+
Binary file paper/anatofuz-sigos.pdf has changed
--- a/paper/anatofuz-sigos.tex	Fri May 01 13:07:45 2020 +0900
+++ b/paper/anatofuz-sigos.tex	Sat May 02 11:41:36 2020 +0900
@@ -95,6 +95,7 @@
 実装用の言語と証明用の言語の両方に適した言語としてContinuation Based C(CbC)がある。
 CbCはCと互換性のあるCの下位言語であり、 状態遷移をベースとした記述に適したプログラミング言語である。
 Cとの互換性のために、 CbCのプログラムをコンパイルすることで動作可能なバイナリに変換が可能である。
+またCbCの基本文法は簡潔であるため、 Agdaなどの定理証明支援系との相互変換や、 CbC自体でのモデル検査が可能であると考えられる。
 すなわちCbCを用いて状態遷移を基本とした単位でプログラミングをすると、 形式手法で証明が可能かつ実際に動作するコードを記述できる。

 現在小さなunixであるxv6 kernelをCbCを用いて再実装している。
@@ -124,19 +125,36 @@
 現在CbCはGCC及びLLVM/clang上にそれぞれ実装されている。


-CbCの例題をCode \ref{src:cbc_example}に示す。
-
+CbCで階乗を求める例題をCode \ref{src:cbc_example}に示す。
+CbCでは関数の代わりにCodeGearという単位でプログラミングを行う。
+CodeGearはコード中では、型の代わりに\texttt{\_\_code}で関数の様に宣言を行う。


-\begin{lstlisting}[frame=lrbt,label=src:cbc_example,caption={c}]
-__code code_gear1(struct str* st) {
-    if (st->number) {
-        goto hoge(...);
+\begin{lstlisting}[frame=lrbt,label=src:cbc_example,caption={Cbで階乗を求める処理}]
+__code factorial(struct F arg) {
+    if (arg.n<0) {
+        exit(1);
+    }
+    if (arg.n==0) {
+      goto arg.next(arg);
+    } else {
+      arg.r *= arg.n;
+      arg.n--;
+      goto factorial(arg);
     }
-    goto code_gear2(foo);
 }
+\end{lstlisting}

-\end{lstlisting}
+\section{xv6のファイルシステムの一部の分析}
+
+xv6のファイルシステムに関する定義ファイルはfs.c中に記述されている。
+この中に出てくる関数に着目し、 この関数をさらにCodeGearに変換していくことで状態遷移単位での記述を試みた。
+
+まず関数内でif文などの分岐を持たない基本単位であるBasic Blockに着目した。
+CbCのCodeGearの粒度はCの関数とアセンブラの中間であるといえるので、 BasicBlockをCodeGearに置き換える事が可能である。
+したがって特定の関数内の処理のBasicBlockを分析し、 BasicBlockに対応したCodeGearに変換することで状態遷移系への変換を行った。
+
+

 \nocite{*}
 \bibliographystyle{ipsjunsrt}
--- a/paper/md2tex.pl	Fri May 01 13:07:45 2020 +0900
+++ b/paper/md2tex.pl	Sat May 02 11:41:36 2020 +0900
@@ -25,6 +25,13 @@
     $line =~ s/# (.*)/\\section{$1}/;
   }

+  if ($line =~ /`([\w_\-\\]+)`/) {
+    my $codeBlock = $1;
+    $codeBlock =~ s/_/\\_/g;
+    print "$codeBlock\n";
+    $line =~ s/`([\w_\-\\]+)`/\\texttt{$codeBlock}/;
+  }
+
   if ($line =~ /```/) {
     $in_codeblock = !$in_codeblock;
     if (!$in_codeblock) {