Mercurial > hg > Papers > 2018 > tobaru-sigos
changeset 9:5790bdc1d515
add gears_structure
| author | tobaru |
|---|---|
| date | Mon, 21 May 2018 17:18:19 +0900 |
| parents | f275411f458d |
| children | d4e58a38aae7 |
| files | Slide/image/gears_structure.png Slide/prosym.html Slide/prosym.md Slide/prosym.pdf.html |
| diffstat | 4 files changed, 177 insertions(+), 22 deletions(-) [+] |
line wrap: on
line diff
--- a/Slide/prosym.html Sun May 20 21:28:30 2018 +0900 +++ b/Slide/prosym.html Mon May 21 17:18:19 2018 +0900 @@ -86,7 +86,7 @@ <!-- === begin markdown block === generated by markdown/1.2.0 on Ruby 2.4.1 (2017-03-22) [x86_64-darwin15] - on 2018-05-20 21:27:27 +0900 with Markdown engine kramdown (1.13.2) + on 2018-05-21 16:36:00 +0900 with Markdown engine kramdown (1.13.2) using options {} --> @@ -96,10 +96,10 @@ <li>現代のOS では拡張性と信頼性を両立させることが要求されている。 <ul> <li>時代と共にハードウェア、サービスが進歩していき、その度に OS を検証できる必要があるため、拡張性が必要。</li> - <li>OS は非決定的な実行を持ち、従来の OS ではテストしきれない部分が残ってしまうため、信頼性が欠けてしまう。</li> + <li>OS は非決定的な実行を持ち、従来の OS ではテストしきれない部分が残ってしまうため、信頼性が欠けてしまうので信頼性のある OS が必要。</li> </ul> </li> - <li>本研究室では、それらを実現することを目標に Gears OS の開発を行なっている。</li> + <li>本研究室では、拡張性と信頼性を実現することを目標に Gears OS の開発を行なっている。</li> </ul> @@ -121,7 +121,7 @@ <ul> <li>形式化とは仕様、実装、実行を Logic で記述する事である。</li> <li>Gears OS では、継続を使った関数型プログラムとして実装を記述する</li> - <li>Logic としては、依存型関数言語である Agda を使う(前の発表)</li> + <li>Logic としては、依存型関数言語である Agda を使う(外間の発表)</li> <li>証明とモデル検査を使って、信頼性を確保する</li> </ul> @@ -147,7 +147,7 @@ <!-- _S9SLIDE_ --> <h2 id="api">並列API</h2> <ul> - <li>Geas OS 信頼性を保証するために、形式化されたモジュールシステムが必要である。</li> + <li>Geas OS 信頼性を保証するために、モジュールシステムが必要である。</li> <li>本研究では、モジュールシステムとその応用である並列APIについて考察する。</li> <li>並列APIは継続を基本とした関数型プログラミングと両立する必要があり、ここでは CbC の goto 文を拡張した par goto を導入する。</li> </ul> @@ -256,8 +256,19 @@ <div class='slide '> <!-- _S9SLIDE_ --> <h2 id="gears-os-">Gears OS の構造</h2> +<ul> + <li>Gears OS は以下の要素で構成されている + <ul> + <li>Context</li> + <li>TaskQueue</li> + <li>TaskManager</li> + <li>Worker</li> + </ul> + </li> +</ul> + <div style="text-align: center;"> - <img src="./image/gearsos.svg" alt="Gears OS の構造" width="600" /> + <img src="./image/gears_structure.png" alt="Gears OS の構造" width="400" /> </div> @@ -317,6 +328,45 @@ </div> <div class='slide '> <!-- _S9SLIDE_ --> +<h2 id="perl--meta-data-gear-">Perl スクリプトによる Meta Data Gear の生成</h2> + +<pre lang="c"><code>__code code1(struct Context *context, Integer *integer1, Integer *integer2, Integer *output) { + // create context + context->task = NEW(struct Context); + initContext(context->task); + + // set task parameter + context->task->next = C_add; + context->task->idgCount = 2; + context->task->idg = context->task->dataNum; + context->task->maxIdg = context->task->idg + 2; + context->task->odg = context->task->maxIdg; + context->task->maxOdg = context->task->odg + 1; + + // create Data Gear Queue + GET_META(integer1)->wait = createSynchronizedQueue(context); + GET_META(integer2)->wait = createSynchronizedQueue(context); + GET_META(integer3)->wait = createSynchronizedQueue(context); + + // set Input Data Gear + context->task->data[context->task->idg+0] = (union Data*)integer1; + context->task->data[context->task->idg+1] = (union Data*)integer2; + + // set Output Data Gear + context->task->data[context->task->odg+0] = (union Data*)integer3; + + + // set TaskManager->spawns parameter + Gearef(context, TaskManager)->taskList = context->taskList; + Gearef(context, TaskManager)->next1 = C_code2; + goto parGotoMeta(context, C_code2); +} +</code></pre> + + +</div> +<div class='slide '> +<!-- _S9SLIDE_ --> <h2 id="section-2">スライドの流れ</h2> <ul> <li>CbC</li>
--- a/Slide/prosym.md Sun May 20 21:28:30 2018 +0900 +++ b/Slide/prosym.md Mon May 21 17:18:19 2018 +0900 @@ -21,8 +21,8 @@ ## Gears OS - 現代のOS では拡張性と信頼性を両立させることが要求されている。 - 時代と共にハードウェア、サービスが進歩していき、その度に OS を検証できる必要があるため、拡張性が必要。 - - OS は非決定的な実行を持ち、従来の OS ではテストしきれない部分が残ってしまうため、信頼性が欠けてしまう。 -- 本研究室では、それらを実現することを目標に Gears OS の開発を行なっている。 + - OS は非決定的な実行を持ち、従来の OS ではテストしきれない部分が残ってしまうため、信頼性が欠けてしまうので信頼性のある OS が必要。 +- 本研究室では、拡張性と信頼性を実現することを目標に Gears OS の開発を行なっている。 % 欠けてしまうで終わってるので "それら"は 分かりづらい % 並列API 研究目的とAPIとの繋がりがない @@ -51,26 +51,25 @@ ## Gears OS での形式化とInterfaceの導入 - 形式化とは仕様、実装、実行を Logic で記述する事である。 - Gears OS では、継続を使った関数型プログラムとして実装を記述する -- Logic としては、依存型関数言語である Agda を使う(前の発表) +- Logic としては、依存型関数言語である Agda を使う(外間の発表) - 証明とモデル検査を使って、信頼性を確保する ## Gears OS の Interface -- この時、Code Gear と Deta Gear は Interface と呼ばれるまとまり(モジュール)で記述される。 +- Code Gear と Deta Gear は Interface と呼ばれるまとまり(モジュール)で記述される。 - Interface 作成時に Code Gear の集合を指定することにより複数の実装を持つことができる。 - Interface は Data Gear で記述されて、Meta Deta Gear と呼ばれる。 - Java などの Class に相当する。 -- Interface を外から呼び出すための Code Gear 群の型 +% - Interface を外から呼び出すための Code Gear 群の型 - Interface を呼び出す時に必要となる引数を全て格納する Data Gear -- 実装に使う Code Gear の番号が含まれている。 -- Code Gear の番号を変更することによって異なる実装を実現できる +% - 実装に使う Code Gear の番号が含まれている。 +% - Code Gear の番号を変更することによって異なる実装を実現できる % Interface は実行時に実装を入れ替える事ができる % 呼び出すものはStack 上に積めない % Contextも集合 -% Inter ## 並列API -- Geas OS 信頼性を保証するために、形式化されたモジュールシステムが必要である。 +- Geas OS 信頼性を保証するために、モジュールシステムが必要である。 - 本研究では、モジュールシステムとその応用である並列APIについて考察する。 - 並列APIは継続を基本とした関数型プログラミングと両立する必要があり、ここでは CbC の goto 文を拡張した par goto を導入する。 @@ -169,8 +168,14 @@ % - Interface 作成時に Code Gear の集合を指定することにより複数の実装を持つことができる。 ## Gears OS の構造 +- Gears OS は以下の要素で構成されている + - Context + - TaskQueue + - TaskManager + - Worker + <div style="text-align: center;"> - <img src="./image/gearsos.svg" alt="Gears OS の構造" width="600"> + <img src="./image/gears_structure.png" alt="Gears OS の構造" width="400"> </div> @@ -197,6 +202,10 @@ % 複数走ったなかの成功したものをコミットするのがexit +<div style="text-align: center;"> + <img src="./image/gears_structure.png" alt="Gears OS の構造" width="400"> +</div> + @@ -213,6 +222,52 @@ } ``` +## Perl スクリプトによる Meta Data Gear の生成 + + +% Task Manager +% + +```c +__code code1(struct Context *context, Integer *integer1, Integer *integer2, Integer *output) { + // create context + context->task = NEW(struct Context); + initContext(context->task); + + // set task parameter + context->task->next = C_add; + context->task->idgCount = 2; + context->task->idg = context->task->dataNum; + context->task->maxIdg = context->task->idg + 2; + context->task->odg = context->task->maxIdg; + context->task->maxOdg = context->task->odg + 1; + + // create Data Gear Queue + GET_META(integer1)->wait = createSynchronizedQueue(context); + GET_META(integer2)->wait = createSynchronizedQueue(context); + GET_META(integer3)->wait = createSynchronizedQueue(context); + + // set Input Data Gear + context->task->data[context->task->idg+0] = (union Data*)integer1; + context->task->data[context->task->idg+1] = (union Data*)integer2; + + // set Output Data Gear + context->task->data[context->task->odg+0] = (union Data*)integer3; + + + // set TaskManager->spawns parameter + Gearef(context, TaskManager)->taskList = context->taskList; + Gearef(context, TaskManager)->next1 = C_code2; + goto parGotoMeta(context, C_code2); +} +``` +% // add taskList Element +% struct Element* element; +% element = &ALLOCATE(context, Element)->Element; +% element->data = (union Data*)context->task; +% element->next = context->taskList; +% context->taskList = element; + % 失敗した時はmeta compitation で処理する
--- a/Slide/prosym.pdf.html Sun May 20 21:28:30 2018 +0900 +++ b/Slide/prosym.pdf.html Mon May 21 17:18:19 2018 +0900 @@ -70,7 +70,7 @@ <!-- === begin markdown block === generated by markdown/1.2.0 on Ruby 2.4.1 (2017-03-22) [x86_64-darwin15] - on 2018-05-20 21:27:27 +0900 with Markdown engine kramdown (1.13.2) + on 2018-05-21 16:36:00 +0900 with Markdown engine kramdown (1.13.2) using options {} --> @@ -80,10 +80,10 @@ <li>現代のOS では拡張性と信頼性を両立させることが要求されている。 <ul> <li>時代と共にハードウェア、サービスが進歩していき、その度に OS を検証できる必要があるため、拡張性が必要。</li> - <li>OS は非決定的な実行を持ち、従来の OS ではテストしきれない部分が残ってしまうため、信頼性が欠けてしまう。</li> + <li>OS は非決定的な実行を持ち、従来の OS ではテストしきれない部分が残ってしまうため、信頼性が欠けてしまうので信頼性のある OS が必要。</li> </ul> </li> - <li>本研究室では、それらを実現することを目標に Gears OS の開発を行なっている。</li> + <li>本研究室では、拡張性と信頼性を実現することを目標に Gears OS の開発を行なっている。</li> </ul> @@ -105,7 +105,7 @@ <ul> <li>形式化とは仕様、実装、実行を Logic で記述する事である。</li> <li>Gears OS では、継続を使った関数型プログラムとして実装を記述する</li> - <li>Logic としては、依存型関数言語である Agda を使う(前の発表)</li> + <li>Logic としては、依存型関数言語である Agda を使う(外間の発表)</li> <li>証明とモデル検査を使って、信頼性を確保する</li> </ul> @@ -131,7 +131,7 @@ <!-- _S9SLIDE_ --> <h2 id="api">並列API</h2> <ul> - <li>Geas OS 信頼性を保証するために、形式化されたモジュールシステムが必要である。</li> + <li>Geas OS 信頼性を保証するために、モジュールシステムが必要である。</li> <li>本研究では、モジュールシステムとその応用である並列APIについて考察する。</li> <li>並列APIは継続を基本とした関数型プログラミングと両立する必要があり、ここでは CbC の goto 文を拡張した par goto を導入する。</li> </ul> @@ -240,8 +240,19 @@ <div class='slide '> <!-- _S9SLIDE_ --> <h2 id="gears-os-">Gears OS の構造</h2> +<ul> + <li>Gears OS は以下の要素で構成されている + <ul> + <li>Context</li> + <li>TaskQueue</li> + <li>TaskManager</li> + <li>Worker</li> + </ul> + </li> +</ul> + <div style="text-align: center;"> - <img src="./image/gearsos.svg" alt="Gears OS の構造" width="600" /> + <img src="./image/gears_structure.png" alt="Gears OS の構造" width="400" /> </div> @@ -301,6 +312,45 @@ </div> <div class='slide '> <!-- _S9SLIDE_ --> +<h2 id="perl--meta-data-gear-">Perl スクリプトによる Meta Data Gear の生成</h2> + +<pre lang="c"><code>__code code1(struct Context *context, Integer *integer1, Integer *integer2, Integer *output) { + // create context + context->task = NEW(struct Context); + initContext(context->task); + + // set task parameter + context->task->next = C_add; + context->task->idgCount = 2; + context->task->idg = context->task->dataNum; + context->task->maxIdg = context->task->idg + 2; + context->task->odg = context->task->maxIdg; + context->task->maxOdg = context->task->odg + 1; + + // create Data Gear Queue + GET_META(integer1)->wait = createSynchronizedQueue(context); + GET_META(integer2)->wait = createSynchronizedQueue(context); + GET_META(integer3)->wait = createSynchronizedQueue(context); + + // set Input Data Gear + context->task->data[context->task->idg+0] = (union Data*)integer1; + context->task->data[context->task->idg+1] = (union Data*)integer2; + + // set Output Data Gear + context->task->data[context->task->odg+0] = (union Data*)integer3; + + + // set TaskManager->spawns parameter + Gearef(context, TaskManager)->taskList = context->taskList; + Gearef(context, TaskManager)->next1 = C_code2; + goto parGotoMeta(context, C_code2); +} +</code></pre> + + +</div> +<div class='slide '> +<!-- _S9SLIDE_ --> <h2 id="section-2">スライドの流れ</h2> <ul> <li>CbC</li>