Ownership types and safe lazy upgrades in object-oriented databases

Abstract This paper describes a novel mechanism for upgrading objects in an object-oriented database. Unlike earlier systems, our mechanism is expressive, supporting a rich set of upgrades; it is efficient and does not stop application access to run an upgrade; it avoids making copies of the database; yet it provides good semantics. Expressive efficient upgrades can lead to problems for the code that upgrades objects. For example, the code might observe broken invariants or interfaces unknown at the time it was written. The paper shows how to use a variant of ownership types to avoid such problems and enable programmers to reason about the correctness of their upgrades. Our approach to correctness is novel, and is a significant contribution of this paper. This paper also presents a new ownership type system. Previous ownership type systems only supported a weak encapsulation property. Enforcing object encapsulation, while supporting subtyping and paradigms like iterators, has been an open problem. Our type system provides a satisfactory solution to this open problem. The novel idea is that we handle inner classes specially--our type system allows objects of inner classes to have privileged access to the representations of the corresponding objects of the outer classes. This principled violation of encapsulation allows programmers to express paradigms like iterators, yet they can reason locally about program correctness