Mercurial > hg > Document > Growi

changeset 66:9e6952aef1e6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
backup 2021-05-25
author autobackup
date Tue, 25 May 2021 00:10:04 +0900
parents 937323467f4d
children a4f167def66b
files user/Itsuki/sigos2021.md
diffstat 1 files changed, 101 insertions(+), 37 deletions(-) [+]
line wrap: on
line diff
--- a/user/Itsuki/sigos2021.md	Mon May 24 00:10:04 2021 +0900
+++ b/user/Itsuki/sigos2021.md	Tue May 25 00:10:04 2021 +0900
@@ -9,39 +9,41 @@
 
 
 
-
 ## 研究概要
 - 当研究室ではOSの信頼性と拡張性の保証を目的としたGearsOSを開発している。
     - GearsOSは開発途上であり、実装が必要な機能が複数存在している。
 - GearsOSの分散ファイルシステムを開発したい。
 - 分散フレームワークChristieの構成をもとにGearsファイルシステムを構築する。
-
+- ファイルシステムの通信機構としてChristieが持つTopologyManagerという機能を使いたい。
 
 ## GearsOS概要
-- GearsOSの目的を説明したい。証明やモデル検査に適した構成にetc
-- メタとノーマルの分離など
-#
-- コンピュータの土台となるOSは高い信頼性が保証されている必要がある。
-- OSのコードや処理の量は膨大となる。
-    - したがって定理支援証明やモデル検査などの形式手法を用いて検証したい。
+- アプリケーションを動かすOSには高い信頼性が保証されている必要がある。
+- OSの処理やコードの量は膨大であり、テストコードを用いた信頼性の保証は困難であると言える。
+    - したがって数学的な背景に基づいた定理支援証明やモデル検査などの形式手法を用いて検証したい。
 - OSを形式手法にて証明するには状態遷移単位での記述が求められる。 
-- メタレベルとノーマルレベルの計算を分離して記述が行える。
+- メタレベルとノーマルレベルの計算を分離して記述が行える構成が必要となる。
     - メタレベルの計算でプログラムの整合性を検証する。
 
 ## Continuation based C(CbC)
 - CbCとは当研究室で開発しているC言語の下位言語である。
-- CbCは関数呼び出しでなく継続を導入している。
-    - スタック領域を用いずjmp命令でコード間を移動することにより軽量な継続を実現している。
-- 関数の代わりにCodeGearという単位でプログラムを行う
+- CbCは関数呼び出しでなくjmp命令で移動する継続を導入している。
+    - スタック領域を用いずjmp命令でコード間を移動することにより軽量な継続を実現している。これを軽量継続と呼ぶ。
+- CbCでは関数の代わりにCodeGearという単位でプログラムを行う
+    - CodeGearによる記述は形式手法に必要な状態遷移そのものとして見ることができる。
+- CbCではこの軽量継続を用いてfor 文などのループ文を実装する。
+
+
 
 ## Gearの概念
 - CodeGearはDataGearと呼ばれる変数データを入力として受け取り、その結果を別のDataGear に書き込む. 
-- 
+- CodeGearは従来のプログラムやスレッド、DataGearは変数データにあたる。
     - 入力のDataGearをInputDataGear、出力されるDataGearをOutputDataGearと呼ぶ。
     - CodeGearが参照できるDataGearはInput/output DataGearに限定される。
--  CbCではこの軽量継続を用いてfor 文などのループ文を実装する。
 - CodeGearは関数呼び出しのスタックを持たないため、一度CodeGearを遷移すると元の処理に戻ってくることができない。
 
+<center><img src="https://i.imgur.com/zCiaOrY.jpg" width="500px"></center>
+<center>
+
 ## CbC記述例
 - CbCを利用したシステムコール のディスパッチ部分を示す。
     - 特定のシステムコール の場合、CbCで実装された処理にgoto文を使って継続する。
@@ -54,7 +56,7 @@
     int num;
     int ret;
     if((num >= NELEM(syscalls)) && (num <= NELEM(cbccodes)) && 
-    cbccodes[num]) {
+        cbccodes[num]) {　　
     proc->cbc_arg.cbc_console_arg.num = num;
     goto (cbccodes[num])(cbc_ret); 
     }
@@ -68,6 +70,8 @@
 ## GearsOS
 - CbCを用いて記述された、CodeGearとその入出力であるDataGearを基本としたOSである。
 - 現在は並列フレームワークとして実装されており、実用的なOSのプロトタイプとして実装を目指している。
+- ノーマルレベルから見るとCodeGearの遷移は単純にCodeGearがDataGearをInput/Outputを繰り返し、コードブロックを移動するように見える。
+    - 実際にはCodeGearから別のCodeGearへの遷移にはデータ整合性の確認などのメタ計算が必要となる。 
 - 遷移する各CodeGearの実行に必要となるメタ計算は、MetaCodeGearと呼ばれるCodeGearごとに実装されたCodeGearで計算する。
     - MetaCodeGear内で参照されるDataGearをMetaDataGearと呼ぶ。
 - MetaCodeGearやMetaDataGearはプログラマが直接実行することはなく、現在はPerlスクリプトにより、GearsOSのビルド時に実行される。
@@ -77,10 +81,8 @@
 CodeGearから別のCodeGearへ遷移する際のDataGearなどの関係性
 </center>    
 
-- 実際には CodeGear の実行の前後に実行される MetaCodeGear や入出力の DataGear を MetaDataGear から取り出すなどのメタ計算が加わる。
-
 ## Context
-- 遷移先の CodeGear と MetaCodeGear の紐付けや、計算 に必要な DataGear を保存や管理を行う MetaDataGear と して context がある。
+- 遷移先の CodeGear と MetaCodeGear の紐付けや、計算 に必要な DataGear を保存や管理を行う MetaDataGearとして context がある。
     - 処理に必要なCodeGearの番号と MetaCodeGear の対応表や、DataGearの格納場所を持つ。
     - 計算に必要なデータ構造と処理を持つデータ構造であることから、contextは従来のOSのプロセスに相当するものと言える。
 
@@ -100,7 +102,7 @@
 
 ### CodeGear(以下CG)
 - プログラム(CG)内に記述された全てのDataGearのkeyにデータが格納されると動作し、DGを参照しながらプログラムを実行する。
-
+- CGMがsetupという処理を行うことで呼び出す。
 
 ### DataGear(以下DG)
 - keyと変数データの組み合わせで構成される。
@@ -111,8 +113,10 @@
 - CG,DG,DGMを管理する。
 - 分散処理のノードに相当するため、それぞれポートを持つ。
 - putという操作でDGを任意のCGMの持つDGMに格納する。
+    
+    
 ### DataGearManager(以下DGM)
-- 格CodeGearManagerが1つづつ所持している。
+- 各CodeGearManagerが1つづつ所持している。
 - データプールになっておりCGMが利用するDGを全て保持している。
 - LocalDGMとRemoteDGMの二種類存在する。(後述)
 
@@ -147,7 +151,7 @@
 public class HelloWorldCodeGear extends CodeGear {
 
     @Take //アノテーション
-    String hellokey;
+    String hellokey; //待ち合わせ&プログラム内で使用するDataGear
 
     @Override
     protected void run(CodeGearManager cgm) { //CGの処理内容
@@ -159,19 +163,19 @@
 
 
 #### LocalDGMとRemoteDGM
-- CGMはDGをputという操作を使って、自身や他ノードのDGMにDGを書き込ませる。
 - DGMにはLocalDGMとRemoteDGMが存在する。
-  - LocalDGMは各ノード固有のデータベースである。
+  - LocalDGMは各ノード固有のデータプールである。
   - RemoteDGMは他ノードのLocalDGMに対応するプールであり、接続しているノードの数だけ存在する。
-- DGMのput操作を行う際にはLocalとRemoteのどちらかを選ぶ.  
+- DGMのput操作を行う際にはLocalとRemoteのどちらかを選ぶ。  
   - Localであれば、LocalのCGMが管理するDGMに対しDGを格納。
-  - RemoteDGMを指定してputすることで、接続している任意のノードにDGを差し込ませることができる。
+  - RemoteDGMを指定してputすることで、接続している任意のノードにDGを送信することができる。
+- CGMの接続をする=接続先のRemoteDGMを作成すると言える。
 
 ![](https://i.imgur.com/BJNVkii.jpg)
 
 
 ## TopologyManager
-- 通信形成をより簡潔に行ってくれる機能である。
+- 通信形成を簡潔に行う機能である。
     - Topologyに参加を表明したノードを自動的に配線する。
     - 自動的に接続しているノードに相対的にラベルをつける。 
 - 静的Topology形成
@@ -180,23 +184,83 @@
 - 動的Topology形成
     - 参加を表明したノードに対し、動的にノード同士の関係を作る。
     - 例えばTreeを構成する場合、参加したノードから順にrootに近い役割を与える。  
-
-```Code
-digraph test {
-	node0 -> node1 [label="right"]
-	node1 -> node2 [label="right"]
-	node2 -> node0 [label="right"]
-}
-```
+- TopologyManagerを利用することで、ソケット接続などの処理を全てTopologyManagerに任せることができる。
 
 
+## GearsOSのファイルアクセスAPI
+- Christieの分散ファイルシステムのAPIをWordCount例題を通して構築する。
+    - WordCount例題とは指定したファイルの中身の文字列を読み取り、文字数と行列数、加えて文字列を出力すると言う例題である. 
+- WordCountのコードブロックは大きく分けて二つに分類できる。
+    - 指定した名前のファイルをFile構造体としてOpenするFileOpenスレッド
+    - ファイル構造体を受け取り、文字列を表示し、文字数と行列、CountUpをするWordCountスレッド
+- WordCountとファイルの接続はUNIXのシェルのようにプログラムの外で接続される。 
+    - この接続は将来的にChristieTopologyManagerで接続を行う。
 
-## GearsOSのファイルアクセス
+<center><img src="https://i.imgur.com/IFffeMq.jpg" width="600px"></center>
 
 ## ChristieAPI
+- GearsOS上のファイルは名前のついた大域的な資源であり, 複数のプロセスから競合的にアクセスされる。 
+- 上記のAPIではファイルとWordCountが直接的に結合されているので競合的なアクセスは起きない。 
+    - そこでChristieを基盤としたDataGearsStreamに名前をつけてアクセスするAPIを導入する。
 
-## FileSystem Implementation
+    
+<center><img src="https://i.imgur.com/K3nYFkh.jpg" width="600px"></center>
+<center>
+WordCountをRemoteDGMを用いて構成する際の遷移図
+</center>    
+    
+-  NodeAにて任意のファイルを開き、DGMを通して1行ごとに文字列をNodeBに送信する。NodeBにてWordCountの処理を行い、OutputとしてNodeBからWordCountの処理を送り返す。
+    
+
+- File Interfaceはファイル内文字列のBlockをWordCountに送信するが、RemoteDGMとして参照ができるWordCountの名前がついたDataGearManagerのploxyに書き込む。
+    
+- DGの受け取りはCodeGearの入力で行われるが、入力されたDGにkeyを設定するmetaCodeGearを使う。
+    - Christieのpushに相当する操作をmeta部分で実装する。
+    - 他のCodeGearがputしたDGに対応するCGがそのcontextで実行される。
+- 同じ名前を持つ(key)DGは複数のCGからアクセスされる。
+- FIleのeofなどはDGにフラグをつけ、関数型プログラミング的に処理される。
+- 
+
+##  FileSystem Implementation
+- GearsOS FileSystemは単なるDGのリストとなり、要求されたDGをリストから参照し、順次送信する形で構成される。
+- 持続的なファイルシステムはリストもしくはB-TreeをSSDなどのデバイスに格納する。    
+- メモリ領域において、CodeGearなどに使われた不要になった資源はメタレベルで回収を行う。
+- DGM自体がファイルの概念に対応すると言える。
+    - 別ノードからファイルを参照する際にはRemoteDGMを通してファイルの中身を送受信して管理する。
+    
+<center><img src="https://i.imgur.com/lcqdiSx.jpg" width="600px"></center>
+<center>
+ファイルを別ノード上から参照する際の遷移図
+</center>
+
+
+## File Persistency
+- 持続性のあるファイルとして保存されたDGMを操作するには、デバイス上に保存されたDGMをLocalDGMとして呼び出せば良い
+- 重複管理や変更履歴管理もDGMが行う。
+<center><img src="https://i.imgur.com/GWzj9qW.jpg " width="600px"></center>
+<center>
+<center>
+デバイス上に保存されたDGMを呼び出す際の遷移図
+</center>
+    
 
 ## 競合的アクセスを含む分散計算の検証
+- ChristieAPI は競合的なアクセスを含むので逐次型プログラミングのように検証することができない. 
+    - TopologyManagerは名前付きDataGearManagerを相互に接続するが、これも動的に変更される。
+- 可能な接続パターンとDGMの内容のパターンは膨大となるが、抽象化を用いることでより様々なレベルでの検証が期待できる。
+- 接続とDGMの内容のパターンが確定すればその範囲でプログラムは関数型プログラミングとして振る舞い、HoareLogicなどで検証が行える。
+    - 証明が複雑な場合でも, DG のパターンをメタ計算で調べるなどの手法を用いることができる.
 
-## 比較とまとめ
\ No newline at end of file
+## 比較
+- UNIX FileSystem は API的には File Stream と Socket Stream は Read-Writeでアクセスするがその設定はプログラム内部で煩雑な処理が必要となる。
+    - GearsOSではこの部分をTopologyManagerが担うため簡潔に行える。
+- UNIXではStreamに型がないので不完全なデータが生じてしまう。また、UNIXファイルシステムにはfsckと呼ばれる修復機能があるが、メモリに対する修復機能は存在しない。
+    - GearsOSではこれらはDGMのメタな機能として実装することができる。
+    - 例えばメモリの一部不良に対応するDGMを作るといったことが考えられる。？
+-  DGMの名前とその中のDataGear Streamに対応するkeyでアクセスする対象が決まる。 
+    -  これはUNIXでいうi-node番号に相当する。i-nodeの構成と名前空間の構成は独立で良いため自由な名前空間の構成が行える。
+
+## まとめ
+- GearsOS におけるファイルシステム API の設計に対して議論を行った
+- API は二種類あり、アプリケーションで閉じた決定的な実行を行う直接接続されたものと、もう一つはDataGearManagerに名前をつけて競合的アクセスを許す形でゆるく接続されるものである
+- DGMはファイルとして見ることもでき、分散環境での通信として見ることもできる。
\ No newline at end of file