Mercurial > hg > Papers > 2018 > parusu-master
annotate paper/introduction.tex @ 82:cae61efc3f26
Fix
author | Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 10 Feb 2018 03:01:54 +0900 |
parents | da3b145398a4 |
children |
rev | line source |
---|---|
6 | 1 \chapter{メタ計算を使った並列処理} |
82 | 2 並列処理は現在主流のマルチコアCPU の性能を発揮するには重要なものになっている。 |
50
d916e1313305
Update Chapter1
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
3 しかし、並列処理のプログラミングはスレッド間の共通資源の競合など非決定的な実行を持っており、その信頼性を保証するには従来のテストやデバッグでは不十分であり、テストしきれない部分が残ってしまう。 |
d916e1313305
Update Chapter1
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
4 |
d916e1313305
Update Chapter1
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
5 また、マルチコア CPU 以外にも GPU や CPU と GPU を複合したヘテロジニアスなプロセッサも並列処理をする上で無視できない。 |
d916e1313305
Update Chapter1
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
6 これらのプロセッサで性能を出すためにはアーキテクチャに合わせた並列プログラミングが必要になる。 |
d916e1313305
Update Chapter1
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
7 並列プログラミングフレームワークでは様々なプロセッサを抽象化し、CPU と同等に扱えるようにする柔軟性が求められる。 |
d916e1313305
Update Chapter1
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
8 |
53
4bdffbb885fe
Update chapter1
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
51
diff
changeset
|
9 本研究室では通常の計算をノーマルレベルとし、並列処理の信頼性をノーマルレベルの計算に対して保証し、拡張性をノーマルレベルとは別の階層のメタレベルの計算で実現することを目標に Gears OS\cite{kkb-master}を設計、開発中である。 |
60 | 10 Gears OS では処理を Code Gear、データを Data Gear という単位を用いてプログラムを記述する。 |
11 Code Gear は入力の Input Data Gear が揃ったら実行され、Output Data Gear を出力する。 | |
59 | 12 この Input/Output Data Gear の関係から依存関係を決定し、Input Data Gear が揃った Code Gear が並列に実行される。 |
50
d916e1313305
Update Chapter1
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
13 |
d916e1313305
Update Chapter1
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
14 Gears OS のプログラムの信頼性の確保はモデル検査、検証を使用して行う。 |
d916e1313305
Update Chapter1
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
15 この信頼性のための計算はメタ計算として記述される。 |
59 | 16 このメタ計算は信頼性の他に CPU、GPU などのアーキテクチャに沿った実行環境の切り替え、データの拡張等の拡張性を提供する。 |
60 | 17 メタ計算の処理は Meta Code Gear、Meta Data Gear で表現する。 |
53
4bdffbb885fe
Update chapter1
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
51
diff
changeset
|
18 Meta Code Gear は 通常の Code Gear 間に実行される。 |
6 | 19 |
53
4bdffbb885fe
Update chapter1
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
51
diff
changeset
|
20 従来の研究では OS の実装言語として Python\cite{Sigurbjarnarson:2016:PVF:3026877.3026879} や Haskell\cite{Chen:2015:UCH:2815400.2815402}\cite{Klein:2009:SFV:1629575.1629596} をノーマルレベルとして採用し、メタレベルで検証を行う研究や、メタ計算の実装を型付きアセンブラ(Typed Assembler)\cite{Yang:2010:SLI:1806596.1806610} を用いる例もある。 |
72
d4ced6adca5e
Move stub Interface Code Gear
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
61
diff
changeset
|
21 Gears OS は ノーマルレベルとメタレベルを共通して表現出来る Continuation Based C(CbC)\cite{utah-master} で実装を行い、証明支援系 Agda\cite{agda} を用いて証明を行う。 |
53
4bdffbb885fe
Update chapter1
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
51
diff
changeset
|
22 CbC は Code Gear の単位でプログラムを記述し、軽量継続を用いてコード間を移動する。 |
4bdffbb885fe
Update chapter1
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
51
diff
changeset
|
23 軽量継続は関数呼び出しとは異なり、呼び出し元に戻らないため、呼び出し元の環境を覚えずに行き先のみを指定する。 |
75 | 24 この CbC は C と互換性のある言語で、型付きアセンブラに比べると大きな表現力を提供する。また Haskell などに比べて関数呼び出しではなく軽量継続を採用しているため、スタック上に隠された環境を持たない。 |
25 そのためメタレベルで使用する資源を明確にできる利点がある。 | |
53
4bdffbb885fe
Update chapter1
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
51
diff
changeset
|
26 |
4bdffbb885fe
Update chapter1
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
51
diff
changeset
|
27 Code Gear 間の継続は次の Code Gear の番号と Context という全ての Code Gear と Data Gear を参照できる Meta Data Gear で行われる。 |
4bdffbb885fe
Update chapter1
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
51
diff
changeset
|
28 Context からノーマルレベルのCode Gear へ接続する際は stub Code Gear という Meta Code Gear を用いる。 |
61 | 29 この stub Code Gear はメタレベルの計算であるため、継続先の Code Gear から自動的に生成されるのが望ましい。生成に必要な情報は Code Gear と Data Gear の集まりから得る。 この集まりを Interface\cite{mitsuki-prosym} として定義している。 |
53
4bdffbb885fe
Update chapter1
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
51
diff
changeset
|
30 |
4bdffbb885fe
Update chapter1
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
51
diff
changeset
|
31 Gears OS でのプロセス、スレッドは Context が担う。 |
60 | 32 並列実行する際は新しく Context を生成し、それを CPU、GPU に割り振る事によって実現される。 |
59 | 33 生成された Context には実行する Code Gear と対応する Input/Output Data Gear が登録され、割り振られた先で Context に設定された Code Gear を実行する。 |
34 このContext を用いた並列処理は新規に実行環境を作り、引数を設定するなどの煩雑なメタレベルの処理であり、ノーマルレベルでは Go 言語\cite{go}の goroutine のような簡潔な並列構文があることが望ましい。 | |
50
d916e1313305
Update Chapter1
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
35 |
60 | 36 本研究では Gears OS の基本設計、マルチコアCPU と CUDA による GPUでの実行機構、並列構文を実装し、例題を用いて Gears OS の並列処理の評価を行う。 |
50
d916e1313305
Update Chapter1
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
37 |
d916e1313305
Update Chapter1
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
38 % これはryokka 向きかなぁ |
d916e1313305
Update Chapter1
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
39 |
d916e1313305
Update Chapter1
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
40 %現代の OS では拡張性と信頼性を両立させることが要求されている。 |
d916e1313305
Update Chapter1
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
41 %時代と主に進歩するハードウェア、サービスに対して OS 自体が拡張される必要がある。 |
d916e1313305
Update Chapter1
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
42 %しかし、OSには非決定的な実行を持っており、その信頼性を保証するには従来のテストとデバッグでは不十分であり、テスト仕切れない部分が残ってしまう。 |
d916e1313305
Update Chapter1
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
43 %これに対処するために証明を用いる方法とプログラムの可能な実行をすべて数え上げるモデル検査を用いる方法がある。 |
d916e1313305
Update Chapter1
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
44 % 証明やモデル検査を用いて OS の検証する方法は様々なものが検討されている。 |
d916e1313305
Update Chapter1
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
45 % 型付きアセンブラ\cite{Yang:2010:SLI:1806596.1806610} |
d916e1313305
Update Chapter1
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
46 % 従来の研究ではPython\cite{Sigurbjarnarson:2016:PVF:3026877.3026879} や Haskell\cite{Chen:2015:UCH:2815400.2815402}\cite{Klein:2009:SFV:1629575.1629596}による記述した OS を検証する研究も存在する。 |
d916e1313305
Update Chapter1
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
47 % また SPIN などのモデル検査を OS の検証に用いた例もである。 |
d916e1313305
Update Chapter1
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
48 % 本研究室では信頼性をノーマルレベルの掲載に対して保証し、拡張性をメタレベルの計算で実現することを目標に Gears OS を開発している。 |