fumola / alignment

alignment

A graph is aligned when what it remembers agrees with what it holds. An edit breaks that in one place; realignment finds how far the break reaches, and mends exactly that. This page is the prose, then the rules.

What alignment is#

Every edge in the graph records an action and what it observed: a get and the value it read, a force and the result it received, a put and the value it wrote. An edge is aligned when that record still agrees with the node it points at — the cell still holds that value, the thunk still has that result. A thunk is aligned when every edge of its trace is, and then its cached result is the result a fresh run would produce: that is the whole reason a cache hit is allowed.

The Recipe has the same idea one level up, for stores rather than edges. A thunk's cache there remembers the store it last ran under, and the cached result may be reused only when the current store is an aligned extension of that one — written $σ_{1} \leq σ_{2}$ . Comparing whole stores is the reference semantics' way of saying it and nobody's way of doing it; the graph's edges are the same fact recorded at the grain of a single observation, so that it can be checked one edge at a time.

Alignment has a state on each edge, Aligned or Signaled, and one invariant, which Nominal Adapton states as well-formedness: every edge into the source of a signaled edge is signaled. Whatever depends, however indirectly, on something that may have changed is marked as possibly changed itself. The invariant is what lets both traversals below stop early.

How an edit breaks it: signaling#

A put to a name that already has a node, with different contents, makes a new version of the node and starts a signaling traversal from it. The traversal visits the edges that point at the cell — its readers — and marks an edge signaled when its record is misaligned with the new contents: a get that recorded some other value, or any force. A put edge is never marked; an allocation is not an observation. Then it continues from the source of each edge it marked, a thunk whose result may now differ, and there it follows only the force edges into that thunk, because only its forcers observed its result — a get of a thunk pointer observes the thunk's body, which nothing here has changed.

It stops at any edge already signaled. By the invariant, everything beyond it is signaled already. This is what makes many edits before one demand cost about as much as one edit: the second traversal finds the first one's marks and goes no further.

A put of the same contents — the same value, or the same thunk body in the same space — is a matched put. It keeps the node and its readers as they are and records only the allocation edge. Nominal Adapton's Eval-refClean. This is what lets a program be re-run inside a live graph and find its own thunks again by name.

let x = `x := 1;
let t = `t := thunk { (@ x) + 1 };
force t;        // 2: a cache miss; t's trace is one get edge
x := 5;         // signals t's get edge, then the force edge into t

How realignment happens: repair#

Nothing more happens until something is demanded. A force of a thunk that has a cached result and no signaled edge in its trace is a cache hit, as before. A force of a thunk whose trace does hold a signaled edge repairs it first, walking the trace in the order the thunk took its actions:

An aligned edge is passed over. A signaled get edge is compared on the spot: if the cell now holds what the edge recorded, the edge is aligned again and the walk goes on; if not, the thunk is misaligned. A signaled force edge has its target brought up to date first — forced, which may repair or re-evaluate that thunk, recursively — and only then is the target's result compared with what the edge recorded. Equal, and the edge is aligned again: this is the cutoff, the reason repair can be cheaper than a re-run, since a thunk whose input changed but whose answer did not stops the change right there.

When every edge realigns, the thunk is aligned and its cached result is the answer. When one cannot, the thunk is re-evaluated: its old trace's edges leave the live graph (the history keeps them), and a new version of the thunk runs as an ordinary cache miss, building a new trace as it goes — and the forces it makes along the way meet the rest of the graph already repaired or waiting to be.

force t         // 6: repair finds the get misaligned (1 recorded, 5 held)
                //    and re-evaluates t as a new version

In the runtime the walk is shared between the graph and the VM, because checking a force edge means forcing a thunk, and forcing runs Fumola code. force_begin answers Repair; the VM asks the graph for one step at a time — aligned, here is the value; force this pointer and bring me its value; misaligned, evaluate this body — and hands each forced value back for the comparison. A force made on repair's behalf records no new edge: the edge under check is the one that gets completed.

Reading it in the history#

Both traversals are written into the event history as they run, bracketed the way a force is: signalingBegin … signalingEnd with an edgeSignaled per edge marked, and repairBegin … repairEnd with an edgeAligned per edge realigned and a removeEdge per edge dropped; repairEnd says whether the thunk realigned or was re-evaluated. Read with one letter per event, the program above is

S[ss]R[x!]

— one signaling that marked two edges (the get, and the force into t), then one repair that removed one edge and re-evaluated. A test reads exactly that string out of the history. The counters under `adapton(`counts) — signalings, edgesSignaled, repairs, edgesAligned, reevaluations, putMatched — are the same story as numbers, and are what the measurement work will read.

The formal view#

The rules are the Recipe's, from adapton-recipe.ott as revised on 2026-09-09 to these words, typeset as the Recipe typesets them. signal is the traversal an edit starts, repair the one a force runs, and the status bit on an edge is aligned or signaled. The runtime is the reference where the two disagree; the disagreements are listed after the rules.

$G$ a graph; $n$ an edge identifier; $t$ a trace, a sequence of edge identifiers; $p ~ ˙$ a graph-node pointer, a full pointer at a meta-moment; $p ~, q ~$ full pointers, a space and a moment, $⟨ ς, ψ ⟩^{s t}$ ; $A$ an action with the value it observed — put, get or force; $b$ a status bit; $A^$ an action pattern, $misaligned (ς, v)$ or $forces$ ; $p ~ ˙ A b q ~$ an edge from a thunk node to what it acted on. A thunk node is $⟨ ς, e, ⟨ t, v ⟩⟩$ — its space, its body, and its cache of trace and value — or $⟨ ς, e, ∙ ⟩$ when it has not run. A judgement $G; π ⊢_{ψ, m}^{ς} \dots ⇓ \dots$ carries the path of thunks being evaluated, the ambient space, and the moment and meta-moment.

Signaling: a node, and a set of edges#

signalNode starts from the node the put changed, with the pattern $misaligned (ς, v)$ . ST-alignedIntoSignaled is where an edge is marked, and its last premise is the recursion — with the pattern $forces$ , so that only force edges are followed from there. ST-alreadySignaled is the early stop; ST-stillAligned is why a put edge, and a get that recorded the value the cell holds again, are left alone.

signalNode

\frac{G _{1} ⊢ signal ( A ^ , incomingEdges ( G _{1} , p ~ ˙ )) ⇓ G _{2}}{G _{1} ⊢ signal ( A ^ , p ~ ˙ ) ⇓ G _{2}}

ST-empty

\frac{x}{G ⊢ signal ( A ^ , \cdot ) ⇓ G}

ST-binary

\frac{G _{1} ⊢ signal ( A ^ , t _{1} ) ⇓ G _{2} G _{2} ⊢ signal ( A ^ , t _{2} ) ⇓ G _{3}}{G _{1} ⊢ signal ( A ^ , t _{1} , t _{2} ) ⇓ G _{3}}

ST-alreadySignaled

\frac{G ( n ) = p ~ ˙ A signaled q ~}{G ⊢ signal ( A ^ , n ) ⇓ G}

ST-stillAligned

\frac{G ( n ) = p ~ ˙ A aligned q ~ A ^ \neq \approx A}{G ⊢ signal ( A ^ , n ) ⇓ G}

ST-alignedIntoSignaled

\frac{G _{1} ( n ) = p ~ ˙ A aligned q ~ A ^ \approx A G _{2} = G _{1} { n \mapsto p ~ ˙ A signaled q ~ } G _{2} ⊢ signal ( forces , p ~ ˙ ) ⇓ G _{3}}{G _{1} ⊢ signal ( A ^ , n ) ⇓ G _{3}}

Repair: a node, and its trace#

RN-aligned and RN-misaligned are the two outcomes for a thunk; the second re-evaluates it into a new version at the next meta-moment, which is the only rule that advances one. The RT- rules walk the trace: RT-binL stops at the first misaligned edge; RT-signaledIntoAligned brings the target up to date and compares, and is the cutoff when the comparison succeeds.

RN-aligned

\frac{G _{1} ( p ~ ) = ⟨ ς , e _{0} , ⟨ t _{0} , v _{0} ⟩⟩ G _{1} ; π ⊢ _{ψ, m}^{ς} repair ( t _{0} ) ⇓ G _{2} ; aligned}{G _{1} ; π ⊢ _{ψ, m}^{ς} repair ( p ~ ) ⇓ G _{2}}

RN-misaligned

\frac{G _{1} ( p ~ ) = ⟨ ς _{0} , e _{0} , ⟨ t _{0} , v _{0} ⟩⟩ G _{1} ; π ⊢ _{ψ, m_{1}}^{ς} repair ( t _{0} ) ⇓ G _{2} ; signaled nextMetaMoment ( G _{2} ) = m _{2} G _{2} { ( p ~ , m _{2} ) \mapsto ⟨ ς _{0} , e _{0} , ∙ ⟩ } ; π , p ~ ⊢ _{ψ, m_{2}}^{ς_{0}} e _{0} ⇓ G _{3} ; t _{3} ; v _{3}}{G _{1} ; π ⊢ _{ψ, m_{1}}^{ς} repair ( p ~ ) ⇓ G _{3} { ( p ~ , m _{2} ) \mapsto ⟨ ς _{0} , e _{0} , ⟨ t _{3} , v _{3} ⟩⟩ }}

RT-empty

\frac{x}{G ; π ⊢ _{ψ, m}^{ς} repair ( \cdot ) ⇓ G ; aligned}

RT-binL

\frac{G _{1} ; π ⊢ _{ψ, m}^{ς} repair ( t _{1} ) ⇓ G _{2} ; signaled}{G _{1} ; π ⊢ _{ψ, m}^{ς} repair ( t _{1} , t _{2} ) ⇓ G _{2} ; signaled}

RT-binR

\frac{G _{1} ; π ⊢ _{ψ, m}^{ς} repair ( t _{1} ) ⇓ G _{2} ; aligned G _{2} ; π ⊢ _{ψ, m}^{ς} repair ( t _{2} ) ⇓ G _{3} ; b}{G _{1} ; π ⊢ _{ψ, m}^{ς} repair ( t _{1} , t _{2} ) ⇓ G _{3} ; b}

RT-alreadyAligned

\frac{G ( n ) = p ~ ˙ A aligned q ~}{G ; π ⊢ _{ψ, m}^{ς} repair ( n ) ⇓ G ; aligned}

RT-signaledIntoAligned

\frac{G _{1} ( n ) = p ~ ˙ A signaled q ~ G _{1} ; π , q ~ ⊢ _{ψ, m}^{ς} repair ( q ~ ) ⇓ G _{2} value ( A ) = value ( G _{2} , q ~ )}{G _{1} ; π ⊢ _{ψ, m}^{ς} repair ( n ) ⇓ G _{2} { n \mapsto p ~ ˙ A aligned q ~ } ; aligned}

RT-misaligned

\frac{G _{1} ( n ) = p ~ ˙ A signaled q ~ G _{1} ; π , q ~ ⊢ _{ψ, m}^{ς} repair ( q ~ ) ⇓ G _{2} value ( A ) \neq = value ( G _{2} , q ~ )}{G _{1} ; π ⊢ _{ψ, m}^{ς} repair ( n ) ⇓ G _{2} ; signaled}

Forcing a thunk pointer#

An empty cache evaluates; a filled cache is repaired first and then read. In both, the force edge is added last, with the value the demander receives.

IE-emptyForce

\frac{p ~ ˙ = (⟨ ς _{2} , ψ ⟩ ^{s t} , m ) G _{2} ( p ~ ˙ ) = ⟨ ς _{0} , e _{0} , ∙ ⟩ G _{1} ; π ⊢ _{ψ, m}^{ς_{1}} e ⇓ G _{2} ; t ; ptr ς _{2} G _{2} ; π , ⟨ ς _{2} , ψ ⟩ ^{s t} ⊢ _{ψ, m}^{ς_{0}} e _{0} ⇓ G _{3} ; t _{3} ; v _{3} addEdge ( G _{3} { p ~ ˙ \mapsto ⟨ ς _{0} , e _{0} , ⟨ t _{3} , v _{3} ⟩⟩ } , top ( π ) force ( v _{3} ) aligned ⟨ ς _{2} , ψ ⟩ ^{s t} ) = ( G _{4} , n )}{G _{1} ; π ⊢ _{ψ, m}^{ς_{1}} force ( e ) ⇓ G _{4} ; t , n ; v _{3}}

IE-repairForce

\frac{p ~ ˙ = (⟨ ς _{2} , ψ ⟩ ^{s t} , m ) G _{2} ( p ~ ˙ ) = ⟨ ς _{0} , e _{0} , ⟨ t _{0} , v _{0} ⟩⟩ G _{1} ; π ⊢ _{ψ, m}^{ς_{1}} e ⇓ G _{2} ; t ; ptr ς _{2} G _{2} ; π ⊢ _{ψ, m}^{ς_{0}} repair (⟨ ς _{2} , ψ ⟩ ^{s t} ) ⇓ G _{3} G _{3} (⟨ ς _{2} , ψ ⟩ ^{s t} ) = ⟨ ς _{0} , e _{0} , ⟨ t _{3} , v _{3} ⟩⟩ addEdge ( G _{3} , top ( π ) force ( v _{3} ) aligned ⟨ ς _{2} , ψ ⟩ ^{s t} ) = ( G _{4} , n )}{G _{1} ; π ⊢ _{ψ, m}^{ς_{1}} force ( e ) ⇓ G _{4} ; t , n ; v _{3}}

Where the runtime and the rules differ#

Found by lining the rules up with the code, and listed for the Recipe to take up; the code is the reference because its behaviour is checkable, against from-scratch runs and by eye in the playground.

repair of a cell	`RT-signaledIntoAligned` repairs the target of every edge, and `repair` of a pointer has rules only for thunks. For a `get` edge the target is a cell; the rule it needs says nothing to do, and the runtime compares directly.
the patterns	The pattern-matching relations have no rules yet. The runtime reads $misaligned (ς, v)$ as: a `get` whose recorded value differs from the new one, or any force; and $forces$ as any force.
edges	The rules' edges target a full pointer with no meta-moment; the runtime's edge type names a node version but fills the meta-moment with the moment of the access. Same meaning; the type is misleading, and readers are indexed by (space, moment) as the rules' `incomingEdges` is.
old edges	The rules keep every edge forever; the runtime removes a re-evaluated thunk's old trace from the live graph, as the papers do, and keeps it in the history.
matched put	The graphical `put` rule is a prose placeholder. The runtime's put of unchanged contents keeps the node (Nominal Adapton's `Eval-refClean`); the rules as written would mint a version and dirty nothing.
a node's version	Looking a node up at the current meta-moment, as `IE-emptyForce` and `IE-repairForce` write it, means its latest version, which is what the runtime's lookup answers. (Three typos the lining-up found — v for v₃ in both force rules' conclusions, G₂ for G₁ in `RT-binL`, ς for ς₀ in `RN-misaligned` — were fixed in the revision.)
get of a thunk	The reference rule yields the pair (space, thunk); the runtime's `get` of a thunk pointer yields the thunk alone.
undelay	"Uses dirtying" in the prose; does not signal in the runtime yet.

What is left#

In the runtime: a cycle check (a thunk that forces itself loops today), signaling on delayed puts, and Nominal Adapton's double-use check for a name allocated with two bodies in one run. In the tools: a playground example that is one graph edited in place, its trails drawn from the signaling and repair walk rather than from a diff of two runs. In the measurement: an oracle that runs the comparative examples as repairs and checks them against a from-scratch run, and the exhaustive sweeps that two-run diffs made too expensive. In the Recipe: the notes above, and the words. The working list, with the reasons, is docs/realignment.md.

graphical/mod.rs The implementation Its module documentation is the rule-by-rule reading guide: Algorithm 1 of the PLDI 2014 paper, the Eval- rules of Nominal Adapton, and the Recipe's, cited at each step.
adapton-recipe The Extended Adapton Recipe The source of the rules above, ott-tex/adapton-recipe.ott.
#106 Signaling and repair: the graphical cache realigns after an edit The change, its tests, and the behaviour that changed with it.
papers Adapton (PLDI 2014) and Nominal Adapton (OOPSLA 2015) Algorithm 1 is the pseudocode this follows; Figures 5, 6 and 8 of Nominal Adapton are the graph semantics and its well-formedness.