## 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.

where

**Recent references**