FA-74961 / CRDT convergence / Open access
Multi-value register: a new write summarizes only the first sibling · case 01
A write meant to resolve a conflict leaves the other concurrent value alive.
ROOT CAUSE
The write context is taken from the first sibling only, so the new vector does not dominate the others.
VERIFIED REPAIR
Build the write context from the pointwise maximum over all current siblings.
Unsuccessful approach: Keeping only the writer's own component forgets peers' components, so the write still fails to dominate remote siblings.
Case contract
Each replica holds siblings [value, version vector]. ["write", r, v] builds the pointwise maximum of all current sibling vectors, increments r's entry, and replaces all siblings with [v, vector]. ["merge", s, d] pools both sibling lists, drops siblings strictly dominated by another pooled sibling, and keeps one copy per identical vector. Return sorted values per replica.
Why this case matters
Multi-value registers expose concurrent writes as siblings instead of silently discarding one.
1 / The failure
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(ops, replicas):
sib = {r: [] for r in replicas}
def dominates(x, y):
keys = set(x) | set(y)
return all(x.get(k, 0) >= y.get(k, 0) for k in keys) and x != y
for op in ops:
if op[0] == 'write':
r, v = op[1], op[2]
vv = {}
for _, c in sib[r][:1]:
for k, cnt in c.items():
vv[k] = max(vv.get(k, 0), cnt)
vv[r] = vv.get(r, 0) + 1
sib[r] = [[v, vv]]
else:
s, d = op[1], op[2]
pool = sib[d] + [[v, dict(c)] for v, c in sib[s]]
kept = []
for v, c in pool:
if any(dominates(c2, c) for _, c2 in pool):
continue
if any(c == c3 for _, c3 in kept):
continue
kept.append([v, c])
sib[d] = kept
return [sorted(v for v, _ in sib[r]) for r in replicas]
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = {
1: [('concurrent writes become siblings', [[['write', 'a', 'x'], ['write', 'b', 'y1'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b', 'c']], [['x', 'y1'], ['x', 'y1'], []]), ('a write after merge supersedes all siblings', [[['write', 'a', 'x'], ['write', 'b', 'y'], ['merge', 'a', 'b'], ['write', 'b', 'z1'], ['merge', 'b', 'a'], ['merge', 'b', 'c']], ['a', 'b', 'c']], [['z1'], ['z1'], ['z1']]), ('merging identical state keeps the value', [[['write', 'a', 'v1'], ['merge', 'a', 'b'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['v1'], ['v1'], []]), ('stale incoming sibling is discarded', [[['write', 'a', 'old'], ['merge', 'a', 'b'], ['write', 'b', 'new'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['old'], ['new'], []]), ('stale local sibling is replaced', [[['write', 'a', 'old'], ['merge', 'a', 'b'], ['write', 'a', 'new1'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['new1'], ['new1'], []]), ('same value written concurrently stays twice', [[['write', 'a', 'same'], ['write', 'b', 'same'], ['merge', 'a', 'c'], ['merge', 'b', 'c']], ['a', 'b', 'c']], [['same'], ['same'], ['same', 'same']]), ('overwrite by the same replica', [[['write', 'c', 'c0'], ['write', 'c', 'c1'], ['merge', 'c', 'a'], ['write', 'b', 'q'], ['merge', 'b', 'a']], ['a', 'b', 'c']], [['c1', 'q'], ['q'], ['c1']]), ('three-way concurrency then resolve', [[['write', 'a', 'p'], ['write', 'b', 'q'], ['write', 'c', 'r'], ['merge', 'a', 'c'], ['merge', 'b', 'c'], ['write', 'c', 'resolved'], ['merge', 'c', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['resolved'], ['resolved'], ['resolved']]), ('repeat merge after own rewrite', [[['write', 'a', 'x1'], ['merge', 'a', 'b'], ['write', 'a', 'x2'], ['write', 'b', 'y'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['x2', 'y'], ['x2', 'y'], []])],
2: [('concurrent writes become siblings', [[['write', 'a', 'x'], ['write', 'b', 'y2'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b', 'c']], [['x', 'y2'], ['x', 'y2'], []]), ('a write after merge supersedes all siblings', [[['write', 'a', 'x'], ['write', 'b', 'y'], ['merge', 'a', 'b'], ['write', 'b', 'z2'], ['merge', 'b', 'a'], ['merge', 'b', 'c']], ['a', 'b', 'c']], [['z2'], ['z2'], ['z2']]), ('merging identical state keeps the value', [[['write', 'a', 'v2'], ['merge', 'a', 'b'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['v2'], ['v2'], []]), ('stale incoming sibling is discarded', [[['write', 'a', 'old'], ['merge', 'a', 'b'], ['write', 'b', 'new'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['old'], ['new'], []]), ('stale local sibling is replaced', [[['write', 'a', 'old'], ['merge', 'a', 'b'], ['write', 'a', 'new2'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['new2'], ['new2'], []]), ('same value written concurrently stays twice', [[['write', 'a', 'same'], ['write', 'b', 'same'], ['merge', 'a', 'c'], ['merge', 'b', 'c']], ['a', 'b', 'c']], [['same'], ['same'], ['same', 'same']]), ('overwrite by the same replica', [[['write', 'c', 'c0'], ['write', 'c', 'c1'], ['write', 'c', 'c2'], ['merge', 'c', 'a'], ['write', 'b', 'q'], ['merge', 'b', 'a']], ['a', 'b', 'c']], [['c2', 'q'], ['q'], ['c2']]), ('three-way concurrency then resolve', [[['write', 'a', 'p'], ['write', 'b', 'q'], ['write', 'c', 'r'], ['merge', 'a', 'c'], ['merge', 'b', 'c'], ['write', 'c', 'resolved'], ['merge', 'c', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['resolved'], ['resolved'], ['resolved']]), ('repeat merge after own rewrite', [[['write', 'a', 'x1'], ['merge', 'a', 'b'], ['write', 'a', 'x2'], ['write', 'b', 'y'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['x2', 'y'], ['x2', 'y'], []])],
3: [('concurrent writes become siblings', [[['write', 'a', 'x'], ['write', 'b', 'y3'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b', 'c']], [['x', 'y3'], ['x', 'y3'], []]), ('a write after merge supersedes all siblings', [[['write', 'a', 'x'], ['write', 'b', 'y'], ['merge', 'a', 'b'], ['write', 'b', 'z3'], ['merge', 'b', 'a'], ['merge', 'b', 'c']], ['a', 'b', 'c']], [['z3'], ['z3'], ['z3']]), ('merging identical state keeps the value', [[['write', 'a', 'v3'], ['merge', 'a', 'b'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['v3'], ['v3'], []]), ('stale incoming sibling is discarded', [[['write', 'a', 'old'], ['merge', 'a', 'b'], ['write', 'b', 'new'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['old'], ['new'], []]), ('stale local sibling is replaced', [[['write', 'a', 'old'], ['merge', 'a', 'b'], ['write', 'a', 'new3'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['new3'], ['new3'], []]), ('same value written concurrently stays twice', [[['write', 'a', 'same'], ['write', 'b', 'same'], ['merge', 'a', 'c'], ['merge', 'b', 'c']], ['a', 'b', 'c']], [['same'], ['same'], ['same', 'same']]), ('overwrite by the same replica', [[['write', 'c', 'c0'], ['write', 'c', 'c1'], ['write', 'c', 'c2'], ['write', 'c', 'c3'], ['merge', 'c', 'a'], ['write', 'b', 'q'], ['merge', 'b', 'a']], ['a', 'b', 'c']], [['c3', 'q'], ['q'], ['c3']]), ('three-way concurrency then resolve', [[['write', 'a', 'p'], ['write', 'b', 'q'], ['write', 'c', 'r'], ['merge', 'a', 'c'], ['merge', 'b', 'c'], ['write', 'c', 'resolved'], ['merge', 'c', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['resolved'], ['resolved'], ['resolved']]), ('repeat merge after own rewrite', [[['write', 'a', 'x1'], ['merge', 'a', 'b'], ['write', 'a', 'x2'], ['write', 'b', 'y'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['x2', 'y'], ['x2', 'y'], []])],
4: [('concurrent writes become siblings', [[['write', 'a', 'x'], ['write', 'b', 'y4'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b', 'c']], [['x', 'y4'], ['x', 'y4'], []]), ('a write after merge supersedes all siblings', [[['write', 'a', 'x'], ['write', 'b', 'y'], ['merge', 'a', 'b'], ['write', 'b', 'z4'], ['merge', 'b', 'a'], ['merge', 'b', 'c']], ['a', 'b', 'c']], [['z4'], ['z4'], ['z4']]), ('merging identical state keeps the value', [[['write', 'a', 'v4'], ['merge', 'a', 'b'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['v4'], ['v4'], []]), ('stale incoming sibling is discarded', [[['write', 'a', 'old'], ['merge', 'a', 'b'], ['write', 'b', 'new'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['old'], ['new'], []]), ('stale local sibling is replaced', [[['write', 'a', 'old'], ['merge', 'a', 'b'], ['write', 'a', 'new4'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['new4'], ['new4'], []]), ('same value written concurrently stays twice', [[['write', 'a', 'same'], ['write', 'b', 'same'], ['merge', 'a', 'c'], ['merge', 'b', 'c']], ['a', 'b', 'c']], [['same'], ['same'], ['same', 'same']]), ('overwrite by the same replica', [[['write', 'c', 'c0'], ['write', 'c', 'c1'], ['write', 'c', 'c2'], ['write', 'c', 'c3'], ['write', 'c', 'c4'], ['merge', 'c', 'a'], ['write', 'b', 'q'], ['merge', 'b', 'a']], ['a', 'b', 'c']], [['c4', 'q'], ['q'], ['c4']]), ('three-way concurrency then resolve', [[['write', 'a', 'p'], ['write', 'b', 'q'], ['write', 'c', 'r'], ['merge', 'a', 'c'], ['merge', 'b', 'c'], ['write', 'c', 'resolved'], ['merge', 'c', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['resolved'], ['resolved'], ['resolved']]), ('repeat merge after own rewrite', [[['write', 'a', 'x1'], ['merge', 'a', 'b'], ['write', 'a', 'x2'], ['write', 'b', 'y'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['x2', 'y'], ['x2', 'y'], []])],
5: [('concurrent writes become siblings', [[['write', 'a', 'x'], ['write', 'b', 'y5'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b', 'c']], [['x', 'y5'], ['x', 'y5'], []]), ('a write after merge supersedes all siblings', [[['write', 'a', 'x'], ['write', 'b', 'y'], ['merge', 'a', 'b'], ['write', 'b', 'z5'], ['merge', 'b', 'a'], ['merge', 'b', 'c']], ['a', 'b', 'c']], [['z5'], ['z5'], ['z5']]), ('merging identical state keeps the value', [[['write', 'a', 'v5'], ['merge', 'a', 'b'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['v5'], ['v5'], []]), ('stale incoming sibling is discarded', [[['write', 'a', 'old'], ['merge', 'a', 'b'], ['write', 'b', 'new'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['old'], ['new'], []]), ('stale local sibling is replaced', [[['write', 'a', 'old'], ['merge', 'a', 'b'], ['write', 'a', 'new5'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['new5'], ['new5'], []]), ('same value written concurrently stays twice', [[['write', 'a', 'same'], ['write', 'b', 'same'], ['merge', 'a', 'c'], ['merge', 'b', 'c']], ['a', 'b', 'c']], [['same'], ['same'], ['same', 'same']]), ('overwrite by the same replica', [[['write', 'c', 'c0'], ['write', 'c', 'c1'], ['write', 'c', 'c2'], ['write', 'c', 'c3'], ['write', 'c', 'c4'], ['write', 'c', 'c5'], ['merge', 'c', 'a'], ['write', 'b', 'q'], ['merge', 'b', 'a']], ['a', 'b', 'c']], [['c5', 'q'], ['q'], ['c5']]), ('three-way concurrency then resolve', [[['write', 'a', 'p'], ['write', 'b', 'q'], ['write', 'c', 'r'], ['merge', 'a', 'c'], ['merge', 'b', 'c'], ['write', 'c', 'resolved'], ['merge', 'c', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['resolved'], ['resolved'], ['resolved']]), ('repeat merge after own rewrite', [[['write', 'a', 'x1'], ['merge', 'a', 'b'], ['write', 'a', 'x2'], ['write', 'b', 'y'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['x2', 'y'], ['x2', 'y'], []])],
}[N]
for label, args, expected in cases:
check(label, solve(*args), expected)
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)
| Boundary fixture | Actual | Expected | Outcome |
|---|---|---|---|
| concurrent writes become siblings | [['x', 'y1'], ['x', 'y1'], []] | [['x', 'y1'], ['x', 'y1'], []] | Passed |
| a write after merge supersedes all siblings | [['x', 'z1'], ['z1'], ['z1']] | [['z1'], ['z1'], ['z1']] | Failed |
| merging identical state keeps the value | [['v1'], ['v1'], []] | [['v1'], ['v1'], []] | Passed |
| stale incoming sibling is discarded | [['old'], ['new'], []] | [['old'], ['new'], []] | Passed |
| stale local sibling is replaced | [['new1'], ['new1'], []] | [['new1'], ['new1'], []] | Passed |
| same value written concurrently stays twice | [['same'], ['same'], ['same', 'same']] | [['same'], ['same'], ['same', 'same']] | Passed |
| overwrite by the same replica | [['c1', 'q'], ['q'], ['c1']] | [['c1', 'q'], ['q'], ['c1']] | Passed |
| three-way concurrency then resolve | [['p', 'resolved'], ['p', 'q', 'resolved'], ['resolved']] | [['resolved'], ['resolved'], ['resolved']] | Failed |
| repeat merge after own rewrite | [['x2', 'y'], ['x2', 'y'], []] | [['x2', 'y'], ['x2', 'y'], []] | Passed |
SHA-256 / d80dcef3d3efde45445a91a1604ab0911b3cd7ddbb8cace43f80653fcfb64ac7
2 / The unsuccessful fix
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(ops, replicas):
sib = {r: [] for r in replicas}
def dominates(x, y):
keys = set(x) | set(y)
return all(x.get(k, 0) >= y.get(k, 0) for k in keys) and x != y
for op in ops:
if op[0] == 'write':
r, v = op[1], op[2]
vv = {}
for _, c in sib[r]:
for k, cnt in c.items():
if k == r:
vv[k] = max(vv.get(k, 0), cnt)
vv[r] = vv.get(r, 0) + 1
sib[r] = [[v, vv]]
else:
s, d = op[1], op[2]
pool = sib[d] + [[v, dict(c)] for v, c in sib[s]]
kept = []
for v, c in pool:
if any(dominates(c2, c) for _, c2 in pool):
continue
if any(c == c3 for _, c3 in kept):
continue
kept.append([v, c])
sib[d] = kept
return [sorted(v for v, _ in sib[r]) for r in replicas]
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = {
1: [('concurrent writes become siblings', [[['write', 'a', 'x'], ['write', 'b', 'y1'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b', 'c']], [['x', 'y1'], ['x', 'y1'], []]), ('a write after merge supersedes all siblings', [[['write', 'a', 'x'], ['write', 'b', 'y'], ['merge', 'a', 'b'], ['write', 'b', 'z1'], ['merge', 'b', 'a'], ['merge', 'b', 'c']], ['a', 'b', 'c']], [['z1'], ['z1'], ['z1']]), ('merging identical state keeps the value', [[['write', 'a', 'v1'], ['merge', 'a', 'b'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['v1'], ['v1'], []]), ('stale incoming sibling is discarded', [[['write', 'a', 'old'], ['merge', 'a', 'b'], ['write', 'b', 'new'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['old'], ['new'], []]), ('stale local sibling is replaced', [[['write', 'a', 'old'], ['merge', 'a', 'b'], ['write', 'a', 'new1'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['new1'], ['new1'], []]), ('same value written concurrently stays twice', [[['write', 'a', 'same'], ['write', 'b', 'same'], ['merge', 'a', 'c'], ['merge', 'b', 'c']], ['a', 'b', 'c']], [['same'], ['same'], ['same', 'same']]), ('overwrite by the same replica', [[['write', 'c', 'c0'], ['write', 'c', 'c1'], ['merge', 'c', 'a'], ['write', 'b', 'q'], ['merge', 'b', 'a']], ['a', 'b', 'c']], [['c1', 'q'], ['q'], ['c1']]), ('three-way concurrency then resolve', [[['write', 'a', 'p'], ['write', 'b', 'q'], ['write', 'c', 'r'], ['merge', 'a', 'c'], ['merge', 'b', 'c'], ['write', 'c', 'resolved'], ['merge', 'c', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['resolved'], ['resolved'], ['resolved']]), ('repeat merge after own rewrite', [[['write', 'a', 'x1'], ['merge', 'a', 'b'], ['write', 'a', 'x2'], ['write', 'b', 'y'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['x2', 'y'], ['x2', 'y'], []])],
2: [('concurrent writes become siblings', [[['write', 'a', 'x'], ['write', 'b', 'y2'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b', 'c']], [['x', 'y2'], ['x', 'y2'], []]), ('a write after merge supersedes all siblings', [[['write', 'a', 'x'], ['write', 'b', 'y'], ['merge', 'a', 'b'], ['write', 'b', 'z2'], ['merge', 'b', 'a'], ['merge', 'b', 'c']], ['a', 'b', 'c']], [['z2'], ['z2'], ['z2']]), ('merging identical state keeps the value', [[['write', 'a', 'v2'], ['merge', 'a', 'b'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['v2'], ['v2'], []]), ('stale incoming sibling is discarded', [[['write', 'a', 'old'], ['merge', 'a', 'b'], ['write', 'b', 'new'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['old'], ['new'], []]), ('stale local sibling is replaced', [[['write', 'a', 'old'], ['merge', 'a', 'b'], ['write', 'a', 'new2'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['new2'], ['new2'], []]), ('same value written concurrently stays twice', [[['write', 'a', 'same'], ['write', 'b', 'same'], ['merge', 'a', 'c'], ['merge', 'b', 'c']], ['a', 'b', 'c']], [['same'], ['same'], ['same', 'same']]), ('overwrite by the same replica', [[['write', 'c', 'c0'], ['write', 'c', 'c1'], ['write', 'c', 'c2'], ['merge', 'c', 'a'], ['write', 'b', 'q'], ['merge', 'b', 'a']], ['a', 'b', 'c']], [['c2', 'q'], ['q'], ['c2']]), ('three-way concurrency then resolve', [[['write', 'a', 'p'], ['write', 'b', 'q'], ['write', 'c', 'r'], ['merge', 'a', 'c'], ['merge', 'b', 'c'], ['write', 'c', 'resolved'], ['merge', 'c', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['resolved'], ['resolved'], ['resolved']]), ('repeat merge after own rewrite', [[['write', 'a', 'x1'], ['merge', 'a', 'b'], ['write', 'a', 'x2'], ['write', 'b', 'y'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['x2', 'y'], ['x2', 'y'], []])],
3: [('concurrent writes become siblings', [[['write', 'a', 'x'], ['write', 'b', 'y3'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b', 'c']], [['x', 'y3'], ['x', 'y3'], []]), ('a write after merge supersedes all siblings', [[['write', 'a', 'x'], ['write', 'b', 'y'], ['merge', 'a', 'b'], ['write', 'b', 'z3'], ['merge', 'b', 'a'], ['merge', 'b', 'c']], ['a', 'b', 'c']], [['z3'], ['z3'], ['z3']]), ('merging identical state keeps the value', [[['write', 'a', 'v3'], ['merge', 'a', 'b'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['v3'], ['v3'], []]), ('stale incoming sibling is discarded', [[['write', 'a', 'old'], ['merge', 'a', 'b'], ['write', 'b', 'new'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['old'], ['new'], []]), ('stale local sibling is replaced', [[['write', 'a', 'old'], ['merge', 'a', 'b'], ['write', 'a', 'new3'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['new3'], ['new3'], []]), ('same value written concurrently stays twice', [[['write', 'a', 'same'], ['write', 'b', 'same'], ['merge', 'a', 'c'], ['merge', 'b', 'c']], ['a', 'b', 'c']], [['same'], ['same'], ['same', 'same']]), ('overwrite by the same replica', [[['write', 'c', 'c0'], ['write', 'c', 'c1'], ['write', 'c', 'c2'], ['write', 'c', 'c3'], ['merge', 'c', 'a'], ['write', 'b', 'q'], ['merge', 'b', 'a']], ['a', 'b', 'c']], [['c3', 'q'], ['q'], ['c3']]), ('three-way concurrency then resolve', [[['write', 'a', 'p'], ['write', 'b', 'q'], ['write', 'c', 'r'], ['merge', 'a', 'c'], ['merge', 'b', 'c'], ['write', 'c', 'resolved'], ['merge', 'c', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['resolved'], ['resolved'], ['resolved']]), ('repeat merge after own rewrite', [[['write', 'a', 'x1'], ['merge', 'a', 'b'], ['write', 'a', 'x2'], ['write', 'b', 'y'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['x2', 'y'], ['x2', 'y'], []])],
4: [('concurrent writes become siblings', [[['write', 'a', 'x'], ['write', 'b', 'y4'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b', 'c']], [['x', 'y4'], ['x', 'y4'], []]), ('a write after merge supersedes all siblings', [[['write', 'a', 'x'], ['write', 'b', 'y'], ['merge', 'a', 'b'], ['write', 'b', 'z4'], ['merge', 'b', 'a'], ['merge', 'b', 'c']], ['a', 'b', 'c']], [['z4'], ['z4'], ['z4']]), ('merging identical state keeps the value', [[['write', 'a', 'v4'], ['merge', 'a', 'b'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['v4'], ['v4'], []]), ('stale incoming sibling is discarded', [[['write', 'a', 'old'], ['merge', 'a', 'b'], ['write', 'b', 'new'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['old'], ['new'], []]), ('stale local sibling is replaced', [[['write', 'a', 'old'], ['merge', 'a', 'b'], ['write', 'a', 'new4'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['new4'], ['new4'], []]), ('same value written concurrently stays twice', [[['write', 'a', 'same'], ['write', 'b', 'same'], ['merge', 'a', 'c'], ['merge', 'b', 'c']], ['a', 'b', 'c']], [['same'], ['same'], ['same', 'same']]), ('overwrite by the same replica', [[['write', 'c', 'c0'], ['write', 'c', 'c1'], ['write', 'c', 'c2'], ['write', 'c', 'c3'], ['write', 'c', 'c4'], ['merge', 'c', 'a'], ['write', 'b', 'q'], ['merge', 'b', 'a']], ['a', 'b', 'c']], [['c4', 'q'], ['q'], ['c4']]), ('three-way concurrency then resolve', [[['write', 'a', 'p'], ['write', 'b', 'q'], ['write', 'c', 'r'], ['merge', 'a', 'c'], ['merge', 'b', 'c'], ['write', 'c', 'resolved'], ['merge', 'c', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['resolved'], ['resolved'], ['resolved']]), ('repeat merge after own rewrite', [[['write', 'a', 'x1'], ['merge', 'a', 'b'], ['write', 'a', 'x2'], ['write', 'b', 'y'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['x2', 'y'], ['x2', 'y'], []])],
5: [('concurrent writes become siblings', [[['write', 'a', 'x'], ['write', 'b', 'y5'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b', 'c']], [['x', 'y5'], ['x', 'y5'], []]), ('a write after merge supersedes all siblings', [[['write', 'a', 'x'], ['write', 'b', 'y'], ['merge', 'a', 'b'], ['write', 'b', 'z5'], ['merge', 'b', 'a'], ['merge', 'b', 'c']], ['a', 'b', 'c']], [['z5'], ['z5'], ['z5']]), ('merging identical state keeps the value', [[['write', 'a', 'v5'], ['merge', 'a', 'b'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['v5'], ['v5'], []]), ('stale incoming sibling is discarded', [[['write', 'a', 'old'], ['merge', 'a', 'b'], ['write', 'b', 'new'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['old'], ['new'], []]), ('stale local sibling is replaced', [[['write', 'a', 'old'], ['merge', 'a', 'b'], ['write', 'a', 'new5'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['new5'], ['new5'], []]), ('same value written concurrently stays twice', [[['write', 'a', 'same'], ['write', 'b', 'same'], ['merge', 'a', 'c'], ['merge', 'b', 'c']], ['a', 'b', 'c']], [['same'], ['same'], ['same', 'same']]), ('overwrite by the same replica', [[['write', 'c', 'c0'], ['write', 'c', 'c1'], ['write', 'c', 'c2'], ['write', 'c', 'c3'], ['write', 'c', 'c4'], ['write', 'c', 'c5'], ['merge', 'c', 'a'], ['write', 'b', 'q'], ['merge', 'b', 'a']], ['a', 'b', 'c']], [['c5', 'q'], ['q'], ['c5']]), ('three-way concurrency then resolve', [[['write', 'a', 'p'], ['write', 'b', 'q'], ['write', 'c', 'r'], ['merge', 'a', 'c'], ['merge', 'b', 'c'], ['write', 'c', 'resolved'], ['merge', 'c', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['resolved'], ['resolved'], ['resolved']]), ('repeat merge after own rewrite', [[['write', 'a', 'x1'], ['merge', 'a', 'b'], ['write', 'a', 'x2'], ['write', 'b', 'y'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['x2', 'y'], ['x2', 'y'], []])],
}[N]
for label, args, expected in cases:
check(label, solve(*args), expected)
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)
| Boundary fixture | Actual | Expected | Outcome |
|---|---|---|---|
| concurrent writes become siblings | [['x', 'y1'], ['x', 'y1'], []] | [['x', 'y1'], ['x', 'y1'], []] | Passed |
| a write after merge supersedes all siblings | [['x', 'z1'], ['z1'], ['z1']] | [['z1'], ['z1'], ['z1']] | Failed |
| merging identical state keeps the value | [['v1'], ['v1'], []] | [['v1'], ['v1'], []] | Passed |
| stale incoming sibling is discarded | [['old'], ['new', 'old'], []] | [['old'], ['new'], []] | Failed |
| stale local sibling is replaced | [['new1'], ['new1'], []] | [['new1'], ['new1'], []] | Passed |
| same value written concurrently stays twice | [['same'], ['same'], ['same', 'same']] | [['same'], ['same'], ['same', 'same']] | Passed |
| overwrite by the same replica | [['c1', 'q'], ['q'], ['c1']] | [['c1', 'q'], ['q'], ['c1']] | Passed |
| three-way concurrency then resolve | [['p', 'resolved'], ['p', 'q', 'resolved'], ['resolved']] | [['resolved'], ['resolved'], ['resolved']] | Failed |
| repeat merge after own rewrite | [['x2', 'y'], ['x2', 'y'], []] | [['x2', 'y'], ['x2', 'y'], []] | Passed |
SHA-256 / 0ba6cd60687de83d6fa8bc08d6d068d15741c22567e424617ea880a83e5efb35
3 / The verified repair
Exit 0"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(ops, replicas):
sib = {r: [] for r in replicas}
def dominates(x, y):
keys = set(x) | set(y)
return all(x.get(k, 0) >= y.get(k, 0) for k in keys) and x != y
for op in ops:
if op[0] == 'write':
r, v = op[1], op[2]
vv = {}
for _, c in sib[r]:
for k, cnt in c.items():
vv[k] = max(vv.get(k, 0), cnt)
vv[r] = vv.get(r, 0) + 1
sib[r] = [[v, vv]]
else:
s, d = op[1], op[2]
pool = sib[d] + [[v, dict(c)] for v, c in sib[s]]
kept = []
for v, c in pool:
if any(dominates(c2, c) for _, c2 in pool):
continue
if any(c == c3 for _, c3 in kept):
continue
kept.append([v, c])
sib[d] = kept
return [sorted(v for v, _ in sib[r]) for r in replicas]
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = {
1: [('concurrent writes become siblings', [[['write', 'a', 'x'], ['write', 'b', 'y1'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b', 'c']], [['x', 'y1'], ['x', 'y1'], []]), ('a write after merge supersedes all siblings', [[['write', 'a', 'x'], ['write', 'b', 'y'], ['merge', 'a', 'b'], ['write', 'b', 'z1'], ['merge', 'b', 'a'], ['merge', 'b', 'c']], ['a', 'b', 'c']], [['z1'], ['z1'], ['z1']]), ('merging identical state keeps the value', [[['write', 'a', 'v1'], ['merge', 'a', 'b'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['v1'], ['v1'], []]), ('stale incoming sibling is discarded', [[['write', 'a', 'old'], ['merge', 'a', 'b'], ['write', 'b', 'new'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['old'], ['new'], []]), ('stale local sibling is replaced', [[['write', 'a', 'old'], ['merge', 'a', 'b'], ['write', 'a', 'new1'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['new1'], ['new1'], []]), ('same value written concurrently stays twice', [[['write', 'a', 'same'], ['write', 'b', 'same'], ['merge', 'a', 'c'], ['merge', 'b', 'c']], ['a', 'b', 'c']], [['same'], ['same'], ['same', 'same']]), ('overwrite by the same replica', [[['write', 'c', 'c0'], ['write', 'c', 'c1'], ['merge', 'c', 'a'], ['write', 'b', 'q'], ['merge', 'b', 'a']], ['a', 'b', 'c']], [['c1', 'q'], ['q'], ['c1']]), ('three-way concurrency then resolve', [[['write', 'a', 'p'], ['write', 'b', 'q'], ['write', 'c', 'r'], ['merge', 'a', 'c'], ['merge', 'b', 'c'], ['write', 'c', 'resolved'], ['merge', 'c', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['resolved'], ['resolved'], ['resolved']]), ('repeat merge after own rewrite', [[['write', 'a', 'x1'], ['merge', 'a', 'b'], ['write', 'a', 'x2'], ['write', 'b', 'y'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['x2', 'y'], ['x2', 'y'], []])],
2: [('concurrent writes become siblings', [[['write', 'a', 'x'], ['write', 'b', 'y2'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b', 'c']], [['x', 'y2'], ['x', 'y2'], []]), ('a write after merge supersedes all siblings', [[['write', 'a', 'x'], ['write', 'b', 'y'], ['merge', 'a', 'b'], ['write', 'b', 'z2'], ['merge', 'b', 'a'], ['merge', 'b', 'c']], ['a', 'b', 'c']], [['z2'], ['z2'], ['z2']]), ('merging identical state keeps the value', [[['write', 'a', 'v2'], ['merge', 'a', 'b'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['v2'], ['v2'], []]), ('stale incoming sibling is discarded', [[['write', 'a', 'old'], ['merge', 'a', 'b'], ['write', 'b', 'new'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['old'], ['new'], []]), ('stale local sibling is replaced', [[['write', 'a', 'old'], ['merge', 'a', 'b'], ['write', 'a', 'new2'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['new2'], ['new2'], []]), ('same value written concurrently stays twice', [[['write', 'a', 'same'], ['write', 'b', 'same'], ['merge', 'a', 'c'], ['merge', 'b', 'c']], ['a', 'b', 'c']], [['same'], ['same'], ['same', 'same']]), ('overwrite by the same replica', [[['write', 'c', 'c0'], ['write', 'c', 'c1'], ['write', 'c', 'c2'], ['merge', 'c', 'a'], ['write', 'b', 'q'], ['merge', 'b', 'a']], ['a', 'b', 'c']], [['c2', 'q'], ['q'], ['c2']]), ('three-way concurrency then resolve', [[['write', 'a', 'p'], ['write', 'b', 'q'], ['write', 'c', 'r'], ['merge', 'a', 'c'], ['merge', 'b', 'c'], ['write', 'c', 'resolved'], ['merge', 'c', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['resolved'], ['resolved'], ['resolved']]), ('repeat merge after own rewrite', [[['write', 'a', 'x1'], ['merge', 'a', 'b'], ['write', 'a', 'x2'], ['write', 'b', 'y'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['x2', 'y'], ['x2', 'y'], []])],
3: [('concurrent writes become siblings', [[['write', 'a', 'x'], ['write', 'b', 'y3'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b', 'c']], [['x', 'y3'], ['x', 'y3'], []]), ('a write after merge supersedes all siblings', [[['write', 'a', 'x'], ['write', 'b', 'y'], ['merge', 'a', 'b'], ['write', 'b', 'z3'], ['merge', 'b', 'a'], ['merge', 'b', 'c']], ['a', 'b', 'c']], [['z3'], ['z3'], ['z3']]), ('merging identical state keeps the value', [[['write', 'a', 'v3'], ['merge', 'a', 'b'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['v3'], ['v3'], []]), ('stale incoming sibling is discarded', [[['write', 'a', 'old'], ['merge', 'a', 'b'], ['write', 'b', 'new'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['old'], ['new'], []]), ('stale local sibling is replaced', [[['write', 'a', 'old'], ['merge', 'a', 'b'], ['write', 'a', 'new3'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['new3'], ['new3'], []]), ('same value written concurrently stays twice', [[['write', 'a', 'same'], ['write', 'b', 'same'], ['merge', 'a', 'c'], ['merge', 'b', 'c']], ['a', 'b', 'c']], [['same'], ['same'], ['same', 'same']]), ('overwrite by the same replica', [[['write', 'c', 'c0'], ['write', 'c', 'c1'], ['write', 'c', 'c2'], ['write', 'c', 'c3'], ['merge', 'c', 'a'], ['write', 'b', 'q'], ['merge', 'b', 'a']], ['a', 'b', 'c']], [['c3', 'q'], ['q'], ['c3']]), ('three-way concurrency then resolve', [[['write', 'a', 'p'], ['write', 'b', 'q'], ['write', 'c', 'r'], ['merge', 'a', 'c'], ['merge', 'b', 'c'], ['write', 'c', 'resolved'], ['merge', 'c', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['resolved'], ['resolved'], ['resolved']]), ('repeat merge after own rewrite', [[['write', 'a', 'x1'], ['merge', 'a', 'b'], ['write', 'a', 'x2'], ['write', 'b', 'y'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['x2', 'y'], ['x2', 'y'], []])],
4: [('concurrent writes become siblings', [[['write', 'a', 'x'], ['write', 'b', 'y4'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b', 'c']], [['x', 'y4'], ['x', 'y4'], []]), ('a write after merge supersedes all siblings', [[['write', 'a', 'x'], ['write', 'b', 'y'], ['merge', 'a', 'b'], ['write', 'b', 'z4'], ['merge', 'b', 'a'], ['merge', 'b', 'c']], ['a', 'b', 'c']], [['z4'], ['z4'], ['z4']]), ('merging identical state keeps the value', [[['write', 'a', 'v4'], ['merge', 'a', 'b'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['v4'], ['v4'], []]), ('stale incoming sibling is discarded', [[['write', 'a', 'old'], ['merge', 'a', 'b'], ['write', 'b', 'new'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['old'], ['new'], []]), ('stale local sibling is replaced', [[['write', 'a', 'old'], ['merge', 'a', 'b'], ['write', 'a', 'new4'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['new4'], ['new4'], []]), ('same value written concurrently stays twice', [[['write', 'a', 'same'], ['write', 'b', 'same'], ['merge', 'a', 'c'], ['merge', 'b', 'c']], ['a', 'b', 'c']], [['same'], ['same'], ['same', 'same']]), ('overwrite by the same replica', [[['write', 'c', 'c0'], ['write', 'c', 'c1'], ['write', 'c', 'c2'], ['write', 'c', 'c3'], ['write', 'c', 'c4'], ['merge', 'c', 'a'], ['write', 'b', 'q'], ['merge', 'b', 'a']], ['a', 'b', 'c']], [['c4', 'q'], ['q'], ['c4']]), ('three-way concurrency then resolve', [[['write', 'a', 'p'], ['write', 'b', 'q'], ['write', 'c', 'r'], ['merge', 'a', 'c'], ['merge', 'b', 'c'], ['write', 'c', 'resolved'], ['merge', 'c', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['resolved'], ['resolved'], ['resolved']]), ('repeat merge after own rewrite', [[['write', 'a', 'x1'], ['merge', 'a', 'b'], ['write', 'a', 'x2'], ['write', 'b', 'y'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['x2', 'y'], ['x2', 'y'], []])],
5: [('concurrent writes become siblings', [[['write', 'a', 'x'], ['write', 'b', 'y5'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b', 'c']], [['x', 'y5'], ['x', 'y5'], []]), ('a write after merge supersedes all siblings', [[['write', 'a', 'x'], ['write', 'b', 'y'], ['merge', 'a', 'b'], ['write', 'b', 'z5'], ['merge', 'b', 'a'], ['merge', 'b', 'c']], ['a', 'b', 'c']], [['z5'], ['z5'], ['z5']]), ('merging identical state keeps the value', [[['write', 'a', 'v5'], ['merge', 'a', 'b'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['v5'], ['v5'], []]), ('stale incoming sibling is discarded', [[['write', 'a', 'old'], ['merge', 'a', 'b'], ['write', 'b', 'new'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['old'], ['new'], []]), ('stale local sibling is replaced', [[['write', 'a', 'old'], ['merge', 'a', 'b'], ['write', 'a', 'new5'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['new5'], ['new5'], []]), ('same value written concurrently stays twice', [[['write', 'a', 'same'], ['write', 'b', 'same'], ['merge', 'a', 'c'], ['merge', 'b', 'c']], ['a', 'b', 'c']], [['same'], ['same'], ['same', 'same']]), ('overwrite by the same replica', [[['write', 'c', 'c0'], ['write', 'c', 'c1'], ['write', 'c', 'c2'], ['write', 'c', 'c3'], ['write', 'c', 'c4'], ['write', 'c', 'c5'], ['merge', 'c', 'a'], ['write', 'b', 'q'], ['merge', 'b', 'a']], ['a', 'b', 'c']], [['c5', 'q'], ['q'], ['c5']]), ('three-way concurrency then resolve', [[['write', 'a', 'p'], ['write', 'b', 'q'], ['write', 'c', 'r'], ['merge', 'a', 'c'], ['merge', 'b', 'c'], ['write', 'c', 'resolved'], ['merge', 'c', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['resolved'], ['resolved'], ['resolved']]), ('repeat merge after own rewrite', [[['write', 'a', 'x1'], ['merge', 'a', 'b'], ['write', 'a', 'x2'], ['write', 'b', 'y'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b', 'c']], [['x2', 'y'], ['x2', 'y'], []])],
}[N]
for label, args, expected in cases:
check(label, solve(*args), expected)
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)
| Boundary fixture | Actual | Expected | Outcome |
|---|---|---|---|
| concurrent writes become siblings | [['x', 'y1'], ['x', 'y1'], []] | [['x', 'y1'], ['x', 'y1'], []] | Passed |
| a write after merge supersedes all siblings | [['z1'], ['z1'], ['z1']] | [['z1'], ['z1'], ['z1']] | Passed |
| merging identical state keeps the value | [['v1'], ['v1'], []] | [['v1'], ['v1'], []] | Passed |
| stale incoming sibling is discarded | [['old'], ['new'], []] | [['old'], ['new'], []] | Passed |
| stale local sibling is replaced | [['new1'], ['new1'], []] | [['new1'], ['new1'], []] | Passed |
| same value written concurrently stays twice | [['same'], ['same'], ['same', 'same']] | [['same'], ['same'], ['same', 'same']] | Passed |
| overwrite by the same replica | [['c1', 'q'], ['q'], ['c1']] | [['c1', 'q'], ['q'], ['c1']] | Passed |
| three-way concurrency then resolve | [['resolved'], ['resolved'], ['resolved']] | [['resolved'], ['resolved'], ['resolved']] | Passed |
| repeat merge after own rewrite | [['x2', 'y'], ['x2', 'y'], []] | [['x2', 'y'], ['x2', 'y'], []] | Passed |
SHA-256 / 7b04ca5bdbd1af01833a51f4f0795c0adbbc35b5be5ef9ee3d1687e5a69bc832
Verification & scope
A deterministic, bounded teaching model of one replicated data type with stipulated operation and merge rules; it is not a production CRDT library and makes no claim of conformance to any specific published design. This reproducer isolates one failure mechanism. Results cover the supplied fixtures. Variants within a family share a test contract and should remain grouped when constructing evaluation splits. Related mechanisms with a shared evaluation_group must also remain together; these controlled models are not independent production incidents.
Observations recorded using Python 3.12.14 at 2026-09-29T14:49:01.618695+00:00.
Case digest / 73d1fbd21cf128324dcd1dab0d21bed801096aadb6fce4d0f72958c1b345b9a2