Context Sensitive Typechecking And Inference: Ownership And Immutability

Abstract

Context sensitivity is one important feature of type systems that helps creating concise type rules and getting accurate types without being too conservative. In a context-sensitive type system, declared types can be resolved to different types according to invocation contexts, such as receiver and assignment contexts. Receiver-context sensitivity is also called viewpoint adaptation, meaning adapting declared types from the viewpoint of receivers. In receiver-context sensitivity, resolution of declared types only depends on receivers' types. In contrast, in assignment-context sensitivity, declared types are resolved based on context types to which declared types are assigned to.

The Checker Framework is a poweful framework for developing pluggable type systems for Java. However, it lacks the ability of supporting receiver- and assignment-context sensitivity, which makes the development of such type systems hard. The Checker Framework Inference is a framework based on the Checker Framework to infer and insert pluggable types for unannotated programs to reduce the overhead of manually doing so. This thesis presents work that adds the two context sensitivity features into the two frameworks and how those features are reused in typechecking and inference and shared between two different type systems --- Generic Universe Type System (GUT) and Practical Immutability for Classes And Objects (PICO).

GUT is an existing light-weight object ownership type system that is receiver-context sensitive. It structures the heap hierarchically to control aliasing and access between objects. GUTInfer is the corresponding inference system to infer GUT types for unannotated programs. GUT is the first type system that introduces the concept of viewpoint adaptation, which inspired us to raise the receiver-context sensitivity feature to the framework level. We adapt the old GUT and GUTInfer implementation to use the new framework-level receiver-context sensitivity feature. We also improve implicits rules of GUT to better handle corner cases.

Immutability is a way to control mutation and avoid unintended side-effects. Object immutability specifies restrictions on objects, such that immutable objects' states can not be changed. It provides many benefits such as safe sharing of objects between threads without the need of synchronization, compile- and run-time optimizations, and easier reasoning about the software behaviour etc. PICO is a novel object and class immutability type system developed using the Checker Framework with the new framework-level context sensitivity features. It transitively guarentees the immutability of the objects that constitute the abstraction of the root object. It supports circular initialization of immutable objects and mutability restrictions on classes that influence all instances of that class. PICO supports creation of objects whose mutability is independent from receivers, which inspired us to add the assignment-context sensitivity feature to the framework level. PICOInfer is the inference system that infers and propagates mutability types to unannotated programs according to PICO's type rules.

We experiment PICO, PICOInfer and GUTInfer on 16 real-world projects up to 71,000 lines of code in total. Our experiments indicate that the new framework-level context sensitivity features work correctly in PICO and GUT. PICO is expressive and flexible enough to be used in real-world programs. Improvements to GUT are also correct.