Miou.Condition
val create : unit -> t
create ()
creates and returns a new condition variable. This condition variable should be associated (in the programmer's mind) with a certain mutex m
and with a certain property P of the data structure that is protected by the mutex m
.
val broadcast : t -> unit
broadcast c
wakes up all threads waiting on the condition variable c
. If there are none, this call has no effect.
It is recommended to call broadcast c
inside a critical section, that is, while the mutex m
associated with c
is locked.
val signal : t -> unit
signal c
wakes up one of the threads waiting on the condition variable c
, if there is one. If there is none, this call has no effect.
It is recommended to call signal c
inside a critical section, that is, while the mutex m
associated with c
is locked.
The call wait c m
is permitted only if m
is the mutex associated with the condition variable c
, and only if m
is currently locked. This call atomically unlocks the mutex m
and suspends he current thread on the condition variable c
. This thread can later be woken up after the condition c
has been signaled via signal
or broadcast
; however, it can also be woken up for no reason. The mutex m
is locked again before wait
returns. One cannot assume that the property P associated with the condition variable c
holds when wait
returns; one must explicitly test whether P holds after calling wait
.