A model checked against the code, and not calibrated by it
The redundancy model was replayed against 300 bench runs of the real code. It agreed, and the calibration step that was supposed to follow was dropped.
dusk models redundancy on hardware that decays over decades. The flight code now has a bench that runs fixed triple redundancy against the shrinking quorum for real: ten seeds, three upset rates and five fault schedules, 20,000 ticks a run, 300 runs per host. The counts came out identical on an Apple M4, a Neoverse N2 and an EPYC 7763. In all 150 pairs the shrinking quorum delivered at least as many correct results, and three times as many when two replicas were lost early.
The next question was whether the model agrees with the code. dusk --bench
replays the bench through the model: the same deaths, the same upset rate, one
tick as one day, 1,000 upset streams per row. It uses the model’s own spread
as the error, so a row where all ten seeds give zero is judged fairly.
Of 18 rows, 17 landed within three standard errors. The last, the shrinking quorum on the common mode schedule at the highest upset rate, was 3.4 low. Rerunning its two phases over 200 seeds matched the model closely: 40.38 results lost against a predicted 40.42 with two replicas, and 19.17 caught against a predicted 19.00 with one. It was chance in ten seeds. The check fails above four.
The plan had a calibration step next. It was dropped, because the bench sets the upset rate and the failure times itself. It cannot measure numbers it was handed. That needs radiation or flight data.
Stuck faults are reported as not modeled. A comment in the code says why: the model knows processors that die, not ones that lie.