Mercurial > hg > Papers > 2019 > menikon-midterm
changeset 3:f0db7d006b4f
add hgignore
| author | e165723 <e165723@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 19 Oct 2019 14:48:19 +0900 |
| parents | 2e8286b5f43b |
| children | afaa3a0ba58d |
| files | .hgignore midterm.mm midterm.tex reference.bib |
| diffstat | 4 files changed, 81 insertions(+), 234 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/.hgignore Sat Oct 19 14:48:19 2019 +0900 @@ -0,0 +1,18 @@ +syntax: glob +.DS_Store +*.swp +*.*~ +*.bbl +*.blg +*.lof +*.lol +*.lot +*.log +*.aux +*.dvi +*.toc +*.cpt +*.swo +*.fls +*.fdb_latexmk +*.synctex.gz \ No newline at end of file
--- a/midterm.mm Thu Oct 17 13:35:43 2019 +0900 +++ b/midterm.mm Sat Oct 19 14:48:19 2019 +0900 @@ -1,18 +1,26 @@ <map version="1.0.1"> <!-- To view this file, download free mind mapping software FreeMind from http://freemind.sourceforge.net --> <node CREATED="1571206003053" ID="ID_30716385" MODIFIED="1571206261800" TEXT="中間予稿"> -<node CREATED="1571206022895" ID="ID_861305952" MODIFIED="1571206129134" POSITION="right" TEXT="ChristieをC#に書き換える意味"/> -<node CREATED="1571206030369" ID="ID_1086333248" MODIFIED="1571206061165" POSITION="left" TEXT="abstract"/> -<node CREATED="1571206034424" ID="ID_1553833030" MODIFIED="1571206147621" POSITION="right" TEXT="Christieとは"/> -<node CREATED="1571206036541" ID="ID_1443907136" MODIFIED="1571206075654" POSITION="left" TEXT="目的"/> -<node CREATED="1571206149784" ID="ID_518309532" MODIFIED="1571206158085" POSITION="right" TEXT="unityとは"/> -<node CREATED="1571206164777" ID="ID_1146942088" MODIFIED="1571206200536" POSITION="left" TEXT="使う機能やアプリケーションの説明"/> -<node CREATED="1571206204127" ID="ID_1463442815" MODIFIED="1571206236669" POSITION="right" TEXT="Christieの書き換え方針"/> -<node CREATED="1571206239975" ID="ID_1182948539" MODIFIED="1571206249598" POSITION="left" TEXT="実現方法"/> +<node CREATED="1571206022895" ID="ID_861305952" MODIFIED="1571287904550" POSITION="right" TEXT="何を目的としているか"> +<node CREATED="1571287939232" ID="ID_689518503" MODIFIED="1571388109335" TEXT=""/> +<node CREATED="1571288379453" ID="ID_142189159" MODIFIED="1571388110675" TEXT=""/> +<node CREATED="1571294882389" ID="ID_877460332" MODIFIED="1571388114009" TEXT=""/> +</node> +<node CREATED="1571206034424" FOLDED="true" ID="ID_1553833030" MODIFIED="1571419845442" POSITION="right" TEXT="CbCとは"> +<node CREATED="1571294955618" ID="ID_1164609171" MODIFIED="1571388108053" TEXT=""/> +</node> +<node CREATED="1571206036541" ID="ID_1443907136" MODIFIED="1571287473110" POSITION="left" TEXT="研究目的"/> +<node CREATED="1571206149784" FOLDED="true" ID="ID_518309532" MODIFIED="1571419831921" POSITION="right" TEXT="xv6とは"> +<node CREATED="1571294977300" ID="ID_1368331454" MODIFIED="1571388103875" TEXT=""/> +</node> +<node CREATED="1571419838480" ID="ID_673888818" MODIFIED="1571419838480" POSITION="right" TEXT=""/> +<node CREATED="1571206164777" ID="ID_1146942088" MODIFIED="1571388088605" POSITION="left" TEXT="CbC"/> +<node CREATED="1571206204127" ID="ID_1463442815" MODIFIED="1571388099036" POSITION="right" TEXT=""/> +<node CREATED="1571287531089" ID="ID_1810785110" MODIFIED="1571419786654" POSITION="left" TEXT="xv6"/> +<node CREATED="1571206239975" ID="ID_1182948539" MODIFIED="1571388095131" POSITION="left" TEXT=""/> <node CREATED="1571206264338" ID="ID_683827298" MODIFIED="1571206271309" POSITION="right" TEXT="今後の課題"/> <node CREATED="1571206272756" ID="ID_1391725770" MODIFIED="1571206279734" POSITION="left" TEXT="今後の課題"/> <node CREATED="1571206443722" ID="ID_1708136445" MODIFIED="1571206471264" POSITION="right" TEXT="参考文献"/> -<node CREATED="1571206473540" ID="ID_1993472279" MODIFIED="1571206473540" POSITION="right" TEXT=""/> <node CREATED="1571206453387" ID="ID_691575842" MODIFIED="1571206459566" POSITION="left" TEXT="参考文献"/> </node> </map>
--- a/midterm.tex Thu Oct 17 13:35:43 2019 +0900 +++ b/midterm.tex Sat Oct 19 14:48:19 2019 +0900 @@ -5,6 +5,9 @@ \usepackage{listings} \usepackage{caption} \usepackage{latexsym} +\usepackage{url} +\usepackage{abstract} +\usepackage{float} %\pagestyle{fancy} \lhead{\parpic{\includegraphics[height=1zw,keepaspectratio,bb=0 0 251 246]{pic/emblem-bitmap.pdf}}琉球大学主催 工学部情報工学科 中間発表予稿} @@ -21,70 +24,62 @@ \setlength{\footskip}{0mm} \pagestyle{empty} +\usepackage{comment} +\usepackage{listings} +\lstset{ + language=C, + tabsize=2, + frame=single, + basicstyle={\ttfamily\footnotesize}, % + identifierstyle={\footnotesize}, % + commentstyle={\footnotesize\itshape}, % + keywordstyle={\footnotesize\bfseries}, % + ndkeywordstyle={\footnotesize}, % + stringstyle={\footnotesize\ttfamily}, + breaklines=true, + captionpos=b, + columns=[l]{fullflexible}, % + xrightmargin=0zw, % + xleftmargin=1zw, % + aboveskip=1zw, + numberstyle={\scriptsize}, % + stepnumber=1, + numbersep=0.5zw, % + lineskip=-0.5ex, +} +\renewcommand{\lstlistingname}{Code} +\usepackage{caption} +\captionsetup[lstlisting]{font={small, tt}} + +\renewcommand{\abstractname}{概要} + \begin{document} -\title{継続を用いたxv6 kernelの書き換え} +\title{xv6 kernel上でのCbCによるinterfaceの実装\\CbC interface implementation in xv6 kernel} \author{学籍番号 : 165723C 氏名 : 坂本昂弘 {}{} 指導教員 : 河野真治} \date{} \maketitle \thispagestyle{fancy} -\section{xv6を継続で書き換える意味} -現代の OS では拡張性と信頼性を両立させることが要求されている． -信頼性をノーマルレベルの計算に対して保証し，拡張性をメタレベルの計算で実現することを目標に Gears OS を設計中である． - -Gears OS は Continuation based C (CbC)\cite{cbc} によってアプリケーションと OS そのものを記述する． -OS の下ではプログラムの記述は通常の処理の他に，メモリ管理，スレッドの待ち合わせやネットワークの管理， -エラーハンドリング等の記述しなければならない処理が存在する． -これらの計算をメタ計算と呼ぶ． -メタ計算を通常の計算から切り離して記述するために，Code Gear，Data Gear という単位を提案している． -CbC はこの Code Gear と Data Gear の単位でプログラムを記述する． -% OS は時代とともに複雑さが増し，OS の信頼性を保証することは難しい． - - -Code Gear は goto による継続で処理を表すことができる． -これにより，状態遷移による OS の記述が可能となり，複雑な OS のモデル検査を可能とする． -また，CbC は 定理証明支援系 Agda に置き換えることができるように構築されている． - -これらを用いて OS の信頼性を保証したい． -CbCの有効性を示すために，基本的な機能を揃えた OS である xv6 を CbC で書き換える. -これにより，OS の個々のシステムコールの持つ状態を明確にすることができると考えている. - -CbC でシステムやアプリケーションを記述するためには，Code Gear と Data Gear を柔軟に再利用する必要があり， -機能を接続するAPIと実装の分離が可能であることが望ましい． -CbC では形式化されたモジュールシステムが提供されている. -xv6 の CbC 書き換えでは, このモジュールシステムを用いる. - -書き換えはまだ部分的であるが, 既存の部分と両立するように設計されている. 従って, xv6 の基本的な -動作には変更はない. 実際に実行速度などはほとんど差がない. 逆に言えばオーバヘッドが存在しないことが確認できた. - +\section{研究目的} \section{Continuation based C} -CbC は処理を Code Gear という単位を用いて記述するプログラミ -ング言語である． Code Gear 間では軽量継続 (goto 文) による -遷移を行うので，継続前の Code Gear に戻 ることはない．この記述方法は -図1のように状態 -遷移ベースのプログラミングに適している． +xv6 kernel上でinterfaceを実装する際,当研究室で開発されたプログラミング言語Continuation based C (CbC)を用いる. +CbCは基本的な処理単位をCodeGearとして定義し，CodeGea間で遷移するようにプログラムを記述するC言語と互換性のあるプログラミング言語である. + +%\lstinputlisting[label=cbcexample, caption=cbc\_example.cbc]{src/cbc_example.cbc} -\begin{figure}[ht] - \begin{center} - \includegraphics[width=70mm]{pic/codesegment.pdf} - \end{center} - \caption{goto による code gear 間の継続} - \label{fig:cbc} -\end{figure} +\section{xv6} +xv6とはMITのオペレーティングコースの教育目的で2006年に開発されたオペレーティングシステムである. +\\xv6はシンプルでUnixに似た構造を持っている. -現在CbCはCコンパイラであるGCC\cite{gcc}及びLLVM\cite{llvm}をバックエンドとしたclang -% MicroCコンパイラ -上で実装されている．今回 xv6 のkernelの部分をこの CbC を 用いて書き換える． - -\section{section3} +\section{xv6のinterface} \section{今後の課題} %\begin{thebibliography}{9} \nocite{*} -%\bibliographystyle{ipsjunsrt} +\bibliographystyle{ipsjunsrt} \bibliography{reference} %\end{thebibliography}
--- a/reference.bib Thu Oct 17 13:35:43 2019 +0900 +++ b/reference.bib Sat Oct 19 14:48:19 2019 +0900 @@ -1,178 +1,4 @@ -@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}, +@misc{xv6, +title = "{Xv6, a simple Unix-like teaching operating system}", +howpublished = {https://pdos.csail.mit.edu/6.828/2019/xv6.html} } - -@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 をベースにした検証手法", - 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}, -} - -