module Kill_index:sig
..end
Monitor.kill
.
A monitor is dead if it has an ancestor whose kill index is dead
.
Kill indices are used so that we can efficiently check whether a monitor is dead or alive, given that a monitor has a pointer to its parent, but not its children. So, there is no way when killing a monitor to visit all of its descendants. Instead, we rely on lazily checking descendants when they are used.
Each monitor has a kill_index : Kill_index.t
, and the scheduler has a single
global_kill_index : Kill_index.t
. We maintain an invariant on the monitor tree that
if a monitor's kill index equals global_kill_index
, then all of its ancestors kill
indices also equal global_kill_index
. This ensures that any monitor whose kill
index equals global_kill_index
is alive.
All kill indices initially start with value Kill_index.initial
. To kill a monitor,
we set that monitor's kill index to Kill_index.dead
and increment the scheduler's
global_kill_index
. A monitor can be in one of three situations:
kill_index = global_kill_index
. The monitor is alive.kill_index = dead
. The monitor is dead. A dead monitor is never revived.kill_index
to dead
. If not, we will set its kill_index
to
global_kill_index
.type
t
include Equal.S
include Invariant.S
val dead : t
val initial : t
val next : t -> t
val sexp_of_t : t -> Sexplib.Sexp.t