/////////////////////////////////////////////////////////////////////
// Papers on Joline (external uniqueness/existential ownership/etc.)
/////////////////////////////////////////////////////////////////////


# Ownership-Based Alias Management

Royal Institute of Technology, Sweden, May 2006.

## ABSTRACT

Object-oriented programming relies on sharing and the mutable states of objects for common data structures, patterns and programming idioms. Sharing and mutable state is a powerful but dangerous combination. Uncontrolled aliasing risks causing representation exposure, where an object's state is exposed and modifiable out of the control of its conceptually owning object. This breaks encapsulation, and hence, in extension, abstraction.

Contemporary object-oriented programming languages' support for alias encapsulation is mediocre and easily circumvented. To this end, several proposals have been put forward that strengthen encapsulation to enable construction of more reliable systems and formally reasoning about properties of programs. These systems are vastly superior to the constructs found in for example C++, Java or C#, but have yet to gain acceptance outside the research community.

In this thesis, we present three constructs for alias management on top of a deep ownership types system in the context of the Joline programming language. Our constructs are fully statically checkable and impose little run-time overhead. We show the formal semantics and soundness proof for our constructs as well as their formal and informal aliasing properties. We show applications and extensions and perform a practical evaluation of our system with our implemented Joline compiler. The evaluation suggests that our constructs are compatible with real-world programming, makes use of some of our own proposed patterns, and encourages further practical studies of programming with ownership-based constructs for alias management.

# External Uniqueness: A Theory of Aggregate Uniqueness for Object-Orientation

Stockholm University, Sweden, September 2004.

## ABSTRACT

Unique pointers is a simple and powerful concept. In an object-oriented programming language, they facilitate reasoning about the state of an object formally and informally, make resource management and memory management easier, and can void the need for synchronisation in the presence of multiple threads.

However, existing implementations of uniqueness are not properly suited to object-oriented programming. A unique pointer to a bridge object in an aggregate only considers the bridge object and not the rest of the aggregate. More importantly, we identify a problem with existing implementations that leads to a violation of one of the ground principles of object-orientation, the principle of abstraction. The problem stems from the fact that in existing implementations of uniqueness, uniqueness is a property of the referenced object, or even the object's class---not a consequence of how the object is being used externally; whether or not an object can be uniquely referenced (and the semantics of a methods invoked on a unique receiver) must be considered when designing a class.

To this end we propose a different form of uniqueness, \emph{external uniqueness}, where all objects can be referenced uniquely, regardless of how they are implemented. An important consequence of our proposal is also the incorporation of innocuous internal pointers in the uniqueness definition. There may be an arbitrary number of references to a unique object, but only one of these may be visible externally. The resulting language is more powerful, in our opinion better suited to object-oriented programming, and also cleaner since it avoids the introduction of second-class constructs necessary in previous proposals to deal with the volatile nature of uniqueness which complicates the languages.

We base our proposal on ownership types, a system for enforcing encapsulation and provide a strong notion of aggregate. The symbiosis of external uniqueness and ownership types is mutually beneficial in that enabling external uniqueness in the presence of ownership types is virtually free, and lifts some of the restrictions in ownership types systems.

We present the design of external uniqueness along with a static semantics to guarantee the proper use of the constructs as well as a dynamic semantics as a basis for proving the important properties and soundness of our systems. We state the proofs and provide proof sketches, but save the complete technical account for the final PhD thesis. }

# External Uniqueness [Subsumes ECOOP 03 Article]

Submitted to SCP. Accepted with revisions. In preparation again.

## ABSTRACT

External uniqueness is a novel form of unique pointers that fit more natural with object-oriented programming. External uniqueness enforces the structural property that a unique pointer is a \emph{dominating node} to the aggregate it references---there may be no other pointer from outside the aggregate to objects in it in the rest of the system. This paper completes previous work by Clarke and the author [CW03b] with the full semantics of the Joline language and proofs of the structural invariants.

# Existential Owners for Ownership Types

Appeared in Journal of Object Technology, vol. 6, no. 4, May--June 2007, pp. 141--159.

## ABSTRACT

This paper describes a lightweight approach to adding run-time checked downcasts to a language in the presence of ownership types without the need for a run-time representation of owners. Previous systems [6] have required owners of objects to be tracked and matched at run-time which is costly in terms of memory and performance. Our proposal avoids run-time overhead to deal with owners and also extends the expressiveness of ownership-based systems enough to handle the Java equals idiom for structural equality comparison. The price is that it is sometimes impossible to downcast a type into a type that can be statically aliased. Our proposal is completely orthogonal and combinable with previous work.

# External Uniqueness is Unique Enough

Appeared at ECOOP 2003 -- European Conference on Object-Oriented Programming, Darmstadt, Germany, August 2003.

## ABSTRACT

External uniqueness is a surprising new way to add unique references to an OOPL. The idea is that an externally unique reference is the only reference into an aggregate from outside the aggregate. Internal references which do not escape the boundary of the aggregate are innocuous and therefore permitted. Based on ownership types, our proposal not only overcomes an abstraction problem from which existing uniqueness proposals suffer, it also enables many examples which are inherently not unique, such as a unique reference to a set of links in a doubly-linked list, without losing the benefits of uniqueness.