The Replay Lattice

Running container

2-way parallelism

Same running container

16-way parallelism

Same 5,000 pseudorandom values. Fixed seed: 1.

Four bit patterns versus one.

Results shown to 13 decimal places.

Change only the degree of parallelism and the analysis returns a different evolutionary tree.

Same binary. Same seeds.

“May contain nuts.”

Settled at the dish that carries it. Nothing added elsewhere can make it false.

The implementation may choose the order.

“Contains no nuts.”

A claim about every ingredient that ever entered the pot. One nut anywhere falsifies it, and no later stirring takes it back out.

A promise about the result, so everything upstream has to keep it.

The bits equal the serial reference.

The bits must not move with the schedule. Tomorrow's run agrees with today's.

The bits may move with the schedule. The default, because only some results need the promise.

It matches the serial reference, rounding error and all.

Determinism today does not mean determinism tomorrow.

One qualifier, on the one value you care about.

The lattice handles it. Once the rounding has happened, nothing can waive it.

A source is ungrounded: the program does not fix its bytes, so replay over it is refused.

“These bytes will be the same next run.”

The run checks it before computing anything.

The lane is part of the value's identity, so common-subexpression elimination can't merge them.

Unannotated code lowers to the identical free kernel.

At most d + 2 passes across d carried edges.

LS-DYNA, pinned order, shared-memory build, serial assembly: “at least 15 percent”.

CCCL gpu_to_gpu, large problem sizes: “20% to 30%”.

The unannotated program and its approx twin lower to the identical free kernel. Pinned by two fixtures.

With no recurrence. At most d + 2 passes when lane information crosses d carried edges.

total := iterate(..., with: (outer, t) => {
  nested := iterate(..., with: (inner, u) => {
    return inner + sum(x)
  })
  return outer + nested
})

Two recurrences, one inside the other.

a := iterate(..., with: (acc, t) => {
  return acc + sum(x)
})
b := iterate(..., with: (acc, t) => {
  return acc + a
})
c := iterate(..., with: (acc, t) => {
  return acc + b
})

Three recurrences in sequence; each reads the previous result.

Pass 1: discover approx

func main() Float {x := indices(count: 1000.0)total := iterate(times: 3.0, from: 0.0,with: (acc, t) => {replay hello := accapprox part := sum(x)return hello + part})return total}

Body and total: approx. The earlier demand still appears satisfied.

Pass 2: feedback reaches acc

func main() Float {x := indices(count: 1000.0)total := iterate(times: 3.0, from: 0.0,with: (acc, t) => {replay hello := accapprox part := sum(x)return hello + part})return total}

Body and total: approx. The replay demand on hello is violated.

Private producer - accepted

func main() Float {x := indices(count: 1000.0)s := sum(x)t := s + 1.0replay e := sum(x * t)return e}

s reaches the result only through e. The demand permits pinning s.

Replay demand satisfied.

Outside read - rejected

func main() Float {x := indices(count: 1000.0)s := sum(x)t := s + 1.0replay e := sum(x * t)return t + e}

t reaches the result without passing through e. Pinning s could change that outside result.

Replay demand cannot be met.

What the theorem needs

1. Graph properly ordered
2. Kernels honour their classes
3. Each node’s lane follows the join rule
4. Choose any two schedules for which:
   4a.At each recurrence step, the carried bits match where required

   4b.The declared lane promises matching bits across these two schedules
5. The computed lane satisfies the declared demand