changeset 10:cd9a64cadfc0

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 13 May 2023 18:30:07 +0900
parents 379c074e3f02
children 63d535445937
files presen.ind
diffstat 1 files changed, 73 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- 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
+
+