{"abstract":"The same slot becomes available while a later borrower still owns it.","category":"Runtime and resources","checks":7,"contract":"A pool starts with size free numbered slots. Get chooses the smallest free slot and increments its generation, or emits None if exhausted. Put [slot,generation] releases only that active handle. Return [issued handles,sorted free slots,sorted active handles]. Generations never wrap in this model.","evaluation_group":"model-57b4fc0aa4ff7abb","failed_approach":"Rejecting returns for idle slots handles immediate double returns but misses stale returns after slot reuse.","family":"runtime-pool-handle-generation","id":"FA-281","implementations":{"attempt":{"sha256":"f29018f7f62bb49befdc6794cfb2671521d35c879e238875e6d67cd035dfe578","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(size, events):\n    free, generations, active, issued = list(range(size)), [0]*size, {}, []\n    for event in events:\n        if event[0] == 'get':\n            if not free:\n                issued.append(None)\n                continue\n            free.sort()\n            slot = free.pop(0)\n            generations[slot] += 1\n            active[slot] = generations[slot]\n            issued.append([slot, active[slot]])\n        else:\n            slot, generation = event[1:]\n            if slot in active:\n                active.pop(slot, None)\n                free.append(slot)\n    return [issued, sorted(free), [[slot, active[slot]] for slot in sorted(active)]]\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nprefix = [event for generation in range(1, N+1) for event in [['get'], ['put', 0, generation]]]\ncheck('old handle cannot release new checkout', solve(1, prefix+[['get'], ['put', 0, N], ['get']]), [[[0, g] for g in range(1, N+2)]+[None], [], [[0, N+1]]])\ncheck('return of never-issued handle', solve(1, [['put', 0, 0], ['get'], ['get']]), [[[0, 1], None], [], [[0, 1]]])\ncheck('valid reuse advances generation', solve(1, [['get'], ['put', 0, 1], ['get']]), [[[0, 1], [0, 2]], [], [[0, 2]]])\ncheck('pool exhaustion is explicit', solve(N, [['get']]*(N+1)), [[[i, 1] for i in range(N)]+[None], [], [[i, 1] for i in range(N)]])\ncheck('zero-sized pool', solve(0, [['get'], ['put', 0, 1]]), [[None], [], []])\ncheck('out-of-range return ignored', solve(N, [['put', N+1, 1]]), [[], list(range(N)), []])\ncheck('no pool activity', solve(N, []), [[], list(range(N)), []])\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":"f9cadb225437ca8b4b5b93e29733e581c6ffc0f441c19155633b61244a7fb1e3","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(size, events):\n    free, generations, active, issued = list(range(size)), [0]*size, {}, []\n    for event in events:\n        if event[0] == 'get':\n            if not free:\n                issued.append(None)\n                continue\n            free.sort()\n            slot = free.pop(0)\n            generations[slot] += 1\n            active[slot] = generations[slot]\n            issued.append([slot, active[slot]])\n        else:\n            slot, generation = event[1:]\n            if 0 <= slot < size:\n                active.pop(slot, None)\n                free.append(slot)\n    return [issued, sorted(free), [[slot, active[slot]] for slot in sorted(active)]]\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nprefix = [event for generation in range(1, N+1) for event in [['get'], ['put', 0, generation]]]\ncheck('old handle cannot release new checkout', solve(1, prefix+[['get'], ['put', 0, N], ['get']]), [[[0, g] for g in range(1, N+2)]+[None], [], [[0, N+1]]])\ncheck('return of never-issued handle', solve(1, [['put', 0, 0], ['get'], ['get']]), [[[0, 1], None], [], [[0, 1]]])\ncheck('valid reuse advances generation', solve(1, [['get'], ['put', 0, 1], ['get']]), [[[0, 1], [0, 2]], [], [[0, 2]]])\ncheck('pool exhaustion is explicit', solve(N, [['get']]*(N+1)), [[[i, 1] for i in range(N)]+[None], [], [[i, 1] for i in range(N)]])\ncheck('zero-sized pool', solve(0, [['get'], ['put', 0, 1]]), [[None], [], []])\ncheck('out-of-range return ignored', solve(N, [['put', N+1, 1]]), [[], list(range(N)), []])\ncheck('no pool activity', solve(N, []), [[], list(range(N)), []])\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":"88f440010cf05106b28a660d1e72717bb30ade2b2c8ebc0e96eaf3849dc64250","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(size, events):\n    free, generations, active, issued = list(range(size)), [0]*size, {}, []\n    for event in events:\n        if event[0] == 'get':\n            if not free:\n                issued.append(None)\n                continue\n            free.sort()\n            slot = free.pop(0)\n            generations[slot] += 1\n            active[slot] = generations[slot]\n            issued.append([slot, active[slot]])\n        else:\n            slot, generation = event[1:]\n            if slot in active and active[slot] == generation:\n                active.pop(slot, None)\n                free.append(slot)\n    return [issued, sorted(free), [[slot, active[slot]] for slot in sorted(active)]]\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nprefix = [event for generation in range(1, N+1) for event in [['get'], ['put', 0, generation]]]\ncheck('old handle cannot release new checkout', solve(1, prefix+[['get'], ['put', 0, N], ['get']]), [[[0, g] for g in range(1, N+2)]+[None], [], [[0, N+1]]])\ncheck('return of never-issued handle', solve(1, [['put', 0, 0], ['get'], ['get']]), [[[0, 1], None], [], [[0, 1]]])\ncheck('valid reuse advances generation', solve(1, [['get'], ['put', 0, 1], ['get']]), [[[0, 1], [0, 2]], [], [[0, 2]]])\ncheck('pool exhaustion is explicit', solve(N, [['get']]*(N+1)), [[[i, 1] for i in range(N)]+[None], [], [[i, 1] for i in range(N)]])\ncheck('zero-sized pool', solve(0, [['get'], ['put', 0, 1]]), [[None], [], []])\ncheck('out-of-range return ignored', solve(N, [['put', N+1, 1]]), [[], list(range(N)), []])\ncheck('no pool activity', solve(N, []), [[], list(range(N)), []])\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":"runtime-pool-handle-generation","generated_at":"2026-09-29T14:36:52.030651+00:00","license":"CC0-1.0","python":"3.12.14","seed":1,"split":"open-access"},"relevance":"Models reusable object handles in a local allocator where delayed callbacks can outlive a checkout; this does not model distributed leases, wall-clock expiration, or thread interleaving.","repair":"Increment generation on checkout and accept a return only for the exact currently active [slot,generation].","root_cause":"Return validation identifies only a pool slot and not the generation of its current checkout.","sha256":"de1f4a002e91297ea1af60b5ba2baa0340a2470d1a967856450f92901a32e1b9","title":"A stale handle returns a newly checked-out object to the pool · case 01","variant":1,"variant_policy":"Five numbered records share a model and may reuse boundary fixtures.","verification":{"attempt":{"elapsed_ms":33.658,"exit_code":1,"observations":[{"actual":[[[0,1],[0,2],[0,3]],[],[[0,3]]],"check":"old handle cannot release new checkout","expected":[[[0,1],[0,2],null],[],[[0,2]]],"passed":false},{"actual":[[[0,1],null],[],[[0,1]]],"check":"return of never-issued handle","expected":[[[0,1],null],[],[[0,1]]],"passed":true},{"actual":[[[0,1],[0,2]],[],[[0,2]]],"check":"valid reuse advances generation","expected":[[[0,1],[0,2]],[],[[0,2]]],"passed":true},{"actual":[[[0,1],null],[],[[0,1]]],"check":"pool exhaustion is explicit","expected":[[[0,1],null],[],[[0,1]]],"passed":true},{"actual":[[null],[],[]],"check":"zero-sized pool","expected":[[null],[],[]],"passed":true},{"actual":[[],[0],[]],"check":"out-of-range return ignored","expected":[[],[0],[]],"passed":true},{"actual":[[],[0],[]],"check":"no pool activity","expected":[[],[0],[]],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"old handle cannot release new checkout\", \"actual\": [[[0, 1], [0, 2], [0, 3]], [], [[0, 3]]], \"expected\": [[[0, 1], [0, 2], null], [], [[0, 2]]], \"passed\": false}, {\"check\": \"return of never-issued handle\", \"actual\": [[[0, 1], null], [], [[0, 1]]], \"expected\": [[[0, 1], null], [], [[0, 1]]], \"passed\": true}, {\"check\": \"valid reuse advances generation\", \"actual\": [[[0, 1], [0, 2]], [], [[0, 2]]], \"expected\": [[[0, 1], [0, 2]], [], [[0, 2]]], \"passed\": true}, {\"check\": \"pool exhaustion is explicit\", \"actual\": [[[0, 1], null], [], [[0, 1]]], \"expected\": [[[0, 1], null], [], [[0, 1]]], \"passed\": true}, {\"check\": \"zero-sized pool\", \"actual\": [[null], [], []], \"expected\": [[null], [], []], \"passed\": true}, {\"check\": \"out-of-range return ignored\", \"actual\": [[], [0], []], \"expected\": [[], [0], []], \"passed\": true}, {\"check\": \"no pool activity\", \"actual\": [[], [0], []], \"expected\": [[], [0], []], \"passed\": true}], \"passed\": false}\n"},"broken":{"elapsed_ms":37.163,"exit_code":1,"observations":[{"actual":[[[0,1],[0,2],[0,3]],[],[[0,3]]],"check":"old handle cannot release new checkout","expected":[[[0,1],[0,2],null],[],[[0,2]]],"passed":false},{"actual":[[[0,1],[0,2]],[],[[0,2]]],"check":"return of never-issued handle","expected":[[[0,1],null],[],[[0,1]]],"passed":false},{"actual":[[[0,1],[0,2]],[],[[0,2]]],"check":"valid reuse advances generation","expected":[[[0,1],[0,2]],[],[[0,2]]],"passed":true},{"actual":[[[0,1],null],[],[[0,1]]],"check":"pool exhaustion is explicit","expected":[[[0,1],null],[],[[0,1]]],"passed":true},{"actual":[[null],[],[]],"check":"zero-sized pool","expected":[[null],[],[]],"passed":true},{"actual":[[],[0],[]],"check":"out-of-range return ignored","expected":[[],[0],[]],"passed":true},{"actual":[[],[0],[]],"check":"no pool activity","expected":[[],[0],[]],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"old handle cannot release new checkout\", \"actual\": [[[0, 1], [0, 2], [0, 3]], [], [[0, 3]]], \"expected\": [[[0, 1], [0, 2], null], [], [[0, 2]]], \"passed\": false}, {\"check\": \"return of never-issued handle\", \"actual\": [[[0, 1], [0, 2]], [], [[0, 2]]], \"expected\": [[[0, 1], null], [], [[0, 1]]], \"passed\": false}, {\"check\": \"valid reuse advances generation\", \"actual\": [[[0, 1], [0, 2]], [], [[0, 2]]], \"expected\": [[[0, 1], [0, 2]], [], [[0, 2]]], \"passed\": true}, {\"check\": \"pool exhaustion is explicit\", \"actual\": [[[0, 1], null], [], [[0, 1]]], \"expected\": [[[0, 1], null], [], [[0, 1]]], \"passed\": true}, {\"check\": \"zero-sized pool\", \"actual\": [[null], [], []], \"expected\": [[null], [], []], \"passed\": true}, {\"check\": \"out-of-range return ignored\", \"actual\": [[], [0], []], \"expected\": [[], [0], []], \"passed\": true}, {\"check\": \"no pool activity\", \"actual\": [[], [0], []], \"expected\": [[], [0], []], \"passed\": true}], \"passed\": false}\n"},"fixed":{"elapsed_ms":35.93,"exit_code":0,"observations":[{"actual":[[[0,1],[0,2],null],[],[[0,2]]],"check":"old handle cannot release new checkout","expected":[[[0,1],[0,2],null],[],[[0,2]]],"passed":true},{"actual":[[[0,1],null],[],[[0,1]]],"check":"return of never-issued handle","expected":[[[0,1],null],[],[[0,1]]],"passed":true},{"actual":[[[0,1],[0,2]],[],[[0,2]]],"check":"valid reuse advances generation","expected":[[[0,1],[0,2]],[],[[0,2]]],"passed":true},{"actual":[[[0,1],null],[],[[0,1]]],"check":"pool exhaustion is explicit","expected":[[[0,1],null],[],[[0,1]]],"passed":true},{"actual":[[null],[],[]],"check":"zero-sized pool","expected":[[null],[],[]],"passed":true},{"actual":[[],[0],[]],"check":"out-of-range return ignored","expected":[[],[0],[]],"passed":true},{"actual":[[],[0],[]],"check":"no pool activity","expected":[[],[0],[]],"passed":true}],"passed":true,"stderr":"","stdout":"{\"observations\": [{\"check\": \"old handle cannot release new checkout\", \"actual\": [[[0, 1], [0, 2], null], [], [[0, 2]]], \"expected\": [[[0, 1], [0, 2], null], [], [[0, 2]]], \"passed\": true}, {\"check\": \"return of never-issued handle\", \"actual\": [[[0, 1], null], [], [[0, 1]]], \"expected\": [[[0, 1], null], [], [[0, 1]]], \"passed\": true}, {\"check\": \"valid reuse advances generation\", \"actual\": [[[0, 1], [0, 2]], [], [[0, 2]]], \"expected\": [[[0, 1], [0, 2]], [], [[0, 2]]], \"passed\": true}, {\"check\": \"pool exhaustion is explicit\", \"actual\": [[[0, 1], null], [], [[0, 1]]], \"expected\": [[[0, 1], null], [], [[0, 1]]], \"passed\": true}, {\"check\": \"zero-sized pool\", \"actual\": [[null], [], []], \"expected\": [[null], [], []], \"passed\": true}, {\"check\": \"out-of-range return ignored\", \"actual\": [[], [0], []], \"expected\": [[], [0], []], \"passed\": true}, {\"check\": \"no pool activity\", \"actual\": [[], [0], []], \"expected\": [[], [0], []], \"passed\": true}], \"passed\": true}\n"}},"verified":true,"visibility":"public"}