Mokhov, Mitchell & Peyton Jones (2018) -- Build Systems a la Carte

The paper

A. Mokhov, N. Mitchell, and S. P. Jones, “Build systems à la carte,” Proceedings of the ACM on Programming Languages, vol. 2, no. ICFP, pp. 1–29, 2018.

doi:10.1145/3236774 · read the paper

A summary of the paper and how gen uses it.

Paper Summary

Mokhov, Mitchell, and Peyton Jones observe that build systems — despite being used by every software developer — are rarely studied systematically. Individual systems (Make, Shake, Bazel, Excel, Nix, Buck) are understood as isolated artifacts, each with its own architecture, terminology, and implementation quirks. The paper asks: is there a unifying framework that can decompose any build system into orthogonal components, compare systems by their design choices, and prototype new systems by recombining those components?

The answer is a purely functional, executable framework implemented in approximately 400 lines of Haskell that models any build system as the composition of two independent choices: a scheduler (how tasks are ordered) and a rebuilder (how the system decides whether a task needs re-execution). The framework’s central abstraction is the polymorphic task type Task c k v = Task { run :: forall f. c f => (k -> f v) -> f v }, where c is a constraint (Applicative for static dependencies, Monad for dynamic), k is the key type, and v is the value type. A task description is completely isolated from stores, caches, and schedulers — it only knows how to compute one output given a fetch callback for its dependencies. The constraint c on the functor f classifies tasks: Task Applicative permits static dependency extraction via the Const functor trick (S3.7), while Task Monad enables dynamic dependencies where the identity of a dependency depends on intermediate computation results (S3.5).

Three schedulers are identified (S4.1). Topological (Make, CloudBuild, Buck) pre-computes a linear build order from statically known dependencies, requiring c = Applicative. Restarting (Excel, Bazel) processes tasks in an arbitrary order, aborting and deferring when an out-of-date dependency is discovered. Suspending (Shake, Nix) suspends the running task when a dependency is requested, recursively bringing it up to date before resuming — the task “blocks” on its dependency, and the scheduler recurses. The suspending scheduler naturally handles dynamic dependencies and achieves minimality when combined with appropriate traces.

Four rebuilders are identified (S4.2). Dirty bit (Make, Excel) — one bit per key, set when inputs change; supports minimality but not early cutoff. Verifying traces (Shake, Ninja) — record dependency hashes from the previous build; verify by checking if current hashes match; supports dynamic dependencies, minimality, and early cutoff. Constructive traces (Bazel, CloudBuild) — store actual result values alongside dependency hashes in a shared cloud cache; enable downloading pre-built results without local execution. Deep constructive traces (Buck, Nix) — record only terminal input hashes, ignoring intermediate dependencies; enable cloud lookup from inputs alone at the cost of requiring deterministic tasks and losing early cutoff.

The 3x4 matrix of scheduler-rebuilder combinations (Table 2, S4.4) yields 12 possible build systems, 8 of which are inhabited by real systems. Nix occupies the cell (Suspending, Deep Constructive Traces) — it uses lazy evaluation as a suspending scheduler and content-addressed derivations as deep constructive traces. The most interesting unoccupied cell is (Suspending, Constructive Traces), which the authors call “Cloud Shake” and implement in 3 lines by composing the suspending scheduler with the ctRebuilder (S5.4, Figure 10).

Correctness is defined precisely (Definition 3.1, S3.6): after a build, (1) no inputs are corrupted, and (2) every non-input key’s stored value equals what recomputing its task with the final store would produce. Minimality (Definition 2.1) requires executing tasks at most once per build and only if they transitively depend on changed inputs. The framework enables formal reasoning about which scheduler-rebuilder combinations satisfy which properties: topological+dirty-bit (Make) is minimal but has no early cutoff; suspending+verifying-traces (Shake) is minimal with early cutoff; restarting+constructive-traces (Bazel) is not minimal (may restart tasks) but supports cloud sharing and early cutoff.

The paper also addresses engineering concerns (S6): partial stores and exceptions, parallelism (each scheduler has a parallel variant), impure/non-deterministic tasks (modeled via MonadPlus), cloud implementation details (communication, offloading, eviction, shallow builds), self-tracking build systems (where task descriptions themselves are tracked for changes), and iterative/cyclic computations. The connection to self-adjusting computation (S7.2) and memoization (S7.3) is noted — the Levenshtein edit distance example demonstrates that a minimal build system with dynamic dependencies subsumes dynamic programming with memoization, and additionally supports incremental recomputation when inputs change.

Key Concepts

• Scheduler/Rebuilder Decomposition (S4, Table 2). Any build system can be factored into two orthogonal components: the scheduler (topological, restarting, or suspending) determines task execution order; the rebuilder (dirty-bit, verifying-traces, constructive-traces, or deep-constructive-traces) determines whether a task needs re-execution. These compose freely: type Scheduler c i ir k v = Rebuilder c ir k v -> Build c i k v.

• Task Constraint Polymorphism (S3.2, S3.4). The constraint c on Task c k v classifies task descriptions by their dependency structure. Applicative = static dependencies extractable without execution; Monad = dynamic dependencies requiring intermediate computation; Functor = linear chains; MonadPlus = non-deterministic tasks. This classification is not ad hoc — it emerges necessarily from the polymorphism of the fetch callback.

• Static Dependency Extraction via Const (S3.7). For Task Applicative, dependencies can be extracted without execution by instantiating f to Const [k], exploiting the Applicative instance of Const to accumulate keys. This is the mechanism that enables topological schedulers.

• Suspending Scheduler (S4.1.3, S5.3). The suspending scheduler recursively brings dependencies up to date when they are requested, suspending the current task. Combined with a done set to avoid redundant work, this achieves minimality for dynamic dependencies. Implemented via continuation-passing or green threads. Nix’s lazy evaluation is a native suspending scheduler — attribute thunks “suspend” until their dependencies are forced.

• Deep Constructive Traces (S4.2.4, S5.4). Record only terminal input hashes, enabling cloud lookup from inputs alone without building any intermediates. Nix’s content-addressed store derivations are this: a derivation’s output hash is determined by the hashes of all its source inputs (recursively to terminal inputs). Trade-off: requires deterministic tasks and cannot support early cutoff at intermediate levels.

• Correctness Definition (S3.6, Definition 3.1). Formal specification: inputs unchanged, non-input values consistent with task recomputation against the final store. Extended for non-determinism (S6.3: result must be one of the possible outputs) and shallow builds (S6.4: only target key and inputs must match a hypothetical correct full store).

• Minimality (S2.1, Definition 2.1). A build system is minimal if it executes each task at most once per build and only when the task transitively depends on inputs that changed since the previous build. Not all correct systems are minimal (Bazel’s restarting scheduler may execute a task multiple times).

• Self-Tracking (S6.5). Build systems that detect changes to task descriptions themselves, not just inputs. Modeled as tasks depending on a key representing their own formula. Excel and Ninja support this; most software build systems do not.

• Memoization Subsumption (S7.3). A minimal build system with dynamic dependencies subsumes memoization (demonstrated via Levenshtein edit distance as Tasks Monad), and additionally provides incremental recomputation — an optimization memoization alone cannot achieve.

How gen uses this

gen splits the paper’s two dimensions across two libraries. Nix’s laziness is the scheduler, and gen-scope’s evaluator runs on it. gen-memo is the rebuilder.

gen-scope: the suspending scheduler

The paper places Nix in the (Suspending scheduler, Deep Constructive Traces) cell of Table 2. Nix’s lazy evaluation is a suspending scheduler in the formal sense of S4.1.3. When gen-scope’s get "host:igloo" "region" forces an _eval thunk that depends on another node’s attribute, Nix suspends the current thunk, evaluates the dependency, and resumes. This is the suspending scheduler from Figure 9:

suspending rebuilder tasks target store = fst $ execState (fetch target) (store, Set.empty)
  where
    fetch key = do
      done <- gets snd
      case tasks key of
        Just task | key `Set.notMember` done -> do
          ...
          newValue <- liftRun newTask fetch  -- fetch recurses: dependency is "suspended"
          ...

• The paper’s done set corresponds to gen-scope’s _eval memoization: once a thunk is forced, Nix caches the result.
• The paper’s fetch callback is gen-scope’s self.get id attrName.
• The paper’s Task is an attribute equation self: id: value.

gen-memo: the rebuilder

gen-memo cites this paper as its theory and implements the rebuilder half of the decomposition. It never evaluates. Given the last evaluation, it decides whether a key must be recomputed, and it is correct when its output is byte-identical to a cold evaluation.

• Verifying traces (S4.2.2) — build records a per-key trace { deps; hash }, the verifying-trace shape.
• Reuse strategies (lib/strategies.nix) — verify is the paper’s verifying-trace check (S4.2). earlyCutoff stops propagation when a recomputed value hashes the same as before (S2.3). needsEval is Reps’ pre-cutoff test.
• Invalidation — dirtySet, affected and affectedSet propagate a change along reverse dependencies to find the keys that must be recomputed.
• Parametric over the dependency oracle — the rebuilder takes its dependency graph as an argument, the same parametricity the paper gives its rebuilders.

The paper’s rebuilder consults build information that persists from one invocation to the next. A pure Nix evaluation has no such persistence, so gen-memo’s memory is the trace from earlier in the same evaluation. It reuses work across overrides and repeated demands within one evaluation. Cross-invocation reuse is left to Nix’s store at the derivation level.

Further directions

Unexploited Ideas

• Constructive traces for attribute caching across evaluations (S4.2.3, S5.4). Constructive traces store actual results indexed by dependency hashes. For gen, this would mean a persistent attribute cache: given the same graph structure and the same input declarations, attribute values could be looked up rather than recomputed. This extends Nix’s derivation-level content-addressing down to the attribute level, and needs a store that outlives one evaluation.

• Self-tracking for aspect change detection (S6.5). The paper models self-tracking as tasks depending on their own formula. In gen, this would mean treating an aspect definition as a hashable input to the attributes computed from it, so a change to the definition itself invalidates exactly those attributes.

• Task constraint classification for static analysis (S3.4, S3.7). The paper’s Applicative/Monad distinction enables static dependency extraction for applicative tasks. In gen-scope, most attributes are monadic (they conditionally access different dependencies), but some are purely applicative (e.g., inherit' always walks the parent chain regardless of values). Identifying applicative attributes would give a static dependency graph for them, supporting precomputed evaluation order.

Research Directions

• Optimal trace granularity for Nix-embedded AGs. The paper’s trace taxonomy (verifying, constructive, deep constructive) applies at the task/key level. In gen-scope, the “task” is an attribute equation and the “key” is a (nodeId, attrName) pair. Per-attribute traces give maximal incrementality but high storage overhead. Per-node traces (invalidate all attributes when any input to the node changes) are coarser but cheaper. Per-subtree traces align with entity boundaries. The trade-off space has not been characterized for lazy-evaluation-embedded AGs.

• Content-addressing as deep constructive traces. Nix already provides deep constructive traces at the derivation level: a derivation’s output is determined by the recursive hash of all terminal inputs. If an attribute’s value is a function of (a) the graph structure hash and (b) the declaration content hashes, the attribute value could be looked up in a content-addressed cache without re-evaluation. This would join gen-scope’s evaluation model to Nix’s store model and allow cross-evaluation attribute sharing.

• Non-deterministic tasks and rule dispatch. The paper models non-determinism via MonadPlus (S6.3). When several gen rules fire at one node, the result should not depend on the order they fire in. The paper’s correctness definition for non-deterministic tasks (S6.3: getValue k result \elem` computeND task result`) gives a way to state that requirement: the final configuration must be one of the possible results of the task, whatever the firing order.

• Self-adjusting computation bridge (S7.2). The paper notes the connection between build systems and self-adjusting computation (Acar et al. 2002, 2007). gen’s fixpoint loops (gen-scope’s circular attributes, which also iterate gen-dispatch’s one-shot rule dispatch to a fixpoint, and gen-program’s model computation) are instances of self-adjusting computation within a single evaluation. Whether the incremental computation literature gives sub-linear re-evaluation cost for them when inputs change, beyond what trace-based rebuilders provide, is open.