2017-05-26 14:30:34 +00:00
|
|
|
(* (c) 2017 Hannes Mehnert, all rights reserved *)
|
|
|
|
|
2018-10-12 23:05:21 +00:00
|
|
|
(** A tree data structure including policies and dynamic usage.
|
2017-05-26 14:30:34 +00:00
|
|
|
|
|
|
|
Considering delegation of resources to someone, and further delegation
|
|
|
|
to others - using a process which is not controlled by the authority -
|
|
|
|
requires runtime tracking of these delegations and the actual usage:
|
|
|
|
|
|
|
|
If Alice may create 2 virtual machines, and she delegates the same
|
|
|
|
capability further to both Bob and Charlie, the authority must still enforce
|
|
|
|
that Alice, Bob, and Charlie are able to run 2 virtual machines in total,
|
|
|
|
rather than 2 each. *)
|
|
|
|
|
|
|
|
(** The type of the resource tree. *)
|
|
|
|
type t
|
|
|
|
|
|
|
|
(** [empty] is the empty tree. *)
|
|
|
|
val empty : t
|
|
|
|
|
|
|
|
(** [find_vm t id] is either [Some vm] or [None]. *)
|
|
|
|
val find_vm : t -> Vmm_core.id -> Vmm_core.vm option
|
|
|
|
|
2018-10-28 18:41:06 +00:00
|
|
|
(** [find_policy t id] is either [Some policy] or [None]. *)
|
|
|
|
val find_policy : t -> Vmm_core.id -> Vmm_core.policy option
|
|
|
|
|
2018-10-12 23:05:21 +00:00
|
|
|
(** [check_vm_policy t vm] checks whether [vm] under [id] in [t] would be
|
|
|
|
allowed under the current policies. *)
|
2018-10-29 16:14:51 +00:00
|
|
|
val check_vm_policy : t -> Vmm_core.id -> Vmm_core.vm_config -> (bool, [> `Msg of string ]) result
|
2018-10-12 23:05:21 +00:00
|
|
|
|
|
|
|
(** [insert_vm t vm] inserts [vm] under [id] in [t], and returns the new [t] or
|
|
|
|
an error. *)
|
2018-10-22 22:54:05 +00:00
|
|
|
val insert_vm : t -> Vmm_core.id -> Vmm_core.vm -> (t, [> `Msg of string]) result
|
2017-05-26 14:30:34 +00:00
|
|
|
|
2018-10-12 23:05:21 +00:00
|
|
|
(** [insert_policy t id policy] inserts [policy] under [id] in [t], and returns
|
|
|
|
the new [t] or an error. *)
|
|
|
|
val insert_policy : t -> Vmm_core.id -> Vmm_core.policy -> (t, [> `Msg of string]) result
|
2017-05-26 14:30:34 +00:00
|
|
|
|
2018-10-28 18:50:48 +00:00
|
|
|
(** [remove_vm t id] removes vm [id] from [t]. *)
|
|
|
|
val remove_vm : t -> Vmm_core.id -> (t, [> `Msg of string ]) result
|
|
|
|
|
|
|
|
(** [remove_policy t id] removes policy [id] from [t]. *)
|
|
|
|
val remove_policy : t -> Vmm_core.id -> (t, [> `Msg of string ]) result
|
2017-05-26 14:30:34 +00:00
|
|
|
|
2018-10-12 23:05:21 +00:00
|
|
|
(** [fold t id f g acc] folds [f] and [g] below [id] over [t]. *)
|
2018-10-22 23:02:14 +00:00
|
|
|
val fold : t -> Vmm_core.id ->
|
|
|
|
(Vmm_core.id -> Vmm_core.vm -> 'a -> 'a) ->
|
2018-10-12 23:05:21 +00:00
|
|
|
(Vmm_core.id -> Vmm_core.policy -> 'a -> 'a) -> 'a -> 'a
|
2018-10-28 18:04:24 +00:00
|
|
|
|
|
|
|
(** [pp] is a pretty printer for [t]. *)
|
|
|
|
val pp : t Fmt.t
|