PaperlayerView exact revision on arXiv

Source-linked AI summary

Equality Saturation: A New Approach to Optimization

Ross Tate, Michael Stepp, Zachary Tatlock, Sorin Lerner

arXiv:1012.1802v3cs.PL

TL;DR

Traditional sequential, destructive optimization suffers from phase ordering and local profitability decisions. The paper uses equality analyses and saturation in a shared IR to preserve multiple optimized versions, then selects among them globally. It presents an approach that addresses ordering, discovers intricate opportunities, and supports translation validation, while acknowledging scope boundaries in semantic preservation and heap modeling.

  • Problem

    Traditional sequential optimizations can make code quality depend on optimization order, while local profitability heuristics cannot account well for future transformations.

  • Method

    Optimizations add equalities to a shared E-PEG-based IR, repeatedly saturating it so multiple optimized versions are represented before global selection.

  • Results

    The approach addresses phase ordering, enables global profitability heuristics, discovers intricate optimization opportunities, and performs translation validation.

  • Takeaways & Limitations

    Equality saturation provides one optimization structure that can optimize programs and validate transformations from other compilers.

  • Takeaways & Limitations

    Semantic preservation is not perfect for non-termination, and heap summary nodes still face a linear-typing challenge when converting PEGs back to CFGs.

Abstract

from arXiv · show

Optimizations in a traditional compiler are applied sequentially, with each optimization destructively modifying the program to produce a transformed program that is then passed to the next optimization. We present a new approach for structuring the optimization phase of a compiler. In our approach, optimizations take the form of equality analyses that add equality information to a common intermediate representation. The optimizer works by repeatedly applying these analyses to infer equivalences between program fragments, thus saturating the intermediate representation with equalities. Once saturated, the intermediate representation encodes multiple optimized versions of the input program. At this point, a profitability heuristic picks the final optimized program from the various programs represented in the saturated representation. Our proposed way of structuring optimizers has a variety of benefits over previous approaches: our approach obviates the need to worry about optimization ordering, enables the use of a global optimization heuristic that selects among fully optimized programs, and can be used to perform translation validation, even on compilers other than our own. We present our approach, formalize it, and describe our choice of intermediate representation. We also present experimental results showing that our approach is practical in terms of time and space overhead, is effective at discovering intricate optimization opportunities, and is effective at performing translation validation for a realistic optimizer.

Introduction

The paper replaces destructive, sequential compiler optimizations with equality analyses over a shared IR that preserves multiple optimized versions. Equality saturation removes ordering concerns, supports global profitability decisions, and enables translation validation.

  • Motivation: Sequential optimizations create phase-ordering problems because earlier transformations can prevent later, more profitable transformations from triggering.Traditional profitability heuristics also decide one optimization at a time, making future transformation effects difficult to assess.
  • Global selection: The saturated IR compactly represents multiple optimized programs, allowing a heuristic to choose among fully optimized candidates with a global view.The prototype uses a Pseudo-Boolean solver and static node costs to select the lowest-cost equivalent program.
  • Approach: Optimizations add equality information to a common IR rather than destructively replacing the program, preserving both original and transformed versions.Repeated equality analyses infer new equivalences until saturation, subject to a bound when analyses cause unbounded expansion.
  • Validation: The approach can perform translation validation by checking whether saturation derives equality between an optimized program and the original.This permits validation of optimizations from existing compilers even when the paper’s profitability heuristic would not select them.
  • Evaluation: The paper instantiates the approach in Peggy and reports that it is practical in time and space, discovers intricate opportunities, and validates a realistic optimizer.The contribution summary identifies optimization, discovery of simple and intricate opportunities, and translation validation as the experimental targets.
  • Intermediate representation: Program Expression Graphs support equality reasoning over computations including branches and loops, while E-PEG equivalence classes efficiently represent exponentially many expressions.E-PEGs also let the saturation engine incorporate previously discovered equalities efficiently.

expressions.

The paper represents imperative programs with equality-friendly PEGs and E-PEGs, allowing many optimization paths to coexist until a final choice or equivalence check is made. This addresses ordering and profitability challenges while supporting translation validation.

  • PEG representation: θ nodes represent the sequence of values taken by each loop-live variable across iterations.The first child gives the initial value, while the second represents later values in terms of prior iterations.
  • PEG representation: PEG operators are pure mathematical functions, enabling referentially transparent equality reasoning even for branches and loops.Stateful operations are represented functionally by threading heap summary nodes through operations.
  • PEG representation: 3% of Java methods are not optimized because the heap-operation linearization procedure is incomplete.PEG reasoning permits duplicated heap summaries, but conversion back to control-flow graphs requires a linear-typing discipline that the solver may fail to find.
  • Equality representation: An E-PEG groups equal PEG nodes into equivalence classes, and saturation repeatedly adds equalities to encode many optimized versions.The saturated E-PEG in the example represents 128 expressions because it contains seven independent equalities.
  • Optimization benefits: Because transformations add information without deleting the original program, the representation can explore optimization sequences without phase-ordering failures.This simultaneously explores possible optimization orders while sharing work common to those sequences.
  • Optimization benefits: A global profitability heuristic can select among versions after later optimizations reveal interactions such as inlining enabling strength reduction.The E-PEG retains both inlined and non-inlined versions while subsequent analyses operate on both.
  • Translation validation: Saturated E-PEGs can establish translation validity by checking whether input and optimized functions belong to the same equivalence class.This supports validation for compilers other than the optimizer that produced the E-PEG.

2. Reasoning about loops

PEGs encode loop-varying values, loop termination, and post-loop values so equality reasoning can analyze single and nested loops. Saturation can derive an inter-loop strength reduction that transforms an equivalent loop into a faster form.

  • Nested loops: The approach can discover unanticipated optimizations across nested loops from a simple axiom set.The section presents inter-loop strength reduction as the relevant optimization for loop structures.
  • Single loops: PEGs represent each loop-varying value with a θ node, each live-after-loop value with an eval node, and loop termination with one pass node.A θ node produces the sequence of values across iterations; eval selects a post-loop value using an index, while pass identifies the terminating iteration.
  • Nested loops: Nested-loop PEGs use depth-subscripted θ, eval, and pass nodes to connect values across inner and outer loop iterations.The representation records initialization on first iterations and values carried from preceding inner-loop or outer-loop computations.
  • Inter-loop strength reduction: The profitability heuristic selects nodes that reconstruct Figure 4(d), optimizing the equivalent code in Figure 4(a) to the faster code in Figure 4(b).The selected form favors sum++ over i*10 + j because the former is cheaper.

Summary.

The examples show how local equality reasoning in PEGs produces non-local code motion, CFG restructuring, loop peeling, and branch hoisting, while a global heuristic selects among resulting versions.

  • Scope: The examples demonstrate that simple local axioms can discover complex optimizations and reason about loop interactions, though several advanced loop optimizations remain unexplored.The paper specifically identifies loop fusion, unrolling, and interchange as requiring further work.
  • Code motion: Local PEG axioms can move computation into loops, turning a multiplication after the loop into a scaled increment and initial value.The transformation distributes multiplication through eval and then applies loop-induction-variable strength reduction.
  • CFG restructuring: Local multiplication distribution through φ nodes can radically restructure an equivalent program’s branching control-flow graph.The example applies distribution through two φ nodes followed by constant folding.
  • Loop peeling: General-purpose axioms can peel a loop while guarding the peeled iteration, and repeated peeling remains available as a candidate transformation.A separated profitability heuristic chooses the best peeling degree after saturation.
  • Branch hoisting: PEG semantics allow eval to distribute through φ and multiplication to factor through eval, hoisting loop-based operations outside a conditional structure.The resulting transformation moves the branch outside the loop and radically restructures the program.

4. Formalization of our Approach

The formalized optimizer converts a CFG to an equality-rich IR, repeatedly applies analyses to saturation, selects a profitable program, and converts it back. Monotonic analyses yield unique saturated normal forms when termination holds, but unrestricted saturation may not terminate.

  • Optimizer pipeline: Optimize converts the input CFG to an IR, saturates it with equalities, selects the best program globally, and converts that program back.These four stages define the paper’s optimizer pipeline.
  • Components: An instantiation combines an equality-reasoning IR, translation functions, a saturation engine, and a global profitability heuristic.The named components are ConvertToIR, ConvertToCFG, Saturate, and SelectBest.
  • Saturation: Saturation repeatedly runs equality analyses that add equalities to an E-PEG, with nondeterminism allowing an analysis to choose among multiple applicable locations.The IR order is based on encoded nodes and equalities.
  • Convergence: For monotonic equality analyses, any trace that reaches a normal form produces the same saturated IR, making the normal form unique.If saturation terminates on all inputs, the engine is convergent.
  • Termination: Unrestricted saturation may not terminate, so bounding individual analysis runs guarantees halting but forfeits the full convergence property when stopped early.The remaining guarantee is that applying an analysis cannot make any search-space area unreachable.

5. PEGs and E-PEGs

PEGs and E-PEGs provide a semantic graph representation in which loop-lifted values, primitive functions, and equalities support reasoning about multiple program versions. Well-formed PEGs have unique semantics, and referential transparency enables value-level equality reasoning.

  • E-PEG representation: An E-PEG is designed to represent multiple optimized versions of an input program simultaneously within one intermediate representation.The paper formalizes the representation before describing its benefits and CFG translations.
  • PEG structure: A PEG is a labeled graph whose nodes denote semantic functions and whose children specify their arguments.The formal structure is the triple ⟨N, L, C⟩.
  • Value domains: PEG values are bottom-lifted for failure or nontermination and loop-lifted so nodes represent values across loop iterations.Loop identifiers and iteration states encode nested-loop structure.
  • Semantic functions: Primitive PEG functions include φ, θℓ, evalℓ, and passℓ, while domain functions lift operators such as +, ∗, and −.These functions are polymorphic and operate over bottom- and loop-lifted values.
  • Semantics: Well-formed PEGs have a unique semantic value for every node satisfying the recursive evaluation equation.The proof uses the strongly connected component DAG and loop nesting structure.
  • Equality reasoning: Referential transparency lets equality reasoning compare constituent expressions and represent complex fragments, including loops, through node equivalence classes and value-level equalities.PEGs can record equalities at individual-value granularity rather than only at whole-program-state level.

6. Representing Imperative Code as PEGs

This section defines SIMPLE, presents its translation into PEGs, and explains the data structures and functions used to construct the representation.

  • The SIMPLE programming language: SIMPLE is a minimal imperative language used to demonstrate conversion into PEGs.A SIMPLE program has one main function, typed parameters, a body, a return type, and a special retvar variable.
  • The SIMPLE programming language: The type system uses program, statement, and expression judgments to track well-typedness and context changes.The judgments state that a program is well-typed, a statement transforms one typing context into another, or an expression has a particular type.
  • Translation algorithm: TranslateProg initializes parameter bindings and translates the program body with TS, returning the PEG node bound to retvar.The algorithm represents parameters as parameter nodes and obtains the final result from the translated body context.
  • Translation algorithm: TS handles sequences, assignments, conditionals, and loops by updating or combining node contexts with PEG constructs such as PHI and THETA.Its cases recursively translate statements and use maps, temporary nodes, and loop-specific PEG nodes to represent control flow.
  • Translation algorithm: TE translates variable references through the current node context and recursively constructs PEG nodes for operator applications.A node context maps each SIMPLE variable to the PEG node representing its current value.

Statements.

The statement translation rules define how assignments, sequencing, branches, and loops update PEG node contexts, with loops requiring fixpoint construction and evaluation nodes.

  • Basic statements: Sequential statements translate the second statement using the context produced by translating the first.Assignments update a variable binding with the PEG node produced by translating its expression.
  • Control flow: Conditional translation creates φ nodes that select between branch-specific bindings using the translated guard node.A φ node is created for each variable defined in both branch contexts.
  • Control flow: While-loop translation uses temporary nodes, θ nodes, a pass node, and eval nodes to represent loop-varying and post-loop values.FixpointTemps resolves temporary-node edges, while pass and eval nodes encode loop termination and final variable values.
  • Implementation and formalization: TranslateProg is the top-level conversion procedure, and the factorial example traces TS contexts while processing a loop.The pseudo-code corresponds closely to the type-directed rules, which are formalized as a constructive deterministic function over typing derivations.
  • Translation judgments: Statement translation takes a type-correctness derivation and an input node context, then returns the context for subsequent statements.The judgment Γ ⊢s : Γ′ ⊲ Ψ ⇝ℓΨ′ formalizes this transformation.

Translation vs. pseudo-code.

The formal translation is closely related to the pseudo-code and provides termination, successful construction, and semantic-preservation guarantees, with a qualified exception for non-termination.

  • Translation vs. pseudo-code: The pseudo-code follows the type-directed translation rules closely, while omitting explicit manipulation of typing derivations.The implementation can be understood as exploring the corresponding derivation bottom-up; explicit derivations would matter for features such as coercions.
  • Correctness guarantees: Structural induction on well-typedness guarantees that the implementation terminates and successfully produces a translation.The type-directed rules provide the invariants supporting these implementation guarantees.
  • Semantic preservation: The translation may discard an infinite SIMPLE loop when it contributes neither to the return value nor to side effects.This is the stated scope boundary for the nearly semantics-preserving result.
  • Semantic preservation: The semantics-preservation theorem states that evaluating a translated PEG yields the same result as evaluating the corresponding SIMPLE program, modulo termination.The theorem is stated for typed programs with parameter values substituted into the PEG, and the proof was formalized in Coq.
  • Preserving effects: Effect tokens can preserve non-termination by making effectful operations reachable from the PEG’s returned effect value.The paper uses effect tokens for non-termination and describes analogous state-threading encodings for other effects.

Preserving Non-Termination.

The paper explains how effect tokens preserve non-termination and outlines reversion from PEGs to SIMPLE, whose correctness depends on CFG-like PEG structure.

  • Preserving non-termination: A pass node must carry a non-termination effect token because evaluating it may fail to terminate when the loop condition never becomes true.Threading the token through the loop makes the pass node part of the returned result and therefore forces its evaluation.
  • Preserving non-termination: In the division-by-zero example, effect tokens keep a potentially non-terminating division reachable even when its value is unused.The division returns an effect-value tuple, whose components are accessed through ρe and ρv.
  • PEG reversion: Reversion converts PEGs back into SIMPLE programs, but the process is more complex because SIMPLE specifies execution order explicitly.The basic correct procedure may duplicate code, so later optimizations perform branch fusion, loop fusion, and code hoisting.
  • CFG-like PEGs: The reversion algorithm assumes that its input PEG context is CFG-like according to the rules in Figure 19.These restrictions simplify reversion, and the optimizer’s Pseudo-Boolean formulation ensures that the selected PEG satisfies them.
  • CFG-like PEGs: CFG-like contexts parallel well-typed statements by mapping an input context Γ to an output context Γ′.The formalism also uses an immutable context to identify variables that generated SIMPLE code may use but not modify.

Statement nodes.

Statement nodes let PEG reversion encode loops, branches, and computations as typed statements while preserving structured control flow. Reversion can also fuse loops and branches to avoid duplicated computation.

  • Statement nodes: Statement nodes represent typed SIMPLE statements as PEG nodes with multiple inputs and outputs for variable bindings.They execute a statement over typed inputs and produce typed outputs.
  • Reversion: PEG reversion replaces eval, pass, and θ nodes with while-loop statement nodes, and φ nodes with if-then-else statement nodes.The resulting PEG contains statement nodes instead of the primitive control-flow operators.
  • Loop translation: Loop reversion constructs a loop body, recursively translates it to a statement, derives a break condition, and emits a while-loop statement node.The generated node initializes loop variables, updates them while the break condition fails, and computes the result afterward.
  • Loop fusion: Loop fusion combines non-nested loop nodes sharing a pass node, allowing one while loop to compute multiple results simultaneously.The final SIMPLE program can contain one loop instead of separate loops for each post-loop variable.
  • Branch fusion: Branch reversion recursively translates branch contexts into statements, producing one if-then-else that computes both branch results while avoiding common redundant work.Must-evaluate computations such as x*x can be shared outside the branches.

MustEval Analysis.

MustEval identifies computations that execute unconditionally so branch reversion can hoist them and reduce duplication. Loop-invariant motion remains conservative when control-flow nodes may bypass evaluation, with peeling enabling some additional hoisting.

  • MustEval Analysis: MustEval returns nodes known to evaluate unconditionally in the current PEG context, and greater precision reduces code duplication in branches.The analysis modularizes identification of computations that can remain outside branch bodies.
  • Branch processing: The refined reversion process marks always-evaluated φ nodes and processes them before recursively reverting remaining branch nodes.This ordering keeps computations such as x*x shared across branch outcomes.
  • Analysis requirements: MustEval must be minimally precise, including an operator or statement node only when all of its inputs are also in the returned set.These requirements ensure trivially unconditional nodes are recognized and φ processing can make progress.
  • Loop-invariant code motion: Loop-invariant code motion avoids hoisting when φ or θ nodes could bypass evaluation, using a conservative control-flow condition to preserve execution frequency.This prevents invariant operations such as 99÷x from executing more often after hoisting.
  • Loop peeling: Loop peeling can expose safe hoisting opportunities, although the resulting code may retain redundancies such as repeated 1+i and d*f computations.The paper repeats peeling until relevant invariant nodes are also used before the loop body.

8. The Peggy Instantiation

Peggy instantiates equality saturation as a Java bytecode optimizer using PEG and E-PEG representations. Its implementation extends the representation to handle Java heaps and exceptions.

  • Implementation: Peggy is a concrete equality-saturation optimizer for Java bytecode programs, operating over the full instruction set with side effects, method calls, heaps, and exceptions.The system instantiates the optimizer architecture described earlier for realistic Java bytecode.
  • Representation: Peggy uses PEG and E-PEG representations and must encode Java-specific concepts such as the heap and exceptions.These concepts introduce implementation challenges beyond the simplified SIMPLE language.
  • Heap modeling: The implementation models heap state with σ-node summaries, adding σ inputs or outputs to operations that may read or write object state.Stack-variable operations remain precise because Java stack variables change only through direct assignments.

Heap.

The paper illustrates Java method-call representation with source-level calls and a corresponding PEG. The supplied passages identify the example but do not explain additional heap encoding details.

  • Example: The example presents Java object method calls and their corresponding PEG representation.The source fragment includes calls on two objects, with the second call consuming the first call’s result.

Exceptions.

Peggy makes exceptions explicit by bundling exceptional state into heap summaries and branching through an exception tester. Its heap linearization and saturation machinery introduce practical constraints during reversion and optimization.

  • Exception representation: Exception state is bundled into σ heap-summary nodes, so potentially throwing operations preserve and return that state alongside regular values.The CFG uses an explicit isException tester to route control to handlers or exceptional exits.
  • Heap linearization: Heap values are linear and cannot be duplicated, making reversion incomplete when branch-local linearization constraints are unsolvable despite a globally valid ordering.This incompleteness occurred in fewer than 3% of compiled Java methods, which Peggy then did not optimize.
  • Heap linearization: A complete global linearization algorithm is difficult because PEGs contain commuting operations, alternative control paths, and complex loops that saturation may distinguish more precisely than reversion.For example, saturation may know that accesses to different array locations commute, while reversion lacks that information.
  • Saturation engine: Peggy’s E-PEG represents many PEGs and their equivalences, while the saturation engine repeatedly matches triggers and adds returned equalities.CreateInitialEPEG initializes the structure; Match finds substitutions and AddEqualities records the resulting equalities.
  • Saturation engine: Saturation can fail to terminate in general, so triggers restrict when equality edges are added and can avoid expansions likely to be useless.The paper presents trigger control as analogous to a technique used in automated theorem provers.
  • Profitability: Despite a crude operator-and-loop-depth cost model, smaller costs usually correspond to cheaper operators or operations moved outside loops after reversion.The model remained a good predictor of relative performance even after branch fusion, loop fusion, and loop-invariant code motion.

9. Evaluation

The evaluation tests Peggy’s practicality, optimization effectiveness, and translation validation. It finds substantial exploration and micro-benchmark gains, but higher compilation time and limited SpecJVM improvements.

  • 9.1. Time and space overhead: Peggy’s four phases together take slightly over 1.5 seconds per method, and end-to-end compilation averages 6 times slower than fully optimized Soot.Nearly all time is spent in the pseudo-Boolean solver, leaving room for faster encodings or profitability heuristics.
  • 9.1. Time and space overhead: Peggy compiled all benchmarks within a 200 MB JVM heap, demonstrating bounded memory use for the evaluated benchmark suite.The experiment measured memory footprint by limiting the JVM heap rather than reporting unrestricted usage.
  • 9.1. Time and space overhead: 84% of compiled methods reached complete saturation without bounds; bounded cases represented more than 2103 input-program versions using 200 MB of heap.The remaining cases reached an engine limit of 500 expressions and lack a completeness guarantee.
  • 9.2. Implementing optimizations: Peggy optimized every micro-benchmark by at least 10%, while Soot produced almost no gains and sometimes slowed the program.On the raytracer, Peggy achieved a 7% speedup; on SpecJVM, neither optimizer improved performance and Peggy was slightly slower on average.
  • 9.2. Implementing optimizations: Simple equality analyses produced complex optimizations, and domain-specific axioms enabled additional application-level transformations.The paper reports that these advanced optimizations required effort similar to implementing the basic analyses.
  • 9.2. Implementing optimizations: Vector axioms made the 5 KLOC raytracer 7% faster and reduced allocated objects by 40%, whereas Soot recovered none of that overhead.The transformation removes temporary immutable vector objects introduced by functional-style code.
  • 9.3. Translation validation: Peggy validated Soot optimizations across 3,416 methods and identified three methods where Soot had transformed terminating loops into infinite loops.The validator also supports a future machine-checkable equivalence proof with a small trusted computing base.

10. Related Work

The paper positions equality saturation among super-optimization, rewrite-system, phase-ordering, translation-validation, and intermediate-representation research. Its E-PEGs distinguish the approach by representing many optimized programs in one structure.

  • Super-optimization: Unlike superoptimizers that mainly scale to small straight-line code, Peggy targets general-purpose optimization of branches and loops.The comparison concerns intended scope rather than a claim of optimality.
  • Rewrite systems: Earlier rewrite systems apply axioms sequentially and destructively, whereas Peggy uses equality saturation without optimization strategies.The contrast is with systems that control rewrite application through built-in or user-defined strategies.
  • Phase ordering: Peggy addresses phase ordering by simultaneously exploring optimization alternatives instead of generating a single destructive sequence.This is the paper’s stated distinction from prior approaches that search for or combine optimization sequences.
  • Translation validation: The same equality-saturation technique supports translation validation, allowing Peggy to check optimized programs produced by another compiler such as Soot.The paper identifies this reuse of the optimization technique as an advantage over previous validation approaches.
  • Intermediate representations: E-PEGs are specialized equality graphs for PEGs, and a single E-PEG can represent many optimized input programs.That representation enables global profitability heuristics and translation validation.
  • Intermediate representations: PEGs differ from SSA-family and dependence-graph representations by omitting explicit CFG control structure, while retaining a functional representation suited to equational reasoning.The paper also contrasts PEGs with DFGs’ side-effecting stores and VDGs’ lambda-based loop representation.
  • Future work: Future work includes generating machine-checkable optimization proofs and addressing heap linearization during PEG-to-CFG reversion with string diagrams.String diagrams are proposed to preserve linearity and potentially remove the quadratic well-formedness component of the profitability formulation.

Appendix A. Axioms

Peggy’s appendix organizes axioms into built-in, code-pattern, arithmetic, Java-specific, design-pattern, outlining, inlining, sigma-invariance, vector, and application-specific groups. Together they express reusable and domain-tailored equalities for optimization.

  • Axiom organization: The axiom library separates general-purpose rules, applicable across programming domains, from domain-specific rules that encode particular applications or programs.The listed axioms are examples needed for the optimizations in Figure 38, not a complete engine inventory.
  • Built-in E-PEG operations: Built-in E-PEG axioms describe θ, eval, and φ behavior, including loop invariance, operator distribution, and identical-branch simplification.These rules apply properties of the specialized PEG operators.
  • Code patterns: Code-pattern axioms express transformations such as complete loop unrolling, loop peeling, and replacing a constant-count loop with a value.The examples are presented as before-and-after source-code patterns.
  • Basic arithmetic: Arithmetic axioms encode algebraic identities, constant simplifications, shifts, inequalities, and commutation properties for addition and multiplication.Examples include A ∗0 = 0, A ∗2 = A << 1, and A + B = B + A.
  • Java-specific rules: Java-specific axioms capture array and field behavior, including read-after-write, non-aliasing reads, and repeated writes to the same location.These rules use explicit inequalities such as I ≠ J to preserve unaffected reads.
  • Inlining: Inlining equates a method’s inputs and outputs with an inlined PEG, exemplified by replacing pow with its loop body.The paper describes inlining as one large axiom application.
  • Sigma-invariance: Sigma-invariance axioms record methods such as List.get, List.size, and Math.sqrt as operations that leave the heap unchanged.They preserve the same σ state across the invocation.
  • Program patterns: Design-pattern axioms remove overhead from wrapper objects and redundant List contains/indexOf searches, while outlining replaces code with equivalent library calls.The appendix also defines method outlining as the opposite of inlining.
Loading 1012.1802v3…