annotate user/ikkun/slide/2020.4.14.md @ 0:e12992dca4a0

init from Growi
author anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
date Wed, 16 Dec 2020 14:05:01 +0900
parents
children b6c284fd5ae4
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
0
e12992dca4a0 init from Growi
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 # Gears OSにおける multi threadにおけるプログラム検証
e12992dca4a0 init from Growi
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
e12992dca4a0 init from Growi
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 # 要約
e12992dca4a0 init from Growi
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 * CbC は処理の移行を goto 用いて行い、データ構造はdate gearにより保持する事でプログラムの処理をcode gear毎の独立したものにする。
e12992dca4a0 init from Growi
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 * Geas OS はCbCで記述されおり、処理を変更する事なく処理の間に自由にメタ処理を挟む事ができる、これにスケジューラーを挟む事でマルチスレッド処理などが可能となる。
e12992dca4a0 init from Growi
anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 * メタ計算部分にモデルチェッキングを入れる事でプログラムを実行しながらにして証明することが可能となる。