# HG changeset patch # User e165723 # Date 1571813711 -32400 # Node ID 66ef03cf117b6a520f40500e3a60e90928a7d90d # Parent 1bd942aef137ae3850c260f28fc5fed218a3be98 fix diff -r 1bd942aef137 -r 66ef03cf117b midterm.pdf Binary file midterm.pdf has changed diff -r 1bd942aef137 -r 66ef03cf117b midterm.tex --- a/midterm.tex Wed Oct 23 15:12:04 2019 +0900 +++ b/midterm.tex Wed Oct 23 15:55:11 2019 +0900 @@ -65,7 +65,7 @@ 信頼性をノーマルレベルの計算に対して保 証し，拡張性をメタレベルの計算で実現することを目標にContinuation based C (CbC)を用いて Gears OS を設計中である. しかし現在は,Gears OSの研究においても様々な問題が存在するため前段階としてシンプルであるが基本的な機能を揃えた OS である xv6 を CbC で書き換えようとしている. -CbCにはCodeGear,DataGearという処理の基本的な概念があり,これらを利用する事によってstackに値を積む事なくプロセス間を遷移することができる. +CbCにはCodeGear,DataGearという処理の基本的な概念があり,これらを利用する事によってstackに値を積む事なくCodeGear間を遷移することができる. そのため,CbCのInterfaceを使うとモジュール化ができる.また, stackが無い事によってOS内部の明確化も実現できる. %CbCを用いた Gears OSの研究を行なっている. %しかし, Gears OS を直接実機に実装することはできなかった為, 前段階としてシンプルであるが基本的な機能を揃えた OS である xv6 を CbC で書き換える. @@ -125,9 +125,9 @@ %コンテキストには引数置き場所が書いてあるー＞CodeGear \section{CbCのInterface} -CbCのInterface は Gears OS のモジュール化の仕組みである. Interface は呼び出しの引数になる Data Gear の集合であり，そこで呼び出される Code Gear のエントリである.呼び出される Code Gear の引数となる Data Gear はここで 全て定義される. Interface を定義することで複数の実装を持つことができる.このInterfaceは,JavaのInterfaceやHaskellの型クラスに対応し,導入することでデータ構造を仕様と実装に分けて記述することが出来る.%CbCを agdaに対応するために関数プログラミングスタイルで書く事によって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とその実装によってモジュール化されたことを表している例である. +以下の図2は, QueueのInterfaceとSingleLinkedQueueの実装例である. %\lstinputlisting[label=cbcexample, caption=CodeGearの継続の例]{src/cbc_queue.cbc} @@ -135,13 +135,14 @@ \begin{center} \includegraphics[width=65mm]{pic/gotoInterface.pdf} \end{center} - \caption{QueueのInterfaceとその実装によるモジュール化} + \caption{QueueのInterfaceとSingleLinkedQueueの実装例} \label{fig:perl6buil} \end{figure} -\section{xv6のinterfaceのモジュール化} +\section{xv6のinterface} -CbCのCodeGear間の遷移時はstackに値を積むことがない.よってCbCのInterfaceを用いる事によってxv6のInterfaceを実装した際, OSの内部が明確化され信頼性を保証することができる. +%CbCのCodeGear間の遷移時はstackに値を積むことがない.よってCbCのInterfaceを用いる事によってxv6のInterfaceを実装した際, OSの内部が明確化され信頼性を保証することができる. +先述したCbCのInterfaceをxv6のInterfaceに実装する事によって仕様と実装を分けて記述できる. 先行研究\cite{CbC}ではxv6のkernelの一部であるsyscallの部分をCbCによって書き換えされている.それを元にxv6のkernel部のどの部分Interfaceをし,実装するべきかを考察した.以下の図3では, syscallのさらに一部分であるsys\_readをInterfaceを用いて実装するとどうなるか考慮したものを簡潔に表した. diff -r 1bd942aef137 -r 66ef03cf117b reference.bib --- a/reference.bib Wed Oct 23 15:12:04 2019 +0900 +++ b/reference.bib Wed Oct 23 15:55:11 2019 +0900 @@ -21,30 +21,12 @@ @article{ agda-ryokka, author = "Hokama MASATAKA and Shinji KONO", - title = "GearsOS の Hoare Logic をベースにした検証手法", + 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},