Binary file paper/anatofuz_prosym_2019.pdf has changed

--- a/paper/anatofuz_prosym_2019.tex	Thu Nov 21 12:51:22 2019 +0900
+++ b/paper/anatofuz_prosym_2019.tex	Thu Nov 21 21:32:26 2019 +0900
@@ -63,13 +63,23 @@
 コンピュータ上で動作するあらゆるソフトウェアや資源を管理するOSは、 高い信頼性が保証されてほしい。
 信頼性の保証にはテストプログラムを用いた検証や、 形式手法を用いた証明を使う手法が存在する。
 頻繁に並列処理を行うOSでは、 スレッド間の共通資源の競合などの非決定的な実行を行う。
-OSの信頼性を保証する上ではテストやデバッグを用いる手法では、 発生しうる状態を完全に保証するのは困難である。
+このため、 OSの信頼性を保証する上で、 テストやデバッグを用いる手法では、 発生しうる状態を完全に保証するのは困難である。
 テストを用いる方法ではなく、 形式手法的なアプローチを用いてOSの信頼性を保証したい。
 そのためには定理証明支援系などで証明が可能な形式と、 等価な形式でOSを記述する必要性がある。
 現在開発しているGearsOSは、 継続を基本とする言語Conitinuation Based C(CbC)で実装されている。
 CbCは状態遷移単位での実行であり、 他の状態に遷移する際に今までの環境を持たない。
 そのため、 CbCで実装した処理は入出力が明確化され、 定理証明支援系で表現可能な形式にする事が可能である。
 
+\section{GearsOSのクロスコンパイル}
+GearsOSはRaspberryPi上での動作を目指している。
+RaspberryPiはARMのCPUが搭載されている為、 動作にはARMのバイナリファイルが必要となる。
+しかしRaspberryPiを利用してGearsOS自身のビルドを行うと、 マシンパワーからビルドに莫大な時間が掛かってしまう。
+従って資源が潤沢な別のマシンでARMのバイナリをビルドするのが望ましい。
+MacBookなどの資源が潤沢なはx84マシンが多く、x86マシン上からARMバイナリのCbCのクロスコンパイラを構成する必要がある。
+GCC上に実装しているCbCコンパイラは、 ARMを出力するように再構築する必要があった。
+他方LLVM/clang上に実装しているCbCコンパイラは、 ARMのライブラリは必要であるものの、 本体を再度ビルドすることなくクロスコンパイラとして利用可能である。
+今回はRaspberryPiのデフォルトOSであるRaspbianから、 ARMのライブラリをx86マシン上に転送し、 LLVM/clang上に実装したCbCコンパイラを用いてビルドした。
+
 
 \nocite{*}
 \bibliographystyle{ipsjsort}