この章では、スレッド間の非同期通信をサポートする、線形チャネルの実装を示します。 これはまた、プログラマ中心 のプログラム検証を主張する良い機会でもあります。
本質的にスレッド間の通信チャネルは、レースコンディションをに対して必要ななんらかの保護メカニズムで包んだキューです。 容量固定のキュー、すなわち生成されたら容量が変わらないようなキューを仮定しましょう。 もしそのキューが満杯なら、そのキューへの要素の挿入は失敗します。 もしそのキューが空なら、そのキューからの要素の削除は失敗します。 満杯のキューへの挿入や空のキューからの削除を防ぐために、まず次のようなキューに対する線形抽象型を導入しましょう:
absvtype queue_vtype(a:vt@ype+, int(*m*), int(*n*)) vtypedef queue(a:vt@ype,m:int,n:int) = queue_vtype(a,m,n)
// fun{a:vt0p} queue_insert {m,n:nat | m > n} (!queue(a, m, n) >> queue(a, m, n+1), a): void // fun{a:vt0p} queue_remove {m,n:nat | n > 0}(!queue(a, m, n) >> queue(a, m, n-1)): (a) //
次のコードは抽象型 queue の別バージョンです:
// absvtype queue_vtype(a:vt@ype+, int(*id*)) = ptr // vtypedef queue(a:vt0p, id:int) = queue_vtype(a, id) vtypedef queue(a:vt0p) = [id:int] queue(a, id) //
// absprop ISNIL(id:int, b:bool) // fun {a:vt0p} queue_isnil{id:int}(!queue(a, id)): [b:bool] (ISNIL(id, b) | bool(b)) //
// absprop ISFUL(id:int, b:bool) // fun {a:vt0p} queue_isful{id:int}(!queue(a, id)): [b:bool] (ISFUL(id, b) | bool(b)) //
これで、与えられたキューへの挿入と削除を表わす関数 queue_insert と queue_remove には次のインターフェイスを割り当てることができます:
// extern fun {a:vt0p} queue_insert {id:int} ( ISFUL(id, false) | xs: !queue(a, id) >> queue(a, id2), x: a ) : #[id2:int] void // extern fun {a:vt0p} queue_remove {id:int} ( ISNIL(id, false) | xs: !queue(a, id) >> queue(a, id2) ) : #[id2:int] a // end-of-fun //
与えられたキューへ queue_insert を呼び出すためには、そのキューが満杯ではないことを示す証明が必要です。 当該キューに queue_isful を呼び出して false が返れば、そのような証明を獲得できます。 同様に、与えられたキューへ queue_remove を呼び出すためには、まずそのキューに queue_isnil を呼び出して、そのキューが空でないことを示す証明を獲得する必要があります。
ここで示した内容は、queue_isnil と queue_isful が持つそのインターフェイスを実際には立証していません。 その代わりここでの焦点は、queue_isnil と queue_isful にそのようなインターフェイスが割り当てられたとき、満杯のキューに queue_insert が呼び出されないことと queue_remove が空のキューに呼び出されないことを保証することです。 私はこのスタイルのプログラミング検証を プログラマ中心 であると呼んでいます。 なぜならその正確さは客観的形式的に確立されたものではないからです。 私自身、プログラマ中心のプログラム検証が実際にとても柔軟で効果的であることを見つけました。 もし非形式的な数学の証明が証明された内容が正当であるかどうか検査するのに役立つと我々が信じるのであれば、プログラマ中心のプログラム検証もまた検証されたプログラムが正しいかどうか検査するのに役立つことを自然に信じることができるでしょう。
それでは、スレッド間の非同期通信のための線形チャネルの実装を開始しましょう。 はじめに、次のような線形抽象型 channel を宣言しましょう:
チャネルに要素を挿入する関数には次のインターフェイスが与えられます: もしそのチャネルが満杯であったら、channel_insert の呼び出し元はブロックします。 同様に、チャネルから要素を削除する関数には次のインターフェイスが与えられます: もしそのチャネルが空であったら、channel_remove の呼び出し元はブロックします。チャネルを次のように表現してみましょう:
// datavtype channel_ = { l0,l1,l2,l3:agz } CHANNEL of @{ cap=intGt(0) , spin=spin_vt(l0) , rfcnt=intGt(0) , mutex=mutex_vt(l1) , CVisnil=condvar_vt(l2) , CVisful=condvar_vt(l3) , queue=ptr // deqarray } (* end of [channel] *) // assume channel_vtype(a:vt0p) = channel_ //
関数 channel_insert には次の実装が与えられます:
implement {a}(*tmp*) channel_insert (chan, x0) = let // val+CHANNEL {l0,l1,l2,l3}(ch) = chan val mutex = unsafe_mutex_vt2t(ch.mutex) val (pfmut | ()) = mutex_lock (mutex) val xs = $UN.castvwtp0{queue(a)}((pfmut | ch.queue)) val ((*void*)) = channel_insert2<a> (chan, xs, x0) prval pfmut = $UN.castview0{locked_v(l1)}(xs) val ((*void*)) = mutex_unlock (pfmut | mutex) // in // nothing end // end of [channel_insert]
implement {a}(*tmp*) channel_insert2 (chan, xs, x0) = let // val+CHANNEL {l0,l1,l2,l3}(ch) = chan // val (pf | isful) = queue_isful (xs) // in // if isful then let prval (pfmut, fpf) = __assert () where { extern praxi __assert (): vtakeout0(locked_v(l1)) } val mutex = unsafe_mutex_vt2t(ch.mutex) val CVisful = unsafe_condvar_vt2t(ch.CVisful) val ((*void*)) = condvar_wait (pfmut | CVisful, mutex) prval ((*void*)) = fpf (pfmut) in channel_insert2 (chan, xs, x0) end // end of [then] else let val isnil = queue_isnil (xs) val ((*void*)) = queue_insert (pf | xs, x0) val ((*void*)) = if isnil.1 then condvar_broadcast(unsafe_condvar_vt2t(ch.CVisnil)) // end of [if] in // nothing end // end of [else] // end // end of [channel_insert2]
channel_insert (と channel_insert2) の上記実装を真似て、channel_remove の実装を導くことは単純でしょう。 これは練習問題とします。
この章で紹介したコード全体とテストコードを含む channel_vt.dats ファイルはオンラインから入手できます。