並行プログラミングでは、共有リソースに対する安全なロックとアンロックは本質的で意欲的な課題です。 この章では、線形型がこの課題を解決するのに有効であることを具体的に説明します。
はじめに、次のような線形抽象型 shared を導入しましょう:
(なんらかのリソースに対する) 観型 VT が与えられたとき、型 shared(VT) の値は、本質的に、型 VT のリソースとなんらかのロックを含んだボックス化レコードです。 リソースを共有リソースにするために、次のような関数 shared_make が呼ばれます。 型 shared(VT) それ自身が線形であることに注意してください。 実装では、スピンロックで保護された線形共有リソースにはリファレンスカウントが内在しています。 関数 shared_ref と shared_unref は共有リソース内のリファレンスカウントを増減させます: もし共有リソースのリファレンスカウントが 1 であったら、その共有リソースへの shared_unref 呼び出しはそれらの表現で使われていたメモリを解放し、その共有リソースに保存されていたリソースを返します。関数 shared_lock は与えられた共有リソースからリソースを獲得し、関数 shared_unlock はその反対です:
// absview locked_v // fun shared_lock{a:vtype}(!shared(a)): (locked_v | a) fun shared_unlock{a:vtype}(locked_v | !shared(a), x: a): void //
予想できることですが共有リソースは、スピンロック、リファレンスカウントと (保管されたリソースを差す) ポインタから成る、ボックス化タプルとして実装できます:
// datavtype shared_ (a:vtype) = SHARED of (spin1_vt(*lock*), int(*count*), ptr) // assume shared = shared_ //
implement shared_ref {a}(sh) = let // val+@SHARED (spin, count, _) = sh // val spin = // for temp. use unsafe_spin_vt2t(spin) // val (pf | ()) = spin_lock(spin) val c0 = count val () = count := c0 + 1 val ((*void*)) = spin_unlock(pf | spin) prval ((*void*)) = fold@sh // in $UN.castvwtp1{shared(a)}(sh) end // end of [shared_ref]
implement shared_unref {a}(sh) = let // val+@SHARED (spin, count, _) = sh // val spin = // for temp. use unsafe_spin_vt2t(spin) // val (pf | ()) = spin_lock(spin) val c0 = count val () = count := c0 - 1 val ((*void*)) = spin_unlock(pf | spin) prval ((*void*)) = fold@sh // in // if c0 <= 1 then let val+~SHARED(spin, _, x) = sh val ((*freed*)) = spin_vt_destroy(spin) in Some_vt($UN.castvwtp0{a}(x)) end // end of [then] else let prval () = $UN.cast2void(sh) in None_vt() end // end of [else] // end // end of [shared_unref]
関数 shared_lock と shared_unlock は次のように実装されます:
implement shared_lock {a}(sh) = let // val+@SHARED(spin, _, x) = sh // val spin = unsafe_spin_vt2t(spin) // val (pf | ()) = spin_lock(spin) // val x0 = $UN.castvwtp0{a}(x) // prval () = fold@sh // in ($UN.castview0(pf) | x0) end // end of [shared_lock]
implement shared_unlock {a}(pf | sh, x0) = let // val+@SHARED(spin, _, x) = sh // val spin = unsafe_spin_vt2t(spin) // val () = x := $UN.castvwtp0{ptr}(x0) // val () = spin_unlock($UN.castview0(pf) | spin) // prval () = fold@sh // in // nothing end // end of [shared_unlock]
この章で紹介したコード全体を含む shared_vt.dats ファイルはオンラインから入手できます。 また、このファイルはロックを保持した動作が: スレッド0が動作し; スレッド1が動作し; スレッド2が動作し; スレッド0が動作し; スレッド1が動作し; スレッド2が動作し; というように動く3つのスレッドの実装も含んでいます。