Module Kill_index

module Kill_index: sig .. end
A timestamp used to implement 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:



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