Mercurial > hg > Papers > 2020 > anatofuz-sigos

comparison paper/anatofuz-sigos.md @ 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 099e7864ee79
children 7c9cac61b14c
comparison
equal deleted inserted replaced
19:13d8fe4cfc5c 20:ca6506bdcda4
79 79
80 この他にCbCからCへ復帰する為のAPIとして、 環境付きgotoという機能がある。 80 この他にCbCからCへ復帰する為のAPIとして、 環境付きgotoという機能がある。
81 これはGCCでは内部コードを生成、 LLVM/clangでは`setjmp`と`longjmp`を使うことでCodeGearの次の継続対象として呼び出し元の関数を設定することが可能となる。 81 これはGCCでは内部コードを生成、 LLVM/clangでは`setjmp`と`longjmp`を使うことでCodeGearの次の継続対象として呼び出し元の関数を設定することが可能となる。
82 したがってプログラマから見ると、通常のCの関数呼び出しの返り値をCodeGearから取得する事が可能となる。 82 したがってプログラマから見ると、通常のCの関数呼び出しの返り値をCodeGearから取得する事が可能となる。
83 83
84 # CbCを用いたxv6の再実装 84 # CbCを用いたOSの実装
85
86 軽量継続を持つCbCを利用して、 証明可能なOSを実装したい。
87 その為には証明に使用される定理証明支援系や、 モデル検査機での表現に適した状態遷移単位での記述が求められる。
88 CbCで使用するCodeGearは、 状態遷移モデルにおける状態そのものとして捉えることが可能である。
89 これらの状態をまとめる構造体として、 CbCの`context`を導入した。
85 90
86 91
87 92
88 # xv6のファイルシステムの一部の分析 93 # xv6のファイルシステムの一部の分析
89 94