Hammer, Phang, Hicks & Foster (2014) -- Adapton: Composable, Demand-Driven Incremental Computation

The paper

M. A. Hammer, K. Y. Phang, M. Hicks, and J. S. Foster, “Adapton,” PLDI ‘14: ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 156–166, 2014.

doi:10.1145/2594291.2594324

This page is our reading of it, not a substitute for it.

Paper Summary

Hammer et al. observe that prior incremental computation (IC), a.k.a. self-adjusting computation, has two crippling drawbacks (S1, p.1). First, recomputation is oblivious to demand: when an input changes, all dependent values are recomputed eagerly, even outputs no observer currently wants. Second, computations are incrementalized as a monolithic unit with little reuse across contexts — because traditional IC imposes a total ordering on its execution trace (typically via the Dietz-Sleator order-maintenance structure [9,15]), three common reuse patterns are impossible: sharing (the same subcomputation F(A1..A100) appears in two cells — traditional IC recomputes the second), swapping (reordering F(A)+F(B) to F(B)*F(A) forces recomputation due to total ordering), and switching (toggling F(A1..A50) to F(A51..A100) and back recomputes from scratch). The motivating example is a spreadsheet where cells are changed, hidden, and shown (S1, p.1; S2, pp.2-3).

The paper’s answer is a core calculus λcdd_ic and its OCaml realization, Adapton. The key insight (S1, p.1) is to combine traditional IC-style reuse with the memoization of thunks from lazy computation. Updates to mutable ref cells merely signal the potential need for recomputation; the actual recomputation is delayed until a thunk reading those cells is forced. Under the hood, both refs and thunks are implemented over a Demanded Computation Graph (DCG), which captures the partial order of which computation’s results feed which other computations — as opposed to the total order of prior IC. This partial order is what enables sharing, swapping, and switching.

Adapton’s second core idea is an explicit inner/outer layer separation (S1-S3), which the authors claim is absent from all prior IC. Inner computations — the bodies of thunks, the incrementally-reused units — may read refs (get) but may neither allocate nor mutate them. Outer computations — the interactive top level, the observer — may allocate refs (ref), mutate them (set), and force thunks, thereby precipitating change propagation. The restriction that inner computations are read-only is precisely what makes them safe to memoize and reuse. Layer purity is enforced in λcdd_ic by the type system (rules Ty-E-Ref, Ty-E-Set are outer-only; Ty-E-Get is layer-polymorphic; Ty-E-Inner coerces an inner computation into an outer context but not vice-versa, and |Γ| strips the outer layer’s recursive functions from the inner layer — Fig 3, p.5). In the OCaml library the layer separation is not statically enforced (OCaml’s types make it hard): an inner computation “implicitly begins when force is called and ends when the call returns” (footnote 1, p.7).

The DCG is the load-bearing data structure (S2, pp.2-3; S5.2, pp.7-8). Each node is a ref (drawn as a square, holds an address + content) or a thunk (drawn as a circle, holds a suspended expression and, once forced, its valuation). Each directed edge points from a thunk to a ref or thunk it depends on: edges targeting refs come from get, edges targeting thunks come from force. Edges are labeled with the value returned by that get/force call — this label is the early-cutoff witness. Edges are stored bidirectionally: each node keeps an ordered list of outgoing edges (appended in get/force order — leftmost created first) and an unordered set of incoming edges, so the graph can be walked caller→callee or callee→caller. The DCG starts empty; nodes are added on aref/athunk/memo-miss; edges are added on get/force during evaluation.

The heart of the algorithm is the two-phase split of change propagation into dirtying and propagation (S2, p.3; S5.2, pp.7-8; Algorithm 1, Fig 8 + the box on p.7). Dirtying runs on set: starting from the mutated ref, traverse incoming edges backward (caller-ward), marking each traversed edge dirty; stop at any edge already dirty (dirty(node): for each incoming edge, if not already dirty, set dirty and recurse to edge.source). This is eager but cheap — it only flips flags, it does not recompute. Propagation/cleaning runs on force: starting from the forced thunk, do an in-order traversal of its outgoing edges (in the order they were added, line 7). For each dirty edge: clean the flag (line 9); if the target is a thunk, recursively propagate into it (lines 10-11); then compare the edge’s stored label against the target’s current value (line 12 — this is the early-cutoff check). If the label still matches, the dependency is unchanged and the subgraph is cut off (not recomputed). If it differs, at least one input changed, so clear all the node’s outgoing edges (line 13) and re-evaluate the thunk (line 14), returning immediately (line 15) since the remaining edges will be rebuilt during re-evaluation. Crucially, propagation traverses bottom-up, left-to-right, in original evaluation/demand order, so it lazily repairs only the parts of the graph currently under demand — a thunk whose result no observer forces is never repaired (the line-6 example does not recompute t2, S2 p.3).

The two phases maintain a key invariant (S5.2, p.8) that amortizes their cost: if an edge is dirty at the end of a dirtying/propagation phase, every edge transitively reachable via incoming edges from its source is also dirty; dually, if an edge is clean, every edge transitively reachable via outgoing edges from its target is also clean. This lets dirtying stop early at already-dirty edges and propagation skip already-clean subgraphs, amortizing dirtying across consecutive sets and propagation across consecutive forces.

Formally (S3-S4), λcdd_ic extends Levy’s call-by-push-value [27,28] — which already has explicit thunk/force and syntactically separates values from computations — with ref/get/set and the inner/outer layer annotations. The incremental semantics (S4, Fig 4, p.5) reduces expressions to demanded computation traces (DCTs) rather than values: judgment K; S1 ⊢ e ⇓ S2; T reads “under prior knowledge K and store S1, e reduces to store S2 and trace T”. Trace events (Fig 6, p.4) are get^a_v (read address a yielding v) and force^e_ẽ[T] (forced thunk expression e, its terminal ẽ, and the sub-trace T). Traces are hierarchical trees — locally consistent, with no global ordering — which is exactly what permits compositional reuse. DCTs are trees; DCGs are graphs (S4.1, p.6): a shared subgraph in the DCG appears as a duplicated subtree in the DCT, so the DCT is easier to reason about but doesn’t explicitly represent sharing. Change propagation K; S ⊢ T1 ↝prop T2 is specified declaratively by checking + patching: the checking judgment S ⊢ √T verifies a trace is consistent with the store (Check-Force: the recorded terminal ẽ still matches trm(T); Check-Get: S(a)=v still holds), and the patching judgment T1{e:T2} ↝patch T3 substitutes a fresh sub-trace for all occurrences of a forced expression e “all at once”, simulating DCG sharing (p.6). Rule Incr-ForceProp performs memoization at force by non-deterministically choosing a prior trace of the same expression e from K and repairing it; importantly, change propagation is NOT initiated at set — it is delayed until the result is demanded by a force (p.6). The semantics are proved sound: every incremental reduction has a corresponding from-scratch reduction with the same terminal, so patched results equal what recomputation from scratch would produce (Thm 4.1 blind-evaluation equivalence, Thm 4.2 subject reduction, Thm 4.3 soundness, p.6).

The named/keyed-allocation and GC concerns surface in two places. Memoization (S5.1, pp.7-8): λcdd_ic memoizes implicitly at force by syntactic equality of expressions, which OCaml cannot do. So the library exposes memo, a constructor of memoized thunks keyed by argument: memo takes a 2-argument function and returns a constructor that, on each call, checks a memo table keyed by the argument — on a miss it allocates a fresh athunk and stores it; on a hit it returns the same athunk (equivalent to choosing the most-recently-patched trace in Incr-ForceProp). Memo tables are weak hash tables, relying on OCaml’s GC to evict athunks that are no longer reachable. Garbage collection of stale graph structure (S5.2, p.8): when a thunk is re-evaluated, its outgoing edges are cleared (line 13) and only relevant ones re-added; the incoming edge sets are stored in weak hash tables so OCaml’s GC removes now-irrelevant edges automatically. The paper explicitly notes (S6.1, p.9) the open problem that mergesort’s limited inter-recursion memoization caused trouble for both Adapton and EagerTotalOrder, and that prior work patched it with adaptive memoization [3] or keyed allocation [17] — a named-allocation discipline they cite as future work, not yet integrated.

Empirically (S6, pp.8-10; Table 1, p.9), Adapton is compared against EagerTotalOrder (traditional totally-ordered monolithic IC, [2]) and LazyNonInc (plain lazy values, no incrementality, set throws) across filter/map/quicksort/mergesort/fold/exptree under four change patterns: lazy (demand one output element), swap, switch, batch (demand entire output). Where traditional IC gets 2×-20× speedups over naive recomputation, Adapton gets 7×-2000×; for mergesort, EagerTotalOrder slows down 6.5× while Adapton speeds up 300×. Adapton wins decisively on the lazy/swap/switch patterns (it can memo-match regardless of total order; e.g. updown1, which EagerTotalOrder cannot memo-match at all). Adapton’s weakness is the batch pattern (all output demanded): it is 1.5×-3.5× slower than EagerTotalOrder, because EagerTotalOrder is optimized to propagate to all outputs unconditionally whereas Adapton’s conditional/demand-checking adds overhead — though it still beats naive. The dirtying cost is observed to grow with demand size (more output demanded → more edges cleaned by propagation → more edges to re-dirty). The case study AS2 (Adapton SpreadSheet, S6.2, pp.9-10) incrementalizes a stateless formula-evaluation spec and gets up to 20× speedups where classic IC always slowed down (up to 100×), with Adapton’s benefit growing exponentially in #sheets and #changes, validating that the sharing pattern is the decisive factor.

Related work (S7) positions Adapton against self-adjusting computation (Acar et al. [2,4]) which uses dynamic dependency graphs (DDGs) but assumes a single totally-ordered trace and ignores the outer layer; non-monotonic IC (Ley-Wild et al. [29,31]) which handles swapping but not sharing/switching, has no laziness, and was never implemented; and FRP [13,14,26] whose dependence DAGs resemble the DCG but reevaluate eagerly (push-based, topological) with no explicit outer-layer demand.

Key Concepts

• Demanded Computation Graph (DCG) (S2 p.2-3; S5.2 p.7-8). Acyclic graph; nodes = aref (square: address + content) or athunk (circle: suspended expr + cached valuation); directed edges = a thunk’s dependency on a ref (via get) or thunk (via force), labeled with the returned value. Edges stored bidirectionally: ordered outgoing list (get/force order) + unordered incoming set (weak). The graph is the trace; it grows by demand and is repaired by demand.

• Demand-driven vs. eager IC (S1 p.1; S2 p.3; S7). Traditional/self-adjusting IC propagates every change to all dependents at set time (eager, push, topological). Adapton makes set only signal change (dirty flags) and defers recomputation to force time (lazy, pull, demand-ordered). Undemanded outputs are never recomputed.

• Inner/outer layer separation (S1, S3, Fig 3 p.5). Inner = thunk bodies, read-only on the store (get only), incrementally reusable. Outer = observer/top-level, may ref/set/force, precipitates change propagation. Type system enforces purity (ref/set are outer-only; inner e coerces inner→outer, not the reverse; |Γ| hides outer recursion from inner). Library does not enforce statically — inner begins at force, ends at return (fn.1 p.7). Claimed novel vs. all prior IC.

• Dirtying (S2 p.3; Alg 1 lines 1-5). On set a, walk incoming edges backward from a, marking edges dirty, stopping at already-dirty edges. Eager, flag-only, no recomputation. Invariant: dirty edge ⟹ all incoming-reachable edges from its source are dirty.

• Cleaning / propagation / repair (S2 p.3; Alg 1 lines 6-15). On force, in-order traverse outgoing edges; clean each dirty flag; recurse into thunk targets; compare stored edge label vs. current target value (early cutoff). Match ⟹ cut off (reuse). Mismatch ⟹ clear outgoing edges + re-evaluate thunk. Bottom-up, left-to-right, original demand order ⟹ lazy, only repairs demanded subgraph. Invariant: clean edge ⟹ all outgoing-reachable edges from its target are clean.

• Memoization composed with change propagation (S4.1 Incr-ForceProp p.6; S5.1 p.7-8). Memo-match at force: reuse a prior trace of the same expression, then repair it via change propagation (check + patch). Patching replaces all occurrences of a forced expr “all at once” = DCG sharing. Library memo keys on argument (syntactic eq impossible in OCaml), returns the same athunk on a hit.

• DCT (trace) vs. DCG (graph) (S4 p.4-6). Incremental semantics reduces to hierarchical demanded computation traces (trees of get^a_v and force^e_ẽ[T] events, locally consistent, no global order). DCTs are trees; DCGs are graphs — a shared DCG subgraph = a duplicated DCT subtree. Trees are easier to reason about formally; graphs capture sharing operationally.

• Sharing / swapping / switching (S1 p.1; S2 p.2-3). The three reuse patterns traditional (totally-ordered) IC cannot do. Sharing: reuse a subcomputation across contexts. Swapping: reorder subcomputations. Switching: toggle between alternatives and reuse the inactive one. The DCG’s partial order supports all three; the total-order trace of prior IC supports none.

• GC of unreachable nodes/edges (S5.1, S5.2 p.7-8). Memo tables and incoming-edge sets are weak hash tables; OCaml’s GC evicts athunks/edges that become unreachable (e.g. after a thunk re-evaluation clears + rebuilds its outgoing edges, the orphaned incoming edges are collected). Keyed/adaptive allocation [3,17] for better reuse (e.g. mergesort) is cited as future work, not integrated.

• Soundness (Thms 4.1-4.3, p.6). Incremental (trace-based) reduction is consistent with from-scratch reduction: patched results equal full-recomputation results. Blind-evaluation equivalence + subject reduction + soundness.

• Call-by-push-value foundation (S3 p.3-4). λcdd_ic = Levy’s CBPV [27,28] (explicit thunk/force, values vs. computations syntactically split, explicit evaluation order) + ref/get/set + inner/outer layers. CBPV chosen as “canonical” since both CBV and CBN translate into it.

Implementation Mapping

Current Usage in Gen Ecosystem

gen-rebuild (Primary — Adapton is the canonical demand-driven IC paper; supplies the lazy two-phase invalidate/revalidate the surface currently lacks)

gen-rebuild is the rebuilder of Mokhov 2018 — it decides whether a node needs recomputation over a dependency graph. Its current 13-op surface (override; verify/constructive/deepConstructive/earlyCutoff; applyDelta/batch/retract/dirtySet; support/why/affected; restabilize) is grounded in Mokhov’s eager, batch-oriented rebuilder taxonomy plus Forgy/Radul/Arntzenius. Mokhov’s rebuilders are all “given a key, is its cached value still valid?” — they presume the scheduler already decided to visit the key. Adapton supplies the missing demand-driven half: a two-phase lazy invalidate-then-revalidate over a DCG, where set only flips dirty flags and recomputation is deferred until a force actually demands the result.

The decisive contrast for gen-rebuild’s design: override recomputes the entire reverse-dependency cone of a changed node (eager, push, breadth-first over dependents), reusing the rest from a flat relocatable store. Adapton’s dirty/clean is lazy and pull-based — dirty marks the cone but recomputes nothing; clean (= force-triggered propagation) walks only the path actually demanded, with early-cutoff at every edge via stored value labels. A node in the dirtied cone whose result is never forced is never recomputed. This is exactly the “swapping/switching/undemanded-output” win Adapton measures (300× on mergesort; AS2 exponential speedup) and exactly what override’s eager cone-recomputation forfeits.

• Files: gen-rebuild op surface (rebuilder strategies + deltas + provenance). Adapton adds the demand-driven invalidate/revalidate axis orthogonal to Mokhov’s batch rebuilders.
• Mapping: Adapton’s set + dirty(node) (Alg 1 lines 1-5) = a lazy dirtySet that recomputes nothing; Adapton’s force + propagate(node) (Alg 1 lines 6-15) = clean/repair, a demand-ordered, early-cutoff revalidation; Adapton’s edge-label comparison (line 12) = earlyCutoff lifted from “compare output hash” to “compare per-dependency stored value”; Adapton’s memo = the warm-cache memo-match (gen-scope’s co-located _eval).

gen-scope (Foundational — the DCG’s force/demand driver and memo are gen-scope’s evaluation model)

Adapton’s force IS gen-scope’s demand-driven HOAG evaluation, and Adapton’s memo IS gen-scope’s co-located _eval memo on lib.fix self. The suspending scheduler that Mokhov attributes to Nix lazy evaluation is precisely how an Adapton force recursively brings dependencies up to date before resuming. The seam (below) is whether the DCG’s dirty flags — mutable per-edge state — can live anywhere in gen-scope’s pure-Nix, mutation-free fixpoint.

• Files: gen-scope eval, _eval memo, self.get.
• Mapping: Adapton force = gen-scope demand on a node attribute; Adapton get edge = gen-scope self.get id attr dependency record; Adapton memo/weak-table = gen-scope _eval thunk memoization (but Nix has no weak refs, so no GC eviction within one evaluation).

gen-graph (Supporting — DCG queries are reverse/forward dependent walks)

Adapton’s bidirectional edges (outgoing list for propagation, incoming set for dirtying) are exactly the two query directions gen-graph already provides for the rebuilder’s frontier. Dirtying walks incoming (callee→caller = dependents); propagation walks outgoing (caller→callee = dependencies).

• Mapping: Adapton dirtying traversal = gen-graph reverse reachability (dependents/affected cone); Adapton propagation traversal = gen-graph forward dependency walk in evaluation order.

Relevance to gen-rebuild Op Surface

Adapton concept	gen-rebuild realization
DCG (S2, S5.2)	The dependency graph the rebuilder decides over; nodes = keys, edges = recorded deps with value labels
set + dirtying (Alg 1 l.1-5)	A lazy dirty op: mark reverse-dep cone, recompute nothing (vs. eager override)
force + propagation (Alg 1 l.6-15)	clean/repair op: demand-ordered, early-cutoff revalidation of only the forced path
Edge-label compare (l.12)	earlyCutoff at per-dependency granularity, not just per-output
memo (S5.1)	Warm-cache memo-match = gen-scope _eval; the “reuse rest from store” half of override
Weak-table GC (S5.1-5.2)	gc op: evict undemanded/orphaned cache entries (no native analogue in pure Nix)
Inner/outer layer (S1, S3)	The read-only-deps vs. mutate-and-observe split: override/applyDelta are outer; node equations are inner
Soundness (Thm 4.3)	Rebuilder correctness: revalidated value = from-scratch value

The paper’s central lesson for gen-rebuild is that demand-driven rebuilding is strictly more general than eager cone recomputation, and it is achieved not by a smarter scheduler but by splitting invalidation from revalidation (dirty vs. clean) and checking value equality at every edge during the demand-ordered walk (early cutoff lifted to per-dependency granularity). override collapses both phases into one eager push; Adapton separates them so undemanded work is never done.

Appendix: Follow-up Work

Unexploited Ideas

• Lazy two-phase dirty/clean as distinct ops (S2 p.3; S5.2 p.7-8). The surface’s dirtySet/override fuse invalidation and recomputation eagerly. Adapton’s separation — dirty flips flags over the reverse-dep cone and recomputes nothing; clean recomputes only the demanded path with per-edge early cutoff — is the missing demand-driven rebuilder. This is the single largest gap the paper exposes.

• Per-dependency early cutoff via edge labels (Alg 1 l.12). earlyCutoff currently compares a node’s output hash. Adapton stores the returned value on each edge and cuts off when the edge label still matches the target’s current value — finer-grained cutoff that stops propagation per-dependency, not per-node. Lifting earlyCutoff to label-bearing edges would let revalidation prune subtrees mid-walk.

• Sharing/swapping/switching as a reuse benchmark (S1, S2, S6). The three patterns total-ordered IC cannot do are a concrete conformance test for gen-rebuild: a faithful demand-driven rebuilder must reuse a subcomputation across contexts (sharing), tolerate reordered dependencies (swapping), and restore an inactive prior result (switching). The flat relocatable store should already give sharing; swapping/switching test whether the rebuilder is truly partial-order, not total-order.

• Weak-table GC of undemanded cache (S5.1, S5.2 p.8). Adapton evicts athunks/edges via OCaml weak hash tables once unreachable. A gc op for gen-rebuild would evict stale or never-demanded entries from the relocatable store — but pure Nix has no weak references and no within-evaluation reachability hook, so this is the least natively expressible idea (see Research Directions).

Potential New Libraries or Features

• dirty / clean ops for gen-rebuild. dirty :: Store -> KeySet -> Store marks the reverse-dep cone of changed keys (flag-only, no recomputation). clean :: Store -> Key -> (Value, Store) (a.k.a. force/demand) performs the demand-ordered, early-cutoff repair of only the path to Key. Together they are the lazy counterpart to override. Scope: large — requires the store to carry per-edge dirty flags and value labels, which in pure Nix must be re-derived each evaluation from a serialized prior-run trace rather than mutated in place.

• force/demand as an explicit driver (S2, S5.2). The surface has no explicit demand entry point distinct from the rebuilder strategies — demand is implicit in override’s cone. Adapton makes force the only thing that triggers recomputation. An explicit demand :: Store -> Key -> (Value, Store) would make gen-rebuild’s pull-based contract first-class and is the natural seam to gen-scope’s self.get.

• memoConstructor / keyed allocation (S5.1 p.7-8; [17]). Adapton’s memo keys thunk allocation by argument and is the named-allocation primitive whose absence hurt mergesort. A keyed-allocation op (alloc :: Key -> Thunk -> Node) would let gen-rebuild stabilize node identity across runs so reuse survives structural change — the prerequisite for swapping/switching reuse and the cited future-work fix [3,17].

Research Directions

• Is dirtying even expressible in pure Nix? (S5.2 p.7-8 — the crux). Adapton’s dirty flags are mutable per-edge state set by set and cleared by force across observer interactions, amortized by an invariant maintained between phases. Nix has no mutation: the _eval memo lives on lib.fix self and is reconstructed from scratch each nix eval. So a flag flipped in place between two interactions has no representation in a single pure evaluation. The honest options are (a) re-derive dirtiness each evaluation by diffing a serialized prior-run trace (DCT/DCG) against the new input set — the dirty set becomes a pure function dirty(priorTrace, changedKeys) rather than a mutated flag, recomputed every run; or (b) externalize the DCG to a store (JSON/Nix file persisted between nix eval invocations) so dirty flags live in the external store and Nix reads/writes it imperatively at the harness level, outside the pure evaluation. Option (a) keeps purity but pays a re-derivation cost each run (and cannot amortize dirtying across sets the way Adapton’s invariant does, since there is no “between sets” inside one evaluation). Option (b) recovers true incrementality but moves the mutable DCG outside gen-scope’s lib.fix self, into the same external trace store gen-rebuild already needs for cross-evaluation incrementality (the rebuilder dimension Mokhov’s mapping flagged as future work). Conclusion: lazy dirty/clean is NOT expressible as in-place mutation in pure Nix; it is expressible either as a pure trace-diff per run (purity-preserving, no amortization) or as an externally-persisted DCG the harness mutates (true incrementality, impure at the harness layer).

• GC without weak references (S5.1, S5.2 p.8). Adapton’s gc relies on OCaml weak hash tables + a tracing collector. Pure Nix has neither weak refs nor a reachability hook within evaluation, and laziness already drops unforced thunks for free within a run. So gc is only meaningful for the external trace store of option (b): evict entries not reachable from any demanded key in the latest run — a pure reachability computation over the persisted DCG, run by the harness, not a within-evaluation collection. There is no faithful in-evaluation gc for pure Nix; the op only makes sense at the external-store layer.

• Inner/outer layer as a static discipline (S3, Fig 3 p.5). Adapton’s type-enforced inner(read-only)/outer(mutate+observe) split has a clean Nix analogue: node equations are inner (they may only self.get, never inject deltas), while override/applyDelta/retract are outer driver ops. Making this a typed/checked boundary in gen-scope — inner attributes provably cannot trigger change propagation — would mirror Adapton’s central novelty and is the precondition for sound memo reuse. Even OCaml-Adapton couldn’t enforce it statically (fn.1 p.7); pure Nix’s purity already enforces the read-only-inner half for free, which is a genuine advantage worth stating.

• Trace-diff dirtying vs. Mokhov verifying traces — granularity (S4 p.4-6; cf. Mokhov S4.2.2). Adapton’s DCT is hierarchical (per-force subtrees) where Mokhov’s verifying trace is flat (per-key dependency-hash list). The DCT’s tree structure is what gives sharing/swapping/switching. The open question for gen-rebuild: should the persisted trace be flat (Mokhov, cheap, per-key) or hierarchical (Adapton, sharing-capable, per-force-subtree)? The hierarchical form is required to faithfully reproduce Adapton’s three patterns but costs more storage and a tree-structured diff. This trade-off is unresolved and is the key design decision for gen-rebuild’s external trace representation.