FA-051 / Distributed coordination / Open access

A revoked writer overwrites its successor's state · case 01

An old lease holder writes after a higher fencing epoch has already committed.

Verified by executionVariant 1 · 6 checks per implementationDownload source bundle ↓JSON ↗

ROOT CAUSE

The protected resource does not enforce the largest fencing token it has observed.

VERIFIED REPAIR

Reject epochs below the resource's stored epoch; allow subsequent writes within its current epoch.

Unsuccessful approach: Requiring a strictly newer epoch for every write blocks valid updates by the current holder.

Case contract

Process [epoch,value] writes in arrival order. Accept epochs >= the stored epoch and return [largest accepted epoch,last accepted value]. Tokens are nonnegative and uniquely allocated per lease.

Why this case matters

Models storage-side fencing after delayed writes outlive a coordinator lease; lease expiry alone cannot stop a paused former holder from sending a request.

1 / The failure

Exit 1

"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(epoch, value, writes):
    for next_epoch, next_value in writes:
        epoch, value = next_epoch, next_value
    return [epoch, value]
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
e = 10*N
check('late revoked writer', solve(e, 'current', [[e-1, 'stale']]), [e, 'current'])
check('same holder writes twice', solve(e, 'a', [[e, 'b'], [e, 'c']]), [e, 'c'])
check('new holder then old arrival', solve(e, 'a', [[e+1, 'new'], [e, 'old']]), [e+1, 'new'])
check('multiple handoffs', solve(e, 'a', [[e+2, 'b'], [e+1, 'c'], [e+3, 'd']]), [e+3, 'd'])
check('idle resource', solve(e, 'kept', []), [e, 'kept'])
check('initial epoch may be zero', solve(0, None, [[0, N]]), [0, N])
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
late revoked writer	`[9, 'stale']`	`[10, 'current']`	Failed
same holder writes twice	`[10, 'c']`	`[10, 'c']`	Passed
new holder then old arrival	`[10, 'old']`	`[11, 'new']`	Failed
multiple handoffs	`[13, 'd']`	`[13, 'd']`	Passed
idle resource	`[10, 'kept']`	`[10, 'kept']`	Passed
initial epoch may be zero	`[0, 1]`	`[0, 1]`	Passed

SHA-256 / ba98821e37640d0bdc96d8f3d700e68edcaba8b53e319f6e580bbae41e017e9d

2 / The unsuccessful fix

Exit 1

"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(epoch, value, writes):
    for next_epoch, next_value in writes:
        if next_epoch > epoch:
            epoch, value = next_epoch, next_value
    return [epoch, value]
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
e = 10*N
check('late revoked writer', solve(e, 'current', [[e-1, 'stale']]), [e, 'current'])
check('same holder writes twice', solve(e, 'a', [[e, 'b'], [e, 'c']]), [e, 'c'])
check('new holder then old arrival', solve(e, 'a', [[e+1, 'new'], [e, 'old']]), [e+1, 'new'])
check('multiple handoffs', solve(e, 'a', [[e+2, 'b'], [e+1, 'c'], [e+3, 'd']]), [e+3, 'd'])
check('idle resource', solve(e, 'kept', []), [e, 'kept'])
check('initial epoch may be zero', solve(0, None, [[0, N]]), [0, N])
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
late revoked writer	`[10, 'current']`	`[10, 'current']`	Passed
same holder writes twice	`[10, 'a']`	`[10, 'c']`	Failed
new holder then old arrival	`[11, 'new']`	`[11, 'new']`	Passed
multiple handoffs	`[13, 'd']`	`[13, 'd']`	Passed
idle resource	`[10, 'kept']`	`[10, 'kept']`	Passed
initial epoch may be zero	`[0, None]`	`[0, 1]`	Failed

SHA-256 / b94903bcf619d24c2932523e45a8224b332b1c647a82db5a069801a0fe473076

3 / The verified repair

Exit 0

"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(epoch, value, writes):
    for next_epoch, next_value in writes:
        if next_epoch >= epoch:
            epoch, value = next_epoch, next_value
    return [epoch, value]
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
e = 10*N
check('late revoked writer', solve(e, 'current', [[e-1, 'stale']]), [e, 'current'])
check('same holder writes twice', solve(e, 'a', [[e, 'b'], [e, 'c']]), [e, 'c'])
check('new holder then old arrival', solve(e, 'a', [[e+1, 'new'], [e, 'old']]), [e+1, 'new'])
check('multiple handoffs', solve(e, 'a', [[e+2, 'b'], [e+1, 'c'], [e+3, 'd']]), [e+3, 'd'])
check('idle resource', solve(e, 'kept', []), [e, 'kept'])
check('initial epoch may be zero', solve(0, None, [[0, N]]), [0, N])
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
late revoked writer	`[10, 'current']`	`[10, 'current']`	Passed
same holder writes twice	`[10, 'c']`	`[10, 'c']`	Passed
new holder then old arrival	`[11, 'new']`	`[11, 'new']`	Passed
multiple handoffs	`[13, 'd']`	`[13, 'd']`	Passed
idle resource	`[10, 'kept']`	`[10, 'kept']`	Passed
initial epoch may be zero	`[0, 1]`	`[0, 1]`	Passed

SHA-256 / f68612fa52804bd028a2e13a381a71d25aaa02259e76ed46765b828b1839158a

Verification & scope

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:36:49.883418+00:00.

Case digest / d494bdf725c04e518bedda59735f4657dbcf208fc3e8324c78a48bb3e3c2924c