Mercurial > hg > Papers > 2019 > anatofuz-prosym-gears
changeset 3:450d0e91835b
tweak
| author | anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 21 Nov 2019 12:40:00 +0900 |
| parents | bee0603ddad4 |
| children | 1a881e24e438 |
| files | paper/Makefile paper/anatofuz_prosym_2019.pdf paper/anatofuz_prosym_2019.tex |
| diffstat | 3 files changed, 6 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- 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
--- 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)で実装されている。