Candidate: Mier Ta
Title: Context Sensitive Typechecking And Inference: Ownership And Immutability
Date: March 29, 2018
Time: 2:30 PM
Place: E5 5047
Supervisor(s): Dietl, Werner M.
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. Resolution of them 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 powerful 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 framework level 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 inspire us to raise the receiver-context sensitivity feature into framework level. We adapt old GUT and GUTInfer implementation to use the new framework-level receiver-context sensitivity feature. We also improve implicits rules and viewpoint adaptation rules of GUT to better handle corner cases.
Object immutability specifies restrictions on objects to avoid mutations to immutable objects. 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 behavior etc. PICO is a novel object and class immutability type system developed using the Checker Framework with the new framework-level context sensitivity feature. It transitively guarantees the immutability of abstract state 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 getting objects whose mutability is independent from receivers to support factory design pattern, which inspires us to add the assignment-context sensitivity feature to framework level. PICOInfer 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 71kSLOC, and verify the correctness of results. 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. New implicit rules and viewpoint adaptation rules updates in GUT make sense.