Mercurial > hg > Papers > 2020 > anatofuz-sigos

changeset 31:29369644f3a9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
date Tue, 05 May 2020 14:41:53 +0900
parents 1a9af340ad4a
children 8113cc6ca01a
files paper/anatofuz-bib.bib paper/anatofuz-sigos.md paper/anatofuz-sigos.pdf paper/anatofuz-sigos.tex
diffstat 4 files changed, 228 insertions(+), 118 deletions(-) [+]
line wrap: on
line diff
--- a/paper/anatofuz-bib.bib	Tue May 05 11:50:58 2020 +0900
+++ b/paper/anatofuz-bib.bib	Tue May 05 14:41:53 2020 +0900
@@ -1,117 +1,209 @@
-@inbook{inbook1,
-	author =	"Knuth, D. E.",
-	title =		"Fundamental Algorithms",
-	series =	"Art of Computer Programming",
-	volume =	1,
-	chapter =	2,
-	pages =		"371--381",
-	publisher =	"Addison-Wesley",
-	address =	"Reading, Massachusetts",
-	edition =	"2nd",
-	year =		1973}
-
-@incollection{incollection1,
-	author =	"Schwartz, Aaaa Jjjj",
-	title =		"Subdividing B{\'e}zier Curves and Surfaces",
-	booktitle =	"Geometric Modeling: Algorithms and New Trends",
-	editor =	"Farin, G. E.",
-	publisher =	"SIAM",
-	address =	"Philadelphia",
-	pages =		"55--66",
-	year =		1987}
-
-@inproceedings{inproceedings1,
-	author =	"Baraff, D",
-	title =		"Curved Surfaces and Coherence for Non-penetrating
-			 Rigid Body Simulation",
-	booktitle =	"SIGGRAPH '90 Proceedings",
-	pages =		"19--28",
-	editor =	"Beach, R. J.",
-	address =	"Dallas, Texas",
-	organization =	"ACM",
-	publisher =	"Addison-Wesley",
-	year =		1990}
-
-@inproceedings{inproceedings2,
-	author =	"Hiroshi Nakashima and others",
-	title =		"OhHelp: A Scalable Domain-Decomposing Dynamic
-			 Load Balancing for Particle-in-Cell Simulations",
-	booktitle =	"Proc.\ Intl.\ Conf. Supercomputing",
-	year =		2009,
-	pages =		"90-99",
-	doi =		"http://doi.acm.org/10.1145/1542275.1542293"}
-
-@manual{manual1,
-	organization =	"Adobe Systems Inc.",
-	title =		"PostScript Language Reference Manual",
-	publisher =	"Addison-Wesley",
-	address =	"Reading, Massachusetts",
-	year =		1985}
-
-@mastersthesis{mastersthesis1,
-	author =	"山下 義行",
-	yomi =		"Yamashita, Y",
-	title =		"文脈自由文法への否定の導入",
-	school =	"筑波大学大学院工学研究科",
-	year =		1989}
-
-
-@phdthesis{phdthesis1,
-	author =	"Weihl, W.",
-	title =		"Specification and Implementation of
-			 Atomic Data Types",
-	school =	"MIT",
-	address =	"Boston",
-	year =		1984}
-
-@proceedings{proceedings1,
-	title =		"Proc. Intl. Conf. on Fifth Generation Computer
-			 Systems",
-	organization =	"Institute for New Generation Computer Technology",
-	volume =	1,
-	year =		1992}
-
-@techreport{techreport1,
-	author =	"Ihsakat Aredon",
-	title =		"{\TeX} 独稽古",
-	type =		"Seminar on Mathematical Sciences",
-	number =	13,
-	institution =	"Department of Mathematics, Keio University",
-	address =	"Yokohama",
-	year =		1989}
-
-
-@webpage{webpage1,
-	author =	"情報処理学会",
-	title =		"コンピュータ博物館設立の提言",
-	organization =	"情報処理学会",
-	url =	"http://www.ipsj.or.jp/03somu/teigen/museum200702.html",
-	refdate =	"2007-02-05"}
-
-@webpage{webpage2,
-	author =	"情報処理学会論文誌編集委員会",
-	title =		"「情報処理学会論文誌（IPSJ Journal）」原稿執筆案内",
-	organization =	"情報処理学会",
-	url="http://www.ipsj.or.jp/08editt/journal/shippitsu/ronbunJ-prms.pdf",
-	refdate =	"2010-10-28"}
-
-@webpage{webpage3,
-	author =	"Alan Kay",
-	title =		"Welcome to Squeakland",
-	organization =	"Squeakland",
-	url =	"http://www.squeakland.org/community/biography/alanbio.html",
-	refdate =	"2007-04-05"}
-
-@webpage{webpage4,
-	author =	"Hiroshi Nakashima",
-	title =		"A {WEB} Page",
-	organization =	"Kyoto University",
-	url =	"http://www.para.media.kyoto-u.ac.jp/~nakashima/a.web.page.of.long.url/",
-	refdate =	"2010-10-30"}
-
-@webpage{webpage5,
-	author =	"Hiroshi Nakashima",
-	title =		"Another {WEB} Page",
-	organization =	"Kyoto University",
-	url =	"http://www.para.media.kyoto-u.ac.jp/~nakashima/a.web.page.of.much.longer.url/",
-	refdate =	"2010-10-30"}
+@article{os,
+    author = {Andrew S.Tanenbaum, Herbert Bos},
+    title = "{Modern Operating Systems}",
+    publisher = {PEASON},
+    year = {2015},
+}
+
+@misc{rpi,
+title     = "{Raspberry Pi — Teach, Learn, and Make with Raspberry Pi}",
+howpublished    = {https://www.raspberrypi.org}
+}
+
+@misc{xv6rpi,
+author    = {Zhiyi Wang},
+title     = "{xv6-rpi}",
+howpublished      = "{https://code.google.com/archive/p/xv6-rpi/}",
+year      = {2013}
+}
+
+@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{
+    hyperKernel,
+  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},
+  journal = {Proceedings of the 26th Symposium on Operating Systems Principles},
+    year = 2017
+}
+
+
+
+@article{
+    agda-ryokka,
+    author = "Hokama MASATAKA and Shinji KONO",
+    title = "GearsOS の Hoare Logic をベースにした検証手法",
+    journal = "ソフトウェアサイエンス研究会",
+    month = "Jan",
+    year = 2019
+}
+
+@inproceedings{agda,
+ author = {Norell, Ulf},
+ title = {Dependently Typed Programming in Agda},
+ booktitle = {Proceedings of the 4th International Workshop on Types in Language Design and Implementation},
+ series = {TLDI '09},
+ year = {2009},
+ isbn = {978-1-60558-420-1},
+ location = {Savannah, GA, USA},
+ pages = {1--2},
+ numpages = {2},
+ url = {http://doi.acm.org/10.1145/1481861.1481862},
+ doi = {10.1145/1481861.1481862},
+ acmid = {1481862},
+ publisher = {ACM},
+ 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/}",
+}
+
+@article{
+    gears,
+    author = "河野 真治 and 伊波 立樹 and  東恩納 琢偉",
+    title = "Code Gear、Data Gear に基づく OS のプロトタイプ",
+    journal = "情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)",
+    month = "May",
+    year = 2016
+}
+
+@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},
+}
+
+
+
+@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},
+}
+
+@techreport{weko_195888_1,
+   author	 = "坂本,昂弘 and 桃原,優 and 河野,真治",
+   title	 = "継続を用いたx.v6 kernelの書き換え",
+   year 	 = "2019",
+   institution	 = "琉球大学工学部情報工学科, 琉球大学大学院理工学研究科情報工学専攻, 琉球大学工学部情報工学科",
+   number	 = "4",
+   month	 = "may"
+}
+
+
+  
+
+
+
+
--- a/paper/anatofuz-sigos.md	Tue May 05 11:50:58 2020 +0900
+++ b/paper/anatofuz-sigos.md	Tue May 05 14:41:53 2020 +0900
@@ -194,4 +194,13 @@
 
     p->sz = PTE_SZ;
     memset(p->tf, 0, sizeof(*p->tf));
-```
\ No newline at end of file
+```
+
+
+# xv6の今後の再実装
+
+xv6ではカーネルパニックの発生時や、 inodeのキャッシュなどをグローバル変数として利用している。
+グローバル変数を使用してしまうと、 CodeGearで定義した状態がDataGear以外のグローバル変数によって変更されてしまう。
+グローバル変数を極力使わず継続を中心とした実装を行いたい。
+
+contextは現在プロセス構造体に埋め込まれており、　kernelそのものの状態を制御するためには各contextを管理する機能が必要であると考えられる。
Binary file paper/anatofuz-sigos.pdf has changed
--- a/paper/anatofuz-sigos.tex	Tue May 05 11:50:58 2020 +0900
+++ b/paper/anatofuz-sigos.tex	Tue May 05 14:41:53 2020 +0900
@@ -302,6 +302,15 @@
     memset(p->tf, 0, sizeof(*p->tf));
 \end{lstlisting}
 
+
+\section{xv6の今後の再実装}
+
+xv6ではカーネルパニックの発生時や、 inodeのキャッシュなどをグローバル変数として利用している。
+グローバル変数を使用してしまうと、 CodeGearで定義した状態がDataGear以外のグローバル変数によって変更されてしまう。
+グローバル変数を極力使わず継続を中心とした実装を行いたい。
+
+contextは現在プロセス構造体に埋め込まれており、　kernelそのものの状態を制御するためには各contextを管理する機能が必要であると考えられる。
+
 \nocite{*}
 \bibliographystyle{ipsjunsrt}
 \bibliography{anatofuz-bib}