LARA

Unique References for Controlling Aliasing

The idea here is to check if a variable is the only way to access a location.

In C, we can perform an “address taken” check:

  • if there is no &x expression in C code anywhere, then x is not aliased

In languages like Java, we can do the following to ensure references are unique:

  • restrict operations so that there is at most one pointer to a given object after every operation
  • disallow x=y where x,y are references
  • instead, allow only statements that maintain the uniqueness invariant:
x = new C();
x = y--;    

same as: x=y; y=null;

x = y.f--;

same as: x=y.f; y.f=null;

p(y--);

same as: t=y; y=null; p(t); - for fresh var t

Relaxation: allow x=y assignment if y is not live afterwards (adding y=null would then have no effect, so we can omit it).

Binary search tree traversal:

  while (n != null && n.data != x) {
    if (x < n.data) {
      n = n.left;
    } else {
      n = n.right;
    }
  }

using unique pointers?

  while (n != null && n.data != x) {
    if (x < n.data) {
      n = n.left--; // ?
    } else {
      n = n.right--; // ?
    }
  }

Linear types and linear logic The idea of linear types is to not allow something to be used multiple times.

  • introduce a type system that tracks resources (e.g. references)
  • basic approach: assumptions are multisets (elements can repeat), cannot use one assumption twice in a proof

What is the invariant that unique reference systems ensure? In every state, the location has at most one incoming edge.

\begin{equation*}
  \forall x1, f1, y.\ \mbox{pointsTo}(x1,f1,y) \land \mbox{pointsTo}(x2,f2,y) \rightarrow (x1,f1)=(x2,f2)
\end{equation*}

where

\begin{equation*}
  \mbox{pointsTo}(x,f,y) = (x.f=y\ \lor\ (x \in \mbox{stackFrames} \land f \in \mbox{localVars} \land \ldots)\ \lor\ x \in \mbox{GLOBAL} \land f \in \mbox{globalVars} \land \ldots))
\end{equation*}

Recent references