Mercurial > hg > Papers > 2020 > tobaru-master

changeset 25:50a4bbf4404a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix reference
author tobaru
date Sun, 09 Feb 2020 03:26:28 +0900
parents a83904322d97
children ee9435951c31
files paper/evaluation.tex paper/master_paper.pdf paper/master_paper.synctex.gz paper/master_paper.tex paper/reference.bib paper/sources.tex paper/summary.tex slide/fig/Memoryconstitution.pdf slide/fig/Memoryconstitution.png
diffstat 9 files changed, 85 insertions(+), 129 deletions(-) [+]
line wrap: on
line diff
--- a/paper/evaluation.tex	Sat Feb 08 19:52:55 2020 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-\chapter{評価}
Binary file paper/master_paper.pdf has changed
Binary file paper/master_paper.synctex.gz has changed
--- a/paper/master_paper.tex	Sat Feb 08 19:52:55 2020 +0900
+++ b/paper/master_paper.tex	Sun Feb 09 03:26:28 2020 +0900
@@ -91,7 +91,7 @@
 \listoftables
 
 %リスト目次
-\lstlistoflistings
+% \lstlistoflistings
 
 %chapters
 % \input{introduction.tex}
@@ -100,7 +100,6 @@
 \input{Xv6.tex}
 \input{Paging.tex}
 \input{cbc_interface.tex}
-\input{evaluation.tex}
 \input{summary.tex}
 
 
--- a/paper/reference.bib	Sat Feb 08 19:52:55 2020 +0900
+++ b/paper/reference.bib	Sun Feb 09 03:26:28 2020 +0900
@@ -1,17 +1,66 @@
-@article{xv6,
-    author = "{Russ Cox, M. Frans Kaashoek, and Robert T. Morris}",
-    title = "{xv6: a simple, Unix-like teaching operating system}",
-    howpublished = "{http://pdos.csail.mit.edu/6.828/xv6/}",
-    year = 2014
+@article{
+    cbc,
+    author = "Kaito TOKKMORI and Shinji KONO",
+    title = "Implementing Continuation based language in LLVM and Clang",
+    journal = "LOLA 2015",
+    month = "July",
+    year = 2015
+}
+
+@misc{xv6,
+  title={Xv6, a simple Unix-like teaching operating system},
+  author={Cox, Russ and Kaashoek, M Frans and Morris, Robert},
+  journal={2013-09-05]. http://pdos. csail. mit. edu/6.828/2012/xv6. html},
+  year={2011}
+}
+
+@article{
+    gears,
+    author = "河野 真治 and 伊波 立樹 and  東恩納 琢偉",
+    title = "Code Gear、Data Gear に基づく OS のプロトタイプ",
+    journal = "情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)",
+    month = "May",
+    year = 2016
 }
 
-@article{os,
-    author = {Andrew S.Tanenbaum, Herbert Bos},
-    title = "{Modern Operating Systems}",
-    publisher = {PEASON},
-    year = {2015},
+@article{
+    gears_cg_dg,
+    author = "宮城光希 and 河野真治",
+    title = "Code Gear と Data Gear を持つ Gears OS の設計",
+    journal = "第59回プログラミング・シンポジウム",
+    month = "Jan",
+    year = 2018,
+}
+
+@article{
+    gears_demo,
+    author = "宮城光希 and 河野真治",
+    title = "継続を中心とした言語 Gears OS のデモンストレーション",
+    journal = "第60回プログラミング・シンポジウム",
+    month = "Jan",
+    year = 2019,
 }
 
+@manual{arm,
+author     = "{ARM Architecture Reference Manual}",
+title  = "{http://infocenter.arm.com/help/topic/com.arm.\\doc.subset.architecture.reference/index.html}"
+}
+
+@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}
+}
+
+@manual{gcc,
+author = "{GNU Compiler Collection (GCC) Internals}",
+title ="{http://gcc.gnu.org/onlinedocs/gccint/}",
+}
+
+
 @misc{rpi,
 title     = "{Raspberry Pi — Teach, Learn, and Make with Raspberry Pi}",
 howpublished    = {https://www.raspberrypi.org}
@@ -25,86 +74,6 @@
 }
 
 @article{
-    cbc,
-    author = "Kaito TOKKMORI and Shinji KONO",
-    title = "Implementing Continuation based language in LLVM and Clang",
-    journal = "LOLA 2015",
-    month = "July",
-    year = 2015
-}
-
-@article{moggi-monad,
-    author     = {Moggi, Eugenio},
-    title      = {Notions of Computation and Monads},
-    journal    = {Inf. Comput.},
-    issue_date = {July 1991},
-    volume     = {93},
-    number     = {1},
-    month      = jul,
-    year       = {1991},
-    issn       = {0890-5401},
-    pages      = {55--92},
-    numpages   = {38},
-    url        = {http://dx.doi.org/10.1016/0890-5401(91)90052-4},
-    doi        = {10.1016/0890-5401(91)90052-4},
-    acmid      = {116984},
-    publisher  = {Academic Press, Inc.},
-    address    = {Duluth, MN, 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},
-}
-
-@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},
-}
-
-@article{
     agda-ryokka,
     author = "Hokama MASATAKA and Shinji KONO",
     title = "GearsOS の Hoare Logic をベースにした検証手法",
@@ -130,38 +99,17 @@
  address = {New York, NY, USA},
  keywords = {dependent types, programming},
 }
-
-@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}
-}
-
-@manual{gcc,
-author = "{GNU Compiler Collection (GCC) Internals}",
-title ="{http://gcc.gnu.org/onlinedocs/gccint/}",
+@book{codereading,
+author = "青柳 隆宏",
+title = "はじめてのOSコードリーディング --UNIX V6で学ぶカーネルのしくみ",
+year = 2013
 }
 
-@article{
-    gears,
-    author = "河野 真治 and 伊波 立樹 and  東恩納 琢偉",
-    title = "Code Gear、Data Gear に基づく OS のプロトタイプ",
-    journal = "情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)",
-    month = "May",
-    year = 2016
+@article{os,
+    author = {Andrew S.Tanenbaum, Herbert Bos},
+    title = "{Modern Operating Systems}",
+    publisher = {PEASON},
+    year = {2015},
 }
 
-@manual{arm,
-author     = "{ARM Architecture Reference Manual}",
-title  = "{http://infocenter.arm.com/help/topic/com.arm.\\doc.subset.architecture.reference/index.html}"
-}
 
-@misc{xv6,
-author     = "{Russ Cox, Frans Kaashoek, Robert Morris}",
-title    = {xv6 a simple, Unix-like teaching operating system},
-howpublished   = {https://pdos.csail.mit.edu/6.828/2018/xv6/book-rev11.pdf},
-}
-
--- a/paper/sources.tex	Sat Feb 08 19:52:55 2020 +0900
+++ b/paper/sources.tex	Sun Feb 09 03:26:28 2020 +0900
@@ -2,15 +2,23 @@
 
 本文中に紹介したソースコードの内、量が膨大なため一部しか掲載できなかったソースコードを示す。
 
-\section{インターフェース内の private メソッドの実装}
+
+
 
+
+\section{インターフェースの 実装}
 Xv6 の元のコードである vm.c \ref{vm_c_all}  をインターフェースで定義した後に、if 文や for 文がある関数を実装側でさらに分けた vm\_impl\_private.cbc をソースコード \ref{vm_impl_private} に示す。
 
 
 
 
+\lstinputlisting[label=vm_impl_private, caption={\footnotesize vm の実装の private}]{./src/vm_impl_private_all.cbc}
+
+
+\section{Xv6 の Paging}
+Paging の記述である Xv6 の vm.c のコードを \ref{vm_c_all} に示す。
+
+
+
 
 \lstinputlisting[label=vm_c_all, caption={\footnotesize Xv6 の vm.c}]{./src/vm_all.c}
-
-
-\lstinputlisting[label=vm_impl_private, caption={\footnotesize vm の実装の private}]{./src/vm_impl_private_all.cbc}
--- a/paper/summary.tex	Sat Feb 08 19:52:55 2020 +0900
+++ b/paper/summary.tex	Sun Feb 09 03:26:28 2020 +0900
@@ -1,5 +1,7 @@
 \chapter{まとめ}
 \section{今後の書き換え方針}
-本論文では、Paging 部分の書き換えの説明を行なった。今後 Xv6 全体の CbC による書き換えを行なっていく
-。
+OS 内部で CbCインターフェースを扱えるようになった。
+また、CMake を使った Linux 上で Arm のバイナリを吐けるように Cross Compile を行えるようになった。
+今後 Xv6 全体の CbC による書き換えを行なっていく。
 
+
Binary file slide/fig/Memoryconstitution.pdf has changed
Binary file slide/fig/Memoryconstitution.png has changed