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
Binary file midterm.pdf has changed
--- 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);
+}