Mercurial > hg > Papers > 2021 > anatofuz-master

changeset 28:af160f988ac8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
from sigos
author anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
date Sat, 30 Jan 2021 22:42:58 +0900
parents dfd4bbbfdf60
children b37d6084d13d
files paper/chapter/introduction.tex paper/master_paper.pdf paper/reference.bib
diffstat 3 files changed, 204 insertions(+), 62 deletions(-) [+]
line wrap: on
line diff
--- a/paper/chapter/introduction.tex	Sat Jan 30 19:43:35 2021 +0900
+++ b/paper/chapter/introduction.tex	Sat Jan 30 22:42:58 2021 +0900
@@ -52,12 +52,13 @@
 証明を行う対象の計算は、 その意味が大きく別けられる。
 OSやプログラムの動作においては本来したい計算がまず存在する。
 これはプログラマが通常プログラミングするものである。
-それ以外にデータをメモリに保存するためにメモリのアロケーションをする処理や、メモリから値を持ってくる処理が入る。
-メモリのほかにCPUの資源管理なども必要となる。
+これら本来行いたい処理のほかに、 CPU、メモリ、スレッドなどの資源管理なども必要となる。
+前者の計算をノーマルレベルの計算と呼び、後者をメタレベルの計算と呼ぶ。
+OSはメタ計算を担当していると言える。
 ユーザーレベルから見ると、データの読み込みなどは資源へのアクセスが必要であるため、システムコールを呼ぶ必要がある。
 システムコール自体もメタ計算である。
-ユーザーが本来やりたい計算以外に、資源管理などのこれら計算を行う上でやらなければならない計算が存在する。
-前者の計算をノーマルレベルの計算と呼び、後者をメタレベルの計算と呼ぶ。
+実装のソースコードはノーマルレベルであり検証用のソースコードはメタ計算だと考えると、OSそのものが
+検証を行ない、システム全体の信頼を高める機能を持つべきだと考える。
 ノーマルレベルの計算を確実に行う為には、メタレベルの計算が重要となる。
 
 
@@ -68,4 +69,15 @@
 メタレベルの計算をノーマルレベルの計算と同等にプログラミングできると、動作するコードに対して様々なアプローチが掛けられる。
 この為にはノーマルレベル、メタレベル共にプログラミングできる言語と環境が必要となる。
 
-プログラムのノーマルレベルの計算とメタレベルの計算を一貫して行う言語として、 Continuation Based C(CbC)を用いる。
\ No newline at end of file
+プログラムのノーマルレベルの計算とメタレベルの計算を一貫して行う言語として、 Continuation Based C(CbC)を用いる。
+ノーマルレベルの計算とメタ計算の両方の実装に適した言語としてContinuation Based C(CbC)がある。
+CbCは基本\texttt{goto}で\texttt{CodeGaar}というコードの単位を遷移する言語である。通常の関数呼び出しと異なり、スタックあ>るいは環境と
+呼ばれる隠れた状態を持たない。このため、計算のための情報は\texttt{CodeGear}の入力にすべてそろっている。
+そのうちのいくつかはメタ計算、つまり、OSが管理する資源であり、その他はアプリケーションを実行するためのデータ(DataGear)で
+ある。
+メタ計算とノーマルレベルの区別は入力のどこを扱うかの差に帰着される。
+CbCはCと互換性のあるCの下位言語であり、 状態遷移をベースとした記述に適したプログラミング言語である。
+Cとの互換性のために、 CbCのプログラムをコンパイルすることで動作可能なバイナリに変換が可能である。
+CbCは\texttt{GCC}\cite{gcc}\cite{weko_82695_1}あるいは\texttt{LLVM}\cite{llvm}\cite{llvmcbc}上で実装されていて、通常のCのアプリケーションやシステムプログラ厶をそのまま包含できる。
+またCbCの基本文法は簡潔であるため、 Agdaなどの定理証明支援系\cite{agda-ryokka}との相互変換や、 CbC自体でのモデル検査が可
+能であると考えられる。
Binary file paper/master_paper.pdf has changed
--- a/paper/reference.bib	Sat Jan 30 19:43:35 2021 +0900
+++ b/paper/reference.bib	Sat Jan 30 22:42:58 2021 +0900
@@ -12,7 +12,7 @@
     title = {Babel},
     howpublished = {\url{https://babeljs.io/}},
 }
-@webpage{eclipse.jdt.pull322,
+@misc{eclipse,
     title = {Add unimplemented methods code action},
     author = {yaohaizh},
     organization = "GitHub",
@@ -20,7 +20,7 @@
     refdate = "2021-01-21",
 }
 
-@webpage{vscode-go,
+@misc{vscode-go,
     title = {golang/vscode-go},
     author = {golang},
     organization = "GitHub",
@@ -28,8 +28,20 @@
     refdate = "2021-01-21",
 }
 
+@misc{rpi,
+  title     = "{Raspberry Pi}",
+  howpublished    = {https://www.raspberrypi.org}
+}
+
+@misc{xv6rpi,
+author    = {Zhiyi Wang},
+title     = "{xv6-rpi}",
+howpublished      = "{\url{https://code.google.com/archive/p/xv6-rpi/}}",
+year      = {2013}
+}
+
 @article{
-    cbc,
+    llvmcbc,
     author = "Kaito TOKKMORI and Shinji KONO",
     title = "Implementing Continuation based language in LLVM and Clang",
     journal = "LOLA 2015",
@@ -37,7 +49,178 @@
     year = 2015
 }
 
-@article{moggi-monad,
+
+@misc{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},
+ doi = {10.1145/1806596.1806610},
+ acmid = {1806610},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ keywords = {operating system, run-time system, type safety, verification},
+}
+
+@misc{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},
+ doi = {10.1145/1629575.1629596},
+ acmid = {1629596},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ keywords = {isabelle/hol, l4, microkernel, sel4},
+}
+
+@article{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},
+ 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
+}
+
+@article{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},
+ 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 ="{\url{http://gcc.gnu.org/onlinedocs/gccint/}}",
+}
+
+@article{weko_195888_1,
+   author	 = "坂本 昂弘 and 桃原 優 and 河野 真治",
+   title	 = "継続を用いたx.v6 kernelの書き換え",
+   year 	 = "2019",
+   institution	 = "琉球大学工学部情報工学科, 琉球大学大学院理工学研究科情報工学専攻, 琉球大学工学部情報工学科",
+   journal = "情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)",
+   number	 = "4",
+   month	 = "may"
+}
+
+@article{weko_82695_1,
+   author	 = "大城 信康 and 河野 真治",
+   title	 = "ContinuationbasedCのGCC4.6上の実装について",
+   journal = "第53回プログラミング・シンポジウム予稿集",
+   year 	 = "2012",
+   volume	 = "2012",
+   number	 = "",
+   pages	 = "69--78",
+   month	 = "jan"
+}
+
+
+
+@article{
+    gears,
+    author = "河野 真治 and 伊波 立樹 and  東恩納 琢偉",
+    title = "Code Gear、Data Gear に基づく OS のプロトタイプ",
+    journal = "情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)",
+    month = "May",
+    year = 2016
+}
+
+@misc{xv6,
+author     = "{Russ Cox, Frans Kaashoek, Robert Morris}",
+title    = {xv6 a simple, Unix-like teaching operating system},
+howpublished   = {\url{https://pdos.csail.mit.edu/6.828/2018/xv6/book-rev11.pdf}},
+}
+
+
+@article{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},
+ doi = {10.1145/2815400.2815402},
+ acmid = {2815402},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+}
+
+@book{lions1996lions,
+  title={Lions' Commentary on UNIX 6th Edition with Source Code},
+  author={Lions, J.},
+  isbn={9781573980135},
+  lccn={55015401},
+  series={Computer classics revisited},
+  url={https://books.google.co.jp/books?id=OlZ3QgAACAAJ},
+  year={1996},
+  publisher={Peer-to-Peer Communications}
+}
+
+
+
+
+@misc{moggi-monad,
     author     = {Moggi, Eugenio},
     title      = {Notions of Computation and Monads},
     journal    = {Inf. Comput.},
@@ -49,62 +232,9 @@
     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},
-}
-