Mercurial > hg > Papers > 2018 > mitsuki-sigos

Binary file Paper/main.pdf has changed
--- a/Paper/main.tex	Fri Dec 22 23:29:20 2017 +0900
+++ b/Paper/main.tex	Sat Dec 23 00:51:46 2017 +0900
@@ -172,7 +172,7 @@
 \end{figure}

 Gears OS は Context と呼ばれる使用されるすべての Code Gear、Data Gear 持っている Meta Data Gear を持つ。
-Gears OS は必要な Code Gear、Data Gear に参照したい場合、この Context を通す必要がある。
+Gears OS は必要な Code Gear、Data Gear を参照したい場合、この Context を通す必要がある。

 しかし Context を通常の計算から直接扱うのはセキュリティ上好ましくない。
 そこで Context から必要なデータを取り出して Code Gear に接続するMeta Code Gear である stub Code Gear を定義し、
@@ -206,8 +206,8 @@
 %Gears OS は必要な Code Gear、Data Gear に参照したい場合、この Context を通す必要がある。
 Code\ref{context} は Context の定義で Code\ref{initcontext} は Context の生成である。

-\lstinputlisting[caption=Context, label=context]{./src/context1.c}
-\lstinputlisting[label=initcontext, caption=initContext]{./src/initcontext.c}
+\lstinputlisting[caption=Contextの定義, label=context]{./src/context1.c}
+\lstinputlisting[label=initcontext, caption=Contextの生成]{./src/initcontext.c}

 Data Gear は union と struct によって表現される。
 Context には Data Gear の Data Type の情報が格納されている。
@@ -216,7 +216,7 @@

 Context は Task でもあり、Taskは通常のOSのスレッドに対応する。
 Task は実行する Code Gear と Data Gear をすべて持っている。
-TaskManager によって Context が生成され Task Queue へ挿入する。
+TaskManager によって Context が生成され TaskQueue へ挿入する。
 Gears OS における Task Queue は Synchronized Queue で実現される。
 Worker は TaskQueue から Task である Context を取得し、 Input/Output Data Gear の依存関係が解決されたものから並列実行される。

@@ -238,13 +238,13 @@
 Code Gear、Data Gear に参照するために Context を通す必要があるが、
 Interface を記述することでデータ構造の api と Data Gear を結びつけることが出来る。

-\lstinputlisting[label=interface, caption=Interface]{./src/Stack.cbc}
+\lstinputlisting[label=interface, caption=StackのInterface]{./src/Stack.cbc}

 Code\ref{implement}は stack の Implement の例である。
 createImpl は関数呼び出しで呼び出され、Implement の初期化と Code Gear のスロットに対応する Code Gear の番号を入れる。
 %return で interface を返し、その先で Code Gear や Data Gear へ継続できるようになる。

-\lstinputlisting[label=implement, caption=Implement]{./src/stackimpl.cbc}
+\lstinputlisting[label=implement, caption=SingleLinkedStackのImplement]{./src/stackimpl.cbc}

 %\section{Gearef、GearImpl}

@@ -274,7 +274,7 @@

 cbc ファイルから、生成した stub Code Gear を加えて stub を加えたコードに変換を行う。(Code\ref{stack_c})

-\lstinputlisting[label=stack_c, caption=stub Code Gear]{./src/ex_stub}
+\lstinputlisting[label=stack_c, caption=stub Code Gear を加えたコード]{./src/ex_stub}

 \section{Context の生成}
 generate\_context は Context.h、Interface.cbc、generate\_stub で生成されたImpl.cbc を見て Context を生成する Perl スクリプトである。
@@ -304,7 +304,7 @@
 Context には Data Gear の Data Type の情報が格納されている。
 この情報から確保される Data Gear のサイズなどを決定する。

-\lstinputlisting[label=init_context, caption=生成されたinitContext]{./src/gencontext.c}
+\lstinputlisting[label=init_context, caption=Perlスクリプトで生成されたinitContext]{./src/gencontext.c}

 %\section{比較}
 %従来の OS は、ユーザーレベルとシステムレベルを持っているが、
--- a/Paper/prosym.bib	Fri Dec 22 23:29:20 2017 +0900
+++ b/Paper/prosym.bib	Sat Dec 23 00:51:46 2017 +0900
@@ -17,63 +17,63 @@
 }

 %@article{
-    llvm,
-    title = "LLVM documentation.",
-    howpublished = "{http://llvm.org/docs/index.html}"
-}
+%    llvm,
+%    title = "LLVM documentation.",
+%    howpublished = "{http://llvm.org/docs/index.html}"
+%}

 %@article{
-    SMT1,
-    author = "Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski, Rafal Kolanski, Gernot Heiser"
-    title = "Comprehensive Formal Verification of an OS Microkernel"
-    journal = "ACM Transactions on Computer Systems (TOCS) 32.1"
-    year = 2014
-}
+%    SMT1,
+%    author = "Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski, Rafal Kolanski, Gernot Heiser"
+%    title = "Comprehensive Formal Verification of an OS Microkernel"
+%    journal = "ACM Transactions on Computer Systems (TOCS) 32.1"
+%    year = 2014
+%}

 %@article{
-    SMT2,
-    author = "Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, Simon Winwood"
-    title = "seL4: Formal Verification of an OS Kernel"
-    journal = "Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles. ACM"
-    year = 2009
-}
+%    SMT2,
+%    author = "Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, Simon Winwood"
+%    title = "seL4: Formal Verification of an OS Kernel"
+%    journal = "Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles. ACM"
+%    year = 2009
+%}

 %@article{
-    type,
-    author = "Jean Yang, Chris Hawblitzel"
-    title = "Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System"
-    journal = "ACM Sigplan Notices. Vol. 45. No. 6. ACM"
-    year = 2010
-}
+%    type,
+%    author = "Jean Yang, Chris Hawblitzel"
+%    title = "Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System"
+%    journal = "ACM Sigplan Notices. Vol. 45. No. 6. ACM"
+%    year = 2010
+%}

 %@article{
-    ,
-    author = "Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjo ̈berg, David Costanzo"
-    title = "CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels"
-    journal = "OSDI"
-    year = 2016
-}
+%    ,
+%    author = "Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjo ̈berg, David Costanzo"
+%    title = "CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels"
+%    journal = "OSDI"
+%    year = 2016
+%}

 %@article{
-    ,
-    author = "Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, Xi Wang"
-    title = "Push-Button Verification of File Systems via Crash Refinement"
-    journal = "OSDI"
-    year = 2016
-}
+%    ,
+%    author = "Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, Xi Wang"
+%    title = "Push-Button Verification of File Systems via Crash Refinement"
+%    journal = "OSDI"
+%    year = 2016
+%}

 %@article{
-    ,
-    author = "Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi Wang"
-    title = "Hyperkernel: Push-Button Verification of an OS Kernel"
-    journal = "Proceedings of the 26th Symposium on Operating Systems Principles. ACM"
-    year = 2017
-}
+%    ,
+%    author = "Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi Wang"
+%    title = "Hyperkernel: Push-Button Verification of an OS Kernel"
+%    journal = "Proceedings of the 26th Symposium on Operating Systems Principles. ACM"
+%    year = 2017
+%}

 %@article{
-    ,
-    author = "Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich"
-    title = "Using Crash Hoare Logic for Certifying the FSCQ File System"
-    journal = "Proceedings of the 25th Symposium on Operating Systems Principles. ACM"
-    year =  2015
-}
+%    ,
+%    author = "Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich"
+%    title = "Using Crash Hoare Logic for Certifying the FSCQ File System"
+%    journal = "Proceedings of the 25th Symposium on Operating Systems Principles. ACM"
+%    year =  2015
+%}