FA-056 / Distributed coordination / Open access
A stale renewal extends a later incarnation of a lease · case 01
A delayed renewal is accepted after the same worker name has reacquired the lease.
ROOT CAUSE
Owner-name equality is mistaken for ownership of a particular acquisition generation.
VERIFIED REPAIR
Renew only when owner and generation match and the existing lease has not expired.
Unsuccessful approach: Checking owner and expiration still accepts a stale request from a previous acquisition by that owner.
Case contract
A lease is [owner,generation,deadline]. A renewal names [owner,generation], now and nonnegative duration. If ownership matches and now < deadline, return a new deadline now+duration; otherwise return the unchanged lease. This models an atomic compare-and-swap at one authoritative clock.
Why this case matters
Models lease ABA during worker restarts and delayed network deliveries without assuming synchronized client clocks or implementing a complete distributed lease protocol.
1 / The failure
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(lease, request, now, duration):
return [lease[0], lease[1], now+duration] if request[0] == lease[0] else list(lease)
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
lease = ['worker', N+1, 100+N]
check('previous incarnation renewal', solve(lease, ['worker', N], 90, 30), lease)
check('current incarnation renewal', solve(lease, ['worker', N+1], 90, N+20), ['worker', N+1, 110+N])
check('deadline already reached', solve(lease, ['worker', N+1], 100+N, 30), lease)
check('different owner', solve(lease, ['other', N+1], 90, 30), lease)
check('future generation is not ownership', solve(lease, ['worker', N+2], 90, 30), lease)
check('explicit zero extension', solve(lease, ['worker', N+1], 90, 0), ['worker', N+1, 90])
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 |
|---|---|---|---|
| previous incarnation renewal | ['worker', 2, 120] | ['worker', 2, 101] | Failed |
| current incarnation renewal | ['worker', 2, 111] | ['worker', 2, 111] | Passed |
| deadline already reached | ['worker', 2, 131] | ['worker', 2, 101] | Failed |
| different owner | ['worker', 2, 101] | ['worker', 2, 101] | Passed |
| future generation is not ownership | ['worker', 2, 120] | ['worker', 2, 101] | Failed |
| explicit zero extension | ['worker', 2, 90] | ['worker', 2, 90] | Passed |
SHA-256 / 932dd9c994d764a203d4c6a5be82e64b8022ce17679e54da4ba106e5e3277bd9
2 / The unsuccessful fix
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(lease, request, now, duration):
return [lease[0], lease[1], now+duration] if request[0] == lease[0] and now < lease[2] else list(lease)
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
lease = ['worker', N+1, 100+N]
check('previous incarnation renewal', solve(lease, ['worker', N], 90, 30), lease)
check('current incarnation renewal', solve(lease, ['worker', N+1], 90, N+20), ['worker', N+1, 110+N])
check('deadline already reached', solve(lease, ['worker', N+1], 100+N, 30), lease)
check('different owner', solve(lease, ['other', N+1], 90, 30), lease)
check('future generation is not ownership', solve(lease, ['worker', N+2], 90, 30), lease)
check('explicit zero extension', solve(lease, ['worker', N+1], 90, 0), ['worker', N+1, 90])
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 |
|---|---|---|---|
| previous incarnation renewal | ['worker', 2, 120] | ['worker', 2, 101] | Failed |
| current incarnation renewal | ['worker', 2, 111] | ['worker', 2, 111] | Passed |
| deadline already reached | ['worker', 2, 101] | ['worker', 2, 101] | Passed |
| different owner | ['worker', 2, 101] | ['worker', 2, 101] | Passed |
| future generation is not ownership | ['worker', 2, 120] | ['worker', 2, 101] | Failed |
| explicit zero extension | ['worker', 2, 90] | ['worker', 2, 90] | Passed |
SHA-256 / ee8d78524f9df26db0de0b4c6b6abe721c37165bcabd11a213e135946d5db955
3 / The verified repair
Exit 0"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(lease, request, now, duration):
return [lease[0], lease[1], now+duration] if request == lease[:2] and now < lease[2] else list(lease)
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
lease = ['worker', N+1, 100+N]
check('previous incarnation renewal', solve(lease, ['worker', N], 90, 30), lease)
check('current incarnation renewal', solve(lease, ['worker', N+1], 90, N+20), ['worker', N+1, 110+N])
check('deadline already reached', solve(lease, ['worker', N+1], 100+N, 30), lease)
check('different owner', solve(lease, ['other', N+1], 90, 30), lease)
check('future generation is not ownership', solve(lease, ['worker', N+2], 90, 30), lease)
check('explicit zero extension', solve(lease, ['worker', N+1], 90, 0), ['worker', N+1, 90])
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 |
|---|---|---|---|
| previous incarnation renewal | ['worker', 2, 101] | ['worker', 2, 101] | Passed |
| current incarnation renewal | ['worker', 2, 111] | ['worker', 2, 111] | Passed |
| deadline already reached | ['worker', 2, 101] | ['worker', 2, 101] | Passed |
| different owner | ['worker', 2, 101] | ['worker', 2, 101] | Passed |
| future generation is not ownership | ['worker', 2, 101] | ['worker', 2, 101] | Passed |
| explicit zero extension | ['worker', 2, 90] | ['worker', 2, 90] | Passed |
SHA-256 / 60a920a3061013eddeb9ba39a731892fefb38c9c4b93218850c74d1de6d2d08c
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.889697+00:00.
Case digest / 9be317b3f1124ad1133df32d89092ee44ed30d0fa8e0ee3804cd8f08909d3574