# HG changeset patch # User tobaru # Date 1526793180 -32400 # Node ID 7f5c0330e711d9cb5336adfb8a11d347796e97c9 # Parent 60405cc47b3a451d860fbaca695373f6f743dd1d add module API diff -r 60405cc47b3a -r 7f5c0330e711 Slide/prosym.html --- a/Slide/prosym.html Tue May 15 19:47:01 2018 +0900 +++ b/Slide/prosym.html Sun May 20 14:13:00 2018 +0900 @@ -86,49 +86,65 @@ -

OS の信頼性

+

Gears OS

-

OS の拡張性

+

API と実装の分離

-

OS の拡張性と信頼性の両立

+

並列API

-

メタ計算

+

スライドの流れ

+ + +
+
+ +

CbC

+
-

CbC

+

CbC

@@ -163,39 +177,105 @@
-

Gears OS

+

CbC の構文

+ +
__code cg0(int a, int b) {
+    goto cg1(a+b);
+}
+__code cg1(int c) {
+    goto cg2(c);
+}
+
+

# スライドの流れ +- CbC +- Gears OS における並列実行 +- 比較 +- 今後の課題

+ + +
+
+ +

Gears における並列実行

+ + +
+
+ +

Interface

+
-

par goto の実行

+

Context

+ + + +
+
+ +

par goto

+ + +
+
+ +

Task

+
+

__exit

+ +
__code code1(Integer *integer1, Integer * integer2, Integer *output) {
+    par goto add(integer1, integer2, output, __exit);
+    goto code2();
+}
+
+ + +
+
+

スライドの流れ

@@ -203,56 +283,83 @@
-

Gears OS におけるメタ計算

+

Gears OS の評価

+
-

Gaears OS の構成

- - -
-
- -

Interface

+

Twice

+
-

Context

+

評価の考察

+
-

Gears OS の並列処理

+

Go 言語との比較

+
-

Synchronized Queue

+

Go 言語との比較

+
-

並列構文

- - -
-
- -

比較

+

スライドの流れ

+

今後の課題

- +
diff -r 60405cc47b3a -r 7f5c0330e711 Slide/prosym.md --- a/Slide/prosym.md Tue May 15 19:47:01 2018 +0900 +++ b/Slide/prosym.md Sun May 20 14:13:00 2018 +0900 @@ -4,22 +4,51 @@ lang: Japanese code-engine: coderay -# OS の信頼性 -- コンピュータの信頼性の基本はメモリなどの資源管理を行う OS である。 -- OS は非決定的な実行を持つため、OS の信頼性を保証するには、証明を用いる方法とプログラムの可能な実行を全て数え上げるモデル検査を用いる必要がある。 - - 従来のテストとデバッグではテスト仕切れない部分が残ってしまい、不十分。 - - モデル検査は無限の状態でなくても巨大な状態を調べる事になり、状態を有限に制限したり、状態を抽象化したりする方法が用いられる。 +% # OS の信頼性 +% - コンピュータの信頼性の基本はメモリなどの資源管理を行う OS である。 +% - OS は非決定的な実行を持つため、OS の信頼性を保証するには、証明を用いる方法とプログラムの可能な実行を全て数え上げるモデル検査を用いる必要がある。 +% - 従来のテストとデバッグではテスト仕切れない部分が残ってしまい、不十分。 +% - モデル検査は無限の状態でなくても巨大な状態を調べる事になり、状態を有限に制限したり、状態を抽象化したりする方法が用いられる。 +% +% # OS の拡張性 +% - 時代とともに進歩するハードウェア、サービスに対応するために OS 自体が拡張される必要がある。 +% - OS を検証する際にも、1度ではなくアプリケーションやサービス、デバイスが新しくなる毎に検証をやり直す必要がある。 +% +% # OS の拡張性と信頼性の両立 +% - OSの拡張性と信頼性の観点から、OS は信頼性と拡張性を両立させることが重要であるといえる。 +% - 本研究室では、OS の信頼性の保証と拡張性を実現することを目標に Gears OS を設計中である。 + +# Gears OS +- 現代のOS では拡張性と信頼性を両立させることが要求されている。 + - 時代と共にハードウェア、サービスが進歩していき、その度に OS を検証できる必要があるため、拡張性が必要。 + - OS は非決定的な実行を持ち、従来の OS ではテストしきれない部分が残ってしまうため、信頼性が欠けてしまう。 +- 本研究室では、それらを実現することを目標に Gears OS の開発を行なっている。 -# OS の拡張性 -- 時代とともに進歩するハードウェア、サービスに対応するために OS 自体が拡張される必要がある。 -- OS を検証する際にも、1度ではなくアプリケーションやサービス、デバイスが新しくなる毎に検証をやり直す必要がある。 +% APIと実装の分離が望ましい理由は？ +# API と実装の分離 +- Gears OS は Continuation based C(以下、CbC)によって記述されている。 +- CbC は Code Gear と Data Gear の単位でプログラムを記述していて、システムやアプリケーションを作る際に、この2つは柔軟に再利用する必要がある。 +- この時に、機能を接続する API と実装の分離が可能であることが望ましい。 + +% 上と繋がってない +% なんでモジュールシステムが必要？ +# 並列API +- Geas OS 信頼性を保証するために、形式化されたモジュールシステムが必要である。 +- 本研究では、モジュールシステムとその応用である並列APIについて考察する。 +- 並列APIは継続を基本とした関数型プログラミングと両立する必要があり、ここでは CbC の goto 文を拡張した par goto を導入する。 -# OS の拡張性と信頼性の両立 -- OSの拡張性と信頼性の観点から、OS は信頼性と拡張性を両立させることが重要であるといえる。 -- 本研究室では、OS の信頼性の保証と拡張性を実現することを目標に Gears OS を設計中である。 -- par gotoかAPIの説明まで書く？ +# スライドの流れ +- CbC +- Gears OS における並列実行 +- 比較 +- 今後の課題 -# メタ計算 + + + + +# CbC +- ノーマルレベルとメタレベルの計算を1つの言語で表現できる言語として、本研究室で設計した CbC(Continuation based C) を用いる。 - ノーマルレベルの計算 - コンピュータの計算はプログラミング言語で計算される。 - その部分をノーマルレベルの計算と呼ぶ。 @@ -29,48 +58,124 @@ - コードの仕様や型などの言語以外の部分 # CbC -- ノーマルレベルとメタレベルの計算を1つの言語で表現できる言語として、本研究室で設計した CbC(Continuation based C) を用いる。 - CbC を用いることで、ノーマルレベルの計算の信頼性をメタレベルから保証できるようになる。 -- CbC は関数呼び出し時の暗黙の環境を使わずに、コードの単位を行き来できる引数付き goto 文を持つ C と互換性のある言語である。 - CbC を用いてCode Gear と Data Gear、メタ構造を導入する。 -# Gears OS -- CbC を用いて導入したCode Gear、Data Gear、メタ構造を用いて、検証された Gears OS を構築したい。 -- 検証には 定理証明支援系である Agda を用いる。 -- Gears の記述をモジュール化するために Interface を導入した。 -- さらに並列処理の記述ように par goto 構文を導入する。 +% - 検証には 定理証明支援系である Agda を用いる。 +% - Gears の記述をモジュール化するために Interface を導入した。 +% - さらに並列処理の記述用に par goto 構文を導入する。 + +% # par goto の実行 +% - 本論文では Interface と par goto の実装を記述し、評価を行なった。 +% - また、マルチ CPU と GPU 上での par goto 文の実行を確認した。 -# par goto の実行 -- 本論文では Interface と par goto の実装を記述し、評価を行なった。 -- また、マルチ CPU と GPU 上での par goto 文の実行を確認した。 - +# CbC の構文 +- CbC の Code Gear は __code という型を持つ関数として記述する。 +- 継続で次の Code Gear に遷移するので、戻り値は持たない。 +- 遷移は goto 文による継続で処理を行い、引数として入出力を行う。 +```c +__code cg0(int a, int b) { + goto cg1(a+b); +} +__code cg1(int c) { + goto cg2(c); +} +``` # スライドの流れ -- Gears OS におけるメタ計算 -- Interface -- Context -- Gears OS の並列処理 -- Synchronized Queue -- 並列構文 +- CbC +- Gears OS における並列実行 - 比較 - 今後の課題 -# Gears OS におけるメタ計算 + +# Gears における並列実行 +- Gears OS ではメタ計算を柔軟に記述するためのプログラミングの単位として Code Gear と Data Gear を用いる。 +- それぞれにメタレベルの単位が存在し、Meta Data Gear と Meta Code Gear と呼ぶ。 +- メタレベルの計算は Perl スクリプトによって生成され、Code Gear で記述される。 + +# Interface +- この時、Code Gear と Deta Gear は Interface と呼ばれるまとまり(モジュール)で記述される。 +- Interface 作成時に Code Gear の集合を指定することにより複数の実装を持つことができる。 + +# Context +- 1つのスレッド内で使われる Interface の Code Gear と Data Gear は Meta Data Gear に格納される。 +- この Meta Data Gear を Context と呼ぶ。 +- Context を複製して複数の CPU に割り当てることにより並列実行が可能になる。 + +# par goto +- Context の複製には par goto を用いる。 +- 他に、入力の同期、タスクスケジューラへの Context の登録が行われる。 + +# Task +- Context は Task でもある。 +- 実行する Code Gear と Data Gear を全て持っている。 + +% ここに入る前に __ の説明欲しい +# __exit +- par goto で生成された Task は __exit に継続することで終了する。 +- GearsOS の Task は Output Data Gear を生成した時点で終了する。 +- そのため、par goto では直接 __exit に継続せず、Output Data Gear への書き出し処理に継続される。 +- Code Gear と Data Gear の依存関係をノーマルレベルで記述できるようになる。 +```c +__code code1(Integer *integer1, Integer * integer2, Integer *output) { + par goto add(integer1, integer2, output, __exit); + goto code2(); +} +``` -# Gaears OS の構成 -# Interface - -# Context +% # Interface -# Gears OS の並列処理 +% # Context + +% # 並列構文 -# Synchronized Queue +# スライドの流れ +- CbC +- Gears OS における並列実行 +- 比較 +- 今後の課題 + + +# Gears OS の評価 +- CPU、GPU環境で Gears OS の測定を行う。 +- 使用した環境は次のようになる。 + +%　表２つ持ってくる -# 並列構文 +# Twice +- 評価には与えられた整数配列の全ての要素を2倍にする例題である Twice を使う。 +- Twice では 通信時間を考慮しなければ、CPU より コア数の多い GPU が有利となる。 +- 要素数2^27のデータに対する Twice の実行結果を示す。 + - CPU では2^27のデータを64個のデータに分割した。 + - kernel only は 通信速度を除いた速度である。 +% グラフ2つ + +# 評価の考察 +- コア数が上がるごとに、処理速度が上がっている。 +- GPUでの実行は 32CPU に比べて約7.2倍の速度向上が見られた。 +- 通信速度を含めると 16CPU より遅い。 -# 比較 +% なんでGo言語？ +# Go 言語との比較 +- Go 言語でも Twice を用いた検証を行い、Gears OS との速度比較を行なった。 + +% グラフ1つ + +# Go 言語との比較 +- 1CPU と 32CPU では約4.33倍の速度向上が見られた。 +- CPU数による速度向上は、Gears OS の方が上だが、処理速度では Go言語の方が速い結果となった。 + +# スライドの流れ +- CbC +- Gears OS における並列実行 +- 比較 +- 今後の課題 # 今後の課題 - +- Go 言語との比較から 1CPU での動作が遅いことがわかった。 +- par goto 文を使用することで、Contextを生成し、並列処理を行う。 +- しかし、Context はメモリ空間の確保や使用する全ての Code Gear Data Gear の設定をする必要があり、生成に時間がかかってしまう事が原因。 +- 処理が軽い場合は Context を生成しないようなチューニングが必要である。 diff -r 60405cc47b3a -r 7f5c0330e711 Slide/prosym.pdf.html --- a/Slide/prosym.pdf.html Tue May 15 19:47:01 2018 +0900 +++ b/Slide/prosym.pdf.html Sun May 20 14:13:00 2018 +0900 @@ -70,49 +70,65 @@ -

OS の信頼性

+

Gears OS

-

OS の拡張性

+

API と実装の分離

-

OS の拡張性と信頼性の両立

+

並列API

-

メタ計算

+

スライドの流れ

+ + +
+
+ +

CbC

+
-

CbC

+

CbC

@@ -147,39 +161,105 @@
-

Gears OS

+

CbC の構文

+ +
__code cg0(int a, int b) {
+    goto cg1(a+b);
+}
+__code cg1(int c) {
+    goto cg2(c);
+}
+
+

# スライドの流れ +- CbC +- Gears OS における並列実行 +- 比較 +- 今後の課題

+ + +
+
+ +

Gears における並列実行

+ + +
+
+ +

Interface

+
-

par goto の実行

+

Context

+ + + +
+
+ +

par goto

+ + +
+
+ +

Task

+
+

__exit

+ +
__code code1(Integer *integer1, Integer * integer2, Integer *output) {
+    par goto add(integer1, integer2, output, __exit);
+    goto code2();
+}
+
+ + +
+
+

スライドの流れ

@@ -187,56 +267,83 @@
-

Gears OS におけるメタ計算

+

Gears OS の評価

+
-

Gaears OS の構成

- - -
-
- -

Interface

+

Twice

+
-

Context

+

評価の考察

+
-

Gears OS の並列処理

+

Go 言語との比較

+
-

Synchronized Queue

+

Go 言語との比較

+
-

並列構文

- - -
-
- -

比較

+

スライドの流れ

+

今後の課題

- +
diff -r 60405cc47b3a -r 7f5c0330e711 sigos.mm --- a/sigos.mm Tue May 15 19:47:01 2018 +0900 +++ b/sigos.mm Sun May 20 14:13:00 2018 +0900 @@ -1,6 +1,6 @@ - + @@ -15,5 +15,13 @@ + + + + + + + +