Speed & Safety with Graph Coloring

Graph coloring gives Composer a useful way to group compatible work after the compiler has established its dependencies and constraints. The Program Semantic Graph (PSG) retains the participants, effects, storage identities and proof premises that explain compatibility. A coloring organizes those facts into candidate execution groups; its validity is checked against the actual constraints.

This design keeps semantic analysis and rewriting in Baker’s nanopasses. Alex uses its Huet zipper and Elements/Patterns/Witnesses to realize the settled graph in admitted portable MLIR forms. Target scheduling, circuit construction and physical placement retain their backend responsibilities.

The parallelization discovery problem

Consider a pipeline that normalizes data, validates the normalized values and then transforms the valid results. Each stage consumes its predecessor. Individual items within a stage may be independent, while the stages still have dependencies. An async expression or a pure function alone does not settle this distinction.

The compiler must establish the actual reads, writes, demand, effects and result contract. For a neighborhood filter, iterations can read overlapping immutable input regions while writing disjoint output locations. An in-place update of the same grid has different dependencies. A random scenario needs its own specified random-stream identity; merely assigning scenarios different indices does not establish independence or reproducibility.

Graph coloring as parallelization inference

Use a conflict graph for a particular purpose. A vertex might be an eligible Baker rewrite proposal or an admitted runtime work item. An edge says that those two vertices cannot belong to the same concurrent group under the recorded premises. A proper coloring assigns different colors to endpoints of each edge.

Same-colored vertices form candidate groups without the represented pairwise conflicts. They still need ready inputs, satisfied joint constraints and a valid publication/execution protocol. Colors do not impose a topological order. An edge in a data-dependency graph has a different meaning from an edge in this conflict graph; a coloring of the former is not automatically a valid schedule.

For Baker proposals, conflict discovery includes semantic read/write footprints, rewiring, aliases, changed proof supports, lookup/absence observations and shared publication state. Distinct source subtrees can depend on one joint premise. Conversely, shared immutable input alone need not prevent independent work.

A tractable coloring component

The compiler needs a sound usable grouping, rather than a minimum color count. A deterministic greedy procedure can visit eligible vertices in a stable order and assign each the first color unused by its already-colored neighbors. For a finite simple conflict graph of maximum degree Δ, this uses at most Δ+1 colors. With suitable adjacency data structures the standard procedure takes linear time in the materialized graph size. See Assadi, Chen and Khanna for this baseline and further coloring algorithms.

That bound concerns coloring the supplied graph. Discovering semantic conflicts, checking arithmetic premises, expanding a compact hypergraph or choosing an optimal partition are separate problems with separate costs. An uncertain relationship can conservatively keep work apart while its owning analysis seeks more evidence. Extra colors affect utilization, not the meaning of the program.

A proposed assignment is checked against every conflict edge and the applicable joint conditions. Bounded heuristics may improve grouping after correctness is established. Exhausting an optimization budget preserves a valid conservative assignment. It cannot turn an unresolved semantic obligation into permission. A principal dimensional type solution and a chosen valid coloring are distinct results; the latter need not be unique or optimal.

Joint constraints in the hypergraph

A joint hyperedge retains the complete participants and roles of an obligation. This helps identify which work depends on a changed premise and which region interface must be revalidated. It also avoids treating a multi-party condition as several unrelated facts.

A shared capacity illustrates why pairwise conflict alone is insufficient. Suppose three proposed allocations each require four units from a ten-unit budget. Every pair fits; the whole group does not. A batch must satisfy the joint capacity constraint even if its pairwise conflict graph has no edge. An exclusive-use constraint can conservatively become pairwise conflicts; a more permissive rule needs its own checked group-admission condition.

Locality, bounded neighborhoods and recognized graph classes may give useful specialized procedures. Their preconditions must be established for the actual region. Hypergraph representation and Ramsey-style structural intuition do not by themselves make arbitrary optimization or proof search polynomial.

Bidirectional zippers and semantic ownership

A zipper supplies focus, path, scope and reconstruction context. It helps a Baker rule identify an occurrence and preserve its origin through a change. Cross-scope aliases, captures and hyperedge participants still require explicit dependency information. Navigation does not discover or prove every dependency by itself.

Baker establishes the rewrite’s prerequisites and proposed graph change. Its fan-out produces proposals against a known snapshot. Fold-in validates their premises, reconciles overlaps and publishes consistent replacements and evidence. Changed facts trigger the owning saturation analyses. Readiness is distinct from confluence and termination; each admitted rule system needs its own argument.

Alex observes the settled outcome at the actual Huet occurrence. It composes Elements through Patterns and Witnesses while preserving graph-to-operation correspondence. Semantic conflict discovery, rule firing and proof settlement do not become a recursive emitter or a second analysis engine inside the zipper.

Arithmetic and permitted decomposition

A fixed reduction tree can execute independent branches concurrently while preserving its grouping. Changing the tree needs additional permission. With binary64 round-to-nearest/ties-to-even, (2^54 + -2^54) + 1 yields 1, while 2^54 + (-2^54 + 1) yields 0. Neither expression overflows. Coloring cannot supply an associativity law for these rounded additions.

An exact construction instead establishes term formation, initialization once, term multiplicity, ingest, every permitted partial and merge, and finalization. Accumulator capacity must cover those intermediate states, even when cancellation makes the final answer small. Fixed-point rescaling, exceptional values and boundary transfers have their own obligations. Memory ownership, publication and progress remain separate requirements.

Numeric Selection §§10.3–10.5 governs these permissions. Pondering Fearless Parallelism explains the distinct numerical contracts and their execution consequences.

Interaction nets and annihilation

Interaction-net rules provide a model of local reduction for admitted regions. A PSG rewrite must establish its correspondence to the selected calculus before using that calculus’s confluence result. Purity, participant readiness and a valid coloring do not establish this correspondence or guarantee termination.

An annihilation can retire active computation while preserving its source identity, surviving consumers and evidence. For numeric expressions, cancellation must respect the actual rounding, special values and intermediate obligations. For deferred computations it must preserve demand, effects and shared state. Equal current values do not authorize merging independently invalidated caches; see Incremental + Interaction Nets.

Static reductions settle in Baker. Dynamic rule execution requires an admitted state, rule and driver contract. Alex witnesses the settled portable structure; a semantic interaction-net dialect is not inserted into the middle end.

The rewrite tape through intermediates

Retain an inspectable chain through match, fan-out, fold-in and serialization:

Full dumps expose retained history. Pruned dumps preserve the needed evidence closure or point to retained records that resolve it. Omission cannot make an original participant look nonexistent or erase why a reduction was accepted. The tape is compiler evidence; it does not require runtime logging or keep retired computation executable.

Incremental reuse validates the recorded dependencies against the new snapshot. A late worker result cannot publish into a newer graph on the strength of a matching node name. Local recoloring may reuse unaffected work only when both its conflict relationships and joint premises remain valid.

Realization and acceptance

Independent maps, neighborhood operations, fixed reduction trees and admitted irregular reductions supply different workloads. Their shape and contracts guide eligible scalar, SIMD, GPU, actor or fabric realizations. Work size alone does not choose a target. Selected operation capabilities, storage, transfers, coordination and complete realization cost determine eligibility and the useful comparison.

Keep coloring purposes explicit: rewrite conflicts, runtime work groups, continuation-frame slot reuse and physical registers have different vertices, edges, constraints and consumers. A reusable algorithm does not merge their semantic contracts. Cache isolation also needs actual aligned bases and padded extents; see Counting the Cost of Coordination.

Acceptance includes independent and conflicting proposals, shared aliases and premises, the three-allocation joint-capacity case, stale/cancelled results, changed dimensional or arithmetic assumptions, and retained full/pruned traces. Numeric tests preserve fixed-tree results and exercise every admitted exact-merge contract. Artifact checks verify the realized operations and modes. Color count, utilization and elapsed time are performance observations, separate from those correctness checks.

See also

• Arithmetic Construction and Placement
• The DCont/INet Duality
• Collect Yourself!