title: Gears OS のモジュール化と並列 API author: Mitsuki Miyagi, Yu Tobaru, Shinji Kono profile: 琉球大学 lang: Japanese code-engine: coderay % # OS の信頼性 % - コンピュータの信頼性の基本はメモリなどの資源管理を行う OS である。 % - OS は非決定的な実行を持つため、OS の信頼性を保証するには、証明を用いる方法とプログラムの可能な実行を全て数え上げるモデル検査を用いる必要がある。 % - 従来のテストとデバッグではテスト仕切れない部分が残ってしまい、不十分。 % - モデル検査は無限の状態でなくても巨大な状態を調べる事になり、状態を有限に制限したり、状態を抽象化したりする方法が用いられる。 % % # OS の拡張性 % - 時代とともに進歩するハードウェア、サービスに対応するために OS 自体が拡張される必要がある。 % - OS を検証する際にも、1度ではなくアプリケーションやサービス、デバイスが新しくなる毎に検証をやり直す必要がある。 % % # OS の拡張性と信頼性の両立 % - OSの拡張性と信頼性の観点から、OS は信頼性と拡張性を両立させることが重要であるといえる。 % - 本研究室では、OS の信頼性の保証と拡張性を実現することを目標に Gears OS を設計中である。 # Gears OS - 現代のOS では拡張性と信頼性を両立させることが要求されている。 - 時代と共にハードウェア、サービスが進歩していき、その度に OS を検証できる必要があるため、拡張性が必要。 - OS は非決定的な実行を持ち、従来の OS ではテストしきれない部分が残ってしまうため、信頼性が欠けてしまう。 - 本研究室では、それらを実現することを目標に Gears OS の開発を行なっている。 % 欠けてしまうで終わってるので　"それら"は 分かりづらい % 並列API 研究目的とAPIとの繋がりがない % モジュールとAPIの説明分ける % 拡張性と信頼性を実現する時に Interfaceと par goto 構文がなぜ必要なのかに繋げる話が必要 % APIと実装の分離が望ましい理由は？ # API と実装の分離 - Gears OS は Continuation based C(以下、CbC)によって記述されている。 - CbC は Code Gear と Data Gear の単位でプログラムを記述していて、システムやアプリケーションを作る際に、この2つは柔軟に再利用する必要がある。 - この時に、機能を接続する API と実装の分離が可能であることが望ましい。 % 上と繋がってない % なんでモジュールシステムが必要？ % 形式化と言わない % 形式化 formalization % ここでいう形式化はInterfaceとは関係ない % interface は仕様とAPIの分離 % 実装の分割 がInterface % まず、形式化が重要(仕様、実装、実行をlogicで記述) % その記述にAgdaを使う % Interfaceはほとんどかかない % TaskScheduler の図も入れる Gears の構成のやつ # 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 の番号を変更することによって異なる実装を実現できる % Interface は実行時に実装を入れ替える事ができる % 呼び出すものはStack 上に積めない % Contextも集合 % Inter # 並列API - Geas OS 信頼性を保証するために、形式化されたモジュールシステムが必要である。 - 本研究では、モジュールシステムとその応用である並列APIについて考察する。 - 並列APIは継続を基本とした関数型プログラミングと両立する必要があり、ここでは CbC の goto 文を拡張した par goto を導入する。 # スライドの流れ - Interface - CbC - Gears OS における並列実行 - 比較 - 今後の課題 # CbC - ノーマルレベルとメタレベルの計算を1つの言語で表現できる言語として、本研究室で設計した CbC を用いる。 - ノーマルレベルの計算 - コンピュータの計算はプログラミング言語で行われる。 - その部分をノーマルレベルの計算と呼ぶ。 - メタレベルの計算 - コードが実行される際の以下の部分が、メタレベルの計算という。 - 処理系の詳細や使用する資源 - コードの仕様や型などの部分 % ノーマルレベルとメタレベルの違い % 以外 = メモリ % 定義されたものに従って形式的にプログラムが記述されるが、その実行の資源や環境がメタレベル % 実行するのはOSや資源 % 実際にはプログラムで記述されていない部分(CPU,メモリの資源、並列処理、外界の影響) この４つ書く % CbC の特徴はメタもかける % OS での資源はCbCでかける % シミュレーションされた外界 % シミュレーションされてない外界はOSとは違うのでCbCで書けない % ぱるすさんの図入れるMeta data Gear # CbC - CbC を用いることで、ノーマルレベルの計算の信頼性をメタレベルから保証できるようになる。 - CbC を用いてCode Gear と Data Gear を導入する。 % - 検証には 定理証明支援系である Agda を用いる。 % - Gears の記述をモジュール化するために Interface を導入した。 % - さらに並列処理の記述用に par goto 構文を導入する。 % # par goto の実行 % - 本論文では Interface と par goto の実装を記述し、評価を行なった。 % - また、マルチ CPU と GPU 上での par goto 文の実行を確認した。 % par goto には構文と実行の話がある % ストーリー的に早いのでここでは入れない # CbC の構文 - CbC の Code Gear は __code という型を持つ関数として記述する。 - 継続で次の Code Gear に遷移するので、戻り値は持たない。 - 遷移は goto 文による継続で処理を行い、引数として入出力を行う。 ```c __code cg0(int a, int b) { goto cg1(a+b); } __code cg1(int c) { goto cg2(c); } ``` - CbC の記述だけでは並列実行にならない % 関数呼び出しで実装したい　なのでpar つける % 意味: 戻り値がなく　exitで呼び出す % par goto (並列実行を実装したい、形式化したい=Agdaの記述をしたい) 並列実行を形式化する % 本文のpar goto を削って載せる % なぜ par goto が必要か % context がこれの先に出てないとだめ % 形式化はどうするの？-> par goto を使う。 % par goto を使えば並列実行されたGears の形式化ができる # スライドの流れ - CbC - Gears OS における並列実行 - 比較 - 今後の課題 # Gears における並列実行 - Gears OS ではメタ計算を柔軟に記述するためのプログラミングの単位として Code Gear と Data Gear を用いる。 - それぞれにメタレベルの単位が存在し、Meta Data Gear と Meta Code Gear と呼ぶ。 - メタレベルの計算は Perl スクリプトによって生成され、Code 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 に割り当てることにより並列実行が可能になる。 - Context は Task でもある。 - Task は実行する Code Gear と Data Gear を全て持っている。 # par goto - Context の複製には par goto を用いる。 - 他に、入力の同期、タスクスケジューラへの Context の登録が行われる。 % exit が説明不足 % code gear の実行は他のシープに邪魔されない。 % 並列実行時の書き換えは許してない # 1つの Code Gear の実行は他の Code Gear に割り込まれない - 共有された Data Gear があった時に、それに対する変更はただ1つの Code Gear だけが許される - 読み込みは複数であってもいい - Agda 側で、並列実行を Code Gear の順次実行としてシミュレーションするため - このような実行になるように Gears OS の実装を行う % 複数走ったなかの成功したものをコミットするのがexit # __exit - 複数実行した時に、共有 Data Gear に書き込みを成功したかを確認する(commit) - par goto で生成された Task は __exit に継続することで終了する - GearsOS の Task は Output Data Gear を生成した時点で終了する - そのため、par goto では直接 __exit に継続せず、Output Data Gear への書き出し処理に継続される。 - Code Gear と Data Gear の依存関係をノーマルレベルで記述できるようになる。 ```c __code code1(Integer *integer1, Integer * integer2, Integer *output) { par goto add(integer1, integer2, output, __exit); goto code2(); } ``` % 失敗した時はmeta compitation で処理する % # Interface % # Context % # 並列構文 # スライドの流れ - CbC - Gears OS における並列実行 - 比較 - 今後の課題 # Gears OS の評価(目的) - 並列構文とそれを実現する Meta Compitation が十分に揃っているかを確認したい - 並列処理の台数効果を確認する - 既存の並列言語と比較して不要なオーバーヘッドがあるか調べたい # Gears OS の評価(環境) - CPU、GPU環境で Gears OS の測定を行う。 - 使用した環境は次のようになる。 - CPU 環境 - Model : Dell PowerEdgeR630 - Memory : 768GB - CPU : 2 × 18-Core Intel Xeon 2.30GHz - CPU 環境 - GPU : GeForce GTX 1070 - Cores : 1920 - ClockSpeed : 1683MHZ - Memory Size : 8GB GDDR5 # Twice - 評価には与えられた整数配列の全ての要素を2倍にする例題である Twice を使う。 - Twice では 通信時間を考慮しなければ、CPU より コア数の多い GPU が有利となる。 - 要素数2^27のデータに対する Twice の実行結果を示す。 - CPU では2^27のデータを64個のデータに分割した。 - kernel only は 通信速度を除いた速度である。
Processor Time(ms)
1 CPU 1181.215
2 CPUs 627.914
4 CPUs 324.059
8 CPUs 159.932
16 CPUs 85.518
32 CPUs 43.496
GPU 127.018
GPU(kernel only) 6.018
# 評価の考察 - コア数が上がるごとに、処理速度が上がっている。 - GPUでの実行は 32CPU に比べて約7.2倍の速度向上が見られた。 - 通信速度を含めると 16CPU より遅い。 % なんでGo言語？ # Go 言語との比較 - Go 言語でも Twice を用いた検証を行い、Gears OS との速度比較を行なった。 - 1CPU と 32CPU では約4.33倍の速度向上が見られた。 - CPU数による速度向上は、Gears OS の方が上だが、処理速度では Go言語の方が速い結果となった。
message
# スライドの流れ - CbC - Gears OS における並列実行 - 比較 - 今後の課題 # 今後の課題 - Go 言語との比較から 1CPU での動作が遅いことがわかった。 - par goto 文を使用することで、Contextを生成し、並列処理を行う。 - しかし、Context はメモリ空間の確保や使用する全ての Code Gear Data Gear の設定をする必要があり、生成に時間がかかってしまう事が原因。 - 処理が軽い場合は Context を生成しないようなチューニングが必要である。