LARA – Lab for Automated Reasoning and Analysis -

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