PowerPoint プレゼンテーション

Types for Safe Locking
(ESOP ’99)
Cormac Flanagan
and
Martίn Abadi
SRC, Compaq
Presenter： Shin SAITO [shin]
Abstract
並列プログラミングの問題の一つ、
「共有データへのアクセス競合
(Race condition)」
を回避するための型システムの提案
 Second-order や
デッドロック回避のための型システム
などへの拡張

Pitfalls in Parallel Programming
 並列プログラミングの落とし穴：
– 競合 (race condition)
– デッドロック (deadlock)
Race Condition

競合 (race condition) とは
– 複数のスレッドがデータ構造を同期を取らずに
操作している状態



非決定性や誤った結果をもたらす
タイミングに依存 → 追跡が困難
解決策
– ロックの導入：ロックを獲得してからデータを操作
Race Condition

競合 (race condition) とは
– 複数のスレッドがデータ構造を同期を取らずに
操作している状態



非決定性や誤った結果をもたらす
タイミングに依存 → 追跡が困難
解決策
– ロックの導入：ロックを獲得してからデータを操作
データにアクセス
thread
lock をとる
A
Race Condition

競合 (race condition) とは
– 複数のスレッドがデータ構造を同期を取らずに
操作している状態



非決定性や誤った結果をもたらす
タイミングに依存 → 追跡が困難
解決策
– ロックの導入
→ デッドロックの可能性
Deadlock

デッドロック (deadlock) とは
– 互いに（他のスレッドが獲得している）ロックを
獲得しようとして停止している状態
thread1
A
thread2
B
Deadlock

デッドロックの解決策
– ロックに半順序を導入
– 複数のロックは小さい方から獲得
thread1
A
lockA < lockB
thread2
B
Static Analysis of
Programming Discipline

以上のような「解決策のルール」
– 守られていることをチェックするのは容易でない
– １ヶ所でも違反 → タイミングに依存するエラー
型システムを用いて静的にチェック
Outline




Target language
Race-free property
Extensions
Future work
Target Language (1/2)

並列、手続き型言語
– スレッド生成
– ロックの生成/獲得/解放
– 参照セルの割当て、参照
Target Language (2/2)

言語仕様
– 共有されるデータ：参照セルで表す
– 参照セルにロックを付加
– 規約：ロックを獲得してデータにアクセスする


守られていることを型システムで保証する
制限
– ロック獲得の構造は入れ子

ロック獲得 → 文実行 → ロック解放
– ロック変数のスコープ
Syntax
e  Exp ::=
—V



(値)
unit
x
px:t.e
(Ｃ言語のｖｏｉｄ)
(変数)
(関数定義)
Syntax
e  Exp ::=
—V
p
(::= unit | x |  x:t.e )
(値)
Syntax
e  Exp ::=
–V
(値)
p
(::= unit | x |  x:t.e )
–ee
(関数適用)
– refm e | !e | e := e
(参照セルの割り当て/参照外し/代入)
– fork e
(スレッド生成)
– new-lock x:m in e
(ロック変数の生成)
– sync e e
(同期=ロックの獲得)
 e; e | let x=e in e
(逐次実行/let 文)
“new-lock” statement
 new-lock
x:m in e
– 新しいロック変数 x と
“singleton lock type” m を宣言
– x, m は e の中で有効
(制約： x を返すことはできない)

拡張可能 (existential type)
“sync” Statement

(一般には) sync l e
– ロック変数 l に関して同期をとる
– e を評価 (実行)
– l を解放
Reference Cell

refm e
– e への参照セルを生成
– m はセルを protect するロック変数の型
– セルの型は Refm t (ただし e:t とする)

!e
– e は参照セルを表す式
– (e: Refm t とするとき) スレッドは型 m に対応する
ロックの獲得が必要
Function Definition

p
x:s.e
– 引数を x (型 s) とする関数の定義

ロック変数は引数にできない
→ 拡張可能 (polymorphism)
– p: permission (lock type の集合)

関数本体の実行時に獲得されているべき
ロックの型の集合 (cf. example)
p
– 型は s → t
Examples
P1  new-lock x:m in
let y = refm 1 in
sync x !y
 P2  new-lock x:m in
let y1 = refm 1
f = y {m}:Refm Int. (y := !y + 1)
in
sync x ( f y1)

Abstract Machine (1/4)
評価方法：call-by-value
 S  State = (, , T)

–  : ロックから {0, 1} への写像 (1: acquired)
–  : 参照セルの location から値への写像
– T : スレッドの列 / Ti : i 番目の要素


(T0 : 初期/main スレッド)
Exp に構文を追加
– in-sync l e: ロックを獲得しているスレッド
Abstract Machine (2/4)
評価の例：
P1  new-lock x:m in
new-lock y:n in
let z = refm 1 in
sync y !z
 初期状態：
(, , P1)

Abstract Machine (3/4)

状態遷移：
– (, , new-lock x:m in
new-lock y:n in
let z = refm 1 in
sync y !z)
→ ([l1  0], , new-lock y:n in
let z = refol1 1 in
sync y !z)
→ ([l1  0, l2  0], , let z = refol1 1 in sync l2 !z)
Abstract Machine (4/4)

状態遷移 (続き)：
– ([l1  0, l2  0], , let z = refol1 1 in sync l2 !z)
→ ([l1  0, l2  0], [z: Refol1 Int  1], sync l2 !z)
→ ([l1  0, l2  1], [z: Refol1 Int  1], in-sync l2 !z)
→ ([l1  0, l2  1], [z: Refol1 Int  1], 1)


ロックの獲得は考慮していない
上の状態は正しく型付けされた式では起こらない
Typing Rules

Judgment form： E; p├ e: t
– E: 環境
E ::=  | E, x:t | E, m::Lock
– p: permission

「式 e は以下の条件で型は t であり、
正しく実行される」
– 環境は E
– p に含まれる型のロックを獲得している
Typing Rules - for locks 
E, m::Lock, x:m; p├ e: t,
t は E で有効な型
 E; p├ (new-lock x:m in e): t
– 返り値に x を含むことはできない

E; p├ e1: m, E; p  {m}├ e2: t
 E; p├ sync e1 e2: t
– m は lock type を表す
– e2 内部では型 m のロックを獲得
Typing Rules - for ref. cells 
E; p├ e: Refm t, m  p  E; p├ !e: t

E; p├ e1: Refm t,
E; p├ e2: t,
mp
 E; p├ (e1 := e2 ): t
– 参照セルにアクセスするにはロックが必要
Typing Rules - for functions 
E, x: s; p├ e: t 
E; ├  x:s.e: s → t
p
p
– 関数呼び出し時に必要な permission を付加

p
E; p├ e1: s → t, E; p├ e2: s
 E; p├ e1 e2: t
– 関数呼び出し時の permission をチェック
Typing Rules - for subtyping 
subpermission
– E├ p,

E├ q,
pq

E├ p  q
subtype rule
– E├ s1  t1, E├ t2  s2, E├ p  q
p
q
 E├ (t1 → t2)  (s1 → s2)

subtyping
– E; p├ e : t,
E├ p  q,
E├ t  s
 E; q├ e: s
Race-free Property

スレッド T がセル r にアクセス
– f = E[ !r ] or f = E[ r := V ]
– E : evaluation context
E ::= [] | E e | V E | refm E | !E | E := e
| r := E | sync E e | in-sync l E
Race-free Property

スレッド T がセル r にアクセス
– f = E[ !r ]

or
f = E[ r := V ]
Race condition
– 複数のスレッドがセル r をアクセス
例： T = in-sync l1 !r | in-sync l2 r := 5
Race-free Property

スレッド T がセル r にアクセス
–

f = E[ !r ]
or
f = E[ r := V ]
Race condition
– 複数のスレッドがセル r をアクセス

Race-free property
1.
2.
3.
4.
各 critical section には高々1つのスレッド … ()
() はリダクションで保存される
well-typed かつ () なら race condition にない
well-typed な式 → race condition に陥らない
Extensions

Polymorphism over Lock Types
– ロック変数を引数に
Existential Types
 Readers-writer Locks
 Deadlock-free types

Deadlock Elimination

Deadlock
– T=
in-sync l1 (sync l2 e1) | in-sync l2 (sync l1 e2)
のようなスレッドを含んでいる状態

Key Idea
– Lock type に順序を導入
– new-lock x:m :: (M1, M2) in e


Mi は lock type の集合
順序： M1  m  M2
Typing Rules (1/2)

Judgment form： E; p, L├ e: t
– L: locking level
L ::= m |  | T

「式 e は well-typed で型は t である」
– p に含まれる型のロックを獲得している
– e が獲得できるロックは L より大
Typing Rules (2/2)

E; p, L├ e1: m,
L  m,
E; p  {m},m├ e2 : t
 E; p, L ├ sync e1 e2 : t
– ロックの順序をチェック
Future Work
型推論
 前述の拡張の正当性の証明


Download Report