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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
6
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 \chapter{メタ計算を使った並列処理}
82
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
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
842a8e04f5b1 Replace space
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
10 Gears OS では処理を Code Gear、データを Data Gear という単位を用いてプログラムを記述する。
842a8e04f5b1 Replace space
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
11 Code Gear は入力の Input Data Gear が揃ったら実行され、Output Data Gear を出力する。
59
ed207d6c511a Add abstract
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents: 55
diff changeset
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
ed207d6c511a Add abstract
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents: 55
diff changeset
16 このメタ計算は信頼性の他に CPU、GPU などのアーキテクチャに沿った実行環境の切り替え、データの拡張等の拡張性を提供する。
60
842a8e04f5b1 Replace space
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
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
106c1d35afd2 Add tex files
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
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
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
24 この CbC は C と互換性のある言語で、型付きアセンブラに比べると大きな表現力を提供する。また Haskell などに比べて関数呼び出しではなく軽量継続を採用しているため、スタック上に隠された環境を持たない。
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents: 72
diff changeset
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
a56f85c0bf90 Fix cite
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
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
842a8e04f5b1 Replace space
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
32 並列実行する際は新しく Context を生成し、それを CPU、GPU に割り振る事によって実現される。
59
ed207d6c511a Add abstract
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents: 55
diff changeset
33 生成された Context には実行する Code Gear と対応する Input/Output Data Gear が登録され、割り振られた先で Context に設定された Code Gear を実行する。
ed207d6c511a Add abstract
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents: 55
diff changeset
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
842a8e04f5b1 Replace space
Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
parents: 59
diff changeset
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 を開発している。