{"abstract":"More callers enter than capacity permits after a duplicate or unowned release.","category":"Runtime and resources","checks":7,"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.","contract_signature":"capacity, events","evaluation_group":"model-af668b4a3378c2ae","failed_approach":"Capping the available counter at capacity still creates a free permit when another caller holds one.","family":"runtime-semaphore-owner-accounting","id":"FA-266","implementations":{"attempt":{"sha256":"dec187174c326cc1ed110b2eec396ae3c50881abd40fb28f93944d34505a1722","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(capacity, events):\n    available, held, accepted = capacity, set(), []\n    for kind, identity in events:\n        if kind == 'acquire':\n            allowed = available > 0 and identity not in held\n            if allowed:\n                held.add(identity)\n                available -= 1\n            accepted.append(allowed)\n        else:\n            held.discard(identity)\n            available = min(capacity, available+1)\n    return [available, sorted(held), accepted]\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nids = ['owner-'+str(i) for i in range(N)]\nfill = [['acquire', identity] for identity in ids]\ncheck('nonholder cannot create spare permit', solve(N, fill+[['release', 'ghost'], ['acquire', 'extra']]), [0, sorted(ids), [True]*N+[False]])\ncheck('duplicate release cannot exceed capacity', solve(N, [['acquire', 'a'], ['release', 'a'], ['release', 'a']]), [N, [], [True]])\ncheck('valid release restores one', solve(N, fill+[['release', ids[0]]]), [1, sorted(ids[1:]), [True]*N])\ncheck('full semaphore rejects acquire', solve(N, fill+[['acquire', 'extra']]), [0, sorted(ids), [True]*N+[False]])\ncheck('same owner cannot acquire twice', solve(N, [['acquire', 'a'], ['acquire', 'a']]), [N-1, ['a'], [True, False]])\ncheck('zero-capacity semaphore', solve(0, [['acquire', 'a'], ['release', 'a']]), [0, [], [False]])\ncheck('idle semaphore', solve(N, []), [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":"955d0c7e73cb755ed24c4ae67cdebbee2f7f13c9913af23118889b0f3762b347","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(capacity, events):\n    available, held, accepted = capacity, set(), []\n    for kind, identity in events:\n        if kind == 'acquire':\n            allowed = available > 0 and identity not in held\n            if allowed:\n                held.add(identity)\n                available -= 1\n            accepted.append(allowed)\n        else:\n            held.discard(identity)\n            available += 1\n    return [available, sorted(held), accepted]\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nids = ['owner-'+str(i) for i in range(N)]\nfill = [['acquire', identity] for identity in ids]\ncheck('nonholder cannot create spare permit', solve(N, fill+[['release', 'ghost'], ['acquire', 'extra']]), [0, sorted(ids), [True]*N+[False]])\ncheck('duplicate release cannot exceed capacity', solve(N, [['acquire', 'a'], ['release', 'a'], ['release', 'a']]), [N, [], [True]])\ncheck('valid release restores one', solve(N, fill+[['release', ids[0]]]), [1, sorted(ids[1:]), [True]*N])\ncheck('full semaphore rejects acquire', solve(N, fill+[['acquire', 'extra']]), [0, sorted(ids), [True]*N+[False]])\ncheck('same owner cannot acquire twice', solve(N, [['acquire', 'a'], ['acquire', 'a']]), [N-1, ['a'], [True, False]])\ncheck('zero-capacity semaphore', solve(0, [['acquire', 'a'], ['release', 'a']]), [0, [], [False]])\ncheck('idle semaphore', solve(N, []), [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-semaphore-owner-accounting","generated_at":"2026-09-29T14:36:51.561845+00:00","license":"CC0-1.0","python":"3.12.14","seed":1,"split":"open-access"},"relevance":"Models ownership-aware permit wrappers where duplicate callbacks and unrelated cleanup paths must not inflate the concurrency allowance.","root_cause":"The available count is incremented without verifying a matching outstanding acquisition.","sha256":"078dc5b963e64d0ea7e9ec3387a32c2f1e7e0459184201e69bf296ef06cbdf54","title":"An unrelated release creates a phantom semaphore permit · case 01","variant":1,"variant_policy":"Five numbered records share a model and may reuse boundary fixtures.","verified":true,"visibility":"public","verification":{"attempt":{"elapsed_ms":36.685,"exit_code":1,"observations":[{"actual":[0,["extra","owner-0"],[true,true]],"check":"nonholder cannot create spare permit","expected":[0,["owner-0"],[true,false]],"passed":false},{"actual":[1,[],[true]],"check":"duplicate release cannot exceed capacity","expected":[1,[],[true]],"passed":true},{"actual":[1,[],[true]],"check":"valid release restores one","expected":[1,[],[true]],"passed":true},{"actual":[0,["owner-0"],[true,false]],"check":"full semaphore rejects acquire","expected":[0,["owner-0"],[true,false]],"passed":true},{"actual":[0,["a"],[true,false]],"check":"same owner cannot acquire twice","expected":[0,["a"],[true,false]],"passed":true},{"actual":[0,[],[false]],"check":"zero-capacity semaphore","expected":[0,[],[false]],"passed":true},{"actual":[1,[],[]],"check":"idle semaphore","expected":[1,[],[]],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"nonholder cannot create spare permit\", \"actual\": [0, [\"extra\", \"owner-0\"], [true, true]], \"expected\": [0, [\"owner-0\"], [true, false]], \"passed\": false}, {\"check\": \"duplicate release cannot exceed capacity\", \"actual\": [1, [], [true]], \"expected\": [1, [], [true]], \"passed\": true}, {\"check\": \"valid release restores one\", \"actual\": [1, [], [true]], \"expected\": [1, [], [true]], \"passed\": true}, {\"check\": \"full semaphore rejects acquire\", \"actual\": [0, [\"owner-0\"], [true, false]], \"expected\": [0, [\"owner-0\"], [true, false]], \"passed\": true}, {\"check\": \"same owner cannot acquire twice\", \"actual\": [0, [\"a\"], [true, false]], \"expected\": [0, [\"a\"], [true, false]], \"passed\": true}, {\"check\": \"zero-capacity semaphore\", \"actual\": [0, [], [false]], \"expected\": [0, [], [false]], \"passed\": true}, {\"check\": \"idle semaphore\", \"actual\": [1, [], []], \"expected\": [1, [], []], \"passed\": true}], \"passed\": false}\n"},"broken":{"elapsed_ms":31.361,"exit_code":1,"observations":[{"actual":[0,["extra","owner-0"],[true,true]],"check":"nonholder cannot create spare permit","expected":[0,["owner-0"],[true,false]],"passed":false},{"actual":[2,[],[true]],"check":"duplicate release cannot exceed capacity","expected":[1,[],[true]],"passed":false},{"actual":[1,[],[true]],"check":"valid release restores one","expected":[1,[],[true]],"passed":true},{"actual":[0,["owner-0"],[true,false]],"check":"full semaphore rejects acquire","expected":[0,["owner-0"],[true,false]],"passed":true},{"actual":[0,["a"],[true,false]],"check":"same owner cannot acquire twice","expected":[0,["a"],[true,false]],"passed":true},{"actual":[1,[],[false]],"check":"zero-capacity semaphore","expected":[0,[],[false]],"passed":false},{"actual":[1,[],[]],"check":"idle semaphore","expected":[1,[],[]],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"nonholder cannot create spare permit\", \"actual\": [0, [\"extra\", \"owner-0\"], [true, true]], \"expected\": [0, [\"owner-0\"], [true, false]], \"passed\": false}, {\"check\": \"duplicate release cannot exceed capacity\", \"actual\": [2, [], [true]], \"expected\": [1, [], [true]], \"passed\": false}, {\"check\": \"valid release restores one\", \"actual\": [1, [], [true]], \"expected\": [1, [], [true]], \"passed\": true}, {\"check\": \"full semaphore rejects acquire\", \"actual\": [0, [\"owner-0\"], [true, false]], \"expected\": [0, [\"owner-0\"], [true, false]], \"passed\": true}, {\"check\": \"same owner cannot acquire twice\", \"actual\": [0, [\"a\"], [true, false]], \"expected\": [0, [\"a\"], [true, false]], \"passed\": true}, {\"check\": \"zero-capacity semaphore\", \"actual\": [1, [], [false]], \"expected\": [0, [], [false]], \"passed\": false}, {\"check\": \"idle semaphore\", \"actual\": [1, [], []], \"expected\": [1, [], []], \"passed\": true}], \"passed\": false}\n"}},"member_only":{"stages":["fixed"],"fields":["implementations.fixed","verification.fixed","harness","repair"],"note":"The verified repair, its recorded checks, the repair description, and the scoring harness are available to members."}}