"""Exhaustive set checks and deterministic replica traces; Python stdlib only.
Run: python experiment.py. This models protocols, not a deployed database.
"""
from pathlib import Path
from itertools import combinations
import csv
import json
import platform
from html import escape
def pairs(nodes, r=2, w=2):
return [{'write': ''.join(ws), 'read': ''.join(rs),
'intersection': ''.join(sorted(set(ws) & set(rs))),
'overlap': len(set(ws) & set(rs))}
for ws in combinations(nodes,w) for rs in combinations(nodes,r)]
def write_csv(path, rows):
with path.open('w',newline='') as f:
writer=csv.DictWriter(f,fieldnames=list(rows[0]))
writer.writeheader()
writer.writerows(rows)
def latest(state, respondents):
return max(state[node] for node in respondents)
def write_back(state, respondents, version):
for node in respondents:
state[node]=max(state[node],version)
def sloppy_trace():
state={node:0 for node in 'ABCDE'}
rows=[]
def record(step,event,result=''):
rows.append({'step':step,'event':event,**state,'result':result})
record(0,'Home replicas A,B,C start at v0; D,E are fallback nodes')
# Write coordinator sees A,D,E. B,C are unreachable from it. E is delayed.
write_back(state,'AD',1)
record(1,'Write targets A,D,E; A,D store v1 and acknowledge','write completes: W=2')
result=latest(state,'BC')
record(2,'Later read coordinator receives B,C; handoff is delayed',f'read returns v{result}: R=2')
assert result == 0
# D's hinted copy is for B. C has not caught up. Acknowledged handoff
# is enough for this chosen later B,C read to encounter v1 at B.
write_back(state,'B',state['D'])
record(3,'D hands its hinted v1 to home replica B')
result=latest(state,'BC')
record(4,'Read B,C again with newest-version selection',f'read returns v{result}')
assert result == 1
return rows
def inversion_trace(repair):
state={node:0 for node in 'ABC'}
rows=[]
def record(step,event,result=''):
rows.append({'step':step,'event':event,**state,'result':result})
record(0,'Initial state')
write_back(state,'A',1)
record(1,'Write v1 reaches A only; write is still pending')
first=latest(state,'AB')
record(2,'Read 1 obtains A,B and selects newest version',f'selected v{first}')
if repair:
write_back(state,'AB',first)
record(3,'Read 1 writes v1 back to A,B and waits for both acknowledgments')
record(4,'Read 1 completes',f'returns v{first}')
second=latest(state,'BC')
record(5,'Read 2 starts later and obtains B,C',f'returns v{second}')
assert (first,second) == ((1,1) if repair else (1,0))
return rows
def svg_start(width,height,title,subtitle):
return [f'']
path.write_text('\n'.join(s))
def trace_svg(path, rows, title, subtitle, nodes):
width,height=1000,155+len(rows)*72
s=svg_start(width,height,title,subtitle)
start=605
for i,node in enumerate(nodes):
s += [f'{node}']
for j,row in enumerate(rows):
y=125+j*72
# Labels split at a word boundary for predictable fit.
words=row['event'].split(); lines=['']
for word in words:
if len(lines[-1])+len(word)>65: lines.append('')
lines[-1]+=(' ' if lines[-1] else '')+word
for k,line in enumerate(lines):
s += [f'{row["step"] if k==0 else ""} {escape(line)}']
if row['result']:
s += [f'{escape(row["result"])}']
for i,node in enumerate(nodes):
value=row[node]
x=start+i*62
color='#8b4345' if value else '#e8e4df'
textcolor='#fff' if value else '#555'
s += [f'',
f'v{value}']
s += ['']; path.write_text('\n'.join(s))
def run(out=None):
out=Path(out or Path(__file__).parent)
(out/'data').mkdir(parents=True,exist_ok=True)
(out/'figures').mkdir(exist_ok=True)
strict=pairs('ABC')
expanded=pairs('ABCDE')
assert len(strict)==9 and all(row['overlap'] for row in strict)
assert len(expanded)==100 and sum(row['overlap']==0 for row in expanded)==30
# Exhaustively check the theorem for all nonempty R,W and N <= 7.
sizes_checked=0; pair_checks=0
for n in range(1,8):
nodes='ABCDEFG'[:n]
for r in range(1,n+1):
for w in range(1,n+1):
rows=pairs(nodes,r,w)
assert all(x['overlap']>0 for x in rows) == (r+w>n)
sizes_checked+=1; pair_checks+=len(rows)
# Every later strict quorum sees a lone completed write, provided latest
# version selection and no state loss or intervening writes.
for row in strict:
state={node:0 for node in 'ABC'}
write_back(state,row['write'],1)
assert latest(state,row['read'])==1
# Every read intersects every majority write-back set after read 1 finishes.
repair_cases=0
for repair_set in combinations('ABC',2):
for read_set in combinations('ABC',2):
state={node:0 for node in 'ABC'}
write_back(state,repair_set,1)
assert latest(state,read_set)==1
repair_cases+=1
sloppy=sloppy_trace()
inversion=inversion_trace(False)
repaired=inversion_trace(True)
for name,rows in [('strict-pairs',strict),('expanded-pairs',expanded),('sloppy-trace',sloppy),
('read-inversion',inversion),('read-writeback',repaired)]:
write_csv(out/'data'/f'{name}.csv',rows)
summary={'strict_pairs':len(strict),'strict_disjoint':0,'expanded_pairs':len(expanded),
'expanded_disjoint':30,'theorem_configurations_checked':sizes_checked,
'theorem_pairs_checked':pair_checks,'writeback_pairs_checked':repair_cases,
'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':platform.python_version(),'run_date':'2026-11-06'}
(out/'data/summary.json').write_text(json.dumps(summary,indent=2)+'\n')
matrix_svg(out/'figures/intersections.svg',strict)
trace_svg(out/'figures/sloppy-trace.svg',sloppy,'A completed write can miss a later read',
'Different reachability: write responds through A,D; later read responds through B,C.', 'ABCDE')
trace_svg(out/'figures/read-inversion.svg',inversion,'An unfinished write can produce a read–read inversion',
'All reads collect two home replicas. This version of the protocol omits synchronous write-back.', 'ABC')
trace_svg(out/'figures/read-writeback.svg',repaired,'Writing back before returning prevents this inversion',
'The selected version reaches a majority before Read 1 completes.', 'ABC')
return summary
if __name__=='__main__':
print(json.dumps(run(),indent=2))