Mercurial > hg > Papers > 2018 > tobaru-sigos

comparison Slide/prosym.md @ 9:5790bdc1d515

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add gears_structure
author tobaru
date Mon, 21 May 2018 17:18:19 +0900
parents f275411f458d
children d4e58a38aae7
comparison
equal deleted inserted replaced
8:f275411f458d 9:5790bdc1d515
19 % - 本研究室では、OS の信頼性の保証と拡張性を実現することを目標に Gears OS を設計中である。 19 % - 本研究室では、OS の信頼性の保証と拡張性を実現することを目標に Gears OS を設計中である。
20 20
21 ## Gears OS 21 ## Gears OS
22 - 現代のOS では拡張性と信頼性を両立させることが要求されている。 22 - 現代のOS では拡張性と信頼性を両立させることが要求されている。
23 - 時代と共にハードウェア、サービスが進歩していき、その度に OS を検証できる必要があるため、拡張性が必要。 23 - 時代と共にハードウェア、サービスが進歩していき、その度に OS を検証できる必要があるため、拡張性が必要。
24 - OS は非決定的な実行を持ち、従来の OS ではテストしきれない部分が残ってしまうため、信頼性が欠けてしまう。 24 - OS は非決定的な実行を持ち、従来の OS ではテストしきれない部分が残ってしまうため、信頼性が欠けてしまうので信頼性のある OS が必要。
25 - 本研究室では、それらを実現することを目標に Gears OS の開発を行なっている。 25 - 本研究室では、拡張性と信頼性を実現することを目標に Gears OS の開発を行なっている。
26 26
27 % 欠けてしまうで終わってるので　"それら"は 分かりづらい 27 % 欠けてしまうで終わってるので　"それら"は 分かりづらい
28 % 並列API 研究目的とAPIとの繋がりがない 28 % 並列API 研究目的とAPIとの繋がりがない
29 % モジュールとAPIの説明分ける 29 % モジュールとAPIの説明分ける
30 % 拡張性と信頼性を実現する時に Interfaceと par goto 構文がなぜ必要なのかに繋げる話が必要 30 % 拡張性と信頼性を実現する時に Interfaceと par goto 構文がなぜ必要なのかに繋げる話が必要
49 % TaskScheduler の図も入れる Gears の構成のやつ 49 % TaskScheduler の図も入れる Gears の構成のやつ
50 50
51 ## Gears OS での形式化とInterfaceの導入 51 ## Gears OS での形式化とInterfaceの導入
52 - 形式化とは仕様、実装、実行を Logic で記述する事である。 52 - 形式化とは仕様、実装、実行を Logic で記述する事である。
53 - Gears OS では、継続を使った関数型プログラムとして実装を記述する 53 - Gears OS では、継続を使った関数型プログラムとして実装を記述する
54 - Logic としては、依存型関数言語である Agda を使う(前の発表) 54 - Logic としては、依存型関数言語である Agda を使う(外間の発表)
55 - 証明とモデル検査を使って、信頼性を確保する 55 - 証明とモデル検査を使って、信頼性を確保する
56 56
57 ## Gears OS の Interface 57 ## Gears OS の Interface
58 - この時、Code Gear と Deta Gear は Interface と呼ばれるまとまり(モジュール)で記述される。 58 - Code Gear と Deta Gear は Interface と呼ばれるまとまり(モジュール)で記述される。
59 - Interface 作成時に Code Gear の集合を指定することにより複数の実装を持つことができる。 59 - Interface 作成時に Code Gear の集合を指定することにより複数の実装を持つことができる。
60 - Interface は Data Gear で記述されて、Meta Deta Gear と呼ばれる。 60 - Interface は Data Gear で記述されて、Meta Deta Gear と呼ばれる。
61 - Java などの Class に相当する。 61 - Java などの Class に相当する。
62 - Interface を外から呼び出すための Code Gear 群の型 62 % - Interface を外から呼び出すための Code Gear 群の型
63 - Interface を呼び出す時に必要となる引数を全て格納する Data Gear 63 - Interface を呼び出す時に必要となる引数を全て格納する Data Gear
64 - 実装に使う Code Gear の番号が含まれている。 64 % - 実装に使う Code Gear の番号が含まれている。
65 - Code Gear の番号を変更することによって異なる実装を実現できる 65 % - Code Gear の番号を変更することによって異なる実装を実現できる
66 66
67 % Interface は実行時に実装を入れ替える事ができる 67 % Interface は実行時に実装を入れ替える事ができる
68 % 呼び出すものはStack 上に積めない 68 % 呼び出すものはStack 上に積めない
69 % Contextも集合 69 % Contextも集合
70 % Inter
71 70
72 ## 並列API 71 ## 並列API
73 - Geas OS 信頼性を保証するために、形式化されたモジュールシステムが必要である。 72 - Geas OS 信頼性を保証するために、モジュールシステムが必要である。
74 - 本研究では、モジュールシステムとその応用である並列APIについて考察する。 73 - 本研究では、モジュールシステムとその応用である並列APIについて考察する。
75 - 並列APIは継続を基本とした関数型プログラミングと両立する必要があり、ここでは CbC の goto 文を拡張した par goto を導入する。 74 - 並列APIは継続を基本とした関数型プログラミングと両立する必要があり、ここでは CbC の goto 文を拡張した par goto を導入する。
76 75
77 ## スライドの流れ 76 ## スライドの流れ
78 - Interface 77 - Interface
167 % ## Interface 166 % ## Interface
168 % - この時、Code Gear と Deta Gear は Interface と呼ばれるまとまり(モジュール)で記述される。 167 % - この時、Code Gear と Deta Gear は Interface と呼ばれるまとまり(モジュール)で記述される。
169 % - Interface 作成時に Code Gear の集合を指定することにより複数の実装を持つことができる。 168 % - Interface 作成時に Code Gear の集合を指定することにより複数の実装を持つことができる。
170 169
171 ## Gears OS の構造 170 ## Gears OS の構造
171 - Gears OS は以下の要素で構成されている
172 - Context
173 - TaskQueue
174 - TaskManager
175 - Worker
176
172 <div style="text-align: center;"> 177 <div style="text-align: center;">
173 <img src="./image/gearsos.svg" alt="Gears OS の構造" width="600"> 178 <img src="./image/gears_structure.png" alt="Gears OS の構造" width="400">
174 </div> 179 </div>
175 180
176 181
177 ## Context 182 ## Context
178 - 1つのスレッド内で使われる Interface の Code Gear と Data Gear は Meta Data Gear に格納される。 183 - 1つのスレッド内で使われる Interface の Code Gear と Data Gear は Meta Data Gear に格納される。
194 - 読み込みは複数であってもいい 199 - 読み込みは複数であってもいい
195 - Agda 側で、並列実行を Code Gear の順次実行としてシミュレーションするため 200 - Agda 側で、並列実行を Code Gear の順次実行としてシミュレーションするため
196 - このような実行になるように Gears OS の実装を行う 201 - このような実行になるように Gears OS の実装を行う
197 202
198 % 複数走ったなかの成功したものをコミットするのがexit 203 % 複数走ったなかの成功したものをコミットするのがexit
204
205 <div style="text-align: center;">
206 <img src="./image/gears_structure.png" alt="Gears OS の構造" width="400">
207 </div>
199 208
200 209
201 210
202 211
203 ## __exit 212 ## __exit
211 par goto add(integer1, integer2, output, __exit); 220 par goto add(integer1, integer2, output, __exit);
212 goto code2(); 221 goto code2();
213 } 222 }
214 ``` 223 ```
215 224
225 ## Perl スクリプトによる Meta Data Gear の生成
226
227
228 % Task Manager
229 %
230
231 ```c
232 __code code1(struct Context *context, Integer *integer1, Integer *integer2, Integer *output) {
233 // create context
234 context->task = NEW(struct Context);
235 initContext(context->task);
236
237 // set task parameter
238 context->task->next = C_add;
239 context->task->idgCount = 2;
240 context->task->idg = context->task->dataNum;
241 context->task->maxIdg = context->task->idg + 2;
242 context->task->odg = context->task->maxIdg;
243 context->task->maxOdg = context->task->odg + 1;
244
245 // create Data Gear Queue
246 GET_META(integer1)->wait = createSynchronizedQueue(context);
247 GET_META(integer2)->wait = createSynchronizedQueue(context);
248 GET_META(integer3)->wait = createSynchronizedQueue(context);
249
250 // set Input Data Gear
251 context->task->data[context->task->idg+0] = (union Data*)integer1;
252 context->task->data[context->task->idg+1] = (union Data*)integer2;
253
254 // set Output Data Gear
255 context->task->data[context->task->odg+0] = (union Data*)integer3;
256
257
258 // set TaskManager->spawns parameter
259 Gearef(context, TaskManager)->taskList = context->taskList;
260 Gearef(context, TaskManager)->next1 = C_code2;
261 goto parGotoMeta(context, C_code2);
262 }
263 ```
264 % // add taskList Element
265 % struct Element* element;
266 % element = &ALLOCATE(context, Element)->Element;
267 % element->data = (union Data*)context->task;
268 % element->next = context->taskList;
269 % context->taskList = element;
270
216 % 失敗した時はmeta compitation で処理する 271 % 失敗した時はmeta compitation で処理する
217 272
218 273
219 274
220 % ## Interface 275 % ## Interface