FA-266 / Runtime and resources / Open access

An unrelated release creates a phantom semaphore permit · case 01

More callers enter than capacity permits after a duplicate or unowned release.

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

ROOT CAUSE

The available count is incremented without verifying a matching outstanding acquisition.

VERIFIED REPAIR

Track active acquisition identities and return a permit only for a currently held acquisition.

Unsuccessful approach: Capping the available counter at capacity still creates a free permit when another caller holds one.

Case contract

A nonnegative capacity counts permits. Each identity may hold at most one. Acquire is nonblocking and returns false if already held or full. Release of a nonholder is a no-op. Return [available,sorted active identities,acquire results]. Transitions are serialized; fairness is not modeled.

Why this case matters

Models ownership-aware permit wrappers where duplicate callbacks and unrelated cleanup paths must not inflate the concurrency allowance.

1 / The failure

Exit 1

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

N = 1
observations = []
def solve(capacity, events):
    available, held, accepted = capacity, set(), []
    for kind, identity in events:
        if kind == 'acquire':
            allowed = available > 0 and identity not in held
            if allowed:
                held.add(identity)
                available -= 1
            accepted.append(allowed)
        else:
            held.discard(identity)
            available += 1
    return [available, sorted(held), accepted]
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
ids = ['owner-'+str(i) for i in range(N)]
fill = [['acquire', identity] for identity in ids]
check('nonholder cannot create spare permit', solve(N, fill+[['release', 'ghost'], ['acquire', 'extra']]), [0, sorted(ids), [True]*N+[False]])
check('duplicate release cannot exceed capacity', solve(N, [['acquire', 'a'], ['release', 'a'], ['release', 'a']]), [N, [], [True]])
check('valid release restores one', solve(N, fill+[['release', ids[0]]]), [1, sorted(ids[1:]), [True]*N])
check('full semaphore rejects acquire', solve(N, fill+[['acquire', 'extra']]), [0, sorted(ids), [True]*N+[False]])
check('same owner cannot acquire twice', solve(N, [['acquire', 'a'], ['acquire', 'a']]), [N-1, ['a'], [True, False]])
check('zero-capacity semaphore', solve(0, [['acquire', 'a'], ['release', 'a']]), [0, [], [False]])
check('idle semaphore', solve(N, []), [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
nonholder cannot create spare permit	`[0, ['extra', 'owner-0'], [True, True]]`	`[0, ['owner-0'], [True, False]]`	Failed
duplicate release cannot exceed capacity	`[2, [], [True]]`	`[1, [], [True]]`	Failed
valid release restores one	`[1, [], [True]]`	`[1, [], [True]]`	Passed
full semaphore rejects acquire	`[0, ['owner-0'], [True, False]]`	`[0, ['owner-0'], [True, False]]`	Passed
same owner cannot acquire twice	`[0, ['a'], [True, False]]`	`[0, ['a'], [True, False]]`	Passed
zero-capacity semaphore	`[1, [], [False]]`	`[0, [], [False]]`	Failed
idle semaphore	`[1, [], []]`	`[1, [], []]`	Passed

SHA-256 / 955d0c7e73cb755ed24c4ae67cdebbee2f7f13c9913af23118889b0f3762b347

2 / The unsuccessful fix

Exit 1

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

N = 1
observations = []
def solve(capacity, events):
    available, held, accepted = capacity, set(), []
    for kind, identity in events:
        if kind == 'acquire':
            allowed = available > 0 and identity not in held
            if allowed:
                held.add(identity)
                available -= 1
            accepted.append(allowed)
        else:
            held.discard(identity)
            available = min(capacity, available+1)
    return [available, sorted(held), accepted]
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
ids = ['owner-'+str(i) for i in range(N)]
fill = [['acquire', identity] for identity in ids]
check('nonholder cannot create spare permit', solve(N, fill+[['release', 'ghost'], ['acquire', 'extra']]), [0, sorted(ids), [True]*N+[False]])
check('duplicate release cannot exceed capacity', solve(N, [['acquire', 'a'], ['release', 'a'], ['release', 'a']]), [N, [], [True]])
check('valid release restores one', solve(N, fill+[['release', ids[0]]]), [1, sorted(ids[1:]), [True]*N])
check('full semaphore rejects acquire', solve(N, fill+[['acquire', 'extra']]), [0, sorted(ids), [True]*N+[False]])
check('same owner cannot acquire twice', solve(N, [['acquire', 'a'], ['acquire', 'a']]), [N-1, ['a'], [True, False]])
check('zero-capacity semaphore', solve(0, [['acquire', 'a'], ['release', 'a']]), [0, [], [False]])
check('idle semaphore', solve(N, []), [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
nonholder cannot create spare permit	`[0, ['extra', 'owner-0'], [True, True]]`	`[0, ['owner-0'], [True, False]]`	Failed
duplicate release cannot exceed capacity	`[1, [], [True]]`	`[1, [], [True]]`	Passed
valid release restores one	`[1, [], [True]]`	`[1, [], [True]]`	Passed
full semaphore rejects acquire	`[0, ['owner-0'], [True, False]]`	`[0, ['owner-0'], [True, False]]`	Passed
same owner cannot acquire twice	`[0, ['a'], [True, False]]`	`[0, ['a'], [True, False]]`	Passed
zero-capacity semaphore	`[0, [], [False]]`	`[0, [], [False]]`	Passed
idle semaphore	`[1, [], []]`	`[1, [], []]`	Passed

SHA-256 / dec187174c326cc1ed110b2eec396ae3c50881abd40fb28f93944d34505a1722

3 / The verified repair

Exit 0

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

N = 1
observations = []
def solve(capacity, events):
    available, held, accepted = capacity, set(), []
    for kind, identity in events:
        if kind == 'acquire':
            allowed = available > 0 and identity not in held
            if allowed:
                held.add(identity)
                available -= 1
            accepted.append(allowed)
        else:
            if identity in held:
                held.remove(identity)
                available += 1
    return [available, sorted(held), accepted]
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
ids = ['owner-'+str(i) for i in range(N)]
fill = [['acquire', identity] for identity in ids]
check('nonholder cannot create spare permit', solve(N, fill+[['release', 'ghost'], ['acquire', 'extra']]), [0, sorted(ids), [True]*N+[False]])
check('duplicate release cannot exceed capacity', solve(N, [['acquire', 'a'], ['release', 'a'], ['release', 'a']]), [N, [], [True]])
check('valid release restores one', solve(N, fill+[['release', ids[0]]]), [1, sorted(ids[1:]), [True]*N])
check('full semaphore rejects acquire', solve(N, fill+[['acquire', 'extra']]), [0, sorted(ids), [True]*N+[False]])
check('same owner cannot acquire twice', solve(N, [['acquire', 'a'], ['acquire', 'a']]), [N-1, ['a'], [True, False]])
check('zero-capacity semaphore', solve(0, [['acquire', 'a'], ['release', 'a']]), [0, [], [False]])
check('idle semaphore', solve(N, []), [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
nonholder cannot create spare permit	`[0, ['owner-0'], [True, False]]`	`[0, ['owner-0'], [True, False]]`	Passed
duplicate release cannot exceed capacity	`[1, [], [True]]`	`[1, [], [True]]`	Passed
valid release restores one	`[1, [], [True]]`	`[1, [], [True]]`	Passed
full semaphore rejects acquire	`[0, ['owner-0'], [True, False]]`	`[0, ['owner-0'], [True, False]]`	Passed
same owner cannot acquire twice	`[0, ['a'], [True, False]]`	`[0, ['a'], [True, False]]`	Passed
zero-capacity semaphore	`[0, [], [False]]`	`[0, [], [False]]`	Passed
idle semaphore	`[1, [], []]`	`[1, [], []]`	Passed

SHA-256 / 7bc47a8561e15eb45ef3f91860e83fb1a3cd91b2fa23da4119acfd6e1d337484

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

Case digest / e2bcc065d2ebe6b9dc037724dacc58d86ec86946e44d3294f1efeae16753d2d4