Alias burying: Unique variables without destructive reads

An unshared object can be accessed without regard to possible conflicts with other parts of a system, whether concurrent or single‐threaded. A unique variable (sometimes known as a ‘free’ or ‘linear’ variable) is one that either is null or else refers to an unshared object. Being able to declare and check which variables are unique improves a programmer's ability to avoid program faults. In previously described uniqueness extensions to imperative languages, a unique variable can be accessed only with a destructive read , which nullifies it after the value is obtained. This approach suffers from several disadvantages: the use of destructive reads increases the complexity of the program which must continually restore nullified values; adding destructive reads changes the semantics of the programming language; and many of the nullifications are actually unnecessary. We demonstrate instead that uniqueness can be preserved through the use of existing language features. We give a modular static analysis that checks (nonexecutable) uniqueness annotations superimposed on an imperative programming language without destructive reads. The ‘alias‐burying’ intuition is that aliases that are ‘dead’ (will never be used again) can be safely ‘buried’ (made undefined). Copyright © 2001 John Wiley & Sons, Ltd.