# Gears OSにおける multi threadにおけるプログラム検証

# 要約
* CbC は処理の移行を goto 用いて行い、データ構造はdate gearにより保持する事でプログラムの処理をcode gear毎の独立したものにする。
* Geas OS はCbCで記述されおり、処理を変更する事なく処理の間に自由にメタ処理を挟む事ができる、これにスケジューラーを挟む事でマルチスレッド処理などが可能となる。
* メタ計算部分にモデルチェッキングを入れる事でプログラムを実行しながらにして証明することが可能となる。