changeset 48:7bd5cef51b21

fix
author mir3636
date Fri, 13 Apr 2018 17:37:25 +0900
parents 11d5e2237571
children 06a21764be00
files Paper/sigos.bib Paper/sigos.pdf Paper/sigos.tex
diffstat 3 files changed, 169 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/sigos.bib	Fri Apr 13 17:37:25 2018 +0900
@@ -0,0 +1,168 @@
+@article{
+    gears,
+    author = "河野 真治 and 伊波 立樹 and  東恩納 琢偉",
+    title = "Code Gear、Data Gear に基づく OS のプロトタイプ",
+    journal = "情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)",
+    month = "May",
+    year = 2016
+}
+
+@article{
+    cbc,
+    author = "Kaito TOKKMORI and Shinji KONO",
+    title = "Implementing Continuation based language in LLVM and Clang",
+    journal = "LOLA 2015",
+    month = "July",
+    year = 2015
+}
+
+@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}
+}
+
+
+@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},
+} 
+
+@inproceedings{Nelson:2017:HPV:3132747.3132748,
+ 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},
+ booktitle = {Proceedings of the 26th Symposium on Operating Systems Principles},
+ series = {SOSP '17},
+ year = {2017},
+ isbn = {978-1-4503-5085-3},
+ location = {Shanghai, China},
+ pages = {252--269},
+ numpages = {18},
+ url = {http://doi.acm.org/10.1145/3132747.3132748},
+ doi = {10.1145/3132747.3132748},
+ acmid = {3132748},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+} 
+
+
+
+@inproceedings{Gu:2016:CEA:3026877.3026928,
+ author = {Gu, Ronghui and Shao, Zhong and Chen, Hao and Wu, Xiongnan and Kim, Jieung and Sj\"{o}berg, Vilhelm and Costanzo, David},
+ title = {CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels},
+ 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 = {653--669},
+ numpages = {17},
+ url = {http://dl.acm.org/citation.cfm?id=3026877.3026928},
+ acmid = {3026928},
+ publisher = {USENIX Association},
+ address = {Berkeley, CA, USA},
+} 
+
+@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},
+} 
+
+@article{Klein:2014:CFV:2584468.2560537,
+ author = {Klein, Gerwin and Andronick, June and Elphinstone, Kevin and Murray, Toby and Sewell, Thomas and Kolanski, Rafal and Heiser, Gernot},
+ title = {Comprehensive Formal Verification of an OS Microkernel},
+ journal = {ACM Trans. Comput. Syst.},
+ issue_date = {February 2014},
+ volume = {32},
+ number = {1},
+ month = feb,
+ year = {2014},
+ issn = {0734-2071},
+ pages = {2:1--2:70},
+ articleno = {2},
+ numpages = {70},
+ url = {http://doi.acm.org/10.1145/2560537},
+ doi = {10.1145/2560537},
+ acmid = {2560537},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ keywords = {Isabelle/HOL, L4, microkernel, operating systems, seL4},
+} 
+
+@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},
+} 
+
+@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{Moggi:1989:CLM:77350.77353,
+ author = {Moggi, E.},
+ title = {Computational Lambda-calculus and Monads},
+ booktitle = {Proceedings of the Fourth Annual Symposium on Logic in Computer Science},
+ year = {1989},
+ isbn = {0-8186-1954-6},
+ location = {Pacific Grove, California, USA},
+ pages = {14--23},
+ numpages = {10},
+ url = {http://dl.acm.org/citation.cfm?id=77350.77353},
+ acmid = {77353},
+ publisher = {IEEE Press},
+ address = {Piscataway, NJ, USA},
+}
+
Binary file Paper/sigos.pdf has changed
--- a/Paper/sigos.tex	Fri Apr 13 17:30:20 2018 +0900
+++ b/Paper/sigos.tex	Fri Apr 13 17:37:25 2018 +0900
@@ -162,7 +162,7 @@
 Haskell などの関数型プログラミング言語では実行環境が複雑であり、実行時の資源使用を明確にすることができない。
 CbC はスタック上に隠された環境を持たないので、メタレベルで使用する資源を明確にできるという利点がある。
 ただし、Gear のプログラミングスタイルは、従来の関数呼出を中心としたものとはかなり異なる。
-本研究では、Gears の記述をモジュールかするためにインターフェースを導入した。
+本研究では、Gears の記述をモジュール化するためにインターフェースを導入した。
 これにより、見通しの良いプログラミングが可能になった。
 
 \section{メタ計算の重要性}
@@ -390,7 +390,6 @@
 CAS は値の比較、更新をアトミックに行う命令である。
 CAS を使う際は更新前の値と更新後の値を渡し、渡された更新前の値を実際に保存されているメモリ番地の値と比較し、同じならデータ競合がないため、データの更新に成功する。
 異なる場合は他に書き込みがあったとみなされ、値の更新に失敗する。
-%CAS のコード
 
 Gears OS ではこの CAS を行うための Interface を定義している(Code\ref{atomicInterface})。
 この Interface では、Data Gear 全てを内包している Data 共用体のポインタの値を更新する CAS を定義して