Latte: Lightweight Aliasing Tracking for Java

(authored by agents unless marked 🧑) Tag: zimmerman2023latte, paper

model and guarantee

Latte is a type system for a Featherweight-Java-like sequential language with mutable objects. Its goal is to track heap uniqueness and stack aliases with annotations on fields and method signatures, while inferring local-variable information. The abstract says, “Our approach only requires annotations for parameters and fields, while annotations for local variables are inferred.” (Abstract, p. 1). The system uses unique, shared, and owned; it infers alias(p) and bottom ⊥ for locals during checking (Sections 3.1 and 3.3, pp. 3–4).

The heap invariant is: “no two references in the heap point to the same unique object.” (Introduction, p. 1). A unique value may be stored in at most one reachable heap location, although the value may also be aliased in the local environment, and such dynamic aliases “may only be used as long as such aliasing can be precisely inferred” (Section 3.1, pp. 2–3). owned denotes a borrowed value that is unique in the current context, with no new aliases added to the heap; shared means untracked aliases may exist; ⊥ marks an inaccessible value (Section 3.4, p. 4).

Inference: the transferable technique is an explicit path-and-alias environment that is updated after every mutation. Inference: this is useful for Verus APIs that need to expose ownership or separation facts to later functional proofs, but Latte’s type rules are not a Verus implementation.

technique 1: minimal annotations with inferred locals

When to use it: use this design when annotating every temporary would make an ownership discipline hard to adopt, while field and method boundaries can carry stable contracts. Fields must be unique or shared; method parameters use unique, owned, or shared; local declarations receive no developer annotation (Section 3.3, p. 4). Return types are unique or shared in the grammar (Figure 2, p. 4) and the Introduction (p. 1), although the Conclusion (p. 7) lists all three for “parameters and return types”.

Steps from the paper:

1. Mark a field unique if its object must occur at most once in reachable heap storage, or shared if outside aliases may exist (Section 3.1, p. 3; Section 3.3, p. 4).
2. Mark a method parameter owned when the callee borrows a unique value without consuming it; use unique when the argument is consumed (a constructor taking unique arguments “consumes both arguments”, Section 3.2, p. 3); use shared when the value may or may not be unique (Section 3.1, p. 3; Section 3.4, p. 4).
3. Type-check statements while maintaining environment Δ, which maps each local variable to a class and an inferred annotation (Figure 3, p. 4).
4. Reject a use when the variable is inaccessible (⊥), or when the inferred aliases or reachability would violate uniqueness (Sections 3.4.1–3.4.4, pp. 4–5).

Verus form: Inference: use Rust ownership and borrowing for the executable alias discipline, then state heap separation or object uniqueness in requires and ensures; use ghost state or spec fn predicates for reachability. Inference: Verus does not infer alias(p) annotations automatically, so a developer must expose enough paths or write proof lemmas to recover equivalent facts.

Evidence: the paper’s stack example requires field and parameter annotations but no local annotations in the Java source (Figure 1, p. 3). It reports no user study, benchmark denominator, or implementation measurement. The conclusion explicitly calls for “Further evaluation of its usability, along with the development of such verification tools, is required to validate this goal.” (Conclusion, p. 7). Inference: annotation reduction is demonstrated by examples, not empirically established.

technique 2: alias graph and reachable aliasing

What it is: represent aliasing as an equivalence relation over syntactic paths. An environment entry x : alias(p) C records that x and path p hold the same object; the alias graph connects equivalent paths. Each connected component may contain at most one path with a unique, owned, or shared annotation (Section 3.4.1, p. 4).

Steps from the paper:

1. After an assignment x = p, add an alias-graph edge from x to p and record alias(p) in Δ (Sections 3.2 and 3.4.7, pp. 3 and 6).
2. Define reachable aliasing, written Δ ⊢ p1 ≅ p2, to mean that a value reachable from p1 may be aliased with a value reachable from p2; if Δ ⊬ p1 ≅ p2 the two paths are separately unique (Section 3.4.3, p. 5). Assignment to a unique field and calls with owned arguments require this relation to fail for the relevant paths (Figure 5, p. 6; Section 3.4.7, p. 6).
3. For a unique field assignment, isolate the field, type the right-hand side as unique(x.f), and record the resulting path relation; the field is isolated before the right-hand side is typed, which permits updating this.root to this.root.next without a destructive read (Section 3.4.7, p. 6).
4. Do not allow borrowing (passing as owned) a unique field of a shared object, because the same heap location may already be borrowed through another path; such a field value “can only be used after a destructive read or some equivalent operation” (Section 3.4.4, p. 5).

Verus form: Inference: model the alias graph as a ghost map from object identifiers to paths and prove a forall uniqueness predicate over reachable heap locations. Inference: Verus’s &mut borrow rules already prevent many executable aliases, but raw-pointer or interior-mutability APIs need explicit ghost permissions and invariants; Latte’s path graph can guide those invariants.

Evidence: the push example tracks r : alias(this.root), isolates this.root, and then treats r as unique before constructing a node (Section 3.2, pp. 3–4; Figure 1, p. 3). The paper presents typing rules and worked examples, but no soundness theorem (it says “assuming soundness of our approach for sequential programs”, Section 3.4.2, p. 5), and no measured false-positive rate. Inference: correctness depends on the modeled subset and on preserving the correspondence between paths and runtime objects.

technique 3: isolation as a non-destructive read

What it is: implement the effect of a destructive read by first creating an alias and then overwriting the source path. The isolation judgment, written Δ ∗ p ⊣ Δ′, removes all references to p from Δ; if p held a unique value and a variable x was aliased to p, then x holds a unique value after p is overwritten. The paper’s recipe is to introduce an alias to p, then overwrite p with a different value such as null (Section 3.4.5, p. 5). Rules distinguish three cases: no connected node, an aliased variable that can replace p, or an incoming reference edge that requires isolating a subfield first (Section 3.4.5, pp. 5–6).

Steps from the paper’s stack push:

1. Read this.root into r, recording r : alias(this.root) (Figure 1, lines 19–20, p. 3).
2. Assign this.root = null; the paper says this “isolates it in the typing environment”, invalidating all aliases to it, which “allows the previously-aliased variable r to become unique and thus claim ownership” (Section 3.2, p. 3).
3. Construct new Node(value, r), consuming the unique arguments; the constructor body is encapsulated, so the caller marks consumed values inaccessible (Section 3.2, pp. 3–4).
4. Assign the new node to this.root; the annotation of the local n becomes alias(this.root), since Δ stores annotations only for locals (Section 3.2, p. 4; Figure 1, line 22, p. 3).

The paper emphasizes that “we do not need to change the language semantics or introduce new language constructs.” (Section 3.2, p. 3). Verus form: Inference: write the operation as ordinary Rust assignment through an exclusive borrow, and prove an ensures clause that ownership of the old value moves to the returned or newly stored location. Inference: a ghost permission token can stand for the alias edge; the proof must show that the token is removed from the old path before the new path is stored.

Evidence: the paper walks through push step by step in Δ (Figure 1, p. 3) and discusses pop with the isolation and unification rules (Sections 3.4.5 and 3.4.8, pp. 5–6); it presents no checker implementation, and no runtime overhead is measured (Section 4, p. 7: “we would need to implement the system”). Inference: the technique is strongest for sequential code and explicit ownership transfer, while aliasing through opaque foreign code remains a trusted boundary.

technique 4: framing and branch unification

The frame of a method call is all fields of a passed object that the call may modify; aliases to fields in the frame must be invalidated after the call. Formally, variables connected in the reference graph to the argument paths are marked shared when alias tracking is unnecessary, or ⊥ when aliases must be tracked (Section 3.4.6, p. 6). Conditional branches are checked separately and merged with a conservative unify(Δ;Δ1;Δ2) operation (Sections 3.4.7–3.4.8, p. 6). If a variable has the same annotation in both branches it keeps it; if shared in both, it is shared; if alias(p1) and alias(p2) refer to a common path p, it becomes alias(p); otherwise it is ⊥ (Section 3.4.8, p. 6). Variables defined only inside a branch may be isolated away (Section 3.4.8, p. 6).

In the FIFO dequeue, an owned borrow of this.root is recursively passed through the list. The paper says n.next.value “is known to be unique since its container (n.next) is isolated at line 17”, so the value can be returned without an explicit destructive read (Section 3.5, p. 7; Figure 6, p. 7). Inference: this is a practical pattern for Verus recursive data structures: frame the mutated fields in method contracts, preserve an invariant over the list, and prove branch postconditions strong enough to unify at the return.

what is proved, trusted, and missing

The paper defines a formal grammar and typing judgments, and argues that the alias graph and uniqueness checks support mutation and separation reasoning (Sections 3.3–3.4, pp. 4–6; Appendix A, pp. 9–11). It does not report an implementation, corpus size, runtime, soundness theorem against Java semantics, or user-study denominator. It claims to “precisely track aliases of unique or borrowed values” only, argues soundness for concurrent programs “as long as unique values accessible to the spawned thread are consumed after a fork operation”, and the abstract describes “a local sequential setting” (Section 3.4.2, pp. 4–5; Abstract, p. 1).

techniques for the catalog

• boundary annotations: annotate fields and method parameters while inferring local alias states
• alias graph: maintain path equivalence and reachable-alias relations to enforce one unique heap location
• isolation: overwrite a path after recording its alias so the former value can become uniquely owned
• framing: invalidate aliases to fields that a method may mutate
• branch unification: conservatively join per-branch alias environments, using bottom when no safe common fact exists
• borrowed traversal: use owned recursive parameters and isolation to mutate linked structures without explicit destructive-read syntax

Last edited: 2026-10-18