# HG changeset patch
# User anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
# Date 1588404615 -32400
# Node ID ca6506bdcda42cad6a877d7da9ec0b146f075843
# Parent  13d8fe4cfc5c4dd2d1807541947dd2d020c6f6be
...

diff -r 13d8fe4cfc5c -r ca6506bdcda4 paper/anatofuz-sigos.md
--- a/paper/anatofuz-sigos.md	Sat May 02 15:22:52 2020 +0900
+++ b/paper/anatofuz-sigos.md	Sat May 02 16:30:15 2020 +0900
@@ -81,7 +81,12 @@
 これはGCCでは内部コードを生成、 LLVM/clangでは`setjmp`と`longjmp`を使うことでCodeGearの次の継続対象として呼び出し元の関数を設定することが可能となる。
 したがってプログラマから見ると、通常のCの関数呼び出しの返り値をCodeGearから取得する事が可能となる。
 
-# CbCを用いたxv6の再実装
+# CbCを用いたOSの実装
+
+軽量継続を持つCbCを利用して、 証明可能なOSを実装したい。
+その為には証明に使用される定理証明支援系や、 モデル検査機での表現に適した状態遷移単位での記述が求められる。
+CbCで使用するCodeGearは、 状態遷移モデルにおける状態そのものとして捉えることが可能である。
+これらの状態をまとめる構造体として、 CbCの`context`を導入した。
 
 
 
diff -r 13d8fe4cfc5c -r ca6506bdcda4 paper/anatofuz-sigos.pdf
Binary file paper/anatofuz-sigos.pdf has changed
diff -r 13d8fe4cfc5c -r ca6506bdcda4 paper/anatofuz-sigos.tex
--- a/paper/anatofuz-sigos.tex	Sat May 02 15:22:52 2020 +0900
+++ b/paper/anatofuz-sigos.tex	Sat May 02 16:30:15 2020 +0900
@@ -157,7 +157,12 @@
 これはGCCでは内部コードを生成、 LLVM/clangでは\texttt{setjmp}と\texttt{longjmp}を使うことでCodeGearの次の継続対象として呼び出し元の関数を設定することが可能となる。
 したがってプログラマから見ると、通常のCの関数呼び出しの返り値をCodeGearから取得する事が可能となる。
 
-\section{CbCを用いたxv6の再実装}
+\section{CbCを用いたOSの実装}
+
+軽量継続を持つCbCを利用して、 証明可能なOSを実装したい。
+その為には証明に使用される定理証明支援系や、 モデル検査機での表現に適した状態遷移単位での記述が求められる。
+CbCで使用するCodeGearは、 状態遷移モデルにおける状態そのものとして捉えることが可能である。
+これらの状態をまとめる構造体として、 CbCの\texttt{context}を導入した。