--- a/.hgignore	Thu Nov 21 21:32:26 2019 +0900
+++ b/.hgignore	Thu Nov 28 12:28:08 2019 +0900
@@ -274,3 +274,103 @@
 *.glstex
 
 # End of https://www.gitignore.io/api/latex
+
+
+# Created by https://www.gitignore.io/api/node
+# Edit at https://www.gitignore.io/?templates=node
+
+### Node ###
+# Logs
+logs
+*.log
+npm-debug.log*
+yarn-debug.log*
+yarn-error.log*
+lerna-debug.log*
+
+# Diagnostic reports (https://nodejs.org/api/report.html)
+report.[0-9]*.[0-9]*.[0-9]*.[0-9]*.json
+
+# Runtime data
+pids
+*.pid
+*.seed
+*.pid.lock
+
+# Directory for instrumented libs generated by jscoverage/JSCover
+lib-cov
+
+# Coverage directory used by tools like istanbul
+coverage
+*.lcov
+
+# nyc test coverage
+.nyc_output
+
+# Grunt intermediate storage (https://gruntjs.com/creating-plugins#storing-task-files)
+.grunt
+
+# Bower dependency directory (https://bower.io/)
+bower_components
+
+# node-waf configuration
+.lock-wscript
+
+# Compiled binary addons (https://nodejs.org/api/addons.html)
+build/Release
+
+# Dependency directories
+node_modules/
+jspm_packages/
+
+# TypeScript v1 declaration files
+typings/
+
+# TypeScript cache
+*.tsbuildinfo
+
+# Optional npm cache directory
+.npm
+
+# Optional eslint cache
+.eslintcache
+
+# Optional REPL history
+.node_repl_history
+
+# Output of 'npm pack'
+*.tgz
+
+# Yarn Integrity file
+.yarn-integrity
+
+# dotenv environment variables file
+.env
+.env.test
+
+# parcel-bundler cache (https://parceljs.org/)
+.cache
+
+# next.js build output
+.next
+
+# nuxt.js build output
+.nuxt
+
+# react / gatsby 
+public/
+
+# vuepress build output
+.vuepress/dist
+
+# Serverless directories
+.serverless/
+
+# FuseBox cache
+.fusebox/
+
+# DynamoDB Local files
+.dynamodb/
+
+# End of https://www.gitignore.io/api/node
+

Binary file paper/anatofuz_prosym_2019.pdf has changed

--- a/paper/anatofuz_prosym_2019.tex	Thu Nov 21 21:32:26 2019 +0900
+++ b/paper/anatofuz_prosym_2019.tex	Thu Nov 28 12:28:08 2019 +0900
@@ -64,23 +64,64 @@
 信頼性の保証にはテストプログラムを用いた検証や、 形式手法を用いた証明を使う手法が存在する。
 頻繁に並列処理を行うOSでは、 スレッド間の共通資源の競合などの非決定的な実行を行う。
 このため、 OSの信頼性を保証する上で、 テストやデバッグを用いる手法では、 発生しうる状態を完全に保証するのは困難である。
+
 テストを用いる方法ではなく、 形式手法的なアプローチを用いてOSの信頼性を保証したい。
 そのためには定理証明支援系などで証明が可能な形式と、 等価な形式でOSを記述する必要性がある。
 現在開発しているGearsOSは、 継続を基本とする言語Conitinuation Based C(CbC)で実装されている。
 CbCは状態遷移単位での実行であり、 他の状態に遷移する際に今までの環境を持たない。
-そのため、 CbCで実装した処理は入出力が明確化され、 定理証明支援系で表現可能な形式にする事が可能である。
+CbCで実装した処理は入出力が明確化され、 定理証明支援系で表現可能な形式にする事が可能である。
+
+\section{Continuation Based C}
+Continuation Based C(CbC) とは GearsOSの記述に利用しているプログラミング言語である。
+C言語の下位言語として設計されており、CコンパイラであるGCC、 LLVM/Clang上に実装が存在する。
+CbCは通常の関数呼び出しとは異なり、 軽量継続を基本としている。
+通常Cの関数呼び出しでは、 スタックポインタを操作し、 ローカル変数や、 レジスタ情報をスタックに保存する。
+これらは通常アセンブラのcall命令として処理される。
+CbCの軽量継続は、 アセンブラレベルでは jmp で表現され、 スタックフレームを操作することなく次の状態に遷移する。
+CbCの状態はCodeGearと呼ばれる単位で記述される。
+
+\section{GersOSの基本単位}
+実行単位としてはCbCで導入されたCodeGearを用いる。
+CodeGearは関数よりも単位が小さく、 かつアセンブラよりも単位が大きく処理を記述することが可能である。
+そのため、 OSの必要な資源管理などのメタ計算を記述するのに適していると考えられる。
+
+GearsOSでは使われる情報を、 DataGearと呼ばれる単位で構成する。
+DataGearはCの構造体のように宣言するが、 すべてのDataGearはContextと呼ばれるデータ構造の中で、 共用体として管理されている。
+CodeGearでは入出力をDataGearで管理している。
+CodeGearの入力で使用されるDataGearを、 InputDataGearと呼び、 出力するDataGearをOutputDataGearと呼ぶ。
+この入出力の組を Task として定義し、 InputDataGearの依存関係が解決されたTaskから、 CodeGearが並列実行される。
+
+
+\section{GearsOSで記述されたxv6}
+GearsOSの機能であるContextなどを用いて、 実際に実機で動作するOSを作成したい。
+実機で動作するOSのベース実装として、 システムコールなどのシンプルなUNIXの機能を持つxv6に着目した。
+xv6はARMプロセッサを持つRaspberryPi上で動作する、 xv6\_rpiというバリエーションが存在する。
+GearsOSを実行で動作させるために、 xv6\_rpiのソースコードをGearsOSで一部再実装している。
+現在はxv6のプロセスである proc構造体に、 GearsOSのcontextを導入し、 GearsOSとしてもxv6としても解釈可能な形で開発している。
+
 
 \section{GearsOSのクロスコンパイル}
 GearsOSはRaspberryPi上での動作を目指している。
 RaspberryPiはARMのCPUが搭載されている為、 動作にはARMのバイナリファイルが必要となる。
-しかしRaspberryPiを利用してGearsOS自身のビルドを行うと、 マシンパワーからビルドに莫大な時間が掛かってしまう。
-従って資源が潤沢な別のマシンでARMのバイナリをビルドするのが望ましい。
-MacBookなどの資源が潤沢なはx84マシンが多く、x86マシン上からARMバイナリのCbCのクロスコンパイラを構成する必要がある。
-GCC上に実装しているCbCコンパイラは、 ARMを出力するように再構築する必要があった。
+しかしRaspberryPiを利用してGearsOS自身のビルドを行うと、 マシンパワーの問題でビルドに莫大な時間が掛かってしまう。
+著者らが使うことが多い、 資源が潤沢なx86マシンから、 ARMにクロスコンパイルする必要がある。
+GCC上に実装しているCbCコンパイラは、 ARMを出力するようにコンパイラを再構築する必要があった。
 他方LLVM/clang上に実装しているCbCコンパイラは、 ARMのライブラリは必要であるものの、 本体を再度ビルドすることなくクロスコンパイラとして利用可能である。
 今回はRaspberryPiのデフォルトOSであるRaspbianから、 ARMのライブラリをx86マシン上に転送し、 LLVM/clang上に実装したCbCコンパイラを用いてビルドした。
+ビルドツールとしてはCMakeを導入している。
+CMakeでクロスコンパイルを行うために、 補助的に一部Perlスクリプトで補完している。
 
 
+
+\section{今後の課題}
+現状はxv6をGearsOSとして書き直している段階であり、 システムコールで呼び出された後のkernel部分の処理を順次Interfaceとして実装している。
+RaspberryPi上で動作する様にクロスコンパイルをする環境はCMakeを利用して構築出来たので、 実際にRaspberryPi上でInterfaceを導入したGearsOSを動作させる必要がある。
+またxv6はUEFIでのブートが組み込まれていので、 これを実装したい。
+UEFIでブートが可能になると、 各種デバイスドライバを組み込むのが容易になる為、 USB3.0の規格であるxHCIなどをxv6上に実装することが可能となる。
+xHCIを実装する事によってxv6を実機で動かした際に、 USB接続をしたキーボードが使用可能となる。
+これらの実装には、 CbCで実装された実装としても使用可能な仕様記述言語を用いる予定である。
+また、 実際にxv6上での処理を定理証明支援系などで証明を行い、 証明しやすい実装と、 処理に適した実装にInterfaceを通して切り替える機構を実装することも課題である。
+
 \nocite{*}
 \bibliographystyle{ipsjsort}
 \bibliography{reference}

--- a/paper/reference.bib	Thu Nov 21 21:32:26 2019 +0900
+++ b/paper/reference.bib	Thu Nov 28 12:28:08 2019 +0900
@@ -15,14 +15,6 @@
     refdate = "2018-11-21",
 }
 
-@webpage{cbcllvm,
-    title = {CbC\_llvm},
-    author = {並列信頼研究室},
-    organization = "琉球大学",
-    url = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC_llvm/}},
-    refdate = "2018-11-21",
-}
-
 
 @techreport{gearsos,
    author	 = "宮城,光希 and 桃原,優 and 河野,真治",