ASIAN 2003 報告 前田俊行.

Presentation on theme: "ASIAN 2003 報告 前田俊行."— Presentation transcript:

1 ASIAN 2003 報告 前田俊行

2 Achieving Type Safety for Low-Level Code
Cyclone プロジェクトの現状について Cyclone = 安全な C 言語の方言 C プログラマが書きたくなるようなメモリ操作を型付けしたい 様々なポインタ型の導入 *, zero-terminated pointer その上で、既存の C コードはなるべく簡単に使いまわしたい 様々なプログラム解析技術を結集 Region inference Linear type (alias analysis) など どうやらOSを書くのに使いたい、らしい

3 Self-configurable Mirror Servers for Automatic Adaptation
クライアントからの要求の増減に自動的に適応してサーバ数を調節するシステムの研究 P2P型のシステム 暇なノードは近隣ノードに「暇なんですけど」と宣伝する 忙しいノードは暇なノードに「働いて下さい」とお願いする スケーラブル No single point of failure 宣伝やお願いを発行するポリシーをプログラミングできる ちゃんと上手く動くっぽい実証データあり (ただしシミュレーション)

4 シミュレーション実験 ミラーサーバ群で2種類のサービスA, B を提供 クライアントからのサービス要求を動的に変化させて以下の数字を計測
サービスを実行しているノード数 1ノードあたりのアクセス数 など ポリシー 実験1ではサービスA, Bとも同優先度 実験2ではサービスB の優先度を上げてある

5 実験1の結果 (ノード数のみ) 実線: サービスA 点線: サービスB P2Pシステムでも 動的適応できた

6 実験2の結果 (ノード数のみ) 実線: サービスA 点線: サービスB P2Pシステムでも 優先度づけできた

7 Unreliable Failure Detectors via Operational Semantics
Unreliable FDs (failure detectors) という分散アルゴリズムの解析手法をスモールステップ operational semantics で言い換えてみましたという研究 言い換えによって見通しがよくなる、らしい 言い換えが正しいことが証明してある

8 Failure Detector: FD FD = (F, H)
F : T(time) → 2P failure pattern (例) F(42) = { 3, 7 } ⇒ 時間 [0, 42] の間にプロセス 3と 7 がクラッシュする H : T × P → 2p failure detector histories (例) H(42, 5) = { 6, 7 } ⇒ 時間 42 においてプロセス 5 はプロセス 6 と 7 がクラッシュしていると考える 上記 H は F と違っていてもよい = Unreliable

9 FDの性質 Completeness と Accuracy であらわす Completeness Accuracy
クラッシュしたプロセスを suspect すること Accuracy クラッシュしていないプロセスを suspect しないこと プロセス i がプロセス j を suspectする = j ∈H (t, i)

10 2種類のCompleteness crashed(F) = ∪tF(t) correct(F) = P＼crashed(F)

11 8種類のAccuracy (1)

12 8種類のAccuracy (2)

13 Operational Semantics Scheme
TI = trusted-immortal processes C = crashed processes

14 Operational Semantics Scheme
i = プロセス i が何かアクション ? を実行する、という意味 suspect i = プロセス i はプロセス j はクラッシュしたと見なす

15 Operational Semantics Scheme
condition χ (Γ, j) = 要求する accuracy によって異なる

16 Operational Semantics
Eventual weak accuracy をいうには◇-SUSPECT に加え、 ∃t. (TIt, Ct) Nt with TIt ≠ 0 を満たす必要がある

17 Operational Semantics
Eventual strong accuracy をいうには◇-SUSPECT に加え、 ∃t. (TIt, Ct) Nt with TIt ∪ Ct = 全プロセス を満たす必要がある

18 Deaccumulation - Improving Provability
Accumulate されたプログラムの自動検証は難しいので、自動的に元のプログラムに変換する方法の研究 (例) P : f (S x1) y1 y2 = f x1 (S (S y1)) (y1 : y2) f y1 y2 = y2 A : g x1 = f x1 [] を、以下のように deaccumulate する D : f (S x1) = sub (f x1) (S (S 0)) (0 : []) f = [] 方法: 1-state macro tree transducer を homomorphism-substitution modular tree transducer に変換する

19 A Calculus for Secure Mobility
Crypto-loc calculus という安全なモバイル計算のモデル(プロセス計算)を提案 以下の3つの概念をまとめて導入している Location Code mobility (weak mobility) Cryptography Observational equivalence でセキュリティプロパティを定義 さらにセキュリティプロパティの証明のために labeled bisimilarity というものを定義 Observational equivalence == Labeled bisimilarity を証明した

20 Syntax: terms

21 Syntax: processes

22 Structural Equivalence

23 Reduction Relations

24 Observational Equivalence
ここで P↓a とはプロセスPが(チャネル) a に何か output すること C はいわゆる evaluation context また、C{P} が closed なとき C は P のclosing evaluation context であるという

25 Labeled Semantics ここで A (agent) = (νa)(σ,P)
～ ここで A (agent) = (νa)(σ,P) σ(= substitution from variables to terms) : “敵”が知り得るデータ a : “敵”が知らない names

26 Labeled Semantics … 続き

27 Labeled Bisimilarity … の準備

28 Labeled Bisimilarity