Mercurial > hg > Papers > 2018 > tobaru-sigos

comparison Slide/prosym.md @ 7:dfa8973bfe10

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add images
author tobaru
date Sun, 20 May 2018 21:12:40 +0900
parents 94494b3cd38b
children f275411f458d
comparison
equal deleted inserted replaced
6:94494b3cd38b 7:dfa8973bfe10
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 % 12 %
13 % # OS の拡張性 13 % ## OS の拡張性
14 % - 時代とともに進歩するハードウェア、サービスに対応するために OS 自体が拡張される必要がある。 14 % - 時代とともに進歩するハードウェア、サービスに対応するために OS 自体が拡張される必要がある。
15 % - OS を検証する際にも、1度ではなくアプリケーションやサービス、デバイスが新しくなる毎に検証をやり直す必要がある。 15 % - OS を検証する際にも、1度ではなくアプリケーションやサービス、デバイスが新しくなる毎に検証をやり直す必要がある。
16 % 16 %
17 % # OS の拡張性と信頼性の両立 17 % ## OS の拡張性と信頼性の両立
18 % - OSの拡張性と信頼性の観点から、OS は信頼性と拡張性を両立させることが重要であるといえる。 18 % - OSの拡張性と信頼性の観点から、OS は信頼性と拡張性を両立させることが重要であるといえる。
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 ではテストしきれない部分が残ってしまうため、信頼性が欠けてしまう。
25 - 本研究室では、それらを実現することを目標に Gears OS の開発を行なっている。 25 - 本研究室では、それらを実現することを目標に Gears OS の開発を行なっている。
26 26
28 % 並列API 研究目的とAPIとの繋がりがない 28 % 並列API 研究目的とAPIとの繋がりがない
29 % モジュールとAPIの説明分ける 29 % モジュールとAPIの説明分ける
30 % 拡張性と信頼性を実現する時に Interfaceと par goto 構文がなぜ必要なのかに繋げる話が必要 30 % 拡張性と信頼性を実現する時に Interfaceと par goto 構文がなぜ必要なのかに繋げる話が必要
31 % APIと実装の分離が望ましい理由は？ 31 % APIと実装の分離が望ましい理由は？
32 32
33 # API と実装の分離 33 ## API と実装の分離
34 - Gears OS は Continuation based C(以下、CbC)によって記述されている。 34 - Gears OS は Continuation based C(以下、CbC)によって記述されている。
35 - CbC は Code Gear と Data Gear の単位でプログラムを記述していて、システムやアプリケーションを作る際に、この2つは柔軟に再利用する必要がある。 35 - CbC は Code Gear と Data Gear の単位でプログラムを記述していて、システムやアプリケーションを作る際に、この2つは柔軟に再利用する必要がある。
36 - この時に、機能を接続する API と実装の分離が可能であることが望ましい。 36 - この時に、機能を接続する API と実装の分離が可能であることが望ましい。
37 37
38 % 上と繋がってない 38 % 上と繋がってない
46 % その記述にAgdaを使う 46 % その記述にAgdaを使う
47 47
48 % Interfaceはほとんどかかない 48 % Interfaceはほとんどかかない
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 群の型
67 % Interface は実行時に実装を入れ替える事ができる 67 % Interface は実行時に実装を入れ替える事ができる
68 % 呼び出すものはStack 上に積めない 68 % 呼び出すものはStack 上に積めない
69 % Contextも集合 69 % Contextも集合
70 % Inter 70 % Inter
71 71
72 # 並列API 72 ## 並列API
73 - Geas OS 信頼性を保証するために、形式化されたモジュールシステムが必要である。 73 - Geas OS 信頼性を保証するために、形式化されたモジュールシステムが必要である。
74 - 本研究では、モジュールシステムとその応用である並列APIについて考察する。 74 - 本研究では、モジュールシステムとその応用である並列APIについて考察する。
75 - 並列APIは継続を基本とした関数型プログラミングと両立する必要があり、ここでは CbC の goto 文を拡張した par goto を導入する。 75 - 並列APIは継続を基本とした関数型プログラミングと両立する必要があり、ここでは CbC の goto 文を拡張した par goto を導入する。
76 76
77 # スライドの流れ 77 ## スライドの流れ
78 - Interface 78 - Interface
79 - <font color="red">CbC</font> 79 - <font color="red">CbC</font>
80 - Gears OS における並列実行 80 - Gears OS における並列実行
81 - 比較 81 - 比較
82 - 今後の課題 82 - 今後の課題
83 83
84 84
85 85
86 86
87 87
88 # CbC 88 ## CbC
89 - ノーマルレベルとメタレベルの計算を1つの言語で表現できる言語として、本研究室で設計した CbC を用いる。 89 - ノーマルレベルとメタレベルの計算を1つの言語で表現できる言語として、本研究室で設計した CbC を用いる。
90 - ノーマルレベルの計算 90 - ノーマルレベルの計算
91 - コンピュータの計算はプログラミング言語で行われる。 91 - コンピュータの計算はプログラミング言語で行われる。
92 - その部分をノーマルレベルの計算と呼ぶ。 92 - その部分をノーマルレベルの計算と呼ぶ。
93 - メタレベルの計算 93 - メタレベルの計算
104 % OS での資源はCbCでかける 104 % OS での資源はCbCでかける
105 % シミュレーションされた外界 105 % シミュレーションされた外界
106 % シミュレーションされてない外界はOSとは違うのでCbCで書けない 106 % シミュレーションされてない外界はOSとは違うのでCbCで書けない
107 % ぱるすさんの図入れるMeta data Gear 107 % ぱるすさんの図入れるMeta data Gear
108 108
109 109 ## CbC
110 # CbC
111 - CbC を用いることで、ノーマルレベルの計算の信頼性をメタレベルから保証できるようになる。 110 - CbC を用いることで、ノーマルレベルの計算の信頼性をメタレベルから保証できるようになる。
112 - CbC を用いてCode Gear と Data Gear を導入する。 111 - CbC を用いてCode Gear と Data Gear を導入する。
113 112
114 113
115 % - 検証には 定理証明支援系である Agda を用いる。 114 % - 検証には 定理証明支援系である Agda を用いる。
116 % - Gears の記述をモジュール化するために Interface を導入した。 115 % - Gears の記述をモジュール化するために Interface を導入した。
117 % - さらに並列処理の記述用に par goto 構文を導入する。 116 % - さらに並列処理の記述用に par goto 構文を導入する。
118 117
119 % # par goto の実行 118 % ## par goto の実行
120 % - 本論文では Interface と par goto の実装を記述し、評価を行なった。 119 % - 本論文では Interface と par goto の実装を記述し、評価を行なった。
121 % - また、マルチ CPU と GPU 上での par goto 文の実行を確認した。 120 % - また、マルチ CPU と GPU 上での par goto 文の実行を確認した。
122 121
123 % par goto には構文と実行の話がある 122 % par goto には構文と実行の話がある
124 % ストーリー的に早いのでここでは入れない 123 % ストーリー的に早いのでここでは入れない
125 124
126 # CbC の構文 125 ## CbC の構文
127 - CbC の Code Gear は __code という型を持つ関数として記述する。 126 - CbC の Code Gear は __code という型を持つ関数として記述する。
128 - 継続で次の Code Gear に遷移するので、戻り値は持たない。 127 - 継続で次の Code Gear に遷移するので、戻り値は持たない。
129 - 遷移は goto 文による継続で処理を行い、引数として入出力を行う。 128 - 遷移は goto 文による継続で処理を行い、引数として入出力を行う。
130 ```c 129 ```c
131 __code cg0(int a, int b) { 130 __code cg0(int a, int b) {
146 % 形式化はどうするの？-> par goto を使う。 145 % 形式化はどうするの？-> par goto を使う。
147 % par goto を使えば並列実行されたGears の形式化ができる 146 % par goto を使えば並列実行されたGears の形式化ができる
148 147
149 148
150 149
151 # スライドの流れ 150 ## スライドの流れ
152 - CbC 151 - CbC
153 - <font color="red">Gears OS における並列実行</font> 152 - <font color="red">Gears OS における並列実行</font>
154 - 比較 153 - 比較
155 - 今後の課題 154 - 今後の課題
156 155
157 156
158 # Gears における並列実行 157 ## Gears における並列実行
159 - Gears OS ではメタ計算を柔軟に記述するためのプログラミングの単位として Code Gear と Data Gear を用いる。 158 - Gears OS ではメタ計算を柔軟に記述するためのプログラミングの単位として Code Gear と Data Gear を用いる。
160 - それぞれにメタレベルの単位が存在し、Meta Data Gear と Meta Code Gear と呼ぶ。 159 - それぞれにメタレベルの単位が存在し、Meta Data Gear と Meta Code Gear と呼ぶ。
161 - メタレベルの計算は Perl スクリプトによって生成され、Code Gear で記述される。 160 - メタレベルの計算は Perl スクリプトによって生成され、Code Gear で記述される。
162 161 <div style="text-align: center;">
163 % # Interface 162 <img src="./image/meta_cg_dg.svg" alt="Gears OS の構造" width="700">
163 </div>
164
165
166
167 % ## Interface
164 % - この時、Code Gear と Deta Gear は Interface と呼ばれるまとまり(モジュール)で記述される。 168 % - この時、Code Gear と Deta Gear は Interface と呼ばれるまとまり(モジュール)で記述される。
165 % - Interface 作成時に Code Gear の集合を指定することにより複数の実装を持つことができる。 169 % - Interface 作成時に Code Gear の集合を指定することにより複数の実装を持つことができる。
166 170
167 # Context 171 ## Gears OS の構造
172 <div style="text-align: center;">
173 <img src="./image/gearsos.svg" alt="Gears OS の構造" width="700">
174 </div>
175
176
177 ## Context
168 - 1つのスレッド内で使われる Interface の Code Gear と Data Gear は Meta Data Gear に格納される。 178 - 1つのスレッド内で使われる Interface の Code Gear と Data Gear は Meta Data Gear に格納される。
169 - この Meta Data Gear を Context と呼ぶ。 179 - この Meta Data Gear を Context と呼ぶ。
170 - Context を複製して複数の CPU に割り当てることにより並列実行が可能になる。 180 - Context を複製して複数の CPU に割り当てることにより並列実行が可能になる。
171 - Context は Task でもある。 181 - Context は Task でもある。
172 - Task は実行する Code Gear と Data Gear を全て持っている。 182 - Task は実行する Code Gear と Data Gear を全て持っている。
173 183
174 # par goto 184 ## par goto
175 - Context の複製には par goto を用いる。 185 - Context の複製には par goto を用いる。
176 - 他に、入力の同期、タスクスケジューラへの Context の登録が行われる。 186 - 他に、入力の同期、タスクスケジューラへの Context の登録が行われる。
177 187
178 % exit が説明不足 188 % exit が説明不足
179 % code gear の実行は他のシープに邪魔されない。 189 % code gear の実行は他のシープに邪魔されない。
180 % 並列実行時の書き換えは許してない 190 % 並列実行時の書き換えは許してない
181 191
182 # 1つの Code Gear の実行は他の Code Gear に割り込まれない 192 ## 1つの Code Gear の実行は他の Code Gear に割り込まれない
183 - 共有された Data Gear があった時に、それに対する変更はただ1つの Code Gear だけが許される 193 - 共有された Data Gear があった時に、それに対する変更はただ1つの Code Gear だけが許される
184 - 読み込みは複数であってもいい 194 - 読み込みは複数であってもいい
185 - Agda 側で、並列実行を Code Gear の順次実行としてシミュレーションするため 195 - Agda 側で、並列実行を Code Gear の順次実行としてシミュレーションするため
186 - このような実行になるように Gears OS の実装を行う 196 - このような実行になるように Gears OS の実装を行う
187 197
188 % 複数走ったなかの成功したものをコミットするのがexit 198 % 複数走ったなかの成功したものをコミットするのがexit
189 199
190 200
191 201
192 202
193 # __exit 203 ## __exit
194 - 複数実行した時に、共有 Data Gear に書き込みを成功したかを確認する(commit) 204 - 複数実行した時に、共有 Data Gear に書き込みを成功したかを確認する(commit)
195 - par goto で生成された Task は __exit に継続することで終了する 205 - par goto で生成された Task は __exit に継続することで終了する
196 - GearsOS の Task は Output Data Gear を生成した時点で終了する 206 - GearsOS の Task は Output Data Gear を生成した時点で終了する
197 - そのため、par goto では直接 __exit に継続せず、Output Data Gear への書き出し処理に継続される。 207 - そのため、par goto では直接 __exit に継続せず、Output Data Gear への書き出し処理に継続される。
198 - Code Gear と Data Gear の依存関係をノーマルレベルで記述できるようになる。 208 - Code Gear と Data Gear の依存関係をノーマルレベルで記述できるようになる。
205 215
206 % 失敗した時はmeta compitation で処理する 216 % 失敗した時はmeta compitation で処理する
207 217
208 218
209 219
210 % # Interface 220 % ## Interface
211 221
212 222
213 % # Context 223 % ## Context
214 224
215 % # 並列構文 225 % ## 並列構文
216 226
217 # スライドの流れ 227 ## スライドの流れ
218 - CbC 228 - CbC
219 - Gears OS における並列実行 229 - Gears OS における並列実行
220 - <font color="red">比較</font> 230 - <font color="red">比較</font>
221 - 今後の課題 231 - 今後の課題
222 232
223 # Gears OS の評価(目的) 233 ## Gears OS の評価(目的)
224 - 並列構文とそれを実現する Meta Compitation が十分に揃っているかを確認したい 234 - 並列構文とそれを実現する Meta Compitation が十分に揃っているかを確認したい
225 - 並列処理の台数効果を確認する 235 - 並列処理の台数効果を確認する
226 - 既存の並列言語と比較して不要なオーバーヘッドがあるか調べたい 236 - 既存の並列言語と比較して不要なオーバーヘッドがあるか調べたい
227 237
228 # Gears OS の評価(環境) 238 ## Gears OS の評価(環境)
229 - CPU、GPU環境で Gears OS の測定を行う。 239 - CPU、GPU環境で Gears OS の測定を行う。
230 - 使用した環境は次のようになる。 240 - 使用した環境は次のようになる。
231 - CPU 環境 241 - CPU 環境
232 - Model : Dell PowerEdgeR630 242 - Model : Dell PowerEdgeR630
233 - Memory : 768GB 243 - Memory : 768GB
236 - GPU : GeForce GTX 1070 246 - GPU : GeForce GTX 1070
237 - Cores : 1920 247 - Cores : 1920
238 - ClockSpeed : 1683MHZ 248 - ClockSpeed : 1683MHZ
239 - Memory Size : 8GB GDDR5 249 - Memory Size : 8GB GDDR5
240 250
241 # Twice 251 ## Twice
242 - 評価には与えられた整数配列の全ての要素を2倍にする例題である Twice を使う。 252 - 評価には与えられた整数配列の全ての要素を2倍にする例題である Twice を使う。
243 - Twice では 通信時間を考慮しなければ、CPU より コア数の多い GPU が有利となる。 253 - Twice では 通信時間を考慮しなければ、CPU より コア数の多い GPU が有利となる。
244 - 要素数2^27のデータに対する Twice の実行結果を示す。 254 - 要素数2^27のデータに対する Twice の実行結果を示す。
245 - CPU では2^27のデータを64個のデータに分割した。 255 - CPU では2^27のデータを64個のデータに分割した。
246 - kernel only は 通信速度を除いた速度である。 256 - kernel only は 通信速度を除いた速度である。
284 <td style="text-align: right;">6.018</td> 294 <td style="text-align: right;">6.018</td>
285 </tr> 295 </tr>
286 </tbody> 296 </tbody>
287 </table> 297 </table>
288 298
289 # 評価の考察 299 ## 評価の考察
290 - コア数が上がるごとに、処理速度が上がっている。 300 - コア数が上がるごとに、処理速度が上がっている。
291 - GPUでの実行は 32CPU に比べて約7.2倍の速度向上が見られた。 301 - GPUでの実行は 32CPU に比べて約7.2倍の速度向上が見られた。
292 - 通信速度を含めると 16CPU より遅い。 302 - 通信速度を含めると 16CPU より遅い。
293 303
294 % なんでGo言語？ 304 % なんでGo言語？
295 # Go 言語との比較 305 ## Go 言語との比較
296 - Go 言語でも Twice を用いた検証を行い、Gears OS との速度比較を行なった。 306 - Go 言語でも Twice を用いた検証を行い、Gears OS との速度比較を行なった。
297 - 1CPU と 32CPU では約4.33倍の速度向上が見られた。 307 - 1CPU と 32CPU では約4.33倍の速度向上が見られた。
298 - CPU数による速度向上は、Gears OS の方が上だが、処理速度では Go言語の方が速い結果となった。 308 - CPU数による速度向上は、Gears OS の方が上だが、処理速度では Go言語の方が速い結果となった。
299 <div style="text-align: center;"> 309 <div style="text-align: center;">
300 <img src="./image/vsgo.svg" alt="message" width="500"> 310 <img src="./image/vsgo.svg" alt="Goとの比較" width="500">
301 </div> 311 </div>
302 312
303 313
304 # スライドの流れ 314 ## スライドの流れ
305 - CbC 315 - CbC
306 - Gears OS における並列実行 316 - Gears OS における並列実行
307 - 比較 317 - 比較
308 - <font color="red">今後の課題</font> 318 - <font color="red">今後の課題</font>
309 319
310 # 今後の課題 320 ## 今後の課題
311 - Go 言語との比較から 1CPU での動作が遅いことがわかった。 321 - Go 言語との比較から 1CPU での動作が遅いことがわかった。
312 - par goto 文を使用することで、Contextを生成し、並列処理を行う。 322 - par goto 文を使用することで、Contextを生成し、並列処理を行う。
313 - しかし、Context はメモリ空間の確保や使用する全ての Code Gear Data Gear の設定をする必要があり、生成に時間がかかってしまう事が原因。 323 - しかし、Context はメモリ空間の確保や使用する全ての Code Gear Data Gear の設定をする必要があり、生成に時間がかかってしまう事が原因。
314 - 処理が軽い場合は Context を生成しないようなチューニングが必要である。 324 - 処理が軽い場合は Context を生成しないようなチューニングが必要である。