Expand description
In this file we handle the “Tree” part of Tree Borrows, i.e. all tree traversal functions, optimizations to trim branches, and keeping track of the relative position of the access to each node being updated. This of course also includes the definition of the tree structure.
Functions here manipulate permissions but are oblivious to them: as
the internals of Permission are private, the update process is a black
box. All we need to know here are
- the fact that updates depend only on the old state, the status of protectors, and the relative position of the access;
- idempotency properties asserted in
perms.rs(for optimizations)
Structs§
- Location
State 🔒 - Data for a reference at single location.
- Location
Tree - The state of the full tree for a particular location: for all nodes, the local permissions of that node, and the tracking for wildcard accesses.
- Node 🔒
- A node in the borrow tree. Each node is uniquely identified by a tag via
the
nodesmap ofTree. - Tree
- Tree structure with both parents and children since we want to be able to traverse the tree efficiently in both directions.
Enums§
- Access
Relatedness - Relative position of the access