全体ミーティング(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 ロックごとに型をつける ロックを型レベルで扱うことができる permission l : (m::Lock) ロックを型レベルで扱うことができる permission ロック(singleton lock type)の集合

スレッド・ロック fork e new-lock x:m in e sync e1 e2 eを実行する新しいスレッドを作る ロックは継承されない new-lock x:m in e 新しいロックをxに束縛してeを評価 mには新しいロックの型が束縛される sync e1 e2 e1 を評価した結果のロックを確保してe2を評価 e2を実行中、ロックe1を保有している

レコード・関数 refm e : Refm t λp x:t1 . e : t1 →p t2 mという型のロックで保護されているレコード 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 Lemma 2 (Mutual Exclusion) ある状態でwell-typedで、状態遷移可能ならば 次の状態もwell-typed Lemma 2 (Mutual Exclusion) ひとつのロックについてCritical Sectionを実行するスレッドはひとつのみ(CSについてwell-formed) ある状態でwell-formedで状態遷移可能ならば 次の状態もwell-formed

競合状態にならないことの証明(2) Lemma 3 Lemma 4 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 open P as m::Lock, y:(m *Refm Int) in sync first(y) !second(y) ∃m::Lock. (m ×Refm Int)

デッドロックを防ぐ ロックにpartial orderをつける 今保有しているロックより上位のロックしか確保できないようにする

デッドロックを防ぐための拡張 m::Lock → m::(m1, m2)と拡張 m1,m2はlock typeの集合 m1 ∋ m1 < m < m2 ∈ m2 permissionを拡張してlocking levelを持たせる locking levelより上のロックしか獲得できない 新しくロックを確保したらそのロックを新しい locking levelとする

まとめ スレッドを用いた並列プログラムに特有の 問題である競合状態とデッドロックについて、型システムを用いて防ぐ方法を示した