{"abstract":"A delayed renewal is accepted after the same worker name has reacquired the lease.","category":"Distributed coordination","checks":6,"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.","evaluation_group":"model-32fcdd36da6b322c","failed_approach":"Checking owner and expiration still accepts a stale request from a previous acquisition by that owner.","family":"dist-lease-renewal-aba","id":"FA-056","implementations":{"attempt":{"sha256":"ee8d78524f9df26db0de0b4c6b6abe721c37165bcabd11a213e135946d5db955","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(lease, request, now, duration):\n    return [lease[0], lease[1], now+duration] if request[0] == lease[0] and now < lease[2] else list(lease)\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nlease = ['worker', N+1, 100+N]\ncheck('previous incarnation renewal', solve(lease, ['worker', N], 90, 30), lease)\ncheck('current incarnation renewal', solve(lease, ['worker', N+1], 90, N+20), ['worker', N+1, 110+N])\ncheck('deadline already reached', solve(lease, ['worker', N+1], 100+N, 30), lease)\ncheck('different owner', solve(lease, ['other', N+1], 90, 30), lease)\ncheck('future generation is not ownership', solve(lease, ['worker', N+2], 90, 30), lease)\ncheck('explicit zero extension', solve(lease, ['worker', N+1], 90, 0), ['worker', N+1, 90])\nprint(json.dumps({\"observations\": observations, \"passed\": all(x[\"passed\"] for x in observations)}, ensure_ascii=False))\nraise SystemExit(0 if all(x[\"passed\"] for x in observations) else 1)\n"},"broken":{"sha256":"932dd9c994d764a203d4c6a5be82e64b8022ce17679e54da4ba106e5e3277bd9","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(lease, request, now, duration):\n    return [lease[0], lease[1], now+duration] if request[0] == lease[0] else list(lease)\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nlease = ['worker', N+1, 100+N]\ncheck('previous incarnation renewal', solve(lease, ['worker', N], 90, 30), lease)\ncheck('current incarnation renewal', solve(lease, ['worker', N+1], 90, N+20), ['worker', N+1, 110+N])\ncheck('deadline already reached', solve(lease, ['worker', N+1], 100+N, 30), lease)\ncheck('different owner', solve(lease, ['other', N+1], 90, 30), lease)\ncheck('future generation is not ownership', solve(lease, ['worker', N+2], 90, 30), lease)\ncheck('explicit zero extension', solve(lease, ['worker', N+1], 90, 0), ['worker', N+1, 90])\nprint(json.dumps({\"observations\": observations, \"passed\": all(x[\"passed\"] for x in observations)}, ensure_ascii=False))\nraise SystemExit(0 if all(x[\"passed\"] for x in observations) else 1)\n"},"fixed":{"sha256":"60a920a3061013eddeb9ba39a731892fefb38c9c4b93218850c74d1de6d2d08c","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(lease, request, now, duration):\n    return [lease[0], lease[1], now+duration] if request == lease[:2] and now < lease[2] else list(lease)\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nlease = ['worker', N+1, 100+N]\ncheck('previous incarnation renewal', solve(lease, ['worker', N], 90, 30), lease)\ncheck('current incarnation renewal', solve(lease, ['worker', N+1], 90, N+20), ['worker', N+1, 110+N])\ncheck('deadline already reached', solve(lease, ['worker', N+1], 100+N, 30), lease)\ncheck('different owner', solve(lease, ['other', N+1], 90, 30), lease)\ncheck('future generation is not ownership', solve(lease, ['worker', N+2], 90, 30), lease)\ncheck('explicit zero extension', solve(lease, ['worker', N+1], 90, 0), ['worker', N+1, 90])\nprint(json.dumps({\"observations\": observations, \"passed\": all(x[\"passed\"] for x in observations)}, ensure_ascii=False))\nraise SystemExit(0 if all(x[\"passed\"] for x in observations) else 1)\n"}},"limitations":" 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.","method":"Deterministic executable model with adversarial boundary fixtures.","provenance":{"created_by":"Failure Map","dependencies":"Python standard library","family":"dist-lease-renewal-aba","generated_at":"2026-09-29T14:36:49.889697+00:00","license":"CC0-1.0","python":"3.12.14","seed":1,"split":"open-access"},"relevance":"Models lease ABA during worker restarts and delayed network deliveries without assuming synchronized client clocks or implementing a complete distributed lease protocol.","repair":"Renew only when owner and generation match and the existing lease has not expired.","root_cause":"Owner-name equality is mistaken for ownership of a particular acquisition generation.","sha256":"9be317b3f1124ad1133df32d89092ee44ed30d0fa8e0ee3804cd8f08909d3574","title":"A stale renewal extends a later incarnation of a lease · case 01","variant":1,"variant_policy":"Five numbered records share a model and may reuse boundary fixtures.","verification":{"attempt":{"elapsed_ms":32.358,"exit_code":1,"observations":[{"actual":["worker",2,120],"check":"previous incarnation renewal","expected":["worker",2,101],"passed":false},{"actual":["worker",2,111],"check":"current incarnation renewal","expected":["worker",2,111],"passed":true},{"actual":["worker",2,101],"check":"deadline already reached","expected":["worker",2,101],"passed":true},{"actual":["worker",2,101],"check":"different owner","expected":["worker",2,101],"passed":true},{"actual":["worker",2,120],"check":"future generation is not ownership","expected":["worker",2,101],"passed":false},{"actual":["worker",2,90],"check":"explicit zero extension","expected":["worker",2,90],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"previous incarnation renewal\", \"actual\": [\"worker\", 2, 120], \"expected\": [\"worker\", 2, 101], \"passed\": false}, {\"check\": \"current incarnation renewal\", \"actual\": [\"worker\", 2, 111], \"expected\": [\"worker\", 2, 111], \"passed\": true}, {\"check\": \"deadline already reached\", \"actual\": [\"worker\", 2, 101], \"expected\": [\"worker\", 2, 101], \"passed\": true}, {\"check\": \"different owner\", \"actual\": [\"worker\", 2, 101], \"expected\": [\"worker\", 2, 101], \"passed\": true}, {\"check\": \"future generation is not ownership\", \"actual\": [\"worker\", 2, 120], \"expected\": [\"worker\", 2, 101], \"passed\": false}, {\"check\": \"explicit zero extension\", \"actual\": [\"worker\", 2, 90], \"expected\": [\"worker\", 2, 90], \"passed\": true}], \"passed\": false}\n"},"broken":{"elapsed_ms":36.442,"exit_code":1,"observations":[{"actual":["worker",2,120],"check":"previous incarnation renewal","expected":["worker",2,101],"passed":false},{"actual":["worker",2,111],"check":"current incarnation renewal","expected":["worker",2,111],"passed":true},{"actual":["worker",2,131],"check":"deadline already reached","expected":["worker",2,101],"passed":false},{"actual":["worker",2,101],"check":"different owner","expected":["worker",2,101],"passed":true},{"actual":["worker",2,120],"check":"future generation is not ownership","expected":["worker",2,101],"passed":false},{"actual":["worker",2,90],"check":"explicit zero extension","expected":["worker",2,90],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"previous incarnation renewal\", \"actual\": [\"worker\", 2, 120], \"expected\": [\"worker\", 2, 101], \"passed\": false}, {\"check\": \"current incarnation renewal\", \"actual\": [\"worker\", 2, 111], \"expected\": [\"worker\", 2, 111], \"passed\": true}, {\"check\": \"deadline already reached\", \"actual\": [\"worker\", 2, 131], \"expected\": [\"worker\", 2, 101], \"passed\": false}, {\"check\": \"different owner\", \"actual\": [\"worker\", 2, 101], \"expected\": [\"worker\", 2, 101], \"passed\": true}, {\"check\": \"future generation is not ownership\", \"actual\": [\"worker\", 2, 120], \"expected\": [\"worker\", 2, 101], \"passed\": false}, {\"check\": \"explicit zero extension\", \"actual\": [\"worker\", 2, 90], \"expected\": [\"worker\", 2, 90], \"passed\": true}], \"passed\": false}\n"},"fixed":{"elapsed_ms":33.814,"exit_code":0,"observations":[{"actual":["worker",2,101],"check":"previous incarnation renewal","expected":["worker",2,101],"passed":true},{"actual":["worker",2,111],"check":"current incarnation renewal","expected":["worker",2,111],"passed":true},{"actual":["worker",2,101],"check":"deadline already reached","expected":["worker",2,101],"passed":true},{"actual":["worker",2,101],"check":"different owner","expected":["worker",2,101],"passed":true},{"actual":["worker",2,101],"check":"future generation is not ownership","expected":["worker",2,101],"passed":true},{"actual":["worker",2,90],"check":"explicit zero extension","expected":["worker",2,90],"passed":true}],"passed":true,"stderr":"","stdout":"{\"observations\": [{\"check\": \"previous incarnation renewal\", \"actual\": [\"worker\", 2, 101], \"expected\": [\"worker\", 2, 101], \"passed\": true}, {\"check\": \"current incarnation renewal\", \"actual\": [\"worker\", 2, 111], \"expected\": [\"worker\", 2, 111], \"passed\": true}, {\"check\": \"deadline already reached\", \"actual\": [\"worker\", 2, 101], \"expected\": [\"worker\", 2, 101], \"passed\": true}, {\"check\": \"different owner\", \"actual\": [\"worker\", 2, 101], \"expected\": [\"worker\", 2, 101], \"passed\": true}, {\"check\": \"future generation is not ownership\", \"actual\": [\"worker\", 2, 101], \"expected\": [\"worker\", 2, 101], \"passed\": true}, {\"check\": \"explicit zero extension\", \"actual\": [\"worker\", 2, 90], \"expected\": [\"worker\", 2, 90], \"passed\": true}], \"passed\": true}\n"}},"verified":true,"visibility":"public"}