Logotyp: till Uppsala universitets webbplats

Programming in an object-oriented language demands a fine balance between flexibility and control. At one level, objects need to interact freely to achieve our implementation goals. At a higher level, architectural constraints that ensure the system can be understood by new developers and can evolve as requirements change must be met. To resolve this tension, researchers have developed type systems expressing ownership and behavioural restrictions such as immutability. This work reports on our consolidation of the resulting discoveries into a single programming language. Our language, Joe 3 , imposes little additional syntactic overhead, yet can encode powerful patterns such as fractional permissions and the reference modes of Flexible Alias Protection.

Active objects offer a structured approach to concurrency, encapsulating both unshared state and a thread of control. For efficient data transfer, data should be passed by reference whenever possible, but this introduces aliasing and undermines the validity of the active objects. This paper proposes a minimal variant of ownership types that preserves the required race freedom invariant yet enables data transfer by reference between active objects (that is, without copying) in many cases, and a cheap clone operation where copying is necessary. Our approach is general and should be adaptable to several existing active object systems.

Ownership type systems give a strong notion of separation between aggregates. Objects belonging to different owners cannot be aliased, and thus a mutating operation internal to one object is guaranteed to be invisible to another. This naturally facilitates reasoning about correctness on a local scale, but also proves beneficial for coarse-grained parallelism as noninterference between statements touching different objects is easily established. For fine-grained parallelism, ownership types fall short as owner-based disjointness only allows separation of the innards of different aggregates, which is very coarse-grained. Concretely: ownership types can reason about the disjointness of two different data structures, but cannot reason about the internal structure or disjointness within the data structure, without resorting to static and overly constraining measures. For similar reasons, ownership fails to determine internal disjointness of external pointers to objects that share a common owner. In this paper, we introduce the novel notion of refined ownership which overcomes these limitations by allowing precise local reasoning about a group of objects even though they belong to the same external owner. Using refined ownership, we can statically check determinism of parallel operations on tree-shaped substructures of a data structure, including operations on values external to the structure, without imposing any non-local alias restrictions.