Class type Plasma_shm.shm_manager
class type shm_manager =object..end
method new_id : kind -> id
allocates a new ID for an shm or buf object
method book_allocation : id -> int -> unit
Books this ID with this (total) size, and pushes the new entry
method delayed_allocation : id -> int -> unit
A delayed allocation is not immediately pushed to the shared
book. This is safe to be called from GC finalisers.
method condition : kind -> condition
Estimate where we are
method push : unit -> unit
Push allocations to the shared book. This also includes delayed
allocations.
method wm : kind -> watermarks
Effective watermarks
method dump : string
Current sums for `Shm and `Buf as debug string
method have_local_allocations : bool
Whether this manager has allocations
