I'm working on a paper about a type system for floating-point reproducibility. It's called the Replay Lattice, and the idea is to let a program state which numerical results must be reproducible, then have the compiler check that requirement.
I came to this through big-data work running across distributed systems, where sometimes the values coming back changed with the amount of infrastructure doing the work. Whether it was more workers, different resources or some other scaling decision, I wanted the job to finish sooner, I didn't want that decision to choose a different answer. This is especially irritating with the golden-file regression tests I'm so fond of. If scaling changes the bits without a code change, the diff stops answering the question I care about.
Did I break something, or did this run arrange the same work differently? Horizontal autoscaling changes how many workers I have, while vertical autoscaling changes the resources each one gets. Both make that a moving target. That frustration, alongside my fondness for golden tests, is what drew me into determinism and eventually the Replay Lattice paper.
Four numbers let me show one way the difference happens:
[10000000000000000, 1, -10000000000000000, 1]
Add those four numbers with one worker and our example gives one. Give it two workers and it gives zero. On paper, the answer is two.
A productive calculation (if your aim is to find trouble).
I can follow every addition here and see how an infrastructure decision reaches into the arithmetic. The Replay Lattice lets the program state which promise that deployment choice needs to keep.
I'm working towards this in Floatyboat, my array language and compiler.
The vectoriser example meets the same rounding problem when replacing a source loop. Here the moving part is the worker count.
A 64-bit float has a limited number of significant binary digits, called its significand. Around ten quadrillion the neighbouring representable values are two apart, so adding one lands between them and rounding to the nearest value with ties to even takes us back to the large value we started with.
Add from left to right:
((10000000000000000 + 1) + -10000000000000000) + 1
= (10000000000000000 + -10000000000000000) + 1
= 1
The big values cancel after the first 1 has disappeared, leaving the last 1 intact.
Now pair the neighbours first:
(10000000000000000 + 1) + (-10000000000000000 + 1)
= 10000000000000000 + -10000000000000000
= 0
Both ones disappear before the large values meet. Each addition follows the same rules, but moving the parentheses changes where information gets rounded away.
How close is the answer to the mathematical sum, and can changing the grouping change it? I need both, because a stable result can still be zero for a sum of two. That's useful for a regression test. Zero is a very stable answer. It's also out by two.
The workers brought parentheses
A straightforward parallel sum splits the input into chunks. Each worker adds its chunk, then the partial sums are combined. Changing the worker count moves the chunk boundaries, which changes the grouping.
Here one worker adds left to right. With two workers each adds a pair, and with four each gets one value before the demonstration combines those partial results left to right. That gives us one, zero and one, following the particular chunking and combining algorithm shown here.
That's rather more responsibility than I wanted to give a worker-count setting, because which results move when I give the job more parallelism is now a deployment question.
Three promises to choose from
We can choose a tree of additions from the number and arrangement of input values, independently of worker count. More workers can take different branches without redrawing the calculation. In the fixed-tree version below, assignments move while the answer stays zero.
The Replay Lattice gives calculations three classes. They describe the execution property we want to preserve:
| Class | What it promises |
|---|---|
exact | Agreement with a specified serial reference under the fixed build. |
replay | The same bits across the schedules included in the model. |
approx | No such schedule constraint. |
If I'm replacing an existing serial calculation, I may need its answer to stay one, so matching that reference satisfies exact even though the mathematical sum is two. The paper calls the reference an oracle. I'm keeping an agreed floating-point calculation, including its rounding error.
For a new calculation I might be happy to choose the fixed tree's stable zero instead, choosing replay because the schedule can change without changing those bits, though judging the numerical accuracy is still my job. Approx leaves scheduling freedom open, even if a free computation happens to agree across many runs. For the old calculation, a golden file containing one will still show me a diff when I choose the stable zero. Stable isn't the whole request.
The classes order the strength of the guarantee:
exact ⊑ replay ⊑ approx
Agreement with the fixed reference also gives agreement across schedules. Agreement across schedules alone can still miss the reference's answer, and neither promise tells me how numerically accurate the answer is.
The schedule model holds the build fixed, so a different host compiler, vector width or ABI falls outside the promise, and that scope belongs in my deployment decision.
A stable tree is a useful start, but its input can still come from an earlier calculation whose answer changes with the schedule, so the compiler has to follow those dependencies too. Otherwise, we've fixed the last addition and left the moving parts upstream.
There's also the input file. If its bytes change overnight, tomorrow's fixed tree adds different numbers. A scheduling promise needs agreed inputs as well as agreed combining rules.
You can read the Replay Lattice paper for the model and its assumptions. Our browser example uses 64-bit floats to make the grouping visible.
What I want from this is fairly practical. I can scale the job and keep the numerical promise I've chosen. Then a golden-file diff can go back to showing me a change in behaviour, instead of sending me off to investigate how many machines happened to be running.