Coupling (WIP)

The PCG tracks ownership and borrowing at a fine-grained level, and in some cases this granularity cannot be "observed" by the type system. For example, lifetime projection nodes can represent a notion of reborrowing that is more precise than Rust's borrow-checker itself. For example, consider the choose function:

#![allow(unused)]
fn main() {
fn choose<'a, T>(choice: bool, lhs: &'a mut T, rhs: &'a mut T) -> &'a mut T {
    if choice {
        lhs
    } else {
        rhs
    }
}
}

The the PCG shape of a call choose(x, y) function: consists of two edges $\mathtt{x}\downarrow {}^{\prime }\mathtt{a}\to \mathtt{result}\downarrow {}^{\prime }\mathtt{a}$ and $\mathtt{y}\downarrow {}^{\prime }\mathtt{a}\to \mathtt{result}\downarrow {}^{\prime }\mathtt{a}$. However, because the compiler only tracks lifetimes, the borrows of x and y will always expire at the same time. Accordingly, the two edges corresponding to the call will always be removed from the graph at the same time. These edges are therefore coupled, because the Rust type system forces the PCG to remove them at the same time.

Motivation

Because the type systems forces a set of coupled edges to be removed "all-at-once", edges that are known to be coupled could be treated as a single hyperedge.

The primary reason for doing so is to provide more information analysis tools. For example, Prusti uses coupling information to generate the shape of magic wands: in the choose, the coupled hyperedge provides precisely the shape of magic wand that Prusti encodes (although this is not always the case).

Another benefit is that coupling can reduce the size of the graphs.

Formal Definitions

Hyperedge

A hyperedge $e$ is an object with an associated set of source nodes and target nodes. The functions $\text{sources}(e)$ and $\text{targets}(e)$ denote the source and target nodes respectively.

Coupled Edges

A coupled edge $c$ is a hyperedge defined by a set of underlying hyperedges, where the sources and targets are defined as follows:

Let $S$ be the union of the sources of $\overline{e}$ and $T$ be the union of the targets of $T$. Then $sources(c)=S\setminus T$ and $targets(c)=T\setminus S$.

Hypergraph

A hypergraph $G$ is a tuple $⟨S,E⟩$ where $S$ is a set of nodes and $E$ is a set of hyperedges. Functions $nodes(G)$ and $edges(G)$ return the sets of nodes and hyperedges respectively.

Blocked Nodes

A node $n$ is blocked in $G$ iff $n\in nodes(G)$ and $n$ is not a leaf in $G$.

Descendant Relation

We define the descendant relation ${⩽}_G$ as

$$s{⩽}_G{s}^{\prime }\text{iff}s=s^{\prime }\text{or}s\text{is a descendant of}{s}^{\prime }\text{in}G.$$

Frontier

A set of nodes $S$ is a frontier of a hypergraph $G$ (denoted $\text{frontier}(S,G)$) iff $S\subseteq nodes(G)$ and $S$ is closed under ${⩽}_G$.

If $S$ is a frontier of $G$, it defines a valid expiry. The valid expiry $G\setminus S$ is the subgraph of $G$ obtained by removing all nodes in $S$ and all edges containing sources or targets in $S$. The expired edges of a valid

Reachable Subgraph

A graph $G^{\prime }$ is a reachable subgraph of a graph $G$ iff there exists a frontier $S$ such that $G\setminus S=G^{\prime }$

Desired Properties of Coupled Edges

Edges that will always be removed from the graph at the same time should definitely be coupled. Formally:

A set of edges $\overline{e}$ expire together on a graph $G$ iff for all reachable subgraphs $G^{\prime }$, $G^{\prime }$ either contains all edges in $\overline{e}$ or none of them, i.e.:

1. $\overline{e}\cap edges(G)=\overline{e}$, or
2. $\overline{e}\cap edges(G)=\varnothing$

If a set of edges $\overline{e}$ expire together on a graph $G$, then there must exist a set of edges $\overline{e^{\prime }}\supseteq \overline{e}$ that are coupled for $G$.

Note that we could in principle define coupling as such, but we could also consider a stronger definition we describe below:

Definition Based on Unblocking Frontier Expiries

Our stronger definition is based on the following two observations:

First, if removing a frontier $S$ does not unblock any node in a graph, there is no way for the removal to be observed in the program. Therefore, such frontiers do not need to be considered for the purpose of asserting properties about a place once it becomes accessible. We can instead define coupling via notion of unblockings of a graph, where an unblocking is an ordered list of the sets of nodes that become available by repeated removal of frontiers.

Unblockings

An unblocking $U$ of a graph $G$ is an ordered partitioning of the non-root nodes of $G$ into non-empty subsets $S_1,\dots ,S_n$, satisfying the property that there exists a frontier $S^{\prime }$ of $G$ with an expiry that unblocks all nodes in $S_1$, and $S_2,\dots S_n$ is an unblocking of $G\setminus S^{\prime }$. The function $Ub(G)$ denotes the set of all unblockings of $G$.

Correspondingly, we can define edges as coupled if they always observably expire together, i.e. at all points when a node becomes accessible, they are either all in the graph or none of them are.

Reachable Subgraphs

Formally, for a graph $G_0$ and an unblocking $U=S_1,\dots ,S_n$ of $G_0$, the reachable subgraphs $R(U,G_0)$ of an unblocking $U=S_1,\dots ,S_n$ is the list of graphs $G_0,\dots ,G_n$ where $\forall i,1⩽i⩽n.G_i=G_{i-1}\setminus S_i$. The function $\hat{R}$ is the lifting of $R$ to sets of unblockings: $$\hat{R}(\overline{U},G)=\bigcup _{U\in \overline{U}}R(U,G)$$

Therefore, edges should be coupled if they are either all present or all absent for each graph in $\hat{R}(Ub(G),G)$.

The second observation is that this set can be computed by considering only a subset of the unblockings in $G$. This is because an unblocking $U$ can subsume an unblocking $U^{\prime }$ in the sense that the reachable subgraphs of $U$ are a superset of the reachable subgraphs of $U^{\prime }$.

Subsumption

An unblocking $U=S_1,\dots ,S_n$ is immediately subsumed by an unblocking $U^{\prime }=S_1^{\prime },\dots S_{n+1}^{\prime }$ (denoted $Sub(U,U^{\prime })$) iff there exists an $i,0⩽i⩽n$ such that $S_i=S_i^{\prime }\cup S_{i+1}^{\prime }$ and $\forall j<i.S_j=S_j^{\prime }$ and $\forall j>i+1.S_j=S_{j+1}^{\prime }$.

$U^{\prime }$ subsumes $U$ (denoted $U<U^{\prime }$) iff $⟨U,U^{\prime }⟩$ is in the transitive closure of $Sub$.

Theorem (Subsumption): If $U<U^{\prime }$, then $R(G,U)\subset R(G,U^{\prime })$

Distinct Unblockings

The distinct unblockings of a graph $G$ (denoted $Dub(G)$) is the subset of $G^{\prime }s$ unblockings obtained by removing all non-minimal elements w.r.t $<$.

Theorem (Distinct Unblockings): For all graphs $G$, $\hat{R}(Ub(G),G)=\hat{R}(Dub(G),G)$

Effective and Maximal Coupling

A set of edges $\overline{e}$ are effectively coupled for a graph $G_0$ iff for all reachable subgraphs $G^{\prime }$ in the distinct unblockings of $G$, $G^{\prime }$ contains either all edges in $\overline{e}$ or none of them. A set of edges $\overline{e}$ is maximally coupled if it is effectively coupled and not a subset of an effectively coupled set.

Theorem (Correctness)

If a set of edges $\overline{e}$ expire together on a graph $G$, then there exists a set of edges $\overline{e^{\prime }}\supseteq \overline{e}$ that are maximally coupled on $G$.

Proof

Recall that a set of edges $\overline{e}$ expire together on $G$ if every reachable subgraph $G^{\prime }$ either contains all edges in $\overline{e}$ or none of them, and that a set of edges are definitely coupled if for all reachable subgraph $G^{\prime \prime }$ in the distinct unblockings of $G$ contains either all edges in $\overline{e}$ or none of them.

Therefore it is sufficient to show that the reachable subgraphs in the distinct unblockings of $G$ is a subset of the reachable subgraphs of $G$. The proof makes use of the following lemma:

Lemma: Valid Expiry on Unions of Frontier Nodes

If $S$ is a frontier of $G$ and $S^{\prime }$ is a frontier of $G\setminus S$, then $S\cup S^{\prime }$ is a frontier of $G$ and:

$$G\setminus S\setminus S^{\prime }=G\setminus (S\cup S^{\prime })$$

Proof is TODO

Then, let $U$ be an arbitrary unblocking of $G$, it follows by induction on the list of frontiers corresponding to the nodes in $U$, that any for every reachable subgraph $G^{\prime }$ of $U$, there exists a frontier $S$ of $G$ such that $G\setminus S=G^{\prime }$. Therefore, for all unblockings $U$ of $G$, the reachable subgraphs of $U$ are a subset of the reachable subgraphs of $G$.

Test Graphs

m function

#![allow(unused)]
fn main() {
fn m<'a: 'c, 'b: 'e, 'c, 'd, 'e, T>(
    x: &'a mut T,
    y: &'b mut T,
) -> (&'c mut T, &'d mut T, &'e mut T)
    where 'a: 'd, 'b: 'd {
         unimplemented!()
}
}

w function

#![allow(unused)]
fn main() {
fn w<'a: 'd, 'b: 'd, 'c: 'e, 'd, 'e T>(
    x: &'a mut T,
    y: &'b mut T,
    z: &'c mut T,
) -> (&'d mut T, &'e mut T) where 'b: 'e {
         unimplemented!()
}
}

Previous Example

Additional Examples from HackMD

One Lifetime Reborrower Function

#![allow(unused)]
fn main() {
fn f<'a>(x: &'a mut T) -> &'a mut T {
    x
}
}

Possible Outlives Reborrower Function

#![allow(unused)]
fn main() {
fn f<'a, 'b: 'a>(x: &'a mut T, y: &'b mut T) -> &'a mut T {
    todo!()
}
}

Non-Bipartite Graph Example