Module tree

Module tree 

Source
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§

LocationState 🔒
Data for a reference at single location.
LocationTree
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 nodes map of Tree.
Tree
Tree structure with both parents and children since we want to be able to traverse the tree efficiently in both directions.

Enums§

AccessRelatedness
Relative position of the access