Mercurial > hg > Papers > 2022 > ikki-master

comparison finalSlide/finalSlide.pdf.html @ 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
comparison
equal deleted inserted replaced
32:fa31358d38f1 33:ab77a291294d
77 <!-- _S9SLIDE_ --> 77 <!-- _S9SLIDE_ -->
78 <h2 id="概要">概要</h2> 78 <h2 id="概要">概要</h2>
79 <ul> 79 <ul>
80 <li>GearsOSの分散ファイルシステムの設計と実装を行った 80 <li>GearsOSの分散ファイルシステムの設計と実装を行った
81 <ul> 81 <ul>
82 <li>ファイル構造の設計</li>
82 <li>APIの定義</li> 83 <li>APIの定義</li>
83 <li>ファイル構造の設計</li> 84 <li>遠隔のファイルのアクセスと保存</li>
84 <li>遠隔のファイルへのアクセス</li> 85 </ul>
85 </ul> 86 </li>
86 </li> 87 <li>GearsOS同様の記述単位な構成</li>
87 <li>自律分散を目指した分散ファイルシステムの設計</li> 88 <li>自律分散を目指した分散ファイルシステムの設計</li>
88 <li>OSレベルのTransactionによるアプリ実装</li> 89 <li>OSレベルのTransactionによるアプリ実装</li>
89 </ul> 90 </ul>
90 91
91 92
94 95
95 <div class='slide'> 96 <div class='slide'>
96 <!-- _S9SLIDE_ --> 97 <!-- _S9SLIDE_ -->
97 <h2 id="gearsos">GearsOS</h2> 98 <h2 id="gearsos">GearsOS</h2>
98 <ul> 99 <ul>
99 <li><strong>CodeGear</strong>と<strong>DataGear</strong>という単位を用いるOS開発プロジェクト</li> 100 <li>CodeGear/DataGearという単位で記述されるOS</li>
100 <li>開発途上段階となる</li> 101 <li>OSの信頼性の保証と拡張性を目指している</li>
101 <li>OSの信頼性の向上と拡張性を目指している 102 <li>ノーマルレベルとメタレベルを分離して記述できる
102 <ul> 103 <ul>
103 <li>OSのプログラムは膨大な量となり、検証は困難である</li> 104 <li>ユーザーが実装したプログラムをメタレベルから検証する</li>
104 </ul>
105 </li>
106 <li>ユーザーが実装したプログラムをメタレベルから検証する
107 <ul>
108 <li>ノーマルレベルとメタレベルを分離して記述できる</li>
109 <li>メタレベル処理を検証用へ切り替えられる</li>
110 <li>定理支援証明系やモデル検査が用いられる</li> 105 <li>定理支援証明系やモデル検査が用いられる</li>
111 </ul> 106 </ul>
112 </li> 107 </li>
113 </ul> 108 </ul>
114 109
116 111
117 </div> 112 </div>
118 113
119 <div class='slide'> 114 <div class='slide'>
120 <!-- _S9SLIDE_ --> 115 <!-- _S9SLIDE_ -->
116 <h2 id="codegearとdatagear">CodeGearとDataGear</h2>
117 <ul>
118 <li>CodeGear
119 <ul>
120 <li>実行Codeの単位</li>
121 <li>入力DataGearと出力DataGearを持つ</li>
122 <li>goto文(jump命令)を使って遷移する</li>
123 <li>実行単位は途中で割り込みされない(Atmocity)</li>
124 </ul>
125 </li>
126 <li>DataGear
127 <ul>
128 <li>変数にあたり、構造体の型を持つ</li>
129 <li>ノーマルレベルでは変更されない(関数型プログラミング)</li>
130 </ul>
131 </li>
132 <li>C言語を拡張する形でCbC言語により実装される</li>
133 </ul>
134
135
136
137 </div>
138
139 <div class='slide'>
140 <!-- _S9SLIDE_ -->
141 <h2 id="codegearとdatagear-1">CodeGearとDataGear</h2>
142 <ul>
143 <li>InputDataGearを受け取って、CodeGearが処理し、OutputDataGearを出力する</li>
144 <li>OutputDataGearは次のCodeGearのInputDataGearとなる</li>
145 </ul>
146 <div style="text-align: center;">
147 　<img src="images/cg-dg.pdf" alt="cgdgの関係図" width="600" />
148 </div>
149
150
151
152 </div>
153
154 <div class='slide'>
155 <!-- _S9SLIDE_ -->
156 <h2 id="gearsosにおけるファイル">GearsOSにおけるファイル</h2>
157 <ul>
158 <li>ファイルデータの最小単位はDataGearとなる
159 <ul>
160 <li>任意の構造体で構成できる</li>
161 </ul>
162 </li>
163 <li>ファイルデータとなるDataGearはQueueに格納される</li>
164 </ul>
165 <div style="text-align: center;">
166 　<img src="images/QueueElement.pdf" alt="Queue" width="800" />
167 </div>
168
169
170
171 </div>
172
173 <div class='slide'>
174 <!-- _S9SLIDE_ -->
175 <h2 id="gearsosにおけるファイル-1">GearsOSにおけるファイル</h2>
176 <ul>
177 <li>ファイルは複数のQueueを持つ赤黒木である
178 <ul>
179 <li>Queueはkeyでアクセスされる</li>
180 <li>Queueはstreamの役割を持つ</li>
181 </ul>
182 </li>
183 </ul>
184
185 <div style="text-align: center;">
186 　<img src="images/newGearsFile.pdf" alt="Queue" width="400" />
187 </div>
188
189
190
191 </div>
192
193 <div class='slide'>
194 <!-- _S9SLIDE_ -->
195 <h2 id="gearsosの分散ファイルシステム">GearsOSの分散ファイルシステム</h2>
196 <ul>
197 <li>GearsOSのファイルは通信の役割も持つ</li>
198 <li>規格が決められたプロトコルを用いない
199 <ul>
200 <li>最低限のデータ(DataGear)でのみ通信を行う</li>
201 <li>分散通信の見通しの確保を目指す</li>
202 </ul>
203 </li>
204 <li>将来的にAPIと通信プロセスは定理支援証明系Agdaで検証を行う</li>
205 </ul>
206
207
208
209 </div>
210
211 <div class='slide'>
212 <!-- _S9SLIDE_ -->
121 <h2 id="transactionalなファイルシステム">Transactionalなファイルシステム</h2> 213 <h2 id="transactionalなファイルシステム">Transactionalなファイルシステム</h2>
122 <ul> 214 <ul>
123 <li>GearsFSはDataGear単位での操作を行う</li> 215 <li>GearsFSはDataGear単位で操作を行う</li>
124 <li>これによりファイルシステムAPIをTransactionとして実装できる 216 <li>これによりAPIをTransactionとして実装できる
125 <ul> 217 <ul>
126 <li>従来のOSのファイルシステムは一部を除きTransactionでない</li> 218 <li>従来ではアプリケーションレベルで実装される</li>
127 <li>Transactionな操作はアプリケーションレベルで実装される</li> 219 </ul>
128 </ul> 220 </li>
129 </li> 221 <li>Transactionは様々な分類のアプリケーションに必要となる</li>
130 <li>Transactionは様々な分類のアプリケーションに利用される</li> 222 <li>GearsOSによるOSレベルのTransactionを用いた開発物の検証を兼ねる</li>
131 <li>GearsOSによるOSレベルのTransactionアプリケーションの実用検証</li> 223 </ul>
132 </ul> 224
133 225
134 226
135 227 </div>
136 </div> 228
137 229 <div class='slide'>
138 <div class='slide'> 230 <!-- _S9SLIDE_ -->
139 <!-- _S9SLIDE_ --> 231 <h2 id="ポスターセッション">ポスターセッション</h2>
140 <h2 id="gearsosのファイルシステムの設計と実装">GearsOSのファイルシステムの設計と実装</h2> 232 <ul>
141 <ul> 233 <li>ファイル構造の詳細</li>
142 <li>CodeGear/DataGear単位で構成される</li> 234 <li>ファイルアクセスAPI</li>
143 <li>ファイルは複数のQueueを持つリストとして実装される</li> 235 <li>proxyを用いたファイル通信の構成解説</li>
144 <li>APIはPut/Take/Peek 236 <li>研究のまとめと課題</li>
145 <ul>
146 <li>key アクセスによるデータ参照</li>
147 <li>プロトコルを用いないデータアクセス手法</li>
148 </ul>
149 </li>
150 <li>分散フレームワークChristieの仕組みを用いる</li>
151 <li>将来的にAPIの正当性は定理支援証明系で検証を行う</li>
152 </ul> 237 </ul>
153 238
154 </div> 239 </div>
155 240
156 241