FA-74966 / CRDT convergence / Open access
Multi-value register: repeated writes by one replica reuse the same counter · case 01
A replica's second write carries the same vector as its first and loses against the stale value.
ROOT CAUSE
The writer's entry is reset to one on every write instead of being incremented.
VERIFIED REPAIR
Increment the writer's entry from the merged context on every write.
Unsuccessful approach: Setting the entry only when absent still reuses the old counter for every later write.
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]:
for k, cnt in c.items():
vv[k] = max(vv.get(k, 0), cnt)
vv[r] = 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'], ['old'], []] | [['new1'], ['new1'], []] | Failed |
| 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 | [['y'], ['y'], []] | [['x2', 'y'], ['x2', 'y'], []] | Failed |
SHA-256 / f70815f5301ebab55481c809640d3cf32e7e2c03a09b207b28b137d41064b011
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():
vv[k] = max(vv.get(k, 0), cnt)
vv.setdefault(r, 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'], ['old'], []] | [['new1'], ['new1'], []] | Failed |
| 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 | [['y'], ['y'], []] | [['x2', 'y'], ['x2', 'y'], []] | Failed |
SHA-256 / a8d11648cc3027d80b3ca8ff1535f64c390582ba2a7cbaf7c5c491161c8d3a63
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.626502+00:00.
Case digest / 27a7def0c7d6e22296782031b22b67fbcc5092035e416da20f6901891b6f6beb