FA-281 / Runtime and resources / Open access

A stale handle returns a newly checked-out object to the pool · case 01

The same slot becomes available while a later borrower still owns it.

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

ROOT CAUSE

Return validation identifies only a pool slot and not the generation of its current checkout.

VERIFIED REPAIR

Increment generation on checkout and accept a return only for the exact currently active [slot,generation].

Unsuccessful approach: Rejecting returns for idle slots handles immediate double returns but misses stale returns after slot reuse.

Case 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.

Why this case matters

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.

1 / The failure

Exit 1

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

N = 1
observations = []
def solve(size, events):
    free, generations, active, issued = list(range(size)), [0]*size, {}, []
    for event in events:
        if event[0] == 'get':
            if not free:
                issued.append(None)
                continue
            free.sort()
            slot = free.pop(0)
            generations[slot] += 1
            active[slot] = generations[slot]
            issued.append([slot, active[slot]])
        else:
            slot, generation = event[1:]
            if 0 <= slot < size:
                active.pop(slot, None)
                free.append(slot)
    return [issued, sorted(free), [[slot, active[slot]] for slot in sorted(active)]]
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
prefix = [event for generation in range(1, N+1) for event in [['get'], ['put', 0, generation]]]
check('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]]])
check('return of never-issued handle', solve(1, [['put', 0, 0], ['get'], ['get']]), [[[0, 1], None], [], [[0, 1]]])
check('valid reuse advances generation', solve(1, [['get'], ['put', 0, 1], ['get']]), [[[0, 1], [0, 2]], [], [[0, 2]]])
check('pool exhaustion is explicit', solve(N, [['get']]*(N+1)), [[[i, 1] for i in range(N)]+[None], [], [[i, 1] for i in range(N)]])
check('zero-sized pool', solve(0, [['get'], ['put', 0, 1]]), [[None], [], []])
check('out-of-range return ignored', solve(N, [['put', N+1, 1]]), [[], list(range(N)), []])
check('no pool activity', solve(N, []), [[], list(range(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
old handle cannot release new checkout	`[[[0, 1], [0, 2], [0, 3]], [], [[0, 3]]]`	`[[[0, 1], [0, 2], None], [], [[0, 2]]]`	Failed
return of never-issued handle	`[[[0, 1], [0, 2]], [], [[0, 2]]]`	`[[[0, 1], None], [], [[0, 1]]]`	Failed
valid reuse advances generation	`[[[0, 1], [0, 2]], [], [[0, 2]]]`	`[[[0, 1], [0, 2]], [], [[0, 2]]]`	Passed
pool exhaustion is explicit	`[[[0, 1], None], [], [[0, 1]]]`	`[[[0, 1], None], [], [[0, 1]]]`	Passed
zero-sized pool	`[[None], [], []]`	`[[None], [], []]`	Passed
out-of-range return ignored	`[[], [0], []]`	`[[], [0], []]`	Passed
no pool activity	`[[], [0], []]`	`[[], [0], []]`	Passed

SHA-256 / f9cadb225437ca8b4b5b93e29733e581c6ffc0f441c19155633b61244a7fb1e3

2 / The unsuccessful fix

Exit 1

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

N = 1
observations = []
def solve(size, events):
    free, generations, active, issued = list(range(size)), [0]*size, {}, []
    for event in events:
        if event[0] == 'get':
            if not free:
                issued.append(None)
                continue
            free.sort()
            slot = free.pop(0)
            generations[slot] += 1
            active[slot] = generations[slot]
            issued.append([slot, active[slot]])
        else:
            slot, generation = event[1:]
            if slot in active:
                active.pop(slot, None)
                free.append(slot)
    return [issued, sorted(free), [[slot, active[slot]] for slot in sorted(active)]]
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
prefix = [event for generation in range(1, N+1) for event in [['get'], ['put', 0, generation]]]
check('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]]])
check('return of never-issued handle', solve(1, [['put', 0, 0], ['get'], ['get']]), [[[0, 1], None], [], [[0, 1]]])
check('valid reuse advances generation', solve(1, [['get'], ['put', 0, 1], ['get']]), [[[0, 1], [0, 2]], [], [[0, 2]]])
check('pool exhaustion is explicit', solve(N, [['get']]*(N+1)), [[[i, 1] for i in range(N)]+[None], [], [[i, 1] for i in range(N)]])
check('zero-sized pool', solve(0, [['get'], ['put', 0, 1]]), [[None], [], []])
check('out-of-range return ignored', solve(N, [['put', N+1, 1]]), [[], list(range(N)), []])
check('no pool activity', solve(N, []), [[], list(range(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
old handle cannot release new checkout	`[[[0, 1], [0, 2], [0, 3]], [], [[0, 3]]]`	`[[[0, 1], [0, 2], None], [], [[0, 2]]]`	Failed
return of never-issued handle	`[[[0, 1], None], [], [[0, 1]]]`	`[[[0, 1], None], [], [[0, 1]]]`	Passed
valid reuse advances generation	`[[[0, 1], [0, 2]], [], [[0, 2]]]`	`[[[0, 1], [0, 2]], [], [[0, 2]]]`	Passed
pool exhaustion is explicit	`[[[0, 1], None], [], [[0, 1]]]`	`[[[0, 1], None], [], [[0, 1]]]`	Passed
zero-sized pool	`[[None], [], []]`	`[[None], [], []]`	Passed
out-of-range return ignored	`[[], [0], []]`	`[[], [0], []]`	Passed
no pool activity	`[[], [0], []]`	`[[], [0], []]`	Passed

SHA-256 / f29018f7f62bb49befdc6794cfb2671521d35c879e238875e6d67cd035dfe578

3 / The verified repair

Exit 0

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

N = 1
observations = []
def solve(size, events):
    free, generations, active, issued = list(range(size)), [0]*size, {}, []
    for event in events:
        if event[0] == 'get':
            if not free:
                issued.append(None)
                continue
            free.sort()
            slot = free.pop(0)
            generations[slot] += 1
            active[slot] = generations[slot]
            issued.append([slot, active[slot]])
        else:
            slot, generation = event[1:]
            if slot in active and active[slot] == generation:
                active.pop(slot, None)
                free.append(slot)
    return [issued, sorted(free), [[slot, active[slot]] for slot in sorted(active)]]
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
prefix = [event for generation in range(1, N+1) for event in [['get'], ['put', 0, generation]]]
check('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]]])
check('return of never-issued handle', solve(1, [['put', 0, 0], ['get'], ['get']]), [[[0, 1], None], [], [[0, 1]]])
check('valid reuse advances generation', solve(1, [['get'], ['put', 0, 1], ['get']]), [[[0, 1], [0, 2]], [], [[0, 2]]])
check('pool exhaustion is explicit', solve(N, [['get']]*(N+1)), [[[i, 1] for i in range(N)]+[None], [], [[i, 1] for i in range(N)]])
check('zero-sized pool', solve(0, [['get'], ['put', 0, 1]]), [[None], [], []])
check('out-of-range return ignored', solve(N, [['put', N+1, 1]]), [[], list(range(N)), []])
check('no pool activity', solve(N, []), [[], list(range(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
old handle cannot release new checkout	`[[[0, 1], [0, 2], None], [], [[0, 2]]]`	`[[[0, 1], [0, 2], None], [], [[0, 2]]]`	Passed
return of never-issued handle	`[[[0, 1], None], [], [[0, 1]]]`	`[[[0, 1], None], [], [[0, 1]]]`	Passed
valid reuse advances generation	`[[[0, 1], [0, 2]], [], [[0, 2]]]`	`[[[0, 1], [0, 2]], [], [[0, 2]]]`	Passed
pool exhaustion is explicit	`[[[0, 1], None], [], [[0, 1]]]`	`[[[0, 1], None], [], [[0, 1]]]`	Passed
zero-sized pool	`[[None], [], []]`	`[[None], [], []]`	Passed
out-of-range return ignored	`[[], [0], []]`	`[[], [0], []]`	Passed
no pool activity	`[[], [0], []]`	`[[], [0], []]`	Passed

SHA-256 / 88f440010cf05106b28a660d1e72717bb30ade2b2c8ebc0e96eaf3849dc64250

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

Case digest / de1f4a002e91297ea1af60b5ba2baa0340a2470d1a967856450f92901a32e1b9