# HG changeset patch
# User anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
# Date 1574307600 -32400
# Node ID 450d0e91835b932497dcc819b8d881fd7f8349fb
# Parent  bee0603ddad4ce4981fe4519760a53e650ed71f1
tweak

diff -r bee0603ddad4 -r 450d0e91835b paper/Makefile
--- a/paper/Makefile	Wed Nov 20 15:23:23 2019 +0900
+++ b/paper/Makefile	Thu Nov 21 12:40:00 2019 +0900
@@ -32,4 +32,4 @@
 
 
 clean:
-	rm -f *.dvi *.aux *.log *.pdf *.ps *.gz *.bbl *.blg *~ *.core *.bbl
+	rm -f *.dvi *.aux *.log *.ps *.gz *.bbl *.blg *~ *.core *.bbl
diff -r bee0603ddad4 -r 450d0e91835b paper/anatofuz_prosym_2019.pdf
Binary file paper/anatofuz_prosym_2019.pdf has changed
diff -r bee0603ddad4 -r 450d0e91835b paper/anatofuz_prosym_2019.tex
--- a/paper/anatofuz_prosym_2019.tex	Wed Nov 20 15:23:23 2019 +0900
+++ b/paper/anatofuz_prosym_2019.tex	Thu Nov 21 12:40:00 2019 +0900
@@ -60,10 +60,12 @@
 
 % Body %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \section{証明可能なOS}
-コンピュータ上で動作するあらゆるソフトウェアや資源を管理するOSは、 高い信頼性が保証されるべきである。
+コンピュータ上で動作するあらゆるソフトウェアや資源を管理するOSは、 高い信頼性が保証されてほしい。
 信頼性の保証にはテストプログラムを用いた検証や、 形式手法を用いた証明を使う手法が存在する。
-頻繁に並行処理を行うOSでは、 テストを用いてバグを発見するのが困難である。
-そのため、 形式手法的なアプローチを用いてOSの信頼性を保証したい。
+頻繁に並列処理を行うOSでは、 スレッド間の共通資源の競合などの非決定的な実行を行う。
+OSの信頼性を保証する上ではテストやデバッグを用いる手法では、 発生しうる状態を完全に保証するのは困難である。
+そのため、 テストを用いる方法ではなく、 形式手法的なアプローチを用いてOSの信頼性を保証したい。
+しかしOSの殆どはC言語やアセンブラで記述されており、 これらでは関数呼び出し時で実行する処理にスタックに積まれた変数や、 グローバル変数などを多様してしまう。
 現在開発しているGearsOSは、 継続を基本とする言語Conitinuation Based C(CbC)で実装されている。