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§
- ErrHandler
Args 🔒 - Data given to the error handler
- Location
State 🔒 - Data for a single location.
- Node 🔒
- A node in the borrow tree. Each node is uniquely identified by a tag via
the
nodesmap ofTree. - Node
AppArgs 🔒 - Data given to the transition function
- Tree
- Tree structure with both parents and children since we want to be able to traverse the tree efficiently in both directions.
- Tree
Visitor 🔒 - Internal contents of
Treewith the minimum of mutable access for the purposes of the tree traversal functions: the permissions (perms) can be updated but not the tree structure (tag_mappingandnodes) - Tree
Visitor 🔒Stack - Stack of nodes left to explore in a tree traversal.
See the docs of
traverse_this_parents_children_otherfor details on the traversal order.
Enums§
- Access
Relatedness - Relative position of the access
- Children
Visit Mode - Continue
Traversal 🔒 - Whether to continue exploring the children recursively or not.
- Recursion
State 🔒