--- a/code-mangement.ind	Sat Apr 15 16:30:15 2023 +0900
+++ b/code-mangement.ind	Mon Apr 17 13:26:48 2023 +0900
@@ -94,6 +94,66 @@
 この大域のcodeGear DBは、kernelを含めたすべてのcodeGearに対するもので全部で共有される。つまり、
 あらゆるversionを含む共有ライブラリとなる。これは全世界でuniqueなDBとしても良い。
 
+--CbCのcodeGear と GearsAgdaの違い
+
+CbCのcodeGearとdataGearは、普通のCの関数と構造体であり、その意味で不思議なところはない。しかし、
+normal levelではpointerが出てこないのが望ましい。なぜなら、メモリ配置は meta levelの問題で
+プログラムの正しさとは直接関係しないからである。つまり、normal levelでの構造体は List や 木
+など以外の再帰的構造でも直接的なポインタ操作は行わない。meta levelでは、メモリの直接操作
+例えば mallocやfree、あるいは共有データの扱いなどをポインタを通して行う。
+
+meta levelでのポインタ操作は、データ構造に対する操作であり、そのlevelに閉じる限り、
+プログラムの正しさはポインタの実装に依存しない。その意味で、meta codeGear も単なる
+noraml level のcodeGear に過ぎない。meta codeGearの証明あるいは、実装をさらにmeta level
+で行うこともできる。
+
+GearsAgda では、すべてはAgdaの構造体で表現される。これらは変数と項であり、基本的に複製可能
+な項である。その意味で、ポインタを持たないと言ってよい。Listや木の実装を配列と番号で行う
+ことはまったく実用的ではないので、普通に再帰的なデータ構造を使ってよい。ただし、それを
+自分自身の codeGear の再帰呼び出しで行うと、codeGearの実行が有界な時間に閉じなくなる。
+なので、loop は軽量継続を用いて、一旦、外にでることになる。これは、この段階でmeta level的に処理が
+割り込まれることも意味している。
+
+GearsAgda で処理された項は、ContextのdataGearに格納される。また、GearsAgdaのcodeGearは、
+Contextのcode tableに格納される。どちらも、メモリ的には番号で管理されることになる。
+GearsAgda の Context は、その意味で、プロセスのメモリ空間そのものを抽象化したものになっている。
+
+
+つまり、CbCのcodeGearと GearsAgdaは、normal level ではポインタを使わないのだが、
+その意味は、CbCと GearsAgda で若干異なる。CbCでの実装は、GearsAgdaでの実装の持つ
+性質を保存する必要がある。
+
+--Contextを通した dataGearとcodeGearの連携
+
+Gears OSでは、Context はCの構造体であり、一つのContextで使用するdataGearとcodeGearは、そこに格納される。
+複数のContextから、dataGearもcodeGearも共有されることがある。その排他制御は、Gears OSのmeta codeGearに
+よって行われる。
+
+Gears OSは、interfaceという構造体でオブジェクト表現していて、これらには、メソッドを格納する配列がある。
+この配列の添字を他のinterfaceが使用する。なので、interface間の呼び出しは、interfaceを表すdataGearと
+そのメソッドの番号で決定される。
+
+引数は、interface毎に Contextに決まった場所が確保される。これは、通常ではstack上に場所を確保する。
+しかし、CbCでは関数呼び出しはstackを使わないので、このようにする必要がある。これは、もちろん、
+マルチスレッドな実行では破壊されるおそれがあるが、Contextはシングルスレッドで実行することになっている
+ので問題ない。
+
+Contextの切り替えは、codeGearの境目で行われるので、Contextと実行しているcodeGearのcode tableの番号で
+状態が決定する。つまり、Gears OSでは、Task Switchにはレジスタは関係しない。割り込みなどは、codeGearの
+境界と独立に起きるが、それをmeta codeGearが境界で Context switchが起きたのと同じようにすることを
+保証する。これは一種の遅延処理となる。もちろん、影響がないなら、割り込み中にmetaな処理を行ってもよい。
+これは、本来はCPUなどのハードウェアでサポートされるべきかもしれない。
+
+dataGearは、metaな情報として、dataGearの構造定義を番号として持っている。これを使うことにより
+任意のdataGearの表示を正しく行うことができる。この情報を取り扱うことは meta level からでしか
+許されないが、CbC的には特に制限はない。
+
+引数として呼び出される dataGearは、Context上に前もって確保されているが、実行時にallocateされる
+dataGearもContextから参照される pool に確保される。これの管理は meta dataGear (Gears OSのkernel)
+が行う。GearsAgda は、この部分はAgdaが管理するので meta的な管理は行われない。しかし、
+Context を用いた並行実行の場合は、Context上での管理の問題が生じる。
+
+
 --codeGearのlinkage
 
 Gears OSのあらゆるコードは、codeGear DBのコードの組み合わせになる。しかし、そのためには、
@@ -136,6 +196,18 @@
 
 このContext内での offsetと呼び出すcodeGearの番号が一致すれば、Kernel側で整合性の問題はない。
 
+--codeGearのコンパイル方法
+
+現在の Gears OSのcodeGearは、interfaceを含む記述を .cbc に書き、それを CbC に変換している。
+この時に、meta codeGear として stub そして、meta dataGearとして Context の定義が生成される。
+
+Context の定義は Application 毎に異なっているが、全部をそろえることも可能である。この変換は
+Perl script で記述されていて、煩雑になっている。これを codeGear / interface 単位で .o と
+meta dataGearにできれば、全体の構成と、interfaceのコンパイルが簡単になると期待される。
+
+ただし、この場合は、Context の中での引数領域のoffset管理、code tableの初期化、code間の
+遷移を扱う codeGearの番号の指定の書き換えなどが必要となる。
+
 --static linkage
 
 コンパイル時に codeGearの結合が明らかならば、それは一つのcodeGearとしてまとめてよい。Contextへの書き込みもさぼることが
@@ -154,4 +226,14 @@
 
 codeGear DBを実装すれば、かなりの部分を後からロードすることが可能になる。
 
+
 --まとめ
+
+Gears OS と GearsAgda における codeGear の管理方法について考察した。将来的には GearsAgda で記述された
+証明付きinterfaceのコードを CbC に変換し、それを Gears OSで正しさを確認しながら組み合わせて、meta計算の
+変更を可能にしながら実行するシステムを作りたい。
+
+
+
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/main.tex	Mon Apr 17 13:26:48 2023 +0900
@@ -0,0 +1,74 @@
+\documentclass[twocolumn]{article}
+\usepackage{luatexja}
+\usepackage{fontspec}
+\usepackage{graphicx}
+\usepackage{float}
+\restylefloat{figue}
+\pagestyle{empty}
+
+%\hoffset -1in \addtolength{\hoffset}{20mm}
+%\voffset -1in \addtolength{\voffset}{20mm}
+%\oddsidemargin 0mm
+\topmargin -4mm
+%\headheight 13pt
+%\headsep 15mm
+%\textheight 43\baselineskip \addtolength{\textheight}{\topskip}
+%\textwidth 160mm
+%\marginparsep 3mm
+%\marginparwidth 15mm
+%\footskip \headsep
+\input usepackage.tex
+\begin{document}
+\setmainfont{STIX Math}%
+\setmonofont{STIXGeneralBol}[
+  Scale=MatchLowercase
+] % or whatever font you prefer
+
+\ltjsetparameter{jacharrange={-3}}
+
+% \input tgrindfig.tex
+\bibliographystyle{plain} % for bibliography
+%
+\include{title}
+%\title{}
+% 英文のみのタイトルならば，\title{ ... } とする．
+
+\date{}
+
+% 所属ラベルの定義
+
+% 和文著者名
+\author{
+{河野真治} \\
+琉球大学工学部\\
+{Shinji KONO} \\
+Faculty of Engineering, University of the Ryukyus\\
+}
+
+\maketitle{}
+\thispagestyle{empty}
+\begin{abstract}
+\input{abstract}
+\input{abstract-e}
+\end{abstract}
+
+% {\em 概要 \vspace{0.5cm}}\
+%\begin{center}
+%{\Large
+%\include{title-e}\
+%\include{author-e}} % \hspace{0.7cm}
+%\end{center}
+
+% {     t \Large Abstract}\
+%\include{abstract-e}
+% \\
+% \hspace{0.5cm}
+
+%
+\input 0.tex
+%
+% \input reference.tex
+
+\bibliography{ref}
+\end{document}
+