Latte: Lightweight Aliasing Tracking for Java

TL;DR

Latte introduces a lightweight aliasing tracking method for Java that minimizes annotations and complexity, supporting destructive reads and practical applications like stack modeling.

Contribution

It presents a novel aliasing tracking approach that reduces annotation requirements and complexity while supporting destructive reads in object-oriented Java programs.

Findings

Effective aliasing and uniqueness tracking with minimal annotations

Supports destructive reads without language or runtime modifications

Practical application demonstrated with stack modeling

Abstract

Many existing systems track aliasing and uniqueness, each with their own trade-off between expressiveness and developer effort. We propose Latte, a new approach that aims to minimize both the amount of annotations and the complexity of invariants necessary for reasoning about aliasing in an object-oriented language with mutation. Our approach only requires annotations for parameters and fields, while annotations for local variables are inferred. Furthermore, it relaxes uniqueness to allow aliasing among local variables, as long as this aliasing can be precisely determined. This enables support for destructive reads without changes to the language or its run-time semantics. Despite this simplicity, we show how this design can still be used for tracking uniqueness and aliasing in a local sequential setting, with practical applications, such as modeling a stack.