Formal requirements for virtualizable third generation architectures

Transcript

1. Formal Requirements for Virtualizable Third Generation Architectures 0x64#10 @yubessy
2. プロセスVM ではなく システムVM の話です
3. とあるエンジニアの週末 久しぶりに自作PC でもつくろう
4. とあるエンジニアの週末 久しぶりに自作PC でもつくろう Corei7 とか買ってきても面白くない
5. とあるエンジニアの週末 久しぶりに自作PC でもつくろう Corei7 とか買ってきても面白くない せっかくなのでCPU をつくろう！
6. とあるエンジニアの週末 久しぶりに自作PC でもつくろう Corei7 とか買ってきても面白くない せっかくなのでCPU をつくろう！ x86 と同じものつくっても面白くない
7. とあるエンジニアの週末 久しぶりに自作PC でもつくろう Corei7 とか買ってきても面白くない せっかくなのでCPU をつくろう！ x86 と同じものつくっても面白くない せっかくなので命令セットを組もう！
8. WAIT
9. そのアー キテクチャ、 仮想化できますか？？？
10. Formal Requirements for Virtualizable Third Generation Architectures Popek, Gerald J., and Goldberg, Robert P. Communications of the ACM 17.7 (1974): 412-421.
11. 論文の内容 仮想化機構に求められる特性を定義 第三世代アー キテクチャのコンピュー タの形式的 な計算モデルを定義 第三世代アー キテクチャの命令セット中の 仮想化に関連する命令に対する分類を導入 第三世代アー キテクチャで仮想化機構を構築する ために命令セットが満たすべき十分条件を導出 ※ 第三世代アー キテクチャ： 当時の最先端アー キテクチャの総称（x86 の源流）
12. 素朴な疑問 仮想化できないアー キテクチャってあるの？ チュー リング完全ならエミュレー ションできるでしょ？
13. エミュレー ション vs. 仮想化 共通点: あるコンピュー タ上で 別のコンピュー タを動作させること エミュレー ション 仮想化 アー キテ クチャ ゲストとホストで 異なる ゲストとホストで 同じ ホストの 役割 ゲストの命令の解 釈・ 翻訳・ 実行 ゲストのリソー ス 利用を監視・ 管理 ゲストの 命令実行 ホストが解釈・ 翻 訳・ 実行 一部を除いて透過 的に実行
14. エミュレー ション vs. 仮想化 エミュレー ション (Emulation) = 代理 ゲストが発行する命令を逐一代わりに実行 仮想化 (Virtualization) = 監視 ゲストが権限のない命令を発行したときのみ介入 → 仮想化はオー べー ヘッドが少ない ※ ここでの「 仮想化」 は 現代でいう「 ハー ドウェア仮想化」 に近い
15. 仮想化機構に求められる特性 仮想化機構を実現するプログラムを仮想マシンモニタ （VMM） と呼ぶ e.g. VMware, VirtualPC, VirtualBox, ... VMM とそれが作り出す仮想環境は次の特性を 持たなければならない 1. 等価性(Equivalence) 2. 資源の管理(Resource Control) 3. 効率性(Ef ciency)
16. 特性1: 等価性(Equivalence) OS やアプリケー ションが、VM 上で実行された場合と 通常のハー ドウェア上で実行された場合とで同じよう に動作する → VM が正しく動作するための特性 VMM の元で動作するプログラムは、 等価な実際 のマシン上で直接実行した場合と本質的に同じ振 る舞いを示さなければならない “ “
17. 特性2: 資源の管理(Resource Control) VMM が、VM に提供する( 仮想) プロセッサや ( 仮想) メモリなどを全てコントロー ル可能である → VM が安全に動作するための特性 VMM は仮想化された資源を完全にその管理下に おかなければならない “ “
18. 特性3: 効率性(Ef ciency) VM が( 仮想) プロセッサに発行する命令の多くを VMM の介入なく直接( 物理) プロセッサで実行できる → VM が効率的に動作するための特性 ※ 統計的に大部分: 命令セット中の割合ではなく、 実 行時の割合 統計的に大部分の機械の命令を VMM の介在なく 実行できなければならない “ “
19. 仮想化可能なアー キテクチャ Popek とGoldberg は、 以上の3 特性を満たすもの だけが完全な仮想化機構であるとした では、 どんなアー キテクチャなら完全な仮想化機構を 構築できるVMM( 完全なVMM) を実現できるか？ Popek とGoldberg は、 第三世代アー キテクチャの コンピュー タの計算モデルを形式的に定義し、 命令セットがある要件を満たせば完全なVMM を 実現できることを証明した
20. 命令の分類 完全な仮想化機構を実現するために命令セットが 満たすべき十分条件を仮想化要件とよぶ 仮想化要件を簡潔に表現するため、 命令セット中の 仮想化に関わる関連する命令に対して次の分類を導入 特権命令 センシティブ命令 制御センシティブ命令 動作センシティブ命令
21. 特権命令 トラップ: マシンの現在の状態を保存した上で マシンの制御をスー パバイザモー ドに移行すること = 実行のために 特権(privillage) が必要な命令 その命令を実行しようとした時、 プロセッサがユ ー ザー モー ドにあれば、 トラップされる命令 “ “
22. センシティブ命令 制御センシティブ命令 動作センシティブ命令 ※ システム資源: プロセッサモー ド・ メモリサイズ等 システム資源の構成を変えようとする命令 “ “ システムの資源の構成に結果が依存する命令 “ “
23. 定理: Popek とGoldberg の仮想化要件 システム資源の構成に影響を与えるor 受ける命令は 常にVMM に制御を渡して実行される → 直接的に資源の管理を保証 （ 逆に） 非特権命令はシステム資源の構成に関係ない のでVMM の介入なしに直接実行できる → 間接的に効率性を保証 全てのセンシティブ命令が特権命令ならば 完全なVMM を構築することができる “ “
24. 証明の骨子 全てのセンシティブ命令が特権命令ならば 資源の管理・ 効率性が保証されることは明らか 証明すべきこと： 「 全てのセンシティブ命令が特権命令であるという条 件下で、 等価性の保証されるVMM が構築できる」 → 実際にVMM の構築手順を示し、 それが等価性を 保証していることを示す ※NOTE: 以下時間なければ割愛
25. 第三世代コンピュー タの計算モデル S = <E, M, P, R>: ( 状態機械における) 状態 E: 主記憶 M: モー ド (supervisor/user) P: プログラムカウンタ R: 再配置レジスタ i: 命令 i(S1) = S2: 命令i によるS1 からS2 への状態遷移 ※I/O や割り込みは考慮しない
26. 再配置レジスタ (Reallocation Register) 現在のメモリ空間のベー スアドレスとサイズを保持 R = (l, b) l: ベー スアドレス b: サイズ 物理アドレス = 論理アドレス + ベー スアドレス ベー スアドレスを変化させることで、 プログラムに 割り当てるメモリ空間を切り替えることが可能 = VM に割り当てるメモリ空間を隔離できる
27. トラップ 命令 i が次の条件をみたすとき、i はトラップである E' (=i の実行後のメモリ) に E, M, P, R (=i の実行前の状態の全構成要素) が保存される M' = supervisor R' = (0, q - 1) ( 全メモリ空間) ※X' は命令実行後の各変数の値 ※q は最大メモリサイズ
28. 特権命令・ センシティブ命令 特権命令 M = user ⇔ i: trap 制御センシティブ命令 M ≠ M' ∨ R ≠ R' 動作センシティブ命令 ∃ R1, R2 s.t. R1 ≠ R2 → E'1 ≠ E'2 ∨ P'1 ≠ P'2 ※ 厳密には多少異なる
29. 等価性とVM map C: 状態機械が取りうる状態の全集合 Cv: 状態機械上にVMM が存在して 状態機械の制御を掌握している状態の集合 Cr: C - Cv 等価性の保証 ⇔ Cr から Cv への単射かつ準同型な写像 f が存在 i.e. VMM が居る状況(Cv) で VMM が居ないように見える状況を作り出せる この写像 f をVM map と呼ぶ
31. VM map の存在証明 論文ではVM map の存在性のみ証明 ※ 実際にはアー キテクチャ毎にいい感じのを作る 全ての命令の効果はM, P, R およびE のうちR で指定 された部分のみに依存 これらで表現できる状態数は高々 有限個 全ての特権命令と全ての状態について f の適用後の状態を定義したテー ブルを作ればよい
32. ＿ 人人人人人人人＿ ＞ 効率性とは ＜ ￣Y^Y^Y^Y^Y^Y￣
33. 閑話休題: x86 仮想化 ('78) x86 アー キテクチャの登場 当初は仮想化要件を満たしていなかった ('99) VMware Virtual Platform の登場 一部の動的命令変換によるオー バー ヘッド ('05-'06) HAV (Hardware-Assisted Virtualization) の登場 Intel Virtualization Technology AMD Virtualization 仮想化要件を満たすようx86 を拡張
34. 自分で命令セットを組むときは ぜひ思い出してみてくださいね！