--- a/paper/chapter/abstract.tex	Thu Feb 04 16:33:44 2021 +0900
+++ b/paper/chapter/abstract.tex	Thu Feb 04 16:59:59 2021 +0900
@@ -8,13 +8,23 @@
 証明を利用して信頼性を保証する定理証明は、 AgdaやCoqなどの定理証明支援系を利用することになる。
 支援系を利用する場合、各支援系でOSを実装しなければならない。
 証明そのものは可能であるが、 支援系で証明されたソースコードがそのままOSとして動作する訳ではない。
-証明されたコードと、実際に動作するOSを記述するC言語などのプログラミング言語の間にはギャップが存在する。
-Cでの実装時に入るバグは取り除けない。
 このためには定理証明されたコードを等価なC言語などに変換する処理系が必要となる。
 
 信頼性を保証するほかの方法として、プログラムの可能な実行をすべて数え上げて仕様を満たしているかを確認するモデル検査がある。
 モデル検査は実際に動作しているプログラムに対して実行することが可能である。
+すでに実装したプログラムのコードに変化を加えずモデル検査を行いたい。
 
+プログラムは本来やりたい計算であるノーマルレベルの計算と、その計算をするのに必要なメタレベルの計算に別けられる。
+メタレベルの計算では資源管理などを行うが、 モデル検査などの証明をメタレベルの計算で行いたい。
 
+この実現にはノーマルレベル、メタレベルの計算の処理の切り分けと、メタレベルの計算をより柔軟に扱うOS、言語処理系が必要となる。
+両レベルを記述できる言語にContinuation Based (CbC)がある。
+CbCはスタック、あるいは環境を持たず継続によって次の処理を行う特徴がある。
+CbCを用いて、拡張性と信頼性を両立するOSであるGearsOSを開発している。
+
+GearsOSの開発ではノーマルレベルのコードとメタレベルのコードの両方が必要であり、メタレベルの計算の数は多岐にわたる。
+GearsOSの開発を進めていくには、メタレベルの計算を柔軟に扱うAPIや、 自動でメタレベルの計算を作製するGearsOSのビルドシステムが必須となる。
+本研究ではGearsOSの信頼性と拡張性の保証につながる、メタ計算に関するAPIについて考察し、言語機能などの拡張を行った。
+また、メタ計算を自動生成しているトランスコンパイラを改良し、従来のGearsOSのシステムよりさらに柔軟性が高いものを考案した。
 \chapter*{Abstract}
 hogefuga

Binary file paper/master_paper.pdf has changed

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/queueStruct.h	Thu Feb 04 16:59:59 2021 +0900
@@ -0,0 +1,11 @@
+struct Queue {
+    union Data* queue;
+    union Data* data;
+    enum Code whenEmpty;
+    enum Code clear;
+    enum Code put;
+    enum Code take;
+    enum Code isEmpty;
+    enum Code next;
+} Queue;
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/queueTake.cbc	Thu Feb 04 16:59:59 2021 +0900
@@ -0,0 +1,5 @@
+__code odgCommitCUDAWorker3(struct CUDAWorker* worker, struct Context* task) {
+    int i = worker->loopCounter;
+    struct Queue* queue = GET_WAIT_LIST(task->data[task->odg+i]);
+    goto queue->take(odgCommitCUDAWorker4);
+}