# HG changeset patch
# User mir3636
# Date 1513957906 -32400
# Node ID 3e81264d47645bf8331cecba9687a370739cc79a
# Parent  490464faf4324dbfdc4df21b00bb03dff33323ab
fix

diff -r 490464faf432 -r 3e81264d4764 Paper/main.pdf
Binary file Paper/main.pdf has changed
diff -r 490464faf432 -r 3e81264d4764 Paper/main.tex
--- 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 は、ユーザーレベルとシステムレベルを持っているが、
diff -r 490464faf432 -r 3e81264d4764 Paper/prosym.bib
--- 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
+%}