What Quorum Arithmetic Leaves Out
Exhaustive finite-set checks and deterministic replica traces. The results show protocol counterexamples, not observed production failure frequencies. The code models fixed quorums, sloppy respondents, and the read write-back mechanism.
Extract the complete package and run from this directory. Python 3.10+, standard library. No network calls.
Run and check
The script executes the experiment and its assertions, then writes the data and figures.
{
"strict_pairs": 9,
"strict_disjoint": 0,
"expanded_pairs": 100,
"expanded_disjoint": 30,
"theorem_configurations_checked": 140,
"theorem_pairs_checked": 21343,
"writeback_pairs_checked": 9,
"sloppy_read_before_handoff": 0,
"sloppy_read_after_handoff": 1,
"sequential_reads_without_writeback": [
1,
0
],
"sequential_reads_with_writeback": [
1,
1
],
"measurement": "Exhaustive finite-set model plus explicit deterministic traces, not a database benchmark or failure probability",
"python": "3.12.14",
"run_date": "2026-11-06"
}
Inspect disjoint respondent pairs
The 30 disjoint pairs are structural counterexamples, not a probability estimate.
Disjoint pairs: 30
[{'write': 'AB', 'read': 'CD', 'intersection': '', 'overlap': 0}, {'write': 'AB', 'read': 'CE', 'intersection': '', 'overlap': 0}, {'write': 'AB', 'read': 'DE', 'intersection': '', 'overlap': 0}, {'write': 'AC', 'read': 'BD', 'intersection': '', 'overlap': 0}, {'write': 'AC', 'read': 'BE', 'intersection': '', 'overlap': 0}, {'write': 'AC', 'read': 'DE', 'intersection': '', 'overlap': 0}, {'write': 'AD', 'read': 'BC', 'intersection': '', 'overlap': 0}, {'write': 'AD', 'read': 'BE', 'intersection': '', 'overlap': 0}, {'write': 'AD', 'read': 'CE', 'intersection': '', 'overlap': 0}, {'write': 'AE', 'read': 'BC', 'intersection': '', 'overlap': 0}]
Compare the read protocol
One pending write reaches A only. Without write-back, sequential reads AB then BC return 1 then 0. Synchronous majority write-back before returning changes this trace to 1 then 1.
Synchronous write-back: False
{'step': 0, 'event': 'Initial state', 'A': 0, 'B': 0, 'C': 0, 'result': ''}
{'step': 1, 'event': 'Write v1 reaches A only; write is still pending', 'A': 1, 'B': 0, 'C': 0, 'result': ''}
{'step': 2, 'event': 'Read 1 obtains A,B and selects newest version', 'A': 1, 'B': 0, 'C': 0, 'result': 'selected v1'}
{'step': 4, 'event': 'Read 1 completes', 'A': 1, 'B': 0, 'C': 0, 'result': 'returns v1'}
{'step': 5, 'event': 'Read 2 starts later and obtains B,C', 'A': 1, 'B': 0, 'C': 0, 'result': 'returns v0'}
Synchronous write-back: True
{'step': 0, 'event': 'Initial state', 'A': 0, 'B': 0, 'C': 0, 'result': ''}
{'step': 1, 'event': 'Write v1 reaches A only; write is still pending', 'A': 1, 'B': 0, 'C': 0, 'result': ''}
{'step': 2, 'event': 'Read 1 obtains A,B and selects newest version', 'A': 1, 'B': 0, 'C': 0, 'result': 'selected v1'}
{'step': 3, 'event': 'Read 1 writes v1 back to A,B and waits for both acknowledgments', 'A': 1, 'B': 1, 'C': 0, 'result': ''}
{'step': 4, 'event': 'Read 1 completes', 'A': 1, 'B': 1, 'C': 0, 'result': 'returns v1'}
{'step': 5, 'event': 'Read 2 starts later and obtains B,C', 'A': 1, 'B': 1, 'C': 0, 'result': 'returns v1'}
Generated figures
Sources
Python runs locally in this page. Saved results and figures are visible before execution.