分散プログラムを形式的証明から抽出する
東京大学大学院情報理工系研究科
萩谷研究室 平井洋一

2009-09-17

大会論文の修正版:
I 余りは空き机に置いてください．
I セッション後に平井が回収します．ということでよろしいでしょうか．

問題: 分散プログラムを正しく書くのは困難
分散プログラムを書き間違えても，なかなか気付かないことがある
I 百万回に一回のバグ
本研究の対象: wait-free プログラム
プロセス間同期無し．実に分散的．

解決法: プログラムでなく形式的証明を書く
形式的証明を書き間違えると，すぐに気付く
I 証明チェッカ
本研究の対象: 知識論理の変種
プロセスの知識を記述できる．

概要

Wait-free プログラム[Herlihy99] の，wait-free protocol.
他のプロセスを待てないできないこと
入力 プロセス a , b に，0 か 1 か
出力 プロセス a と b の両方が，相手の入力を出力する．

Wait-free プログラムの例
入力 プロセス a , b に，0 か 1 か
出力 少なくとも片方が，相手の入力を出力する．
*shm_x = *shm_y = -1; /* 共有メモリの初期化 *//* 以下並列実行
¶³
¶ */

³

int a(int x) {*shm_x = x;
if (*shm_y != -1)
return *shm_y;
else
return -1;}µ´

int b(int y) {*shm_y = y;if (*shm_x != -1)
return *shm_x;
else
return -1;}´µ*shm x と*shm y は別．Sequential consistency を仮定

仕様Γ `G ∆
Γ 実行前に全部成立と仮定∆ 実行後に一つ成立と保証
G 実行に関与するプロセス

Γ, ∆ は論理式の有限列
ϕ ::= P | Ka ϕ | ϕ ∨ ϕ | ϕ ∧ ϕKa ϕ プロセス a が ϕ を知ってる∧, ∨ かつ, または仕様の例
Ka P ∧ Kb Q `{a ,b } Kb Ka P ∨ Ka Kb Q
P であることを a が知っていて，Q であることを b が知っている ならば→ a , b の wait-free プログラムで →Q であることを b が知っていることをa が知っているか，P であることを a が知っていることをb が知っている ようにできる

証明: 実現可能な仕様を網羅する
Γ `G ∆, ϕϕ, Γ0 `G ∆0Γ, Γ0 `G ∆, ∆0(axiom)ϕ `G ϕ(comm)Ka ϕ, Kb ψ `{a ,b }∪G Ka Kb ψ, Kb Ka ϕ(nec)(K∧)

Ka (∧∧(cut)(K)Ka ϕ `{a }∪G ϕ∆ `G Γ∨∨(上のほうに (comm) が無い)Γ) `G ∪{a } Ka ( ∆)Ka ϕ, Ka ψ `G Ka (ϕ ∧ ψ)(∨ 左)Γ, ϕ `G ∆Γ0 , ϕ0 `G ∆00
Γ, Γ , ϕ ∨ ϕ0 ` ∆, ∆0(∧ 左)Γ, ϕ, ϕ0 `G ∆Γ, ϕ ∧ ϕ0 `G ∆(K∨)

Ka (ϕ ∨ ψ) `G Ka ϕ, Ka ψ(∨ 右)(∧ 右)Γ `G ∆, ϕ, ϕ0Γ `G ∆, ϕ ∨ ϕ0

Γ `G ∆, ϕΓ0 `G ∆0 , ϕ00
Γ, Γ `G ∆, ∆0 , ϕ ∧ ϕ0

証明の例

Wait-free プログラムの抽出(comm) 7→
各プロセスが，共有メモリに書いてから読む(cut),(∨ 左),(∧ 右) 7→
プロセスごとの連接;

各変数への代入が一度だけになるように，変数をたくさん使う．

示したことI

健全性:¶

仕様に証明がある ⇒仕様をみたす wait-free プロ
グラムが有るµ[Herlihy99] による wait-free 計算の特徴づけで使われた，単体的複体上に意味論をつくった (続く)．

³´

意味論の概要 (1)x = 0 でプロセス a が起動

x=0a意味論の概要 (2)x = 0 はプロセス a の知識

x=0a

K a(x=0)

意味論の概要 (3)y = 1 でプロセス b が起動
プロセス a の知識は，わからない
K b(y=1)y=1b

K a(x=0)

意味論の概要 (4)プロセス a , b の両方の状態が見える視点からは，少なくとも片方で成立する命題は成立する
x=0aK a(x=0)

K a(x=0) K b(y=1)

K b(y=1)
y=1bK a(x=0)

意味論の概要 (5)Wait-free protocol は単体的複体の分割である [Herlihy99]．
K a(x=0)bx=0a

K a(x=0)

K a(x=0)ab

K a(x=0)

大会論文の修正理由:
つまらない話だった
意味論が，もっとゆるかった
I 証明体系も，ゆるかった
I 超健全性が成立: 実現可能な任意の仕様を，「何もしない」
プログラムが満たす
I 抽出しても嬉しくない
I

大会論文の修正理由:
意味論がゆるすぎる
hold, but not wanted

K a(x=0)x=0a

K a(x=0)

K a(x=0)K aK b(x=0)

bFuture workI

完全性を示す¶³

仕様に証明がある ⇐=仕様満たす wait-free プログラム有µI関連研究との比較:
動的知識論理 [Ditmarsch07],
単体的複体上の知識論理 [Porter04]

I[Attiya04] の wait-free 計算を扱う(while 文が入る)´

Future future work:

もっと弱くSequential consistency が成り立たない場合を調べる
I 計算を scale させたい．
I 公理を弱くして，cut 除去可能な論理を得たい(仕様を保ちプログラムを短く変形できる)

Future future work:

もっと強くプリミティブを様相として追加する機構を作る
I 「ここだけは同期が必要」と証明中に明示する

参考文献[Herlihy99]

Herlihy, M. and Shavit, N.: The Topological Structure of
Asynchronous Computability, J. ACM, Vol. 46, No. 6, 1999,
pp. 858–923.

[Attiya04]

Attiya, H. and Welch, J.: Distributed Computing
Fundamentals, Simulations, and Advanced Topics, 2nd
Edition , Wiley, 2004.

[Ditmarsch07] Ditmarsch, H. v., Hoek, W. v. d., and Kooi, B.: Dynamic
Epistemic Logic, Springer, 2007.
[Porter04]

Porter, T: Interpreted systems and Kripke models for
multiagent systems from a categorical perspective, Theor.
Comput. Sci, Vol. 323, No. 1–3, 2004, pp. 235–266.