# HG changeset patch # User e165723 # Date 1571758544 -32400 # Node ID da87ba72714ab334a85d2090453d4cf3fffc1bad # Parent 566ce65437eac5fcc9d1bc0df42ab5990e851b09 pre complete diff -r 566ce65437ea -r da87ba72714a midterm.pdf Binary file midterm.pdf has changed diff -r 566ce65437ea -r da87ba72714a midterm.tex --- a/midterm.tex Tue Oct 22 19:18:30 2019 +0900 +++ b/midterm.tex Wed Oct 23 00:35:44 2019 +0900 @@ -66,18 +66,18 @@ しかし現在は,Gears OSの研究においても様々な問題が存在するため前段階としてシンプルであるが基本的な機能を揃えた OS である xv6 を CbC で書き換えようとしている. CbCにはCodeGear,DataGearという処理の基本的な概念があり,これらを利用する事によってstackに値を積む事なくプロセス間を遷移することができる. -そのため,CbCのinterfaceを使うとモジュール化ができる.また, stackが無い事によってOS内部の明確化も実現できる. +そのため,CbCのInterfaceを使うとモジュール化ができる.また, stackが無い事によってOS内部の明確化も実現できる. %CbCを用いた Gears OSの研究を行なっている. %しかし, Gears OS を直接実機に実装することはできなかった為, 前段階としてシンプルであるが基本的な機能を揃えた OS である xv6 を CbC で書き換える. %形式手法 さらにCbC は 定理証明支援系 Agda に置き換えることができるように構築されている.Agdaを利用する事により,CbCの関数などが正常な動きをしているのかどうかを判断することが可能となる． %CbCのinterfaceを使うとモジュール化ができる.また, stackが無い事によってOS内部の明確化も実現できる. -これらのことを用い,CbCのinterfaceをxv6に搭載する事によりkernelの中の処理を明確にし, OSの信頼性を保証したい. -また,xv6のinterface実装によりモジュール化が可能とし,拡張性の実現を目指す. +これらのことを用い,CbCのInterfaceをxv6に搭載する事によりkernelの中の処理を明確にし, OSの信頼性を保証したい. +また,xv6のInterface実装によりモジュール化が可能とし,拡張性の実現を目指す. \section{xv6} -xv6とはMITのオペレーティングコースの教育目的で2006年に開発されたオペレーティングシステムである. +xv6\cite{xv6}とはMITのオペレーティングコースの教育目的で2006年に開発されたオペレーティングシステムである. xv6 はオリジナルである v6 が非常に古いC言語で書かれている為, ANSI-Cに書き換えられ x86 に再実装された. xv6 はreadやwriteなどのsystemcall,プロセス,仮想メモリ,カーネルとユーザーの分離,割り込み,ファイルシステムなどUnixの基本的な構造を持っている. \section{Continuation based C} @@ -90,7 +90,7 @@ またCbCにおけるCodeGear間の継続にはスタックが使用できず,呼び出し元の環境などを持たない為軽量継続と呼ぶ. 現在CbCはCコンパイラであるGCC及びLLVMをバックエンドとしたclang上で実装されている． -今回 ,このCbCに存在するinterfaceをxv6に実装していく. +今回 ,このCbCに存在するInterfaceをxv6に実装していく. @@ -124,14 +124,41 @@ %パルスさんの修論 %コンテキストには引数置き場所が書いてあるー＞CodeGear -\section{CbCのinterface} +\section{CbCのInterface} +CbCのInterface は Gears OS のモジュール化の仕組みである. Interface は呼び出しの引数になる Data Gear の集合であり，そこで呼び出される Code Gear のエントリである.呼び出される Code Gear の引数となる Data Gear はここで 全て定義される. Interface を定義することで複数の実装を持つことができる.このInterfaceは,JavaのInterfaceやHaskellの型クラスに対応している.%CbCを agdaに対応するために関数プログラミングスタイルで書く事によってInterfaceの検証も可能になる. + +以下の図2は,QueueのInterfaceとその実装によってモジュール化されたことを表している. + +\begin{figure}[ht] + \begin{center} + \includegraphics[width=65mm]{pic/gotoInterface.pdf} + \end{center} + \caption{図} + \label{fig:perl6buil} +\end{figure} \section{xv6のinterfaceのモジュール化} +CbCのCodeGear間の遷移時はstackに値を積むことがない.よってCbCのInterfaceを用いる事によってxv6のInterfaceを実装した際, OSの内部が明確化され信頼性を保証することができる. + +先行研究\cite{CbC}ではxv6のkernelの一部であるsyscallの部分をCbCによって書き換えされている.それを元にxv6のkernel部のどの部分Interfaceをし,実装するべきかを考察した.以下の図3では, syscallのさらに一部分であるsys\_readをInterfaceを用いて実装するとどうなるか考慮したものを簡潔に表した. +%\newpage +\begin{figure}[ht] + \begin{center} + \includegraphics[width=65mm]{pic/xv6_interface.pdf} + \end{center} + \caption{sys\_readのInterfaceとその実装の考案} + \label{fig:perl6buil} +\end{figure} + +xv6のkernel部がどのような動きをし,処理はどんな手順を踏むのかを考慮しながらxv6にInterfaceを実装していく. + %呼び出されたCodeGearの番号とcontext上のinterfaceの引数で状態が分かる． \section{今後の課題} -先行研究(参考文献[3])によって,xv6のkernelの一部をCbCの特徴でもある継続を用いモジュール化された. -しかし現在では, xv6にinterfaceはまだ搭載されていない.そのため今後, xv6のkernelをinterfaceを用いる事によってどのようにモジュール化できるか考察しながらCbCのinterfaceをxv6に実装していく必要がある. +先行研究\cite{CbC}によって,xv6のkernelの一部をCbCの特徴でもある継続を用いモジュール化された. +しかし現在では, xv6にinterfaceはまだ搭載されていない.そのため今後, xv6のkernelをinterfaceを用いる事によってどのようにモジュール化できるかInterfaceとその実装を考察しながらCbCのinterfaceをxv6に実装していく必要がある. +また,CbCのIntterfaceを利用しているためAgdaを用いて検証することが可能であるため,実装が正しい実装なのか検証することも求められる. + %\begin{thebibliography}{9} \nocite{*} diff -r 566ce65437ea -r da87ba72714a pic/gotoInterface.pdf Binary file pic/gotoInterface.pdf has changed diff -r 566ce65437ea -r da87ba72714a pic/xv6_interface.graffle Binary file pic/xv6_interface.graffle has changed diff -r 566ce65437ea -r da87ba72714a pic/xv6_interface.pdf Binary file pic/xv6_interface.pdf has changed diff -r 566ce65437ea -r da87ba72714a reference.bib --- a/reference.bib Tue Oct 22 19:18:30 2019 +0900 +++ b/reference.bib Wed Oct 23 00:35:44 2019 +0900 @@ -7,13 +7,57 @@ @article{GearsOS, author = "伊波立樹 and 河野真治", title = "Gears OS の並列処理", - journal = "琉球大学工学部情報工学科平成29年度学位論文(修士)", + journal = "琉球大学工学部情報工学科平成30年度学位論文(修士)", year = 2018 } @article{CbC, author = "宮城光希 and 河野真治", title = "継続を基本とした言語による OS のモジュール化", - journal = "琉球大学工学部情報工学科平成30年度学位論文(修士)", + journal = "琉球大学工学部情報工学科平成31年度学位論文(修士)", + year = 2019 +} + +@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{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}, +}