Lesson 19.9 — Escape analysis and shape analysis¶
Techniques: escape analysis (Choi et al.'s connection graphs and escape states; stack allocation, scalar replacement and lock elision; Go's and HotSpot's implementations); shape analysis (an overview: Sagiv, Reps and Wilhelm's three-valued logic and TVLA; separation logic and list-segment abstraction, as in Facebook Infer) · Pebble implements: nothing (Pebble has no heap allocation of its own; the lab's capture question for DSE is the intraprocedural core of escape analysis) · Prerequisites: Lesson 19.2 (capture tracking), Lesson 19.4, abstract interpretation (Lesson 14.7) · Time: 4 hours
1. Problem and motivation¶
Points-to analysis answers "where may this pointer point?". Two related questions drive important optimizations and verifications.
Escape analysis¶
Does this object outlive its creator or leave its thread? If an object allocated in a method is never reachable after the method returns, it can live on the stack (or be split into scalars: scalar replacement); if it is never reachable from another thread, locks on it can be removed (lock elision). Choi, Gupta, Serrano, Sreedhar and Midkiff defined escape analysis for Java with connection graphs and three escape states [Cho99]. HotSpot's C2 JIT follows their design [HotSpot-EA]; the Go compiler decides stack versus heap allocation for every new, &T{} and make with its own escape analysis [Go-Escape]. Capture tracking (Lesson 19.2) is the intraprocedural core of the same question.
Shape analysis¶
What does the heap look like? Points-to sets name allocation sites, so every node of a linked list built in a loop is the same abstract object, and the analysis cannot tell a list from a cycle or a tree from a DAG. Shape analysis keeps enough structure to prove properties such as "x points to an acyclic list" or "these two lists share no node". Sagiv, Reps and Wilhelm's parametric framework uses three-valued logic with summary nodes (TVLA) [SRW02]; separation logic describes heaps with a separating conjunction and inductive predicates such as list segments [Rey02], and Calcagno, Distefano, O'Hearn and Yang made it compositional with bi-abduction, the analysis inside Facebook Infer [CDOY09, Infer-Biabduction]. Shape analysis is used in verifiers and bug finders, not in optimizing compilers.
2. Definitions and algorithms¶
Escape analysis¶
Definition 19.9.1 (Escape states)
The escape lattice is \(\mathsf{NoEscape} \sqsubset \mathsf{ArgEscape} \sqsubset \mathsf{GlobalEscape}\). An object allocated in method \(m\) is \(\mathsf{NoEscape}\) if it is not reachable from any global, parameter, return value or other thread after \(m\) returns; \(\mathsf{ArgEscape}\) if it is reachable from \(m\)'s parameters or return value but not from globals or other threads; \(\mathsf{GlobalEscape}\) otherwise [Cho99].
Definition 19.9.2 (Connection graph)
A connection graph of a method has nodes for local variables, parameters, globals, the method's
return value, allocation sites (object nodes) and fields of object nodes. Edges: a points-to edge
from a variable or field to an object it may reference, and a deferred edge \(x \to y\) for an
assignment x = y (resolved lazily, like a copy edge in Andersen's graph). Each node carries an
escape state; globals, and objects passed to native code or other threads, start as
\(\mathsf{GlobalEscape}\); parameters and the return value as \(\mathsf{ArgEscape}\).
Algorithm 19.9.3 (Escape analysis over a connection graph)
- Input: a method; summaries (the escape states of callee parameters) for its calls.
- Output: an escape state per allocation site.
- Precondition: callee summaries are available bottom-up (or calls are treated as \(\mathsf{GlobalEscape}\) for their arguments).
- Postcondition: every object reachable in the connection graph from a node of state \(e\) has state \(\sqsupseteq e\) (Theorem 19.9.6).
- Invariant: escape states only increase; each node's state is at least the join of the states of the nodes that reach it.
function Escape(m):
build the connection graph G of m:
x = new h: x →pt obj_h
x = y: deferred edge x → y
x.f = y: for each obj o with x →pt o: field node o.f, deferred edge o.f → y
x = y.f: for each obj o with y →pt o: deferred edge x → o.f
global g = y: state(y) ← GlobalEscape
return y: state(y) ← ArgEscape at least
call g(a1, …): state(ai) ← summary state of g's parameter i (GlobalEscape if unknown)
resolve deferred edges (as Andersen's copy edges: Algorithm 19.4.4)
worklist propagation: for every edge u → w (points-to, deferred or field):
state(w) ← state(w) ⊔ state(u) # escape flows along reachability
return { h ↦ state(obj_h) }
A \(\mathsf{NoEscape}\) object can be stack-allocated or scalar-replaced; an object that does not escape its thread (neither \(\mathsf{GlobalEscape}\) nor passed to a thread-starting call) can have its locks elided.
Shape analysis¶
Definition 19.9.4 (Three-valued structures and canonical abstraction)
A three-valued logical structure over predicates \(P\) has a finite set of individuals \(U\) and,
for each \(k\)-ary predicate \(p\), a map \(\iota(p) : U^k \to \{0, \tfrac12, 1\}\) (1 true, 0 false,
\(\tfrac12\) unknown); a unary predicate \(\mathit{sm}\) marks summary individuals, which stand for
one or more concrete nodes. Canonical abstraction merges all concrete nodes that agree on the
unary abstraction predicates (e.g. "pointed to by x", "reachable from x") into one individual;
a predicate value becomes \(\tfrac12\) where the merged nodes disagree [SRW02]. In separation logic,
a symbolic heap \(\Pi \wedge \Sigma\) describes a heap by a spatial formula \(\Sigma\) built from
\(x \mapsto y\) ("the cell at \(x\) holds \(y\)"), \(\mathrm{lseg}(x, y)\) ("an acyclic list segment from \(x\)
to \(y\)") and the separating conjunction \(\ast\) (disjoint heaps) [Rey02].
Algorithm 19.9.5 (Shape analysis by abstract interpretation with list-segment abstraction)
- Input: a program that manipulates singly-linked lists (fields
next); a precondition as a symbolic heap. - Output: at each program point, a finite set of symbolic heaps (a disjunction) that describes every reachable concrete heap.
- Precondition: the abstraction rules below are sound entailments of separation logic.
- Postcondition: the fixed point over-approximates every execution (Theorem 19.9.7).
- Invariant: every symbolic heap in a set is in normal form: no two list segments can be merged, every non-program variable is shared.
function Shape(program, pre):
S[entry] ← {pre}; worklist over program points
for a statement at point ℓ and each symbolic heap H in S[ℓ]:
H' ← SymbolicExecute(statement, H) # x = y.next: materialize (unfold lseg(y, z) into
# y ↦ y' ∗ lseg(y', z), with a case y = z); update
H'' ← Abstract(H') # rewrite y ↦ z ∗ z ↦ w ⇝ lseg(y, w) when z is
# not a program variable (forget the middle)
add H'' to S[next point] unless it is entailed by a heap already there
until no set changes (finitely many normal forms up to renaming ⇒ termination)
TVLA's version replaces SymbolicExecute/Abstract by focus (materialize a definite individual
out of a summary), predicate update formulas, coerce (sharpen with integrity constraints) and
blur (canonical abstraction) [SRW02].
3. Worked example¶
Escape analysis¶
The Go program of the first box (§7), with Go's decisions and the connection-graph reasoning of Algorithm 19.9.3:
| function | allocation | connection graph facts | state | Go's decision |
|---|---|---|---|---|
sum |
&point{1, 2} → p |
p is only dereferenced (p.x, p.y) |
NoEscape | "does not escape" (stack) |
leak |
q := point{3, 4}, &q returned |
return → ArgEscape; the object outlives the frame |
ArgEscape | "moved to heap: q" |
store |
&point{n, n} → r |
global = r → GlobalEscape |
GlobalEscape | "escapes to heap" |
slice |
make([]int, 8) → s |
only indexed; constant size | NoEscape | "does not escape" (stack) |
leak's object is only ArgEscape — no thread or global sees it — but Go must still heap-allocate it because the caller receives it; a caller that inlines leak could keep it on its own stack (Go's inlining happens before escape analysis, as the "can inline" lines show). The HotSpot box shows the payoff of NoEscape: C2 scalar-replaces the Point of sum, so 10 million calls allocate 0 MB instead of 240 MB.
Shape analysis¶
Building a list in a loop from \(x = \mathsf{null}\): while (c) { t = malloc(); t->next = x; x = t; }. The symbolic heaps at the loop head, iteration by iteration (Algorithm 19.9.5):
| iteration | heap after the body | after abstraction | new at the head? |
|---|---|---|---|
| 0 (entry) | — | \(x = \mathsf{null} \wedge \mathsf{emp}\) | yes |
| 1 | \(x \mapsto \mathsf{null}\) | \(x \mapsto \mathsf{null}\) (nothing to merge) | yes |
| 2 | \(x \mapsto t' \ast t' \mapsto \mathsf{null}\) | \(\mathrm{lseg}(x, \mathsf{null})\) (\(t'\) is not a program variable) | yes |
| 3 | \(x \mapsto x' \ast \mathrm{lseg}(x', \mathsf{null})\) | \(\mathrm{lseg}(x, \mathsf{null})\) | no: entailed by iteration 2's heap |
The fixed point \(\{ x = \mathsf{null} \wedge \mathsf{emp},\ x \mapsto \mathsf{null},\ \mathrm{lseg}(x, \mathsf{null}) \}\) proves that x always points to an acyclic, null-terminated list — something a points-to analysis (one abstract object for the malloc site, pointing to itself) cannot express. In TVLA the same result is a structure with a definite node pointed to by x and a summary node for the rest, with reachable-from-x true on both and next \(\tfrac12\) among the summarized nodes.
4. Invariants and correctness¶
Escape analysis¶
Theorem 19.9.6 (NoEscape objects are dead after their method returns)
If Algorithm 19.9.3 assigns \(\mathsf{NoEscape}\) to allocation site \(h\) in method \(m\), then no object created at \(h\) in an activation of \(m\) is reachable (from globals, other threads or the caller's frame) after that activation returns; so allocating it in \(m\)'s stack frame is safe.
Proof
After \(m\) returns, the only roots through which the caller or other code can reach objects created in \(m\) are globals, other threads, objects reachable from \(m\)'s parameters (the caller's objects, possibly modified by \(m\)) and \(m\)'s return value. The connection graph over-approximates reachability during \(m\) (it is an Andersen-style points-to graph with fields: Theorem 19.4.12's argument applies, with call summaries sound by assumption). Every root is initialised with state \(\mathsf{ArgEscape}\) or \(\mathsf{GlobalEscape}\), and the propagation makes every node reachable from a root at least that state. So an object with state \(\mathsf{NoEscape}\) is not reachable from any root in the graph, hence not in any execution; nothing can dereference it after the frame is gone.
Shape analysis¶
Theorem 19.9.7 (Soundness of shape abstraction)
If the symbolic execution rules and the abstraction rules are sound (every concrete heap satisfying the input formula, after the statement, satisfies the output formula), then the fixed point of Algorithm 19.9.5 describes every concrete heap reachable at each program point, and the algorithm terminates.
Proof sketch (full proofs: [SRW02, §4] (the embedding theorem for three-valued structures); [CDOY09, §3–4] for separation logic with bi-abduction)
Soundness is the abstract-interpretation argument of Ch 14: each step maps a formula describing a set of concrete heaps to a formula describing (a superset of) their successors, and abstraction only weakens formulas (an entailment \(H' \vdash H''\)), so by induction on execution length every concrete heap is described. In the three-valued setting the key fact is the embedding theorem: a formula evaluated in a structure that embeds a concrete structure gives a value that is \(\tfrac12\) or equal to the concrete value, so conclusions drawn from definite values hold concretely. Termination: normal forms mention only program variables and a bounded number of shared nodes (for lists: nodes pointed to by variables), so up to renaming there are finitely many, and the disjunctive domain is finite.
5. Complexity¶
| Technique | Time | Space | Variables |
|---|---|---|---|
| Escape analysis (per method) | connection graph construction \(O(s)\) plus resolution as Andersen on the method: \(O(n^3)\) worst case, near-linear in practice; bottom-up over the call graph | \(O(n^2)\) | \(s\) statements, \(n\) graph nodes |
| Shape analysis (TVLA) | exponential: up to \(2^{k}\) abstract individuals for \(k\) unary abstraction predicates, and sets of structures | exponential | \(k\) abstraction predicates |
| Shape analysis (separation logic, lists) | number of normal-form symbolic heaps: exponential in the number of pointer variables (which variables share, which segments exist) | same | program variables |
Justification. Escape analysis is a points-to analysis restricted to one method plus a monotone propagation over a three-element lattice (each node changes at most twice). Canonical abstraction maps each concrete node to one of \(2^k\) valuations of the abstraction predicates, so a structure has at most \(2^k\) individuals, and the analysis keeps sets of such structures. Pathological family for separation-logic list analysis: \(v\) list variables pointing into one list can appear in any order along it: \(v!\) orderings of shared nodes, each a distinct normal form. Go's escape analysis runs on every package at every build; shape analysis is used by verifiers and bug finders that can afford seconds to minutes per procedure (Infer analyses procedures independently, which is what makes it scale to large code bases [CDOY09]).
6. Variants and refinements¶
Escape analysis¶
- Partial escape analysis (Graal): an object may escape on some paths only; allocate it lazily on those paths ("materialize") and keep it scalar elsewhere; trade-off: control-flow-sensitive state per object.
- Interprocedural summaries (Go's parameter tags: "leaks to heap", "leaks to result"): every call site reuses them; trade-off: coarse per-parameter facts.
- Thread-escape analysis for lock elision and for separating thread-local heaps; trade-off: needs knowledge of thread-starting calls.
Shape analysis¶
- TVLA [SRW02]: arbitrary user-defined predicates (reachability, sharing, cyclicity); trade-off: precision tuned by the predicate set, exponential cost.
- Separation-logic list and tree abstractions with bi-abduction [CDOY09]: compositional per-procedure specs; trade-off: fixed predicate families (lists, trees), less expressive than TVLA but scalable.
- Graph grammars and forest automata: other shape abstractions for complex structures; trade-off: specialised implementations.
7. In real compilers¶
Escape analysis¶
Go, HotSpot
Go src/cmd/compile/internal/escape/escape.go — the header comment states the two invariants
(pointers to stack objects are never stored in the heap and never outlive the object) and the
"directed weighted graph" of locations with dereference counts as weights [Go-Escape] (go1.24.7).
HotSpot src/hotspot/share/opto/escape.cpp — ConnectionGraph::compute_escape builds Choi et
al.'s connection graph for a C2 compilation unit; non-escaping allocations are scalar-replaced and
their locks eliminated [HotSpot-EA] (JDK 21). LLVM has no heap-to-stack pass for C malloc in its
default pipeline, but its capture tracking (Lesson 19.2) answers the same question for allocas and
noalias calls.
The Go compiler's escape decisions
Reproduce (go 1.24.7 (linux/amd64)):
cat > esc.go <<'GO'
package esc
type point struct{ x, y int }
func sum(n int) int { // p stays on the stack: its address never leaves sum
p := &point{1, 2}
return p.x + p.y + n
}
func leak() *point { // q escapes through the return value: heap
q := point{3, 4}
return &q
}
var global *point
func store(n int) { // r escapes into a global: heap
r := &point{n, n}
global = r
}
func slice(n int) int { // a small constant-size slice stays on the stack
s := make([]int, 8)
s[n%8] = n
return s[0]
}
GO
cat > go.mod <<'MOD'
module esc
go 1.24
MOD
go build -gcflags=-m . 2>&1 | grep -v '^#'
Output (complete):
./esc.go:5:6: can inline sum
./esc.go:10:6: can inline leak
./esc.go:17:6: can inline store
./esc.go:22:6: can inline slice
./esc.go:6:7: &point{...} does not escape
./esc.go:11:2: moved to heap: q
./esc.go:18:7: &point{...} escapes to heap
./esc.go:23:11: make([]int, 8) does not escape
What to notice: the four decisions of the §3 table: &point{...} in sum and make([]int, 8) "does not escape" (stack); q is "moved to heap" because its address is returned; the literal in store "escapes to heap" through the global. The "can inline" lines show that inlining runs first, which can turn an ArgEscape object into a NoEscape one in the caller.
HotSpot C2: escape analysis removes the allocation
Reproduce (OpenJDK 21.0.10 (Ubuntu build 21.0.10+7); Linux x86-64):
unset JAVA_TOOL_OPTIONS
cat > EA.java <<'J'
import java.lang.management.ManagementFactory;
public class EA {
record Point(int x, int y) {}
static int sum(int n) { Point p = new Point(n, n + 1); return p.x() + p.y(); } // p never escapes
public static void main(String[] args) {
var mx = (com.sun.management.ThreadMXBean) ManagementFactory.getThreadMXBean();
long t = Thread.currentThread().threadId(), s = 0;
for (int i = 0; i < 200_000; i++) s += sum(i); // warm up: C2 compiles sum
long before = mx.getThreadAllocatedBytes(t);
for (int i = 0; i < 10_000_000; i++) s += sum(i);
long after = mx.getThreadAllocatedBytes(t);
System.out.println("allocated " + (after - before) / 1_000_000 + " MB for 10M calls (s=" + s + ")");
}
}
J
javac EA.java
echo "== default (C2 escape analysis on):"; java -XX:+UseSerialGC EA 2>/dev/null
echo "== -XX:-DoEscapeAnalysis:"; java -XX:+UseSerialGC -XX:-DoEscapeAnalysis EA 2>/dev/null
echo "== the diagnostic printer needs a debug JVM:"; java -XX:+PrintEscapeAnalysis -version 2>&1 | grep -v JAVA_TOOL | head -2
Output (complete):
== default (C2 escape analysis on):
allocated 0 MB for 10M calls (s=100040000000000)
== -XX:-DoEscapeAnalysis:
allocated 240 MB for 10M calls (s=100040000000000)
== the diagnostic printer needs a debug JVM:
Error: VM option 'PrintEscapeAnalysis' is notproduct and is available only in debug version of VM.
Error: Could not create the Java Virtual Machine.
What to notice: with escape analysis on (the default), 10 million calls of sum allocate 0 MB: the Point never escapes and C2 scalar-replaces it (Theorem 19.9.6); with -XX:-DoEscapeAnalysis the same loop allocates 240 MB (10 million 24-byte objects). The diagnostic -XX:+PrintEscapeAnalysis is a notproduct flag that only debug builds of the JVM accept, as the last lines show.
Shape analysis¶
Infer
Facebook Infer infer/src/biabduction/Predicates.mli — the heap predicates of its separation-logic
analysis: Hpointsto (\(x \mapsto \dots\)), Hlseg (list segments, non-empty or possibly empty) and
Hdllseg (doubly-linked segments) [Infer-Biabduction, CDOY09] (Infer 1.2.0). TVLA was a research
system from Tel Aviv University [SRW02]. No production optimizing compiler runs shape analysis.
Infer's separation-logic heap predicates
Reproduce (curl 8.5.0; source at tag v1.2.0):
curl -sL https://raw.githubusercontent.com/facebook/infer/v1.2.0/infer/src/biabduction/Predicates.mli -o Predicates.mli
sed -n '/^type lseg_kind =/,/Lseg_PE/p' Predicates.mli
grep -nE '^ \| H(pointsto|lseg|dllseg) of' Predicates.mli
Output (complete):
type lseg_kind =
| Lseg_NE (** nonempty (possibly circular) listseg *)
| Lseg_PE (** possibly empty (possibly circular) listseg *)
120: | Hpointsto of Exp.t * 'inst strexp0 * Exp.t
123: | Hlseg of lseg_kind * 'inst hpara0 * Exp.t * Exp.t * Exp.t list
127: | Hdllseg of lseg_kind * 'inst hpara_dll0 * Exp.t * Exp.t * Exp.t * Exp.t * Exp.t list
What to notice: the symbolic-heap vocabulary of Definition 19.9.4: a points-to predicate, a list-segment predicate Hlseg with the two kinds Lseg_NE (non-empty) and Lseg_PE (possibly empty), and doubly-linked segments — exactly what the §3 trace uses.
8. Comparison¶
| Technique | Power / precision | Speed (asymptotic · practical) | Output / error quality | Implementation effort | Typical use |
|---|---|---|---|---|---|
| Escape analysis | Three states per allocation site; flow-insensitive per method (partial EA adds path sensitivity) | near-linear per method · runs on every Go build and every C2 compilation | Per-site decisions ("moved to heap: q"); explains allocations | Medium | Go (stack vs heap), HotSpot C2 and Graal (scalar replacement, lock elision) |
| Shape analysis | Proves list/tree shapes, acyclicity, disjointness; far beyond points-to | exponential · seconds to minutes per procedure | Symbolic heaps or 3-valued structures; can prove memory safety | High | Verifiers and bug finders (Infer, TVLA-based research tools) |
Choose escape analysis whenever allocation cost matters (managed languages): it is cheap and its decisions are local. Choose shape analysis for verification and bug finding on heap-manipulating code, where points-to sets cannot express the property you need.
9. Assessment¶
- Quiz:
escape-go-decisions,escape-lattice(tagescape);shape-lseg-fixpoint,shape-vs-pointsto(tagshape). - Drill: none: escape states are a propagation over a three-element lattice on the points-to graph (practise the graph with
./course drill points-to-andersen), and shape analysis is covered at overview depth with the quiz tracing the list-building fixpoint. - Flashcards: tags
escape,shape. - Exercises: none; exercise E1's non-escaping-local rule (via
PointerMayBeCaptured) is the intraprocedural core of escape analysis.
References¶
See the chapter references.