Mercurial > hg > Papers > 2022 > ikki-master

changeset 33:ab77a291294d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tweak finalSlide
author ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
date Sat, 12 Feb 2022 21:43:10 +0900
parents fa31358d38f1
children 181eec546ad2
files finalSlide/finalSlide.html finalSlide/finalSlide.md finalSlide/finalSlide.pdf.html
diffstat 3 files changed, 285 insertions(+), 76 deletions(-) [+]
line wrap: on
line diff
--- a/finalSlide/finalSlide.html	Sat Feb 12 19:59:58 2022 +0900
+++ b/finalSlide/finalSlide.html	Sat Feb 12 21:43:10 2022 +0900
@@ -95,11 +95,12 @@
 <ul>
   <li>GearsOSの分散ファイルシステムの設計と実装を行った
     <ul>
+      <li>ファイル構造の設計</li>
       <li>APIの定義</li>
-      <li>ファイル構造の設計</li>
-      <li>遠隔のファイルへのアクセス</li>
+      <li>遠隔のファイルのアクセスと保存</li>
     </ul>
   </li>
+  <li>GearsOS同様の記述単位な構成</li>
   <li>自律分散を目指した分散ファイルシステムの設計</li>
   <li>OSレベルのTransactionによるアプリ実装</li>
 </ul>
@@ -112,17 +113,11 @@
   <!-- _S9SLIDE_ -->
 <h2 id="gearsos">GearsOS</h2>
 <ul>
-  <li><strong>CodeGear</strong>と<strong>DataGear</strong>という単位を用いるOS開発プロジェクト</li>
-  <li>開発途上段階となる</li>
-  <li>OSの信頼性の向上と拡張性を目指している
+  <li>CodeGear/DataGearという単位で記述されるOS</li>
+  <li>OSの信頼性の保証と拡張性を目指している</li>
+  <li>ノーマルレベルとメタレベルを分離して記述できる
     <ul>
-      <li>OSのプログラムは膨大な量となり、検証は困難である</li>
-    </ul>
-  </li>
-  <li>ユーザーが実装したプログラムをメタレベルから検証する
-    <ul>
-      <li>ノーマルレベルとメタレベルを分離して記述できる</li>
-      <li>メタレベル処理を検証用へ切り替えられる</li>
+      <li>ユーザーが実装したプログラムをメタレベルから検証する</li>
       <li>定理支援証明系やモデル検査が用いられる</li>
     </ul>
   </li>
@@ -134,17 +129,23 @@
 
 <div class='slide'>
   <!-- _S9SLIDE_ -->
-<h2 id="transactionalなファイルシステム">Transactionalなファイルシステム</h2>
+<h2 id="codegearとdatagear">CodeGearとDataGear</h2>
 <ul>
-  <li>GearsFSはDataGear単位での操作を行う</li>
-  <li>これによりファイルシステムAPIをTransactionとして実装できる
+  <li>CodeGear
     <ul>
-      <li>従来のOSのファイルシステムは一部を除きTransactionでない</li>
-      <li>Transactionな操作はアプリケーションレベルで実装される</li>
+      <li>実行Codeの単位</li>
+      <li>入力DataGearと出力DataGearを持つ</li>
+      <li>goto文(jump命令)を使って遷移する</li>
+      <li>実行単位は途中で割り込みされない(Atmocity)</li>
     </ul>
   </li>
-  <li>Transactionは様々な分類のアプリケーションに利用される</li>
-  <li>GearsOSによるOSレベルのTransactionアプリケーションの実用検証</li>
+  <li>DataGear
+    <ul>
+      <li>変数にあたり、構造体の型を持つ</li>
+      <li>ノーマルレベルでは変更されない(関数型プログラミング)</li>
+    </ul>
+  </li>
+  <li>C言語を拡張する形でCbC言語により実装される</li>
 </ul>
 
 
@@ -153,18 +154,102 @@
 
 <div class='slide'>
   <!-- _S9SLIDE_ -->
-<h2 id="gearsosのファイルシステムの設計と実装">GearsOSのファイルシステムの設計と実装</h2>
+<h2 id="codegearとdatagear-1">CodeGearとDataGear</h2>
+<ul>
+  <li>InputDataGearを受け取って、CodeGearが処理し、OutputDataGearを出力する</li>
+  <li>OutputDataGearは次のCodeGearのInputDataGearとなる</li>
+</ul>
+<div style="text-align: center;">
+  　<img src="images/cg-dg.pdf" alt="cgdgの関係図" width="600" />
+</div>
+
+
+
+</div>
+
+<div class='slide'>
+  <!-- _S9SLIDE_ -->
+<h2 id="gearsosにおけるファイル">GearsOSにおけるファイル</h2>
 <ul>
-  <li>CodeGear/DataGear単位で構成される</li>
-  <li>ファイルは複数のQueueを持つリストとして実装される</li>
-  <li>APIはPut/Take/Peek
+  <li>ファイルデータの最小単位はDataGearとなる
     <ul>
-      <li>key アクセスによるデータ参照</li>
-      <li>プロトコルを用いないデータアクセス手法</li>
+      <li>任意の構造体で構成できる</li>
+    </ul>
+  </li>
+  <li>ファイルデータとなるDataGearはQueueに格納される</li>
+</ul>
+<div style="text-align: center;">
+  　<img src="images/QueueElement.pdf" alt="Queue" width="800" />
+</div>
+
+
+
+</div>
+
+<div class='slide'>
+  <!-- _S9SLIDE_ -->
+<h2 id="gearsosにおけるファイル-1">GearsOSにおけるファイル</h2>
+<ul>
+  <li>ファイルは複数のQueueを持つ赤黒木である
+    <ul>
+      <li>Queueはkeyでアクセスされる</li>
+      <li>Queueはstreamの役割を持つ</li>
     </ul>
   </li>
-  <li>分散フレームワークChristieの仕組みを用いる</li>
-  <li>将来的にAPIの正当性は定理支援証明系で検証を行う</li>
+</ul>
+
+<div style="text-align: center;">
+  　<img src="images/newGearsFile.pdf" alt="Queue" width="400" />
+</div>
+
+
+
+</div>
+
+<div class='slide'>
+  <!-- _S9SLIDE_ -->
+<h2 id="gearsosの分散ファイルシステム">GearsOSの分散ファイルシステム</h2>
+<ul>
+  <li>GearsOSのファイルは通信の役割も持つ</li>
+  <li>規格が決められたプロトコルを用いない
+    <ul>
+      <li>最低限のデータ(DataGear)でのみ通信を行う</li>
+      <li>分散通信の見通しの確保を目指す</li>
+    </ul>
+  </li>
+  <li>将来的にAPIと通信プロセスは定理支援証明系Agdaで検証を行う</li>
+</ul>
+
+
+
+</div>
+
+<div class='slide'>
+  <!-- _S9SLIDE_ -->
+<h2 id="transactionalなファイルシステム">Transactionalなファイルシステム</h2>
+<ul>
+  <li>GearsFSはDataGear単位で操作を行う</li>
+  <li>これによりAPIをTransactionとして実装できる
+    <ul>
+      <li>従来ではアプリケーションレベルで実装される</li>
+    </ul>
+  </li>
+  <li>Transactionは様々な分類のアプリケーションに必要となる</li>
+  <li>GearsOSによるOSレベルのTransactionを用いた開発物の検証を兼ねる</li>
+</ul>
+
+
+
+</div>
+
+<div class='slide'>
+  <!-- _S9SLIDE_ -->
+<h2 id="ポスターセッション">ポスターセッション</h2>
+<ul>
+  <li>ファイル構造の詳細</li>
+  <li>ファイルアクセスAPI</li>
+  <li>proxyを用いたファイル通信の構成解説</li>
+  <li>研究のまとめと課題</li>
 </ul>
 
 </div>
--- a/finalSlide/finalSlide.md	Sat Feb 12 19:59:58 2022 +0900
+++ b/finalSlide/finalSlide.md	Sat Feb 12 21:43:10 2022 +0900
@@ -8,33 +8,72 @@
 - GearsOSの分散ファイルシステムの設計と実装を行った
   - ファイル構造の設計
   - APIの定義
-  - 遠隔のファイルへのアクセス
+  - 遠隔のファイルのアクセスと保存
+- GearsOS同様の記述単位な構成
 - 自律分散を目指した分散ファイルシステムの設計
 - OSレベルのTransactionによるアプリ実装
 
 ## GearsOS
-- **CodeGear**と**DataGear**という単位を用いるOS開発プロジェクト
-- 開発途上段階となる
-- OSの信頼性の向上と拡張性を目指している
-  - OSのプログラムは膨大な量となり、検証は困難である
-- ユーザーが実装したプログラムをメタレベルから検証する
-  - ノーマルレベルとメタレベルを分離して記述できる
-  - メタレベル処理を検証用へ切り替えられる
+- CodeGear/DataGearという単位で記述されるOS
+- OSの信頼性の保証と拡張性を目指している
+- ノーマルレベルとメタレベルを分離して記述できる
+  - ユーザーが実装したプログラムをメタレベルから検証する
   - 定理支援証明系やモデル検査が用いられる
 
+
+## CodeGearとDataGear
+- CodeGear
+  - 実行Codeの単位
+  - 入力DataGearと出力DataGearを持つ
+  - goto文(jump命令)を使って遷移する
+  - 実行単位は途中で割り込みされない(Atmocity)
+- DataGear
+  - 変数にあたり、構造体の型を持つ
+  - ノーマルレベルでは変更されない(関数型プログラミング)
+- C言語を拡張する形でCbC言語により実装される
+
+## CodeGearとDataGear
+- InputDataGearを受け取って、CodeGearが処理し、OutputDataGearを出力する
+- OutputDataGearは次のCodeGearのInputDataGearとなる
+<div style="text-align: center;">
+  　<img src="images/cg-dg.pdf" alt=cgdgの関係図 width="600">
+</div>
+
+
+## GearsOSにおけるファイル
+- ファイルデータの最小単位はDataGearとなる
+  - 任意の構造体で構成できる
+- ファイルデータとなるDataGearはQueueに格納される
+<div style="text-align: center;">
+  　<img src="images/QueueElement.pdf" alt=Queue width="800">
+</div>
+
+## GearsOSにおけるファイル
+- ファイルは複数のQueueを持つ赤黒木である
+  - Queueはkeyでアクセスされる
+  - Queueはstreamの役割を持つ
+
+<div style="text-align: center;">
+  　<img src="images/newGearsFile.pdf" alt=Queue width="400">
+</div>
+
+
+## GearsOSの分散ファイルシステム
+- GearsOSのファイルは通信の役割も持つ
+- 規格が決められたプロトコルを用いない
+  - 最低限のデータ(DataGear)でのみ通信を行う
+  - 分散通信の見通しの確保を目指す
+- 将来的にAPIと通信プロセスは定理支援証明系Agdaで検証を行う
+
 ## Transactionalなファイルシステム
-- GearsFSはDataGear単位での操作を行う
-- これによりファイルシステムAPIをTransactionとして実装できる
-  - 従来のOSのファイルシステムは一部を除きTransactionでない
-  - Transactionな操作はアプリケーションレベルで実装される
-- Transactionは様々な分類のアプリケーションに利用される
-- GearsOSによるOSレベルなTransactionによるアプリケーションの検証
+- GearsFSはDataGear単位で操作を行う
+- これによりAPIをTransactionとして実装できる
+  - 従来ではアプリケーションレベルで実装される
+- Transactionは様々な分類のアプリケーションに必要となる
+- GearsOSによるOSレベルのTransactionを用いた開発物の検証を兼ねる
 
-## 自律分散を目指した分散ファイルシステム
-- CodeGear/DataGear単位で構成される
-- ファイルは複数のQueueを持つリストとして実装される
-- APIはPut/Take/Peek
-  - key アクセスによるデータ参照
-  - プロトコルを用いないデータアクセス手法
-- 分散フレームワークChristieの仕組みを用いる
-- 将来的にAPIの正当性は定理支援証明系で検証を行う
+## ポスターセッション
+- ファイル構造の詳細
+- ファイルアクセスAPI
+- proxyを用いたファイル通信の構成解説
+- 研究のまとめと課題
--- a/finalSlide/finalSlide.pdf.html	Sat Feb 12 19:59:58 2022 +0900
+++ b/finalSlide/finalSlide.pdf.html	Sat Feb 12 21:43:10 2022 +0900
@@ -79,11 +79,12 @@
 <ul>
   <li>GearsOSの分散ファイルシステムの設計と実装を行った
     <ul>
+      <li>ファイル構造の設計</li>
       <li>APIの定義</li>
-      <li>ファイル構造の設計</li>
-      <li>遠隔のファイルへのアクセス</li>
+      <li>遠隔のファイルのアクセスと保存</li>
     </ul>
   </li>
+  <li>GearsOS同様の記述単位な構成</li>
   <li>自律分散を目指した分散ファイルシステムの設計</li>
   <li>OSレベルのTransactionによるアプリ実装</li>
 </ul>
@@ -96,17 +97,11 @@
   <!-- _S9SLIDE_ -->
 <h2 id="gearsos">GearsOS</h2>
 <ul>
-  <li><strong>CodeGear</strong>と<strong>DataGear</strong>という単位を用いるOS開発プロジェクト</li>
-  <li>開発途上段階となる</li>
-  <li>OSの信頼性の向上と拡張性を目指している
+  <li>CodeGear/DataGearという単位で記述されるOS</li>
+  <li>OSの信頼性の保証と拡張性を目指している</li>
+  <li>ノーマルレベルとメタレベルを分離して記述できる
     <ul>
-      <li>OSのプログラムは膨大な量となり、検証は困難である</li>
-    </ul>
-  </li>
-  <li>ユーザーが実装したプログラムをメタレベルから検証する
-    <ul>
-      <li>ノーマルレベルとメタレベルを分離して記述できる</li>
-      <li>メタレベル処理を検証用へ切り替えられる</li>
+      <li>ユーザーが実装したプログラムをメタレベルから検証する</li>
       <li>定理支援証明系やモデル検査が用いられる</li>
     </ul>
   </li>
@@ -118,17 +113,23 @@
 
 <div class='slide'>
   <!-- _S9SLIDE_ -->
-<h2 id="transactionalなファイルシステム">Transactionalなファイルシステム</h2>
+<h2 id="codegearとdatagear">CodeGearとDataGear</h2>
 <ul>
-  <li>GearsFSはDataGear単位での操作を行う</li>
-  <li>これによりファイルシステムAPIをTransactionとして実装できる
+  <li>CodeGear
     <ul>
-      <li>従来のOSのファイルシステムは一部を除きTransactionでない</li>
-      <li>Transactionな操作はアプリケーションレベルで実装される</li>
+      <li>実行Codeの単位</li>
+      <li>入力DataGearと出力DataGearを持つ</li>
+      <li>goto文(jump命令)を使って遷移する</li>
+      <li>実行単位は途中で割り込みされない(Atmocity)</li>
     </ul>
   </li>
-  <li>Transactionは様々な分類のアプリケーションに利用される</li>
-  <li>GearsOSによるOSレベルのTransactionアプリケーションの実用検証</li>
+  <li>DataGear
+    <ul>
+      <li>変数にあたり、構造体の型を持つ</li>
+      <li>ノーマルレベルでは変更されない(関数型プログラミング)</li>
+    </ul>
+  </li>
+  <li>C言語を拡張する形でCbC言語により実装される</li>
 </ul>
 
 
@@ -137,18 +138,102 @@
 
 <div class='slide'>
   <!-- _S9SLIDE_ -->
-<h2 id="gearsosのファイルシステムの設計と実装">GearsOSのファイルシステムの設計と実装</h2>
+<h2 id="codegearとdatagear-1">CodeGearとDataGear</h2>
+<ul>
+  <li>InputDataGearを受け取って、CodeGearが処理し、OutputDataGearを出力する</li>
+  <li>OutputDataGearは次のCodeGearのInputDataGearとなる</li>
+</ul>
+<div style="text-align: center;">
+  　<img src="images/cg-dg.pdf" alt="cgdgの関係図" width="600" />
+</div>
+
+
+
+</div>
+
+<div class='slide'>
+  <!-- _S9SLIDE_ -->
+<h2 id="gearsosにおけるファイル">GearsOSにおけるファイル</h2>
 <ul>
-  <li>CodeGear/DataGear単位で構成される</li>
-  <li>ファイルは複数のQueueを持つリストとして実装される</li>
-  <li>APIはPut/Take/Peek
+  <li>ファイルデータの最小単位はDataGearとなる
     <ul>
-      <li>key アクセスによるデータ参照</li>
-      <li>プロトコルを用いないデータアクセス手法</li>
+      <li>任意の構造体で構成できる</li>
+    </ul>
+  </li>
+  <li>ファイルデータとなるDataGearはQueueに格納される</li>
+</ul>
+<div style="text-align: center;">
+  　<img src="images/QueueElement.pdf" alt="Queue" width="800" />
+</div>
+
+
+
+</div>
+
+<div class='slide'>
+  <!-- _S9SLIDE_ -->
+<h2 id="gearsosにおけるファイル-1">GearsOSにおけるファイル</h2>
+<ul>
+  <li>ファイルは複数のQueueを持つ赤黒木である
+    <ul>
+      <li>Queueはkeyでアクセスされる</li>
+      <li>Queueはstreamの役割を持つ</li>
     </ul>
   </li>
-  <li>分散フレームワークChristieの仕組みを用いる</li>
-  <li>将来的にAPIの正当性は定理支援証明系で検証を行う</li>
+</ul>
+
+<div style="text-align: center;">
+  　<img src="images/newGearsFile.pdf" alt="Queue" width="400" />
+</div>
+
+
+
+</div>
+
+<div class='slide'>
+  <!-- _S9SLIDE_ -->
+<h2 id="gearsosの分散ファイルシステム">GearsOSの分散ファイルシステム</h2>
+<ul>
+  <li>GearsOSのファイルは通信の役割も持つ</li>
+  <li>規格が決められたプロトコルを用いない
+    <ul>
+      <li>最低限のデータ(DataGear)でのみ通信を行う</li>
+      <li>分散通信の見通しの確保を目指す</li>
+    </ul>
+  </li>
+  <li>将来的にAPIと通信プロセスは定理支援証明系Agdaで検証を行う</li>
+</ul>
+
+
+
+</div>
+
+<div class='slide'>
+  <!-- _S9SLIDE_ -->
+<h2 id="transactionalなファイルシステム">Transactionalなファイルシステム</h2>
+<ul>
+  <li>GearsFSはDataGear単位で操作を行う</li>
+  <li>これによりAPIをTransactionとして実装できる
+    <ul>
+      <li>従来ではアプリケーションレベルで実装される</li>
+    </ul>
+  </li>
+  <li>Transactionは様々な分類のアプリケーションに必要となる</li>
+  <li>GearsOSによるOSレベルのTransactionを用いた開発物の検証を兼ねる</li>
+</ul>
+
+
+
+</div>
+
+<div class='slide'>
+  <!-- _S9SLIDE_ -->
+<h2 id="ポスターセッション">ポスターセッション</h2>
+<ul>
+  <li>ファイル構造の詳細</li>
+  <li>ファイルアクセスAPI</li>
+  <li>proxyを用いたファイル通信の構成解説</li>
+  <li>研究のまとめと課題</li>
 </ul>
 
 </div>