--- a/Paper/sigos.bib	Sun Apr 22 18:58:59 2018 +0900
+++ b/Paper/sigos.bib	Mon Apr 23 16:48:56 2018 +0900
@@ -16,6 +16,11 @@
     year = 2015
 }
 
+@manual{gcc,
+author = "{GNU Compiler Collection (GCC) Internals}",
+title ="{http://gcc.gnu.org/onlinedocs/gccint/}",
+}
+
 @InProceedings{llvm,
 author    = {Chris Lattner and Vikram Adve},
 title     = "{LLVM: A Compilation Framework for Lifelong Program Analysis \& Transformation}",
@@ -25,144 +30,9 @@
 year      = {2004}
 }
 
-
-@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},
- booktitle = {Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation},
- series = {PLDI '10},
- year = {2010},
- isbn = {978-1-4503-0019-3},
- location = {Toronto, Ontario, Canada},
- pages = {99--110},
- numpages = {12},
- url = {http://doi.acm.org/10.1145/1806596.1806610},
- doi = {10.1145/1806596.1806610},
- acmid = {1806610},
- publisher = {ACM},
- address = {New York, NY, USA},
- keywords = {operating system, run-time system, type safety, verification},
+@misc{openmp,
+    title = "OpenMP: Simple, portable, scalable SMP programming",
+    howpublished = {\url{http://www.openmp.org,}},
+    note = {Accessed: 2018/02/05(Mon)}
 }
 
-@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},
-}
-

Binary file Paper/sigos.pdf has changed

--- a/Paper/sigos.tex	Sun Apr 22 18:58:59 2018 +0900
+++ b/Paper/sigos.tex	Mon Apr 23 16:48:56 2018 +0900
@@ -104,8 +104,8 @@
 ハードウェア、サービスに対応して OS 自体が拡張される必要がある。
 OS は非決定的な実行を持ち、その信頼性を保証するには、従来のテストとデバッグでは不十分であり、テストしきれない部分が残ってしまう。
 これに対処するためには、証明を用いる方法とプログラムの可能な実行をすべて数え上げるモデル検査を用いる方法がある。
-モデル検査は無限の状態ではなくても巨大な状態を調べることになり、状態を有限に制限したり状態を抽象化したりする方法が用いられている
-図\ref{fig:verification}。
+モデル検査は無限の状態ではなくても巨大な状態を調べることになり、状態を有限に制限したり状態を抽象化したりする方法が用いられている。
+(図\ref{fig:verification})
 \begin{figure}[ht]
  \begin{center}
   \includegraphics[width=70mm]{./pic/verification.pdf}
@@ -148,7 +148,7 @@
 
 \section{Gears におけるメタ計算}
 Gears OS ではメタ計算を柔軟に記述するためのプログラミング言語の単位として Code Gear、Data Gear という単位を用いる。
-Code Gear、Data Gear にはそれぞれメタレベルの単位である Meta Code Gear、Meta Data Gear が存在し、これらを用いてメタ計算を実現する。図\ref{fig:metaCS}
+Code Gear、Data Gear にはそれぞれメタレベルの単位である Meta Code Gear、Meta Data Gear が存在し、これらを用いてメタ計算を実現する。(図\ref{fig:metaCS})
 
 \begin{figure}[ht]
  \begin{center}
@@ -235,7 +235,7 @@
 
 Code\ref{interface}は stack の Interface である。
 Code Gear、Data Gear に参照するために Context を通す必要があるが、
-Interface を記述することでデータ構造の api と Data Gear を結びつけることが出来る。
+Interface を記述することでデータ構造の API と Data Gear を結びつけることが出来る。
 
 \lstinputlisting[label=interface, caption=StackのInterface]{./src/Stack.cbc}
 
@@ -271,7 +271,7 @@
 
 Context は Meta Data Gear に相当し、Code Gear や Data Gear を管理している。
 
-generate\_context は context の定義 (Code\ref{context}) を読み宣言されている Data Gear を取得する。
+generate\_context は context.h を読み宣言されている Data Gear を取得する。
 Code Gear の取得は指定された generate\_stub で生成されたコードから \_\_code 型を見て行う。
 取得した Code Gear、Data Gear の enum の定義は enumCode.h、enumData.h に生成される。
 
@@ -439,7 +439,7 @@
 Twice は並列実行の依存関係もなく、データ並列での実行に適した課題である。
 そのため、 通信時間を考慮しなければ CPU よりコア数が多い GPU が有利となる。
 
-要素数$2^{27}$ のデータに対する Twice の実行結果を 表\ref{tab:wice}、図\ref{fig:twice}に示す。
+要素数$2^{27}$ のデータに対する Twice の実行結果を 表\ref{tab:twice}、図\ref{fig:twice}に示す。
 CPU 実行の際は $2^{27}$ のデータを 64個のTask に分割して並列実行を行っている。
 GPU では1次元の block 数を $2^{15}$、 block 内の thread 数を $2^{10}$ で kernel の実行を行った。
 ここでの ``GPU`` は CPU、GPU 間のデータの通信時間も含めた時間、 ``GPU(kernel only)`` は kernel のみの実行時間である。
@@ -629,7 +629,7 @@
 Go、OpenMP との比較から、 Gears OS が1CPU での動作が遅いということがわかった。
 Gears OS は par goto 文を使用することで Context を生成し、並列処理を行う。
 しかし、Context はメモリ空間の確保や使用する全ての Code/Data Gear を設定する必要があり、生成にある程度の時間がかかってしまう。
-そこで、 par goto のコンパイルタイミングで実行する Code Gear のフローをモデル検査で解析し、処理が軽い場合はContext を生成せずに、関数呼び出しを行う等の最適化を行>うといったチューニングが必要である。
+そこで、 par goto のコンパイルタイミングで実行する Code Gear のフローをモデル検査で解析し、処理が軽い場合はContext を生成せずに、関数呼び出しを行う等の最適化を行なうといったチューニングが必要である。
 
 
 \nocite{*}