# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1683970207 -32400
# Node ID cd9a64cadfc0c1069abf9ee2dbaf0652c7475cde
# Parent  379c074e3f0262a29dc9775ae2a27469b5bf58f4
...

diff -r 379c074e3f02 -r cd9a64cadfc0 presen.ind
--- a/presen.ind	Fri May 12 19:59:07 2023 +0900
+++ b/presen.ind	Sat May 13 18:30:07 2023 +0900
@@ -1,4 +1,76 @@
 -title: Gears OSの CodeGear Management
 
--author:  仲吉菜々子, 河野真治  
+-author:  仲吉菜々子, 河野真治  \n 琉球大学工学部
+
+--3種類のGears OS 
+
+  Gears OS   CbCで書かれた TaskManager
+  GearsAgda  Agda で書いた証明付きの Gears OS
+  x.v6 Gears  Raspi 上で動く Gears OS
+
+--Gears OS の実装
+
+  single a.out
+  no code loading
+  all startic linked
+  converting .cbc to .c
+
+  context (process を表す dataGear )
+
+--CbC の interface 記述からの変換
+
+CbC は stack がない
+
+引数は Context 上のcodeGear の interface に書き込む
+
+context は single thread なので問題ない
+
+stack を自前で持つのは問題ない 
+
+関数呼び出しが禁止されているわけじゃない
+
+--CbC の interface 記述からの変換
+
+つまり Context から引数を取り出す部分
+
+次の継続の引数を Context に書き込む部分 stub がある
+
+stab は番号付けられていて Context の code table に格納される
 
+goto meta で番号で行き先を指定する
+
+--システム全体の信頼性には code をOSが管理するべき
+
+code pool があって、正しい組み合わせだけが許される
+
+実際に簡易な Model 検査を走らせても良い (Coverageのみとか)
+
+code の組み合わせの記述は例えば Ruby の Gemfile のようなもの
+
+ちゃんと動くかどうかの検証は外部で行う
+
+--codeGear の dynamic loading
+
+stub は Context 上の interface を読み書きする
+
+それがつじつまがあっていれば表に登録するだけで良い
+
+Context 上の interface の位置はシステム内では codeGear load 時に決まる
+
+   つまり link は簡単
+
+--static linking
+
+現在の Gears OS は全部いっぺんに compile されるので、実際の Context への書き込みは起きない
+
+コンパイラが無駄なコードを削除してしまう
+
+しかし、dynamic loading では、それはできない
+
+前もって複数のcodeをまとめてコンパイルすることで余計な書き込みを避けられる
+
+--validity
+
+--x.v6 implementatiion
+
+