# HG changeset patch
# User tobaru
# Date 1526818360 -32400
# Node ID dfa8973bfe1004ac8f27391a2149f393ec5a9c66
# Parent 94494b3cd38b9535abfebc21e209793d95eb19f4
add images
diff -r 94494b3cd38b -r dfa8973bfe10 Slide/image/env.pdf
Binary file Slide/image/env.pdf has changed
diff -r 94494b3cd38b -r dfa8973bfe10 Slide/image/env1.pdf
Binary file Slide/image/env1.pdf has changed
diff -r 94494b3cd38b -r dfa8973bfe10 Slide/image/env1_1.pdf
Binary file Slide/image/env1_1.pdf has changed
diff -r 94494b3cd38b -r dfa8973bfe10 Slide/image/env2.pdf
Binary file Slide/image/env2.pdf has changed
diff -r 94494b3cd38b -r dfa8973bfe10 Slide/image/env3.pdf
Binary file Slide/image/env3.pdf has changed
diff -r 94494b3cd38b -r dfa8973bfe10 Slide/image/gearsos.svg
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Slide/image/gearsos.svg Sun May 20 21:12:40 2018 +0900
@@ -0,0 +1,581 @@
+
+
diff -r 94494b3cd38b -r dfa8973bfe10 Slide/image/meta_cg_dg.svg
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Slide/image/meta_cg_dg.svg Sun May 20 21:12:40 2018 +0900
@@ -0,0 +1,247 @@
+
+
diff -r 94494b3cd38b -r dfa8973bfe10 Slide/prosym.html
--- a/Slide/prosym.html Sun May 20 18:45:11 2018 +0900
+++ b/Slide/prosym.html Sun May 20 21:12:40 2018 +0900
@@ -86,12 +86,12 @@
-Gears OS
+Gears OS
- 現代のOS では拡張性と信頼性を両立させることが要求されている。
@@ -106,7 +106,7 @@
-
API と実装の分離
+
API と実装の分離
- Gears OS は Continuation based C(以下、CbC)によって記述されている。
- CbC は Code Gear と Data Gear の単位でプログラムを記述していて、システムやアプリケーションを作る際に、この2つは柔軟に再利用する必要がある。
@@ -117,7 +117,35 @@
-
並列API
+
Gears OS での形式化とInterfaceの導入
+
+ - 形式化とは仕様、実装、実行を Logic で記述する事である。
+ - Gears OS では、継続を使った関数型プログラムとして実装を記述する
+ - Logic としては、依存型関数言語である Agda を使う(前の発表)
+ - 証明とモデル検査を使って、信頼性を確保する
+
+
+
+
+
+
Gears OS の Interface
+
+ - この時、Code Gear と Deta Gear は Interface と呼ばれるまとまり(モジュール)で記述される。
+ - Interface 作成時に Code Gear の集合を指定することにより複数の実装を持つことができる。
+ - Interface は Data Gear で記述されて、Meta Deta Gear と呼ばれる。
+ - Java などの Class に相当する。
+ - Interface を外から呼び出すための Code Gear 群の型
+ - Interface を呼び出す時に必要となる引数を全て格納する Data Gear
+ - 実装に使う Code Gear の番号が含まれている。
+ - Code Gear の番号を変更することによって異なる実装を実現できる
+
+
+
+
+
+
並列API
- Geas OS 信頼性を保証するために、形式化されたモジュールシステムが必要である。
- 本研究では、モジュールシステムとその応用である並列APIについて考察する。
@@ -128,8 +156,9 @@
-
スライドの流れ
+
スライドの流れ
+ - Interface
-
CbC
@@ -142,7 +171,7 @@
-
CbC
+
CbC
- ノーマルレベルとメタレベルの計算を1つの言語で表現できる言語として、本研究室で設計した CbC を用いる。
- ノーマルレベルの計算
@@ -156,7 +185,7 @@
- コードが実行される際の以下の部分が、メタレベルの計算という。
- 処理系の詳細や使用する資源
- - コードの仕様や型などの言語以外の部分
+ - コードの仕様や型などの部分
@@ -167,17 +196,17 @@
-
CbC
+
CbC
- CbC を用いることで、ノーマルレベルの計算の信頼性をメタレベルから保証できるようになる。
- - CbC を用いてCode Gear と Data Gear、メタ構造を導入する。
+ - CbC を用いてCode Gear と Data Gear を導入する。
-
CbC の構文
+
CbC の構文
- CbC の Code Gear は __code という型を持つ関数として記述する。
- 継続で次の Code Gear に遷移するので、戻り値は持たない。
@@ -190,12 +219,15 @@
goto cg2(c);
}
+
-
スライドの流れ
+
スライドの流れ
- CbC
-
@@ -209,39 +241,43 @@
-
Gears における並列実行
+
Gears における並列実行
- Gears OS ではメタ計算を柔軟に記述するためのプログラミングの単位として Code Gear と Data Gear を用いる。
- それぞれにメタレベルの単位が存在し、Meta Data Gear と Meta Code Gear と呼ぶ。
- メタレベルの計算は Perl スクリプトによって生成され、Code Gear で記述される。
+
+
+
+
+
+
+
+
Gears OS の構造
+
+
+
+
+
+
+
+
Context
+
+ - 1つのスレッド内で使われる Interface の Code Gear と Data Gear は Meta Data Gear に格納される。
+ - この Meta Data Gear を Context と呼ぶ。
+ - Context を複製して複数の CPU に割り当てることにより並列実行が可能になる。
+ - Context は Task でもある。
+ - Task は実行する Code Gear と Data 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
+
par goto
- Context の複製には par goto を用いる。
- 他に、入力の同期、タスクスケジューラへの Context の登録が行われる。
@@ -251,20 +287,23 @@
-
Task
+
1つの Code Gear の実行は他の Code Gear に割り込まれない
- - Context は Task でもある。
- - 実行する Code Gear と Data Gear を全て持っている。
+ - 共有された Data Gear があった時に、それに対する変更はただ1つの Code Gear だけが許される
+ - 読み込みは複数であってもいい
+ - Agda 側で、並列実行を Code Gear の順次実行としてシミュレーションするため
+ - このような実行になるように Gears OS の実装を行う
-
__exit
+
__exit
- - par goto で生成された Task は __exit に継続することで終了する。
- - GearsOS の Task は Output Data Gear を生成した時点で終了する。
+ - 複数実行した時に、共有 Data Gear に書き込みを成功したかを確認する(commit)
+ - par goto で生成された Task は __exit に継続することで終了する
+ - GearsOS の Task は Output Data Gear を生成した時点で終了する
- そのため、par goto では直接 __exit に継続せず、Output Data Gear への書き出し処理に継続される。
- Code Gear と Data Gear の依存関係をノーマルレベルで記述できるようになる。
@@ -278,7 +317,7 @@
-
スライドの流れ
+
スライドの流れ
- CbC
- Gears OS における並列実行
@@ -292,7 +331,18 @@
-
Gears OS の評価
+
Gears OS の評価(目的)
+
+ - 並列構文とそれを実現する Meta Compitation が十分に揃っているかを確認したい
+ - 並列処理の台数効果を確認する
+ - 既存の並列言語と比較して不要なオーバーヘッドがあるか調べたい
+
+
+
+
+
+
Gears OS の評価(環境)
- CPU、GPU環境で Gears OS の測定を行う。
- 使用した環境は次のようになる。
@@ -320,7 +370,7 @@
-
Twice
+
Twice
- 評価には与えられた整数配列の全ての要素を2倍にする例題である Twice を使う。
- Twice では 通信時間を考慮しなければ、CPU より コア数の多い GPU が有利となる。
@@ -377,7 +427,7 @@
-
評価の考察
+
評価の考察
- コア数が上がるごとに、処理速度が上がっている。
- GPUでの実行は 32CPU に比べて約7.2倍の速度向上が見られた。
@@ -388,21 +438,21 @@
-
Go 言語との比較
+
Go 言語との比較
- Go 言語でも Twice を用いた検証を行い、Gears OS との速度比較を行なった。
- 1CPU と 32CPU では約4.33倍の速度向上が見られた。
- CPU数による速度向上は、Gears OS の方が上だが、処理速度では Go言語の方が速い結果となった。
-
+
-
スライドの流れ
+
スライドの流れ
- CbC
- Gears OS における並列実行
@@ -416,7 +466,7 @@
-
今後の課題
+
今後の課題
- Go 言語との比較から 1CPU での動作が遅いことがわかった。
- par goto 文を使用することで、Contextを生成し、並列処理を行う。
diff -r 94494b3cd38b -r dfa8973bfe10 Slide/prosym.md
--- a/Slide/prosym.md Sun May 20 18:45:11 2018 +0900
+++ b/Slide/prosym.md Sun May 20 21:12:40 2018 +0900
@@ -4,21 +4,21 @@
lang: Japanese
code-engine: coderay
-% # OS の信頼性
+% ## OS の信頼性
% - コンピュータの信頼性の基本はメモリなどの資源管理を行う OS である。
% - OS は非決定的な実行を持つため、OS の信頼性を保証するには、証明を用いる方法とプログラムの可能な実行を全て数え上げるモデル検査を用いる必要がある。
% - 従来のテストとデバッグではテスト仕切れない部分が残ってしまい、不十分。
% - モデル検査は無限の状態でなくても巨大な状態を調べる事になり、状態を有限に制限したり、状態を抽象化したりする方法が用いられる。
%
-% # OS の拡張性
+% ## OS の拡張性
% - 時代とともに進歩するハードウェア、サービスに対応するために OS 自体が拡張される必要がある。
% - OS を検証する際にも、1度ではなくアプリケーションやサービス、デバイスが新しくなる毎に検証をやり直す必要がある。
%
-% # OS の拡張性と信頼性の両立
+% ## OS の拡張性と信頼性の両立
% - OSの拡張性と信頼性の観点から、OS は信頼性と拡張性を両立させることが重要であるといえる。
% - 本研究室では、OS の信頼性の保証と拡張性を実現することを目標に Gears OS を設計中である。
-# Gears OS
+## Gears OS
- 現代のOS では拡張性と信頼性を両立させることが要求されている。
- 時代と共にハードウェア、サービスが進歩していき、その度に OS を検証できる必要があるため、拡張性が必要。
- OS は非決定的な実行を持ち、従来の OS ではテストしきれない部分が残ってしまうため、信頼性が欠けてしまう。
@@ -30,7 +30,7 @@
% 拡張性と信頼性を実現する時に Interfaceと par goto 構文がなぜ必要なのかに繋げる話が必要
% APIと実装の分離が望ましい理由は？
-# API と実装の分離
+## API と実装の分離
- Gears OS は Continuation based C(以下、CbC)によって記述されている。
- CbC は Code Gear と Data Gear の単位でプログラムを記述していて、システムやアプリケーションを作る際に、この2つは柔軟に再利用する必要がある。
- この時に、機能を接続する API と実装の分離が可能であることが望ましい。
@@ -48,13 +48,13 @@
% Interfaceはほとんどかかない
% TaskScheduler の図も入れる Gears の構成のやつ
-# Gears OS での形式化とInterfaceの導入
+## Gears OS での形式化とInterfaceの導入
- 形式化とは仕様、実装、実行を Logic で記述する事である。
- Gears OS では、継続を使った関数型プログラムとして実装を記述する
- Logic としては、依存型関数言語である Agda を使う(前の発表)
- 証明とモデル検査を使って、信頼性を確保する
-# Gears OS の Interface
+## Gears OS の Interface
- この時、Code Gear と Deta Gear は Interface と呼ばれるまとまり(モジュール)で記述される。
- Interface 作成時に Code Gear の集合を指定することにより複数の実装を持つことができる。
- Interface は Data Gear で記述されて、Meta Deta Gear と呼ばれる。
@@ -69,12 +69,12 @@
% Contextも集合
% Inter
-# 並列API
+## 並列API
- Geas OS 信頼性を保証するために、形式化されたモジュールシステムが必要である。
- 本研究では、モジュールシステムとその応用である並列APIについて考察する。
- 並列APIは継続を基本とした関数型プログラミングと両立する必要があり、ここでは CbC の goto 文を拡張した par goto を導入する。
-# スライドの流れ
+## スライドの流れ
- Interface
- CbC
- Gears OS における並列実行
@@ -85,7 +85,7 @@
-# CbC
+## CbC
- ノーマルレベルとメタレベルの計算を1つの言語で表現できる言語として、本研究室で設計した CbC を用いる。
- ノーマルレベルの計算
- コンピュータの計算はプログラミング言語で行われる。
@@ -106,8 +106,7 @@
% シミュレーションされてない外界はOSとは違うのでCbCで書けない
% ぱるすさんの図入れるMeta data Gear
-
-# CbC
+## CbC
- CbC を用いることで、ノーマルレベルの計算の信頼性をメタレベルから保証できるようになる。
- CbC を用いてCode Gear と Data Gear を導入する。
@@ -116,14 +115,14 @@
% - Gears の記述をモジュール化するために Interface を導入した。
% - さらに並列処理の記述用に par goto 構文を導入する。
-% # par goto の実行
+% ## par goto の実行
% - 本論文では Interface と par goto の実装を記述し、評価を行なった。
% - また、マルチ CPU と GPU 上での par goto 文の実行を確認した。
% par goto には構文と実行の話がある
% ストーリー的に早いのでここでは入れない
-# CbC の構文
+## CbC の構文
- CbC の Code Gear は __code という型を持つ関数として記述する。
- 継続で次の Code Gear に遷移するので、戻り値は持たない。
- 遷移は goto 文による継続で処理を行い、引数として入出力を行う。
@@ -148,30 +147,41 @@
-# スライドの流れ
+## スライドの流れ
- CbC
- Gears OS における並列実行
- 比較
- 今後の課題
-# Gears における並列実行
+## Gears における並列実行
- Gears OS ではメタ計算を柔軟に記述するためのプログラミングの単位として Code Gear と Data Gear を用いる。
- それぞれにメタレベルの単位が存在し、Meta Data Gear と Meta Code Gear と呼ぶ。
- メタレベルの計算は Perl スクリプトによって生成され、Code Gear で記述される。
+
+
+
+
+
-
+
Gears OS
+Gears OS
- 現代のOS では拡張性と信頼性を両立させることが要求されている。
-
API と実装の分離
+
API と実装の分離
- Gears OS は Continuation based C(以下、CbC)によって記述されている。
- CbC は Code Gear と Data Gear の単位でプログラムを記述していて、システムやアプリケーションを作る際に、この2つは柔軟に再利用する必要がある。
@@ -101,7 +101,35 @@
-
並列API
+
Gears OS での形式化とInterfaceの導入
+
+ - 形式化とは仕様、実装、実行を Logic で記述する事である。
+ - Gears OS では、継続を使った関数型プログラムとして実装を記述する
+ - Logic としては、依存型関数言語である Agda を使う(前の発表)
+ - 証明とモデル検査を使って、信頼性を確保する
+
+
+
+
+
+
Gears OS の Interface
+
+ - この時、Code Gear と Deta Gear は Interface と呼ばれるまとまり(モジュール)で記述される。
+ - Interface 作成時に Code Gear の集合を指定することにより複数の実装を持つことができる。
+ - Interface は Data Gear で記述されて、Meta Deta Gear と呼ばれる。
+ - Java などの Class に相当する。
+ - Interface を外から呼び出すための Code Gear 群の型
+ - Interface を呼び出す時に必要となる引数を全て格納する Data Gear
+ - 実装に使う Code Gear の番号が含まれている。
+ - Code Gear の番号を変更することによって異なる実装を実現できる
+
+
+
+
+
+
並列API
- Geas OS 信頼性を保証するために、形式化されたモジュールシステムが必要である。
- 本研究では、モジュールシステムとその応用である並列APIについて考察する。
@@ -112,8 +140,9 @@
-
スライドの流れ
+
スライドの流れ
+ - Interface
-
CbC
@@ -126,7 +155,7 @@
-
CbC
+
CbC
- ノーマルレベルとメタレベルの計算を1つの言語で表現できる言語として、本研究室で設計した CbC を用いる。
- ノーマルレベルの計算
@@ -140,7 +169,7 @@
- コードが実行される際の以下の部分が、メタレベルの計算という。
- 処理系の詳細や使用する資源
- - コードの仕様や型などの言語以外の部分
+ - コードの仕様や型などの部分
@@ -151,17 +180,17 @@
-
CbC
+
CbC
- CbC を用いることで、ノーマルレベルの計算の信頼性をメタレベルから保証できるようになる。
- - CbC を用いてCode Gear と Data Gear、メタ構造を導入する。
+ - CbC を用いてCode Gear と Data Gear を導入する。
-
CbC の構文
+
CbC の構文
- CbC の Code Gear は __code という型を持つ関数として記述する。
- 継続で次の Code Gear に遷移するので、戻り値は持たない。
@@ -174,12 +203,15 @@
goto cg2(c);
}
+
-
スライドの流れ
+
スライドの流れ
- CbC
-
@@ -193,39 +225,43 @@
-
Gears における並列実行
+
Gears における並列実行
- Gears OS ではメタ計算を柔軟に記述するためのプログラミングの単位として Code Gear と Data Gear を用いる。
- それぞれにメタレベルの単位が存在し、Meta Data Gear と Meta Code Gear と呼ぶ。
- メタレベルの計算は Perl スクリプトによって生成され、Code Gear で記述される。
+
+
+
+
+
+
+
+
Gears OS の構造
+
+
+
+
+
+
+
+
Context
+
+ - 1つのスレッド内で使われる Interface の Code Gear と Data Gear は Meta Data Gear に格納される。
+ - この Meta Data Gear を Context と呼ぶ。
+ - Context を複製して複数の CPU に割り当てることにより並列実行が可能になる。
+ - Context は Task でもある。
+ - Task は実行する Code Gear と Data 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
+
par goto
- Context の複製には par goto を用いる。
- 他に、入力の同期、タスクスケジューラへの Context の登録が行われる。
@@ -235,20 +271,23 @@
-
Task
+
1つの Code Gear の実行は他の Code Gear に割り込まれない
- - Context は Task でもある。
- - 実行する Code Gear と Data Gear を全て持っている。
+ - 共有された Data Gear があった時に、それに対する変更はただ1つの Code Gear だけが許される
+ - 読み込みは複数であってもいい
+ - Agda 側で、並列実行を Code Gear の順次実行としてシミュレーションするため
+ - このような実行になるように Gears OS の実装を行う
-
__exit
+
__exit
- - par goto で生成された Task は __exit に継続することで終了する。
- - GearsOS の Task は Output Data Gear を生成した時点で終了する。
+ - 複数実行した時に、共有 Data Gear に書き込みを成功したかを確認する(commit)
+ - par goto で生成された Task は __exit に継続することで終了する
+ - GearsOS の Task は Output Data Gear を生成した時点で終了する
- そのため、par goto では直接 __exit に継続せず、Output Data Gear への書き出し処理に継続される。
- Code Gear と Data Gear の依存関係をノーマルレベルで記述できるようになる。
@@ -262,7 +301,7 @@
-
スライドの流れ
+
スライドの流れ
- CbC
- Gears OS における並列実行
@@ -276,7 +315,18 @@
-
Gears OS の評価
+
Gears OS の評価(目的)
+
+ - 並列構文とそれを実現する Meta Compitation が十分に揃っているかを確認したい
+ - 並列処理の台数効果を確認する
+ - 既存の並列言語と比較して不要なオーバーヘッドがあるか調べたい
+
+
+
+
+
+
Gears OS の評価(環境)
- CPU、GPU環境で Gears OS の測定を行う。
- 使用した環境は次のようになる。
@@ -304,7 +354,7 @@
-
Twice
+
Twice
- 評価には与えられた整数配列の全ての要素を2倍にする例題である Twice を使う。
- Twice では 通信時間を考慮しなければ、CPU より コア数の多い GPU が有利となる。
@@ -361,7 +411,7 @@
-
評価の考察
+
評価の考察
- コア数が上がるごとに、処理速度が上がっている。
- GPUでの実行は 32CPU に比べて約7.2倍の速度向上が見られた。
@@ -372,21 +422,21 @@
-
Go 言語との比較
+
Go 言語との比較
- Go 言語でも Twice を用いた検証を行い、Gears OS との速度比較を行なった。
- 1CPU と 32CPU では約4.33倍の速度向上が見られた。
- CPU数による速度向上は、Gears OS の方が上だが、処理速度では Go言語の方が速い結果となった。
-
+
-
スライドの流れ
+
スライドの流れ
- CbC
- Gears OS における並列実行
@@ -400,7 +450,7 @@
-
今後の課題
+
今後の課題
- Go 言語との比較から 1CPU での動作が遅いことがわかった。
- par goto 文を使用することで、Contextを生成し、並列処理を行う。