9/15

全体ミーティング(9/15)
村田雅之
今日の発表内容
• Types for Safe Locking
– C. Flanagan and M. Abadi
– Proceedings of the 8th European Symposium on
Programming Languages and Systems, 1999
並列プログラム特有の問題
• 競合状態(race condition)
– 複数のスレッドが1つのデータに同時にアクセス
する
• デッドロック
– 既に確保されたロックを互いに要求し合って
各スレッドの処理が進行しなくなる
• タイミングに依存するため解析が難しい
問題の解決法
• type systemで解決する
• 命令型言語を対象とする
– call-by-value
– スレッド・ロックに関わる操作
– レコード (reference cell)
singleton lock type
• ロックごとに型をつける
– l : (m::Lock)
• ロックを型レベルで扱うことができる
• permission
– ロック(singleton lock type)の集合
スレッド・ロック
• fork e
– eを実行する新しいスレッドを作る
– ロックは継承されない
• new-lock x:m in e
– 新しいロックをxに束縛してeを評価
– mには新しいロックの型が束縛される
• sync e1 e2
– e1 を評価した結果のロックを確保してe2を評価
– e2を実行中、ロックe1を保有している
レコード・関数
• refm e : Refm t
– mという型のロックで保護されているレコード
• λp x:t1 . e : t1 →p t2
– p(permission)にあるロックを持っていないと
関数を適用することができない
型のチェック
• あるレコードにアクセスするには対応する
ロックを保有していなければならない
– Exp Deref , Exp Set
• 関数適用のときにpermissionがチェックされる
– Exp Appl
Operational Semantics
• ロックの環境、レコードの環境、各スレッドの
状態の3つの組で表す(abstract machine)
• スレッドの実行順は任意
• expressionを拡張
– in-sync l f
• l(ロック)を保有した状態でfを評価する
競合状態の定義
• 2つ以上のスレッドで同じ場所へのreference
rについて !r (dereference)またはr := V (set) を
評価している状態
• abstract machineがこの状態に遷移しない
ことを示す
→競合状態が発生しない
競合状態にならないことの証明(1)
• Lemma 1
– ある状態でwell-typedで、状態遷移可能ならば
次の状態もwell-typed
• Lemma 2 (Mutual Exclusion)
– ひとつのロックについてCritical Sectionを実行する
スレッドはひとつのみ(CSについてwell-formed)
– ある状態でwell-formedで状態遷移可能ならば
次の状態もwell-formed
競合状態にならないことの証明(2)
• Lemma 3
– well-typedなスレッドはロックを持っていない限り
レコードにアクセスしない
• Lemma 4
– well-typedでcritical sectionについてwell-formed
ならば競合状態でない
• 以上4つから、well-typedなプログラムは
競合状態に遷移しないことがいえる
polymorphism over lock types
• 任意のロックを扱う関数が書ける
• 例
let f = Λn::Lock.
λz. Refn Int.
z := z+1 in
new-lock x:m in f[m] (Refm 0)
existential types (1)
• new-lock x:m in eの返り値に新しく確保した
ロックを含むことができなかった
– 違うsingleton lock typeで同じ名前のものができて
混乱しないように
• 複数回同じnew-lockが呼ばれた時など？
• new-lockで新しく作ったロックを含む型を
existential typeとして返すことでこれを克服
existential types (2)
P = new-lock x:n in
let y = (x, (refn 0)) in
pack m::Lock = n with y
∃m::Lock. (m ×Refm Int)
open P as m::Lock, y:(m *Refm Int) in
sync first(y) !second(y)
デッドロックを防ぐ
• ロックにpartial orderをつける
• 今保有しているロックより上位のロックしか確
保できないようにする
デッドロックを防ぐための拡張
• m::Lock → m::(m1, m2)と拡張
– m1,m2はlock typeの集合
– m1 ∋ m1 < m < m2 ∈ m2
• permissionを拡張してlocking levelを持たせる
– locking levelより上のロックしか獲得できない
– 新しくロックを確保したらそのロックを新しい
locking levelとする
まとめ
• スレッドを用いた並列プログラムに特有の
問題である競合状態とデッドロックについて、
型システムを用いて防ぐ方法を示した

Download Report