Mercurial > hg > Papers > 2019 > menikon-midterm
changeset 16:1bd942aef137
fix
author | e165723 <e165723@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 23 Oct 2019 15:12:04 +0900 |
parents | a5ac9d556fda |
children | 66ef03cf117b |
files | midterm.pdf midterm.tex src/cbc_queue.cbc |
diffstat | 3 files changed, 22 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/midterm.tex Wed Oct 23 00:49:43 2019 +0900 +++ b/midterm.tex Wed Oct 23 15:12:04 2019 +0900 @@ -125,9 +125,11 @@ %コンテキストには引数置き場所が書いてあるー>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とその実装によってモジュール化されたことを表している例である. + +%\lstinputlisting[label=cbcexample, caption=CodeGearの継続の例]{src/cbc_queue.cbc} \begin{figure}[ht] \begin{center} @@ -142,6 +144,7 @@ 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}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/cbc_queue.cbc Wed Oct 23 15:12:04 2019 +0900 @@ -0,0 +1,17 @@ +__code code1(struct Context *context) { + Queue* queue = createSingleLinkedQueue(context); + Node* node = &ALLOCATE(context, Node)->Node; + node->color = Red; + Gearef(context, Queue)->queue = (union Data*) queue; + Gearef(context, Queue)->data = (union Data*) node; + Gearef(context, Queue)->next = C_queueTest2; + goto meta(context, queue->put); +}__code code1(struct Context *context) { + Queue* queue = createSingleLinkedQueue(context); + Node* node = &ALLOCATE(context, Node)->Node; + node->color = Red; + Gearef(context, Queue)->queue = (union Data*) queue; + Gearef(context, Queue)->data = (union Data*) node; + Gearef(context, Queue)->next = C_queueTest2; + goto meta(context, queue->put); +}