Mercurial > hg > Papers > 2018 > tobaru-sigos

comparison Slide/prosym.md @ 3:7f5c0330e711

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add module API
author tobaru
date Sun, 20 May 2018 14:13:00 +0900
parents 60405cc47b3a
children c456e4d68e1a
comparison
equal deleted inserted replaced
2:60405cc47b3a 3:7f5c0330e711
2 author: Mitsuki Miyagi, Yu Tobaru, Shinji Kono 2 author: Mitsuki Miyagi, Yu Tobaru, Shinji Kono
3 profile: 琉球大学 3 profile: 琉球大学
4 lang: Japanese 4 lang: Japanese
5 code-engine: coderay 5 code-engine: coderay
6 6
7 # OS の信頼性 7 % # OS の信頼性
8 - コンピュータの信頼性の基本はメモリなどの資源管理を行う OS である。 8 % - コンピュータの信頼性の基本はメモリなどの資源管理を行う OS である。
9 - OS は非決定的な実行を持つため、OS の信頼性を保証するには、証明を用いる方法とプログラムの可能な実行を全て数え上げるモデル検査を用いる必要がある。 9 % - OS は非決定的な実行を持つため、OS の信頼性を保証するには、証明を用いる方法とプログラムの可能な実行を全て数え上げるモデル検査を用いる必要がある。
10 - 従来のテストとデバッグではテスト仕切れない部分が残ってしまい、不十分。 10 % - 従来のテストとデバッグではテスト仕切れない部分が残ってしまい、不十分。
11 - モデル検査は無限の状態でなくても巨大な状態を調べる事になり、状態を有限に制限したり、状態を抽象化したりする方法が用いられる。 11 % - モデル検査は無限の状態でなくても巨大な状態を調べる事になり、状態を有限に制限したり、状態を抽象化したりする方法が用いられる。
12 %
13 % # OS の拡張性
14 % - 時代とともに進歩するハードウェア、サービスに対応するために OS 自体が拡張される必要がある。
15 % - OS を検証する際にも、1度ではなくアプリケーションやサービス、デバイスが新しくなる毎に検証をやり直す必要がある。
16 %
17 % # OS の拡張性と信頼性の両立
18 % - OSの拡張性と信頼性の観点から、OS は信頼性と拡張性を両立させることが重要であるといえる。
19 % - 本研究室では、OS の信頼性の保証と拡張性を実現することを目標に Gears OS を設計中である。
20
21 # Gears OS
22 - 現代のOS では拡張性と信頼性を両立させることが要求されている。
23 - 時代と共にハードウェア、サービスが進歩していき、その度に OS を検証できる必要があるため、拡張性が必要。
24 - OS は非決定的な実行を持ち、従来の OS ではテストしきれない部分が残ってしまうため、信頼性が欠けてしまう。
25 - 本研究室では、それらを実現することを目標に Gears OS の開発を行なっている。
12 26
13 # OS の拡張性 27 % APIと実装の分離が望ましい理由は？
14 - 時代とともに進歩するハードウェア、サービスに対応するために OS 自体が拡張される必要がある。 28 # API と実装の分離
15 - OS を検証する際にも、1度ではなくアプリケーションやサービス、デバイスが新しくなる毎に検証をやり直す必要がある。 29 - Gears OS は Continuation based C(以下、CbC)によって記述されている。
30 - CbC は Code Gear と Data Gear の単位でプログラムを記述していて、システムやアプリケーションを作る際に、この2つは柔軟に再利用する必要がある。
31 - この時に、機能を接続する API と実装の分離が可能であることが望ましい。
16 32
17 # OS の拡張性と信頼性の両立 33 % 上と繋がってない
18 - OSの拡張性と信頼性の観点から、OS は信頼性と拡張性を両立させることが重要であるといえる。 34 % なんでモジュールシステムが必要？
19 - 本研究室では、OS の信頼性の保証と拡張性を実現することを目標に Gears OS を設計中である。 35 # 並列API
20 - par gotoかAPIの説明まで書く？ 36 - Geas OS 信頼性を保証するために、形式化されたモジュールシステムが必要である。
37 - 本研究では、モジュールシステムとその応用である並列APIについて考察する。
38 - 並列APIは継続を基本とした関数型プログラミングと両立する必要があり、ここでは CbC の goto 文を拡張した par goto を導入する。
21 39
22 # メタ計算 40 # スライドの流れ
41 - <font color="red">CbC</font>
42 - Gears OS における並列実行
43 - 比較
44 - 今後の課題
45
46
47
48
49
50 # CbC
51 - ノーマルレベルとメタレベルの計算を1つの言語で表現できる言語として、本研究室で設計した CbC(Continuation based C) を用いる。
23 - ノーマルレベルの計算 52 - ノーマルレベルの計算
24 - コンピュータの計算はプログラミング言語で計算される。 53 - コンピュータの計算はプログラミング言語で計算される。
25 - その部分をノーマルレベルの計算と呼ぶ。 54 - その部分をノーマルレベルの計算と呼ぶ。
26 - メタレベルの計算 55 - メタレベルの計算
27 - コードが実行される際の以下の部分が、メタレベルの計算という。 56 - コードが実行される際の以下の部分が、メタレベルの計算という。
28 - 処理系の詳細や使用する資源 57 - 処理系の詳細や使用する資源
29 - コードの仕様や型などの言語以外の部分 58 - コードの仕様や型などの言語以外の部分
30 59
31 # CbC 60 # CbC
32 - ノーマルレベルとメタレベルの計算を1つの言語で表現できる言語として、本研究室で設計した CbC(Continuation based C) を用いる。
33 - CbC を用いることで、ノーマルレベルの計算の信頼性をメタレベルから保証できるようになる。 61 - CbC を用いることで、ノーマルレベルの計算の信頼性をメタレベルから保証できるようになる。
34 - CbC は関数呼び出し時の暗黙の環境を使わずに、コードの単位を行き来できる引数付き goto 文を持つ C と互換性のある言語である。
35 - CbC を用いてCode Gear と Data Gear、メタ構造を導入する。 62 - CbC を用いてCode Gear と Data Gear、メタ構造を導入する。
36 63
37 # Gears OS 64 % - 検証には 定理証明支援系である Agda を用いる。
38 - CbC を用いて導入したCode Gear、Data Gear、メタ構造を用いて、検証された Gears OS を構築したい。 65 % - Gears の記述をモジュール化するために Interface を導入した。
39 - 検証には 定理証明支援系である Agda を用いる。 66 % - さらに並列処理の記述用に par goto 構文を導入する。
40 - Gears の記述をモジュール化するために Interface を導入した。
41 - さらに並列処理の記述ように par goto 構文を導入する。
42 67
43 # par goto の実行 68 % # par goto の実行
44 - 本論文では Interface と par goto の実装を記述し、評価を行なった。 69 % - 本論文では Interface と par goto の実装を記述し、評価を行なった。
45 - また、マルチ CPU と GPU 上での par goto 文の実行を確認した。 70 % - また、マルチ CPU と GPU 上での par goto 文の実行を確認した。
46 71
72 # CbC の構文
73 - CbC の Code Gear は __code という型を持つ関数として記述する。
74 - 継続で次の Code Gear に遷移するので、戻り値は持たない。
75 - 遷移は goto 文による継続で処理を行い、引数として入出力を行う。
76 ```c
77 __code cg0(int a, int b) {
78 goto cg1(a+b);
79 }
80 __code cg1(int c) {
81 goto cg2(c);
82 }
83 ```
47 # スライドの流れ 84 # スライドの流れ
48 - <font color="red">Gears OS におけるメタ計算</font> 85 - CbC
49 - Interface 86 - <font color="red">Gears OS における並列実行</font>
50 - Context
51 - Gears OS の並列処理
52 - Synchronized Queue
53 - 並列構文
54 - 比較 87 - 比較
55 - 今後の課題 88 - 今後の課題
56 89
57 # Gears OS におけるメタ計算 90
91 # Gears における並列実行
92 - Gears OS ではメタ計算を柔軟に記述するためのプログラミングの単位として Code Gear と Data Gear を用いる。
93 - それぞれにメタレベルの単位が存在し、Meta Data Gear と Meta Code Gear と呼ぶ。
94 - メタレベルの計算は Perl スクリプトによって生成され、Code Gear で記述される。
95
96 # Interface
97 - この時、Code Gear と Deta Gear は Interface と呼ばれるまとまり(モジュール)で記述される。
98 - Interface 作成時に Code Gear の集合を指定することにより複数の実装を持つことができる。
99
100 # Context
101 - 1つのスレッド内で使われる Interface の Code Gear と Data Gear は Meta Data Gear に格納される。
102 - この Meta Data Gear を Context と呼ぶ。
103 - Context を複製して複数の CPU に割り当てることにより並列実行が可能になる。
104
105 # par goto
106 - Context の複製には par goto を用いる。
107 - 他に、入力の同期、タスクスケジューラへの Context の登録が行われる。
108
109 # Task
110 - Context は Task でもある。
111 - 実行する Code Gear と Data Gear を全て持っている。
112
113 % ここに入る前に __ の説明欲しい
114 # __exit
115 - par goto で生成された Task は __exit に継続することで終了する。
116 - GearsOS の Task は Output Data Gear を生成した時点で終了する。
117 - そのため、par goto では直接 __exit に継続せず、Output Data Gear への書き出し処理に継続される。
118 - Code Gear と Data Gear の依存関係をノーマルレベルで記述できるようになる。
119 ```c
120 __code code1(Integer *integer1, Integer * integer2, Integer *output) {
121 par goto add(integer1, integer2, output, __exit);
122 goto code2();
123 }
124 ```
58 125
59 126
60 # Gaears OS の構成
61 127
62 # Interface 128 % # Interface
63
64 # Context
65 129
66 130
67 # Gears OS の並列処理 131 % # Context
68 132
69 # Synchronized Queue 133 % # 並列構文
70 134
71 # 並列構文 135 # スライドの流れ
136 - CbC
137 - Gears OS における並列実行
138 - <font color="red">比較</font>
139 - 今後の課題
72 140
73 # 比較 141
142 # Gears OS の評価
143 - CPU、GPU環境で Gears OS の測定を行う。
144 - 使用した環境は次のようになる。
145
146 %　表２つ持ってくる
147
148 # Twice
149 - 評価には与えられた整数配列の全ての要素を2倍にする例題である Twice を使う。
150 - Twice では 通信時間を考慮しなければ、CPU より コア数の多い GPU が有利となる。
151 - 要素数2^27のデータに対する Twice の実行結果を示す。
152 - CPU では2^27のデータを64個のデータに分割した。
153 - kernel only は 通信速度を除いた速度である。
154 % グラフ2つ
155
156 # 評価の考察
157 - コア数が上がるごとに、処理速度が上がっている。
158 - GPUでの実行は 32CPU に比べて約7.2倍の速度向上が見られた。
159 - 通信速度を含めると 16CPU より遅い。
160
161 % なんでGo言語？
162 # Go 言語との比較
163 - Go 言語でも Twice を用いた検証を行い、Gears OS との速度比較を行なった。
164
165 % グラフ1つ
166
167 # Go 言語との比較
168 - 1CPU と 32CPU では約4.33倍の速度向上が見られた。
169 - CPU数による速度向上は、Gears OS の方が上だが、処理速度では Go言語の方が速い結果となった。
170
171 # スライドの流れ
172 - CbC
173 - Gears OS における並列実行
174 - 比較
175 - <font color="red">今後の課題</font>
74 176
75 # 今後の課題 177 # 今後の課題
76 178 - Go 言語との比較から 1CPU での動作が遅いことがわかった。
179 - par goto 文を使用することで、Contextを生成し、並列処理を行う。
180 - しかし、Context はメモリ空間の確保や使用する全ての Code Gear Data Gear の設定をする必要があり、生成に時間がかかってしまう事が原因。
181 - 処理が軽い場合は Context を生成しないようなチューニングが必要である。