The Replay Lattice

Why I wrote it

Changing the worker count could change my distributed jobs' result bits. I asked it to finish sooner. Now there's another answer to explain.

I love golden-file regression tests.

Save a known result, change the code, compare what comes back, and I have something concrete to investigate instead of deciding whether the whole output looks convincing or remembering what each row used to be.

Except now the saved result changed. Was it my code? Or did autoscaling arrange the same calculation differently? I could check the change, the input, the workers.... I wanted the diff to explain my change. Now I had to investigate the machines too.

I want reproducibility checked. Let's start with four numbers so we can follow where the trouble comes from:

[10000000000000000, 1, -10000000000000000, 1]

On paper these add up to two. Using 64-bit floats we get one, well, one when adding left to right as the browser does. Add the neighbours in pairs and we get zero. Near the large numbers adding one can round back to the number we started with. Moving the parentheses changes where those ones disappear.

The ones are doing their best.

A parallel sum can split its input into one chunk per worker. Changing the worker count then changes the grouping. In the example below try two workers, then one. Choose Fixed tree and try again.

Fixed tree keeps returning zero.

We've made the answer repeatable without making it two. Which answer have we agreed to reproduce? Matching a chosen floating-point reference and getting the mathematical answer are separate questions.

While working on Floatyboat (my array language) an optimiser merged two reductions over the same input. A reduction combines many inputs into one result, as a sum does. One was unrestricted and the other had to preserve a reproducibility requirement. From the optimiser's view, here was the same job being done twice, and combining them was a sensible way to do less work with the information it had.

My promise wasn't there. I needed that promise to survive the compiler changing the program. And it has to reach back through the calculation. Fixing the final sum's grouping doesn't help if an earlier operation already made its input depend on the schedule.

The Replay Lattice carries one of three classes with each value. exact requires agreement with a specified serial reference under the fixed build. replay requires matching bits across the schedules in the model. approx imposes no such schedule constraint.

When calculations meet their histories contribute to the result's class. A declaration asking for a stronger guarantee can then be rejected with a path to the earlier operation that weakened it.

That's the part of a diagnostic I need most.

Pointing at my declaration tells me where I asked for reproducibility, following the path back tells me which calculation stopped me getting it, and that gives me somewhere to start changing the program.

Writing the paper has been harder than I wanted it to be. It's hard to know how much of the topic I need to cover, and trying to explain the design finds holes in it very quickly.

Explain one part, find another hole, go back and.... Then I have another thing to work out and another thing to explain.

It can feel a bit Sisyphean.

There's always more to say, but the page limit never changes. I want enough room to follow the thought and keep the paper interesting to read and get it succinct enough without losing that rhythm. That has taken work.

Abstract

Add the same floating-point numbers in a different order, and the last bits of the sum can change. A parallel reduction groups its input by worker count, and one program can then return different bits on different worker counts. So a promise of bit-for-bit reproducibility depends on an unannounced schedule.

A floating-point value’s determinism is a demand carried on the value, one that holds only if every operation that ever touched the value obeyed it. Almost every mechanism the field has built to govern reordering is instead a grant attached to a site, a licence to reorder at one place in the program text. A grant is true where it is written. A demand’s truth is settled upstream, by the value’s history, which no single site can see. We present the Replay Lattice with three schedule-class contracts, exact below replay below approx, carried on every value of a pure dataflow array language, joined over the dependency path, checked at each declaration, and discharged into backend lowering obligations.

Two theorems come with the lattice. Soundness is a two-run induction over the dataflow graph, mechanised in Coq. The poisoning law says one free reordering taints everything downstream, and its proof is one line on top of the join.

We also audit our own evidence, finding ten occasions on which a passing check of ours had proved nothing, and repairing every one. The usual figure, no rejections over an unannotated corpus, holds by construction for a demand-only checker, which is why we do not offer it as evidence.

Finally, the artefact ships the checker and its nineteen must-fail controls. The result is a language in which these bits must not depend on the schedule is a sentence the compiler checks.

Scope and evidence

Floatyboat supplies the language-design problem. The manuscript explores the proposed type system through a smaller demonstration language, lanelang, and its checker. The proof in Coq checks the type system's soundness in a model of the language, and each implementation still needs checks of its own. On a fixed build the evidence covers changes of schedule. Other toolchains and hardware are outside that evidence.

The PDFs and recorded figure evidence on this site come from the artefact's 0.3.0 release at commit c5c4321. They are a fixed snapshot. The public artefact repository can change separately. The recorded source and checker output are in the evidence snapshot.