Obtaining Capability to a Place

The operation to obtain capability $c$ to a place $p$ in a PCG $\mathcal{G}$ proceeds as follows.

When performing this operation to satisfy the place capability required for a statement, the analysis guarantees that no live mutable borrows conflicting with $p$¹. At a high level, capability to $p$ is obtained by first collapsing the owned places in $\mathcal{G}$ to $p$

Step 1 - Label dereferences of shared borrows stored in $p$

Reborrows of shared references derived from $p$ (i.e. from any postfix of $p$) will survive even if $p$ is moved or mutated. Therefore, if $c$ permits the function to mutate $p$ (i.e. $c\ne \text{R}$), then the analysis labels all places that project from shared references derived from $p$.

Formally:

If $c\ne \text{R}$, then for each place $p^{\prime }$ in $\mathcal{G}$ where:

• $p^{\prime }$ is a strict postfix of $p$, and
• $p^{\prime }$ is a shared reference, and
• $\ast p^{\prime }$ is in $\mathcal{G}$

The analysis labels every postfix of $p^{\prime }$ in $\mathcal{G}$.

Step 2 - Collapse

Implementation

This operation is implemented as PlaceObtainer::obtain

The obtain(p, o) operation reorganizes a PCG state to a new state in where the PCG node for a place $p$ is present in the graph. The parameter o is an Obtain Type which describes the reason for the expansion. The reason $o$ is either:

• To obtain a specified capability to the place
• To access the place because it is the borrowed place of a two-phase borrow

An Obtain Type is associated with a result capability $c$ which is either the specified capability (in the first case), or Read (in the case of access for two-phase borrows).

Note that a place node for $p$ is not necessarily present in the graph before this occurs.

This proceeds as follows:

Step 1 - Label dereferences of shared borrows stored in $p$

(Same as high-level description)

Step 2 - Upgrading Closest Ancestor From R to E

This step is included to handle a relatively uncommon case (see the Rationale section below).

If the obtain operation is called with permission $W$ or $E$ and the closest ancestor $p^{\prime }$ to $p$, that is, the longest prefix of $p$ for which there exists a node in the graph, has $R$ capability, we upgrade $p^{\prime }$'s capability to $E$ in exchange for removing capability to all pre- and postfix places of $p^{\prime }$ in the graph (excluding $p^{\prime }$ itself).

This is sound because if we need to obtain non-read capability to place, and there are any ancestors of place in the graph with R capability, one such ancestor originally had E capability was subsequently downgraded. This function finds such an ancestor (if one exists), and performs the capability exchange.

Rationale

It's possible that we want to obtain exclusive or write permission to a field that we currently only have read access for. For example, consider the following case:

• There is an existing shared borrow of (*c).f1
• Therefore we have read permission to *c, (*c).f1, and (*c).f2
• Then, we want to create a mutable borrow of (*c).f2
• This requires obtaining exclusive permission to (*c).f2

We can upgrade capability of (*c).f2 from R to E by downgrading all other pre-and postfix places of (*c).f2 to None (in this case c and *c). In the example, (*c).f2 is actually the closest read ancestor, but this is not always the case (e.g. if we wanted to obtain (*c).f2.f3 instead)

Step 3 - Collapse

Then, if a node for $p$ exists in the graph and $p$'s capability is not at least as strong as $c$, collapse the subgraph rooted at $p$ (and obtain capability $c$ for $p$) by performing the collapse(p, c) operation.

collapse

The collapse(p) operation is implemented as follows:

• For each $p^{\prime }$ such that $p$ is a prefix of $p^{\prime }$ (from longest to shortest) and there is a node for $p^{\prime }$ in the graph:
  • perform the Collapse Repack Operation on $p^{\prime }$.
  • For each lifetime ${}^{\prime }r$ in the type of $p^{\prime }$:
    • Create a new lifetime projection node $p^{\prime }\downarrow {}^{\prime }r$
    • For each lifetime projection node $p^{\prime \prime }\downarrow {}^{\prime }r$ where $p^{\prime \prime }$ is an expansion of $p^{\prime }$:
      • Label $p^{\prime \prime }$
      • Create a new BorrowFlow edge $\{p^{\prime \prime }\downarrow {}^{\prime }r\}\to \{p^{\prime }\downarrow {}^{\prime }r\}$

Step 4 - Labelling $p$

At this point, if $c$ is $W$, we know that a subsequent operation will mutate $p$. As a result, if there exists a lifetime projection node for $p$ (for example, if $p$ stores a borrow that has since been reborrowed), it will no longer be tied to the current value of $p$. So, we label $p$ with reason ReAssign.

Step 5 - Expand

At this point there should be a node for some prefix $p^{\prime }$ of $p$ in the graph such that $\mathcal{C}[p^{\prime }]⩾c$.

We expand the graph to $p$ (and obtain the capability for $p$) by performing the expandTo(p, o) operation.

expandTo

The expandTo operation is implemented as follows:

• For each strict prefix $p^{\prime }$ of $p$ (from shortest to longest):
  • If expanding $p^{\prime }$ one level adds new edges to the graph, then
    • We expand the lifetime projections of $p^{\prime }$ one level

The operation to expand a place one level is the expandPlaceOneLevel operation, and the operation to expand the lifetime projections one level is expandLifetimeProjectionsOneLevel.

expandLifetimeProjectionsOneLevel

expandLifetimeProjectionsOneLevel is defined with three parameters:

• $p_b$: The place to expand
• $e$: The target expansion of $p_b$
• $o$: The Obtain Type

The operation is implemented as follows:

• Let $\overline{p}$ be the expansion of $p_b$ using $e$
• For each lifetime projection $p_b\downarrow r$ of $p_b$:
  • Let ${\overline{rp}}_r$ be the set of lifetime projections in $\overline{p}$ with lifetime $r$
  • If ${\overline{rp}}_r$ is nonempty²:
    • We identify the base lifetime projection $r{p}_b$ as follows:
      • Let $l$ be the current snapshot location
      • If $o$ is not an obtain for capability R:
        • $r{p}_b=p_b\downarrow r\text{at}l$
      • Otherwise, if $p_b$ is blocked by a two-phase borrow live at $l$:
        • Let $l^{\prime }$ be the reservation location of the conflicting borrow
        • $r{p}_b=p_b\downarrow r\text{at}{l}^{\prime }$
      • Otherwise, $r{p}_b=p_b\downarrow r$
    • Create a new Borrow PCG Expansion hyperedge $e=\{r{p}_b\}\to {\overline{rp}}_r$

1. If the program requires capability to the place to do some action, then the place cannot be borrowed mutably. This invariant does not hold when we are obtaining capability to the place in order to construct a loop abstraction. ↩

2. This could happen e.g. expanding an x : Option<&'a T> to a x@None ↩