Mercurial > hg > Papers > 2018 > parusu-master

--- a/paper/evaluation.tex	Sun Feb 04 22:42:13 2018 +0900
+++ b/paper/evaluation.tex	Mon Feb 05 03:11:35 2018 +0900
@@ -138,5 +138,18 @@
 GPU で実行される Task 同士の依存関係の解決の際はCuDevicePtr などのGPU のメモリへのポインタを渡し、CPU でデータが必要になったときに初めて GPU から CPU へデータの通信を行うメタ計算の実装が必要となる。

 \section{OpenMP との比較}
+OpenMP\cite{openmp} は C、 C++ のプログラムにアノテーションを付けることで並列化を行う。
+アノテーションを \coderef{openMP} のように for 文の前につけることで、ループの並列化を行う。
+
+\lstinputlisting[caption=OpenMP での Twice, label=code:openMP]{./src/openMP.c}
+
+OpenMP は既存のコードにアノテーションを付けるだけで並列化を行えるため、変更が少なくて済む。
+しかし、 ループのみの並列化ではプログラム全体の並列度が上がらずアムダールの法則により性能向上が頭打ちになってしまう。
+OpenMP はループの並列化 ではなくブロック単位での並列実行もサポートしているが、アノテーションの記述が増えてしまう。
+また、 OpenMPはコードとデータを厳密に分離していないため、データの待ち合わせ処理をバリア等のアノテーションで記述する。
+
+Gears OS では Input Data Gear が揃った Code Gear は並列に実行されるため、プログラム全体の並列度を高めることが出来る。
+また 並列処理のコードとデータの依存関係を``par goto'' で簡潔に記述することが出来る。

 \section{Go との比較}
+Go言語\cite{go}
--- a/paper/gearsOS.tex	Sun Feb 04 22:42:13 2018 +0900
+++ b/paper/gearsOS.tex	Mon Feb 05 03:11:35 2018 +0900
@@ -35,7 +35,7 @@
 \section{Continuation based C}
 Gears OS の実装は本研究室で開発されている CbC(Continuation based C) を用いて行う。
 CbC は Code Gear を基本的な処理単位として記述できるプログラミング言語である。
-CbC の処理系として llvm/clang\cite{kaito-lola} と gcc\cite{nobu-prosym} による実装などが存在する。
+CbC の処理系として llvm\cite{llvm}/clang と gcc による実装などが存在する\cite{kaito-lola}\cite{nobu-prosym}。

 CbC の記述例を\coderef{cg1}に、 実際にこのソースコードが実行される際の遷移を\figref{cg1}に示す。
 CbC の Code Gear は \_\_code という型を持つ関数として記述する。
--- a/paper/introduction.tex	Sun Feb 04 22:42:13 2018 +0900
+++ b/paper/introduction.tex	Mon Feb 05 03:11:35 2018 +0900
@@ -1,3 +1,13 @@
 \chapter{メタ計算を使った並列処理}
+現代の OS では拡張性と信頼性を両立させることが要求されている。
+時代と主に進歩するハードウェア、サービスに対して OS 自体が拡張される必要がある。
+しかし、OSには非決定的な実行を持っており、その信頼性を保証するには従来のテストとデバッグでは不十分であり、テスト仕切れない部分が残ってしまう。
+これに対処するために証明を用いる方法とプログラムの可能な実行をすべて数え上げるモデル検査を用いる方法がある。

+% これはryokka 向き
+証明やモデル検査を用いて OS の検証する方法は様々なものが検討されている。
+型付きアセンブラ\cite{Yang:2010:SLI:1806596.1806610}
+従来の研究ではPython\cite{Sigurbjarnarson:2016:PVF:3026877.3026879} や Haskell\cite{Chen:2015:UCH:2815400.2815402}\cite{Klein:2009:SFV:1629575.1629596}による記述した OS を検証する研究も存在する。
+また SPIN などのモデル検査を OS の検証に用いた例もである。
+本研究室では信頼性をノーマルレベルの掲載に対して保証し、拡張性をメタレベルの計算で実現することを目標に Gears OS を開発している。
 \section{本論文の構成}
Binary file paper/master_paper.pdf has changed
--- a/paper/reference.bib	Sun Feb 04 22:42:13 2018 +0900
+++ b/paper/reference.bib	Mon Feb 05 03:11:35 2018 +0900
@@ -15,6 +15,76 @@
     keywords = {compare_and_swap, concurrent queue, lock-free, multiprogramming, non-blocking},
 }

+@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{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},
+}
+
+
+@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{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},
+}
+
 @article{moggi-monad,
     author     = {Moggi, Eugenio},
     title      = {Notions of Computation and Monads},
@@ -54,6 +124,16 @@
     month = "jan"
 }

+
+@InProceedings{llvm,
+author    = {Chris Lattner and Vikram Adve},
+title     = "{LLVM: A Compilation Framework for Lifelong Program Analysis \& Transformation}",
+booktitle = "{Proceedings of the 2004 International Symposium on Code Generation and Optimization (CGO'04)}",
+address   = {Palo Alto, California},
+month     = {Mar},
+year      = {2004}
+}
+
 @article{kaito-lola,
     author  = "Kaito, Tokumori and Shinji, Kono",
     title   = "Implementing Continuation based language in LLVM and Clang",
@@ -93,10 +173,16 @@
     note = {Accessed: 2016/02/06(Mon)}
 }

+@misc{openmp,
+    title = "OpenMP: Simple, portable, scalable SMP programming",
+    howpublished = {\url{http://www.openmp.org,}},
+    note = {Accessed: 2018/02/05(Mon)}
+}
+
 @misc{cuda,
     title = {CUDA Zone | NVIDIA Developer},
     howpublished = {\url{https://developer.nvidia.com/cuda-zone}},
-    note = {Accessed: 2016/02/06(Mon)}
+    note = {Accessed: 2018/02/05(Mon)}
 }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/openMP.c	Mon Feb 05 03:11:35 2018 +0900
@@ -0,0 +1,4 @@
+#pragma omp parallel for
+for(int i = 0; i < length; i++) {
+    a[i] = a[i] * 2;
+}