--- a/Paper/main.tex	Sat Dec 23 11:52:17 2017 +0900
+++ b/Paper/main.tex	Sat Dec 23 16:30:09 2017 +0900
@@ -67,6 +67,59 @@
 \maketitle
 
 % Body %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\section{OSの拡張性と信頼性の両立}
+
+さまざまなコンピュータの信頼性の基本はメモリなどの資源管理を行うOSである。OSの信頼性を保証する事自体が難しいが、時代とともに進歩する
+ハードウェア、サービスに対応してOS自体が拡張される必要がある。OSは非決定的な実行を持ち、その信頼性を保証するには、従来のテストとデバッグでは不十分
+であり、テストしきれない部分が残ってしまう。これに対処するためには、証明を用いる方法とプログラムの可能な実行をすべて数え上げるモデル検査を用いる方法が
+ある。モデル検査は無限の状態ではなくても巨大な状態を調べることになり、状態を有限に制限したり状態を抽象化したりする方法が用いられている
+図\ref{fig:verification}。
+\begin{figure}[ht]
+ \begin{center}
+  \includegraphics[width=70mm]{./pic/verification.pdf}
+ \end{center}
+ \caption{証明とモデル検査によるOSの検証}
+ \label{fig:verification}
+\end{figure}
+
+証明やモデル検査を用いてOSを検証する方法はさまざまなものが検討されている。検証は一度ですむものではなく、アプリケーションやサービス、デバイスが新しく
+なることに検証をやり直す必要がある。つまり信頼性と拡張性を両立させることが重要である。
+
+コンピュータの計算はプログラミング言語で記述されるが、その言語の実行は操作的意味論の定義などで規定される。プログラミング言語で記述される部分を
+ノーマルレベルの計算と呼ぶ。コードが実行される時には、処理系の詳細や使用する資源、あるいは、コードの仕様や型などの言語以外の部分が服属する。
+これをメタレベルの計算という。この二つのレベルを同じ言語で記述できるようにして、ノーマルレベルの計算の信頼性をメタレベルから保証できるようにしたい。
+ノーマルレベルでの正当性を保証しつつ、新しく付け加えられたデバイスやプログラムを含む正当性を検証したい。
+
+本論文では、ノーマルレベルとメタレベルを共通して表現できる言語として Continuation based C(以下CbC)\cite{cbc}を用いる。CbC は関数呼出時の暗黙の環境(Environment)
+を使わずに、コードの単位を行き来できる引数付きgoto文(parametarized goto)を持つCと互換性のある言語である。これを用いて、Code Gear と Data Gear、さらに
+そのMeta 構造を導入する。これらを用いて、検証されたGears OSを構築したい。
+図\ref{fig:MetaGear}。
+\begin{figure}[ht]
+ \begin{center}
+  \includegraphics[width=70mm]{./pic/verification.pdf}
+ \end{center}
+ \caption{Gearsのメタ計算}
+ \label{fig:MetaGear}
+\end{figure}
+
+本論文では、Gears OSの要素である Code Gear、Data Gea、そして、Meta Code Gear 、Meta Data Gear の構成を示す。これらは、CbC に変換されて実行される。
+Gears OS は、Task Scheduler をCPUやGPU毎に持ち、一つのTaskに対応する Context というMeta Data Gear を使用しながら計算を実行する。
+
+Meta Gear を入れかえることにより、ノーマルレベルのGearをモデル検査することができるようにしたい。ノーマルレベルでのCode GearとData Gear は
+継続を基本とした関数型プログラミング的な記述に対応する。この記述を定理証明支援系であるAgdaを用いて直接に証明できるようにしたい。
+
+従来の研究でメタ計算を用いる場合は、関数型言語ではMonadを用いる\cite{Moggi:1989:CLM:77350.77353}。これはHakell では実行時の環境を記述する構文として使われている。
+OSの研究では、メタ計算の記述に型つきアセンブラ(Typed Assembler)を用いることがある\cite{Yang:2010:SLI:1806596.1806610}。PythonやHaskellによる記述をノーマルレベルとして
+採用したOSの検証の研究もある\cite{Klein:2009:SFV:1629575.1629596,Chen:2015:UCH:2815400.2815402}。
+SMITなどのモデル検査をOSの検証に用いた例もある\cite{Sigurbjarnarson:2016:PVF:3026877.3026879}。
+
+本研究で用いる Meta Gear は制限されたMonadに相当し、型つきアセンブラよりは大きな表現単位を提供する。
+Haskellなどの関数型プログラミング言語では実行環境が複雑であり、実行時の資源使用を明確にすることができない。CbC はスタック上に隠された
+環境を持たないので、メタレベルで使用する資源を明確にできるという利点がある。ただし、Gear のプログラミングスタイルは、従来の関数呼出
+を中心としたものとはかなり異なる。本研究では、Gearsの記述をモジュールかするためにインターフェースを導入した。これにより、
+見通しの良いプログラミングが可能になった。
+
+
 \section{メタ計算の重要性}
 プログラムを記述する際、ノーマルレベルの処理の他に、メモリ管理、スレッド管理、CPU や GPU の資源管理等、記述しなければならない処理が存在する。
 これらの計算をメタ計算と呼ぶ。
@@ -306,7 +359,54 @@
 
 \lstinputlisting[label=init_context, caption=Perlスクリプトで生成されたinitContext]{./src/gencontext.c}
 
-%\section{比較}
+\section{比較}
+
+従来のプログラミングスタイルとの比較。
+Gears のプログラミングは関数呼出を中心とするプログラミングとはかなり異なる。
+Gears は関数呼出を禁止しているわけではなく、使用する資源の制御に問題がないなら普通に関数呼出して良い。
+Linux kernel などでは関数呼出の大半はインライン展開されることを期待してプログラミングされており、
+関数呼出で予測できないスタックの爆発やCPU資源の浪費が起きないようにプログラミングされている。
+Gears では Gears 間のプログラミングは戻り先や使用する資源を明示する必要がある。
+
+goto 文での引数は通常の関数呼出と異なり、スタック(環境)に積むことができない。引数に必要な情報を含むData Gearを
+持ち歩くスタイルとなる。一つのインタフェース内部では、これらは共通している。実際、これらはメタレベルでは、
+Context というMeta Data Gear にすべて格納されている。メタレベルは、Data Gearの詳細な型は使用されない。
+ノーマルレベルに移行する際に stub Code Gear を通して詳細な型が接続される。
+
+インタフェースを再利用する際には、呼び出すインタフェースが持つ引数は保存される必要がある。これらは、実際には
+Context 内にあるので自動的に保存されている。ノーマルレベルの記述では、... の部分にその意味が込めれている。
+これは、可変長引数の...と同じ意味だと考えても良い。ただ、LLVM/GCCレベルでそれを実装するのは比較的難しい。
+なので、今回はScriptによる変換を採用している。
+
+ノーマルレベルの記述と関数型プログラミングの記述の比較。Gear は必ず継続を渡す必要がある。これは一段の
+関数呼出を許しているのと同等である。70年代のFortan の関数呼出は決まった場所に戻り先を格納するので
+再起呼出ができなかったのと同じである。例えばCode Gears 以下のような型を持つ。ここで t は継続の型である。
+Stack は Stack を受けとる Stack -> t というCode Gearを継続として引数で受けとる。popStack はこの引数を
+呼び出す。
+
+     popStack : {a t : Set} -> Stack -> (Stack -> t) -> t
+
+つまり、Code Gear は制限された関数の形式を持っている。Data Gear は、関数型言語の直積や排他的論理和(Sum)を含むデータ型に
+対応する。しかし、一つのContext で実行されるData Gear は、一つの巨大なSumに含まれるようになっている。これを
+メタレベルでは、中の型の詳細に立ち入ることなく実行する。
+
+Context はノーマルレベルのData Gearの他に様々なメタ情報を持つ。例えば、メモリ管理情報や実行されるCPU、あるいは、Taskの
+状態、待ち合わせているData Gearなどである。これらの情報はCやアセンブラのレベルで実装されるのと同時に、通常のGearの
+プログラミングにも対応する。例えば、CPUをかそうてきにGearsで記述すればソフトウェア的な並列実行を実現し、実際の
+GPUを用いればGPUによる並列実行となる。この実行をモデル検査的な状態数え上げに対応させればモデル検査を実行できる。
+
+Haskell などを実行可能仕様記述として用いるOSの検証\cite{}と、Code Gearを用いる手法は類似しているが、Code Gearの場合は、
+記述を制限し、Code と仕様の対応、さらにCodeと資源の対応が明確になる利点がある。
+
+型つきアセンブラは、より低レベルの関数型の記述であると言える。アセンブラの記述自体は小さく扱いやすいが、
+OSレベルあるいはアプリケーションレベルからの距離が大きい。型の整合性を保証するだけではOSの検証としては
+不十分なので、証明やモデル検査を用いることになるが、記述量が多いのが、その際に欠点となる。
+Code Gearは、より大きな単位であり、プログラミングレベルの抽象化が可能になっているので、これらの記述の
+大きさの欠点をカバーできる可能性がある。
+
+証明手法は、従来では Hoare Logic のような Post Condition / Pre Condition を用いる方法が使われている。
+現在のGearsは、Agda への変換は考えているが、その上の具体的な証明方法はまだ用意されていない。
+
 %従来の OS は、ユーザーレベルとシステムレベルを持っているが、
 %システムレベルではメタ計算の分離ができない。
 %しかし Gears ではメタ計算を Meta Code Gear 単位で記述するため、メタ計算を階層化できる。

Binary file Paper/pic/MetaGear.graffle has changed

Binary file Paper/pic/MetaGear.pdf has changed

Binary file Paper/pic/verification.graffle has changed

Binary file Paper/pic/verification.pdf has changed

--- a/Paper/prosym.bib	Sat Dec 23 11:52:17 2017 +0900
+++ b/Paper/prosym.bib	Sat Dec 23 16:30:09 2017 +0900
@@ -26,6 +26,113 @@
 }
 
 
+@inproceedings{Sigurbjarnarson:2016:PVF:3026877.3026879,
+ author = {Sigurbjarnarson, Helgi and Bornholt, James and Torlak, Emina and Wang, Xi},
+ title = {Push-button Verification of File Systems via Crash Refinement},
+ booktitle = {Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation},
+ series = {OSDI'16},
+ year = {2016},
+ isbn = {978-1-931971-33-1},
+ location = {Savannah, GA, USA},
+ pages = {1--16},
+ numpages = {16},
+ url = {http://dl.acm.org/citation.cfm?id=3026877.3026879},
+ acmid = {3026879},
+ publisher = {USENIX Association},
+ address = {Berkeley, CA, USA},
+} 
+
+@inproceedings{Nelson:2017:HPV:3132747.3132748,
+ author = {Nelson, Luke and Sigurbjarnarson, Helgi and Zhang, Kaiyuan and Johnson, Dylan and Bornholt, James and Torlak, Emina and Wang, Xi},
+ title = {Hyperkernel: Push-Button Verification of an OS Kernel},
+ booktitle = {Proceedings of the 26th Symposium on Operating Systems Principles},
+ series = {SOSP '17},
+ year = {2017},
+ isbn = {978-1-4503-5085-3},
+ location = {Shanghai, China},
+ pages = {252--269},
+ numpages = {18},
+ url = {http://doi.acm.org/10.1145/3132747.3132748},
+ doi = {10.1145/3132747.3132748},
+ acmid = {3132748},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+} 
+
+
+
+@inproceedings{Gu:2016:CEA:3026877.3026928,
+ author = {Gu, Ronghui and Shao, Zhong and Chen, Hao and Wu, Xiongnan and Kim, Jieung and Sj\"{o}berg, Vilhelm and Costanzo, David},
+ title = {CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels},
+ booktitle = {Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation},
+ series = {OSDI'16},
+ year = {2016},
+ isbn = {978-1-931971-33-1},
+ location = {Savannah, GA, USA},
+ pages = {653--669},
+ numpages = {17},
+ url = {http://dl.acm.org/citation.cfm?id=3026877.3026928},
+ acmid = {3026928},
+ publisher = {USENIX Association},
+ address = {Berkeley, CA, USA},
+} 
+
+@inproceedings{Klein:2009:SFV:1629575.1629596,
+ author = {Klein, Gerwin and Elphinstone, Kevin and Heiser, Gernot and Andronick, June and Cock, David and Derrin, Philip and Elkaduwe, Dhammika and Engelhardt, Kai and Kolanski, Rafal and Norrish, Michael and Sewell, Thomas and Tuch, Harvey and Winwood, Simon},
+ title = {seL4: Formal Verification of an OS Kernel},
+ booktitle = {Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles},
+ series = {SOSP '09},
+ year = {2009},
+ isbn = {978-1-60558-752-3},
+ location = {Big Sky, Montana, USA},
+ pages = {207--220},
+ numpages = {14},
+ url = {http://doi.acm.org/10.1145/1629575.1629596},
+ doi = {10.1145/1629575.1629596},
+ acmid = {1629596},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ keywords = {isabelle/hol, l4, microkernel, sel4},
+} 
+
+@article{Klein:2014:CFV:2584468.2560537,
+ author = {Klein, Gerwin and Andronick, June and Elphinstone, Kevin and Murray, Toby and Sewell, Thomas and Kolanski, Rafal and Heiser, Gernot},
+ title = {Comprehensive Formal Verification of an OS Microkernel},
+ journal = {ACM Trans. Comput. Syst.},
+ issue_date = {February 2014},
+ volume = {32},
+ number = {1},
+ month = feb,
+ year = {2014},
+ issn = {0734-2071},
+ pages = {2:1--2:70},
+ articleno = {2},
+ numpages = {70},
+ url = {http://doi.acm.org/10.1145/2560537},
+ doi = {10.1145/2560537},
+ acmid = {2560537},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ keywords = {Isabelle/HOL, L4, microkernel, operating systems, seL4},
+} 
+
+@inproceedings{Chen:2015:UCH:2815400.2815402,
+ author = {Chen, Haogang and Ziegler, Daniel and Chajed, Tej and Chlipala, Adam and Kaashoek, M. Frans and Zeldovich, Nickolai},
+ title = {Using Crash Hoare Logic for Certifying the FSCQ File System},
+ booktitle = {Proceedings of the 25th Symposium on Operating Systems Principles},
+ series = {SOSP '15},
+ year = {2015},
+ isbn = {978-1-4503-3834-9},
+ location = {Monterey, California},
+ pages = {18--37},
+ numpages = {20},
+ url = {http://doi.acm.org/10.1145/2815400.2815402},
+ doi = {10.1145/2815400.2815402},
+ acmid = {2815402},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+} 
+
 @inproceedings{Yang:2010:SLI:1806596.1806610,
  author = {Yang, Jean and Hawblitzel, Chris},
  title = {Safe to the Last Instruction: Automated Verification of a Type-safe Operating System},
@@ -44,3 +151,18 @@
  keywords = {operating system, run-time system, type safety, verification},
 }
 
+@inproceedings{Moggi:1989:CLM:77350.77353,
+ author = {Moggi, E.},
+ title = {Computational Lambda-calculus and Monads},
+ booktitle = {Proceedings of the Fourth Annual Symposium on Logic in Computer Science},
+ year = {1989},
+ isbn = {0-8186-1954-6},
+ location = {Pacific Grove, California, USA},
+ pages = {14--23},
+ numpages = {10},
+ url = {http://dl.acm.org/citation.cfm?id=77350.77353},
+ acmid = {77353},
+ publisher = {IEEE Press},
+ address = {Piscataway, NJ, USA},
+}
+