Mercurial > hg > Papers > 2022 > ikki-master

changeset 37:8efb5398e604

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tweak
author ichikitakahiro <e165713@ie.u-ryukyu.ac.jp>
date Mon, 14 Feb 2022 17:43:19 +0900
parents f636dbf689e1
children e5570db4fcb4
files finalSlide/finalSlide.html finalSlide/finalSlide.md finalSlide/finalSlide.pdf.html
diffstat 3 files changed, 72 insertions(+), 81 deletions(-) [+]
line wrap: on
line diff
--- a/finalSlide/finalSlide.html	Mon Feb 14 16:46:02 2022 +0900
+++ b/finalSlide/finalSlide.html	Mon Feb 14 17:43:19 2022 +0900
@@ -93,22 +93,18 @@
 <!-- _S9SLIDE_ -->
 <h2 id="継続を導入したgearsos">継続を導入したGearsOS</h2>
 <ul>
-  <li>GearsOSは関数遷移でなく、継続を導入したOS開発プロジェクトである</li>
-  <li>関数遷移でなく、<strong>CodeGear</strong>と言う単位で記述する
+  <li>継続を導入した、信頼性の保証を目指したOS開発プロジェクトである</li>
+  <li>関数遷移を用いず、<strong>CodeGear</strong>と言う単位で記述を行う
     <ul>
-      <li>各CodeGearをjump命令で推移することで処理が実行される</li>
+      <li>複数のCodeGearをgoto(jump命令)で遷移することで処理が実行される</li>
     </ul>
   </li>
-  <li>OSの信頼性の向上を目指して開発されている
+  <li>OS自体の検証はプログラムが膨大な量となるため、テストコードを用いるのは難しい</li>
+  <li>GearsOSではメタレベルの処理からユーザープログラムの検証をする構成となる
     <ul>
-      <li>OSのプログラムは膨大なため検証が困難である</li>
-    </ul>
-  </li>
-  <li>GearsOSはノーマルレベルとメタレベルの処理を分けて記述できる
-    <ul>
-      <li>メタレベルな処理を実行用や検証用なものに切り替えるができる</li>
-      <li>これによりユーザープログラムの検証を行う</li>
-      <li>検証は定理支援証明系やモデル検査を用いる</li>
+      <li>GearsOSはノーマルレベルとメタレベルを分けて記述できる</li>
+      <li>メタレベルな処理を検証用のものに切り替えることで検証を行う</li>
+      <li>信頼性の検証には定理支援証明系やモデル検査を用いる</li>
     </ul>
   </li>
 </ul>
@@ -121,20 +117,20 @@
   <!-- _S9SLIDE_ -->
 <h2 id="gearsosのファイルシステム開発">GearsOSのファイルシステム開発</h2>
 <ul>
-  <li>GearsOSは現段階で言語フレームワークとして実装されている</li>
-  <li>GearsOSの分散ファイルシステムを開発したい
+  <li>GearsOSは現段階でファイルシステムを持っていない</li>
+  <li>開発にあたりGearsOSファイルシステムの要件定義を行った
     <ul>
-      <li>ファイルシステムも同様にGear単位で操作したい</li>
-      <li>煩雑な分散処理を簡潔に構成したい</li>
+      <li>ファイルシステムも同様にGear単位で操作する</li>
+      <li>煩雑な分散処理記述やノードの接続を簡潔に行いたい</li>
       <li>従来ではアプリケーションが持つ機能の一部を取り入れたい
         <ul>
           <li>Transaction</li>
-          <li>バックアップ</li>
+          <li>バックアップなど</li>
         </ul>
       </li>
     </ul>
   </li>
-  <li>分散フレームワークChrisiteの仕組みで問題の一部を解決をはかる</li>
+  <li>分散フレームワークChrisiteの仕組みでGearsFSの要件を満たしたい</li>
 </ul>
 
 
@@ -145,14 +141,14 @@
   <!-- _S9SLIDE_ -->
 <h2 id="分散フレームワークchristie">分散フレームワークChristie</h2>
 <ul>
-  <li>Javaで書かれた分散フレームワークである
+  <li>当研究室が開発する、Javaで書かれた分散フレームワークである
     <ul>
       <li>GearsOSと似たGearと言うプログラミング概念を持つ</li>
-      <li>規格が決められたプロトコルを持たず、データのみの送受信で通信する</li>
-      <li>自立分散を目指した設計となっている</li>
+      <li>規格が決められたプロトコルを持たず、ノード間の通信はデータの書き込みで送受信で行う</li>
+      <li>通信されるデータを意識しながら分散処理の記述が行える</li>
+      <li>これらの構成は自立分散を目指した設計となっている</li>
     </ul>
   </li>
-  <li>通信されるデータを意識しながら分散処理の記述が行える</li>
 </ul>
 
 
@@ -165,12 +161,12 @@
 <ul>
   <li>Christieの仕組みを分散ファイルシステムに応用/検証を行いたい
     <ul>
-      <li>複数のstreamを持ち、通信を行うファイル構造</li>
+      <li>GearsOSのファイルは複数のstreamを持ち、通信自体も行う</li>
       <li>APIは通信部分を含め3種類で構成される</li>
     </ul>
   </li>
-  <li>プロトコルを用いないことで、分散ネットワーク内の通信の見通しを確保する</li>
-  <li>簡潔な記述による分散処理構成</li>
+  <li>簡潔な記述による分散処理の構成を目指す</li>
+  <li>Christieの通信の仕組みにより、分散ネットワーク内の通信の見通しを確保する</li>
   <li>APIやプロセスの正当性は将来的に定理支援証明系agdaで検証される</li>
 </ul>
 
@@ -180,15 +176,15 @@
 
 <div class='slide'>
   <!-- _S9SLIDE_ -->
-<h2 id="gearsosが持つosレベルなtransactionの検証">GearsOSが持つOSレベルなTransactionの検証</h2>
+<h2 id="gearsosが持つosレベルなtransactionの実装検証">GearsOSが持つOSレベルなTransactionの実装検証</h2>
 <ul>
   <li>GearsOSはAPIレベルでTransactionな記述が行える
     <ul>
       <li>従来のアプリケーションでは、ユーザーレベルで実装される</li>
-      <li>GearsOSのOSレベルで実装されるTransactionの実装検証を行いたい</li>
+      <li>GearsOSのAPIレベルで実装されるTransactionの実装検証を兼ねる</li>
     </ul>
   </li>
-  <li>OSのTransactionが保証されていれば、アプリケーションの信頼性の保証となる</li>
+  <li>OS自体のTransactionが保証されていれば、アプリケーションの信頼性が高まる</li>
 </ul>
 
 
--- a/finalSlide/finalSlide.md	Mon Feb 14 16:46:02 2022 +0900
+++ b/finalSlide/finalSlide.md	Mon Feb 14 17:43:19 2022 +0900
@@ -7,47 +7,46 @@
 
 
 ## 継続を導入したGearsOS
-- GearsOSは関数遷移でなく、継続を導入したOS開発プロジェクトである
-- 関数遷移でなく、**CodeGear**と言う単位で記述する
-  - 各CodeGearをjump命令で推移することで処理が実行される
-- OSの信頼性の向上を目指して開発されている
-  - OSのプログラムは膨大なため検証が困難である
-- GearsOSはノーマルレベルとメタレベルの処理を分けて記述できる
-  - メタレベルな処理を実行用や検証用なものに切り替えるができる
-  - これによりユーザープログラムの検証を行う
-  - 検証は定理支援証明系やモデル検査を用いる
+- 継続を導入した、信頼性の保証を目指したOS開発プロジェクトである
+- 関数遷移を用いず、**CodeGear**と言う単位で記述を行う
+  - 複数のCodeGearをgoto(jump命令)で遷移することで処理が実行される  
+- OS自体の検証はプログラムが膨大な量となるため、テストコードを用いるのは難しい
+- GearsOSではメタレベルの処理からユーザープログラムの検証をする構成となる
+  - GearsOSはノーマルレベルとメタレベルを分けて記述できる
+  - メタレベルな処理を検証用のものに切り替えることで検証を行う
+  - 信頼性の検証には定理支援証明系やモデル検査を用いる
 
 ## GearsOSのファイルシステム開発
-- GearsOSは現段階で言語フレームワークとして実装されている
-- GearsOSの分散ファイルシステムを開発したい
-  - ファイルシステムも同様にGear単位で操作したい
-  - 煩雑な分散処理を簡潔に構成したい
+- GearsOSは現段階でファイルシステムを持っていない
+- 開発にあたりGearsOSファイルシステムの要件定義を行った
+  - ファイルシステムも同様にGear単位で操作する
+  - 煩雑な分散処理記述やノードの接続を簡潔に行いたい
   - 従来ではアプリケーションが持つ機能の一部を取り入れたい
     - Transaction
-    - バックアップ
-- 分散フレームワークChrisiteの仕組みで問題の一部を解決をはかる
+    - バックアップなど
+- 分散フレームワークChrisiteの仕組みでGearsFSの要件を満たしたい
 
 
 ## 分散フレームワークChristie
-- Javaで書かれた分散フレームワークである
+- 当研究室が開発する、Javaで書かれた分散フレームワークである
   - GearsOSと似たGearと言うプログラミング概念を持つ
-  - 規格が決められたプロトコルを持たず、データのみの送受信で通信する  
-  - 自立分散を目指した設計となっている
-- 通信されるデータを意識しながら分散処理の記述が行える
+  - 規格が決められたプロトコルを持たず、ノード間の通信はデータの書き込みで送受信で行う  
+  - 通信されるデータを意識しながら分散処理の記述が行える  
+  - これらの構成は自立分散を目指した設計となっている
 
 ## Christie likeな通信の分散ファイルシステムの提案
 - Christieの仕組みを分散ファイルシステムに応用/検証を行いたい
-  - 複数のstreamを持ち、通信を行うファイル構造
+  - GearsOSのファイルは複数のstreamを持ち、通信自体も行う
   - APIは通信部分を含め3種類で構成される
-- プロトコルを用いないことで、分散ネットワーク内の通信の見通しを確保する
-- 簡潔な記述による分散処理構成
+- 簡潔な記述による分散処理の構成を目指す
+- Christieの通信の仕組みにより、分散ネットワーク内の通信の見通しを確保する
 - APIやプロセスの正当性は将来的に定理支援証明系agdaで検証される
 
-## GearsOSが持つOSレベルなTransactionの検証
+## GearsOSが持つOSレベルなTransactionの実装検証
 - GearsOSはAPIレベルでTransactionな記述が行える
   - 従来のアプリケーションでは、ユーザーレベルで実装される
-  - GearsOSのOSレベルで実装されるTransactionの実装検証を行いたい
-- OSのTransactionが保証されていれば、アプリケーションの信頼性の保証となる
+  - GearsOSのAPIレベルで実装されるTransactionの実装検証を兼ねる
+- OS自体のTransactionが保証されていれば、アプリケーションの信頼性が高まる
 
 ## ポスター発表
 - GearsOSのChristie likeなファイルシステムの設計と実装
--- a/finalSlide/finalSlide.pdf.html	Mon Feb 14 16:46:02 2022 +0900
+++ b/finalSlide/finalSlide.pdf.html	Mon Feb 14 17:43:19 2022 +0900
@@ -77,22 +77,18 @@
 <!-- _S9SLIDE_ -->
 <h2 id="継続を導入したgearsos">継続を導入したGearsOS</h2>
 <ul>
-  <li>GearsOSは関数遷移でなく、継続を導入したOS開発プロジェクトである</li>
-  <li>関数遷移でなく、<strong>CodeGear</strong>と言う単位で記述する
+  <li>継続を導入した、信頼性の保証を目指したOS開発プロジェクトである</li>
+  <li>関数遷移を用いず、<strong>CodeGear</strong>と言う単位で記述を行う
     <ul>
-      <li>各CodeGearをjump命令で推移することで処理が実行される</li>
+      <li>複数のCodeGearをgoto(jump命令)で遷移することで処理が実行される</li>
     </ul>
   </li>
-  <li>OSの信頼性の向上を目指して開発されている
+  <li>OS自体の検証はプログラムが膨大な量となるため、テストコードを用いるのは難しい</li>
+  <li>GearsOSではメタレベルの処理からユーザープログラムの検証をする構成となる
     <ul>
-      <li>OSのプログラムは膨大なため検証が困難である</li>
-    </ul>
-  </li>
-  <li>GearsOSはノーマルレベルとメタレベルの処理を分けて記述できる
-    <ul>
-      <li>メタレベルな処理を実行用や検証用なものに切り替えるができる</li>
-      <li>これによりユーザープログラムの検証を行う</li>
-      <li>検証は定理支援証明系やモデル検査を用いる</li>
+      <li>GearsOSはノーマルレベルとメタレベルを分けて記述できる</li>
+      <li>メタレベルな処理を検証用のものに切り替えることで検証を行う</li>
+      <li>信頼性の検証には定理支援証明系やモデル検査を用いる</li>
     </ul>
   </li>
 </ul>
@@ -105,20 +101,20 @@
   <!-- _S9SLIDE_ -->
 <h2 id="gearsosのファイルシステム開発">GearsOSのファイルシステム開発</h2>
 <ul>
-  <li>GearsOSは現段階で言語フレームワークとして実装されている</li>
-  <li>GearsOSの分散ファイルシステムを開発したい
+  <li>GearsOSは現段階でファイルシステムを持っていない</li>
+  <li>開発にあたりGearsOSファイルシステムの要件定義を行った
     <ul>
-      <li>ファイルシステムも同様にGear単位で操作したい</li>
-      <li>煩雑な分散処理を簡潔に構成したい</li>
+      <li>ファイルシステムも同様にGear単位で操作する</li>
+      <li>煩雑な分散処理記述やノードの接続を簡潔に行いたい</li>
       <li>従来ではアプリケーションが持つ機能の一部を取り入れたい
         <ul>
           <li>Transaction</li>
-          <li>バックアップ</li>
+          <li>バックアップなど</li>
         </ul>
       </li>
     </ul>
   </li>
-  <li>分散フレームワークChrisiteの仕組みで問題の一部を解決をはかる</li>
+  <li>分散フレームワークChrisiteの仕組みでGearsFSの要件を満たしたい</li>
 </ul>
 
 
@@ -129,14 +125,14 @@
   <!-- _S9SLIDE_ -->
 <h2 id="分散フレームワークchristie">分散フレームワークChristie</h2>
 <ul>
-  <li>Javaで書かれた分散フレームワークである
+  <li>当研究室が開発する、Javaで書かれた分散フレームワークである
     <ul>
       <li>GearsOSと似たGearと言うプログラミング概念を持つ</li>
-      <li>規格が決められたプロトコルを持たず、データのみの送受信で通信する</li>
-      <li>自立分散を目指した設計となっている</li>
+      <li>規格が決められたプロトコルを持たず、ノード間の通信はデータの書き込みで送受信で行う</li>
+      <li>通信されるデータを意識しながら分散処理の記述が行える</li>
+      <li>これらの構成は自立分散を目指した設計となっている</li>
     </ul>
   </li>
-  <li>通信されるデータを意識しながら分散処理の記述が行える</li>
 </ul>
 
 
@@ -149,12 +145,12 @@
 <ul>
   <li>Christieの仕組みを分散ファイルシステムに応用/検証を行いたい
     <ul>
-      <li>複数のstreamを持ち、通信を行うファイル構造</li>
+      <li>GearsOSのファイルは複数のstreamを持ち、通信自体も行う</li>
       <li>APIは通信部分を含め3種類で構成される</li>
     </ul>
   </li>
-  <li>プロトコルを用いないことで、分散ネットワーク内の通信の見通しを確保する</li>
-  <li>簡潔な記述による分散処理構成</li>
+  <li>簡潔な記述による分散処理の構成を目指す</li>
+  <li>Christieの通信の仕組みにより、分散ネットワーク内の通信の見通しを確保する</li>
   <li>APIやプロセスの正当性は将来的に定理支援証明系agdaで検証される</li>
 </ul>
 
@@ -164,15 +160,15 @@
 
 <div class='slide'>
   <!-- _S9SLIDE_ -->
-<h2 id="gearsosが持つosレベルなtransactionの検証">GearsOSが持つOSレベルなTransactionの検証</h2>
+<h2 id="gearsosが持つosレベルなtransactionの実装検証">GearsOSが持つOSレベルなTransactionの実装検証</h2>
 <ul>
   <li>GearsOSはAPIレベルでTransactionな記述が行える
     <ul>
       <li>従来のアプリケーションでは、ユーザーレベルで実装される</li>
-      <li>GearsOSのOSレベルで実装されるTransactionの実装検証を行いたい</li>
+      <li>GearsOSのAPIレベルで実装されるTransactionの実装検証を兼ねる</li>
     </ul>
   </li>
-  <li>OSのTransactionが保証されていれば、アプリケーションの信頼性の保証となる</li>
+  <li>OS自体のTransactionが保証されていれば、アプリケーションの信頼性が高まる</li>
 </ul>