Mercurial > hg > Papers > 2020 > anatofuz-sigos

changeset 20:ca6506bdcda4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
date Sat, 02 May 2020 16:30:15 +0900
parents 13d8fe4cfc5c
children 7c9cac61b14c
files paper/anatofuz-sigos.md paper/anatofuz-sigos.pdf paper/anatofuz-sigos.tex
diffstat 3 files changed, 12 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- 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`を導入した。
 
 
 
Binary file paper/anatofuz-sigos.pdf has changed
--- 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}を導入した。