FA-47166 / Bounded deques / Open access

Deque pressure emits pause repeatedly while above high watermark · case 01

Deque pressure emits pause repeatedly while above high watermark.

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

ROOT CAUSE

Deque pressure emits pause repeatedly while above high watermark.

VERIFIED REPAIR

Restore the documented pause edge invariant in watermark-transitions.

Unsuccessful approach: The partial repair still applies the incorrect transition to an admitted boundary or multi-element case.

Case contract

Bounded deque pressure notifications are edge-triggered: unpaused producers pause on an upward high crossing; paused producers resume on a downward low crossing. Return state, ordered notification list and distances to both thresholds.

Why this case matters

Controlled bounded deque implementation model with explicit storage and lifecycle observations.

1 / The failure

Exit 1

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

N = 1
observations = []
def solve(x):
    old,new,low,high,paused=x
    events=[]
    state=paused
    if not paused and new>=high:
        state=True
        events.append('pause')
    if paused and old>low>=new:
        state=False
        events.append('resume')
    at_high=new>=high
    at_low=new<=low
    headroom=max(0,high-new)
    excess=max(0,new-low)
    return [state,events,at_high,at_low,headroom,excess]
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('0', solve([2,5,2,5,False]), {1: [True, ['pause'], True, False, 0, 3], 2: [True, ['pause'], True, False, 0, 3], 3: [True, ['pause'], True, False, 0, 3], 4: [True, ['pause'], True, False, 0, 3], 5: [True, ['pause'], True, False, 0, 3]}[N])
check('1', solve([5,2,2,5,True]), {1: [False, ['resume'], False, True, 3, 0], 2: [False, ['resume'], False, True, 3, 0], 3: [False, ['resume'], False, True, 3, 0], 4: [False, ['resume'], False, True, 3, 0], 5: [False, ['resume'], False, True, 3, 0]}[N])
check('2', solve([5,6,2,5,False]), {1: [False, [], True, False, 0, 4], 2: [False, [], True, False, 0, 4], 3: [False, [], True, False, 0, 4], 4: [False, [], True, False, 0, 4], 5: [False, [], True, False, 0, 4]}[N])
check('3', solve([2,1,2,5,True]), {1: [True, [], False, True, 4, 0], 2: [True, [], False, True, 4, 0], 3: [True, [], False, True, 4, 0], 4: [True, [], False, True, 4, 0], 5: [True, [], False, True, 4, 0]}[N])
check('4', solve([N,N,0,N+3,False]), {1: [False, [], False, False, 3, 1], 2: [False, [], False, False, 3, 2], 3: [False, [], False, False, 3, 3], 4: [False, [], False, False, 3, 4], 5: [False, [], False, False, 3, 5]}[N])
check('5', solve([3,4,2,5,False]), {1: [False, [], False, False, 1, 2], 2: [False, [], False, False, 1, 2], 3: [False, [], False, False, 1, 2], 4: [False, [], False, False, 1, 2], 5: [False, [], False, False, 1, 2]}[N])
check('6', solve([6,1,2,5,True]), {1: [False, ['resume'], False, True, 4, 0], 2: [False, ['resume'], False, True, 4, 0], 3: [False, ['resume'], False, True, 4, 0], 4: [False, ['resume'], False, True, 4, 0], 5: [False, ['resume'], False, True, 4, 0]}[N])
check('7', solve([1,7,2,5,False]), {1: [True, ['pause'], True, False, 0, 5], 2: [True, ['pause'], True, False, 0, 5], 3: [True, ['pause'], True, False, 0, 5], 4: [True, ['pause'], True, False, 0, 5], 5: [True, ['pause'], True, False, 0, 5]}[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
0	`[True, ['pause'], True, False, 0, 3]`	`[True, ['pause'], True, False, 0, 3]`	Passed
1	`[False, ['resume'], False, True, 3, 0]`	`[False, ['resume'], False, True, 3, 0]`	Passed
2	`[True, ['pause'], True, False, 0, 4]`	`[False, [], True, False, 0, 4]`	Failed
3	`[True, [], False, True, 4, 0]`	`[True, [], False, True, 4, 0]`	Passed
4	`[False, [], False, False, 3, 1]`	`[False, [], False, False, 3, 1]`	Passed
5	`[False, [], False, False, 1, 2]`	`[False, [], False, False, 1, 2]`	Passed
6	`[False, ['resume'], False, True, 4, 0]`	`[False, ['resume'], False, True, 4, 0]`	Passed
7	`[True, ['pause'], True, False, 0, 5]`	`[True, ['pause'], True, False, 0, 5]`	Passed

SHA-256 / 16fd67fba00b285e4c65dfa667fda29e771f78590390a10ea3d4390b6c60c60f

2 / The unsuccessful fix

Exit 1

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

N = 1
observations = []
def solve(x):
    old,new,low,high,paused=x
    events=[]
    state=paused
    if not paused and new>=high and old!=new:
        state=True
        events.append('pause')
    if paused and old>low>=new:
        state=False
        events.append('resume')
    at_high=new>=high
    at_low=new<=low
    headroom=max(0,high-new)
    excess=max(0,new-low)
    return [state,events,at_high,at_low,headroom,excess]
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('0', solve([2,5,2,5,False]), {1: [True, ['pause'], True, False, 0, 3], 2: [True, ['pause'], True, False, 0, 3], 3: [True, ['pause'], True, False, 0, 3], 4: [True, ['pause'], True, False, 0, 3], 5: [True, ['pause'], True, False, 0, 3]}[N])
check('1', solve([5,2,2,5,True]), {1: [False, ['resume'], False, True, 3, 0], 2: [False, ['resume'], False, True, 3, 0], 3: [False, ['resume'], False, True, 3, 0], 4: [False, ['resume'], False, True, 3, 0], 5: [False, ['resume'], False, True, 3, 0]}[N])
check('2', solve([5,6,2,5,False]), {1: [False, [], True, False, 0, 4], 2: [False, [], True, False, 0, 4], 3: [False, [], True, False, 0, 4], 4: [False, [], True, False, 0, 4], 5: [False, [], True, False, 0, 4]}[N])
check('3', solve([2,1,2,5,True]), {1: [True, [], False, True, 4, 0], 2: [True, [], False, True, 4, 0], 3: [True, [], False, True, 4, 0], 4: [True, [], False, True, 4, 0], 5: [True, [], False, True, 4, 0]}[N])
check('4', solve([N,N,0,N+3,False]), {1: [False, [], False, False, 3, 1], 2: [False, [], False, False, 3, 2], 3: [False, [], False, False, 3, 3], 4: [False, [], False, False, 3, 4], 5: [False, [], False, False, 3, 5]}[N])
check('5', solve([3,4,2,5,False]), {1: [False, [], False, False, 1, 2], 2: [False, [], False, False, 1, 2], 3: [False, [], False, False, 1, 2], 4: [False, [], False, False, 1, 2], 5: [False, [], False, False, 1, 2]}[N])
check('6', solve([6,1,2,5,True]), {1: [False, ['resume'], False, True, 4, 0], 2: [False, ['resume'], False, True, 4, 0], 3: [False, ['resume'], False, True, 4, 0], 4: [False, ['resume'], False, True, 4, 0], 5: [False, ['resume'], False, True, 4, 0]}[N])
check('7', solve([1,7,2,5,False]), {1: [True, ['pause'], True, False, 0, 5], 2: [True, ['pause'], True, False, 0, 5], 3: [True, ['pause'], True, False, 0, 5], 4: [True, ['pause'], True, False, 0, 5], 5: [True, ['pause'], True, False, 0, 5]}[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
0	`[True, ['pause'], True, False, 0, 3]`	`[True, ['pause'], True, False, 0, 3]`	Passed
1	`[False, ['resume'], False, True, 3, 0]`	`[False, ['resume'], False, True, 3, 0]`	Passed
2	`[True, ['pause'], True, False, 0, 4]`	`[False, [], True, False, 0, 4]`	Failed
3	`[True, [], False, True, 4, 0]`	`[True, [], False, True, 4, 0]`	Passed
4	`[False, [], False, False, 3, 1]`	`[False, [], False, False, 3, 1]`	Passed
5	`[False, [], False, False, 1, 2]`	`[False, [], False, False, 1, 2]`	Passed
6	`[False, ['resume'], False, True, 4, 0]`	`[False, ['resume'], False, True, 4, 0]`	Passed
7	`[True, ['pause'], True, False, 0, 5]`	`[True, ['pause'], True, False, 0, 5]`	Passed

SHA-256 / c443d8e7649a9403576e12235be39283fdbaebe493345004e34e5fa6f29f25e6

3 / The verified repair

Exit 0

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

N = 1
observations = []
def solve(x):
    old,new,low,high,paused=x
    events=[]
    state=paused
    if not paused and old<high<=new:
        state=True
        events.append('pause')
    if paused and old>low>=new:
        state=False
        events.append('resume')
    at_high=new>=high
    at_low=new<=low
    headroom=max(0,high-new)
    excess=max(0,new-low)
    return [state,events,at_high,at_low,headroom,excess]
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('0', solve([2,5,2,5,False]), {1: [True, ['pause'], True, False, 0, 3], 2: [True, ['pause'], True, False, 0, 3], 3: [True, ['pause'], True, False, 0, 3], 4: [True, ['pause'], True, False, 0, 3], 5: [True, ['pause'], True, False, 0, 3]}[N])
check('1', solve([5,2,2,5,True]), {1: [False, ['resume'], False, True, 3, 0], 2: [False, ['resume'], False, True, 3, 0], 3: [False, ['resume'], False, True, 3, 0], 4: [False, ['resume'], False, True, 3, 0], 5: [False, ['resume'], False, True, 3, 0]}[N])
check('2', solve([5,6,2,5,False]), {1: [False, [], True, False, 0, 4], 2: [False, [], True, False, 0, 4], 3: [False, [], True, False, 0, 4], 4: [False, [], True, False, 0, 4], 5: [False, [], True, False, 0, 4]}[N])
check('3', solve([2,1,2,5,True]), {1: [True, [], False, True, 4, 0], 2: [True, [], False, True, 4, 0], 3: [True, [], False, True, 4, 0], 4: [True, [], False, True, 4, 0], 5: [True, [], False, True, 4, 0]}[N])
check('4', solve([N,N,0,N+3,False]), {1: [False, [], False, False, 3, 1], 2: [False, [], False, False, 3, 2], 3: [False, [], False, False, 3, 3], 4: [False, [], False, False, 3, 4], 5: [False, [], False, False, 3, 5]}[N])
check('5', solve([3,4,2,5,False]), {1: [False, [], False, False, 1, 2], 2: [False, [], False, False, 1, 2], 3: [False, [], False, False, 1, 2], 4: [False, [], False, False, 1, 2], 5: [False, [], False, False, 1, 2]}[N])
check('6', solve([6,1,2,5,True]), {1: [False, ['resume'], False, True, 4, 0], 2: [False, ['resume'], False, True, 4, 0], 3: [False, ['resume'], False, True, 4, 0], 4: [False, ['resume'], False, True, 4, 0], 5: [False, ['resume'], False, True, 4, 0]}[N])
check('7', solve([1,7,2,5,False]), {1: [True, ['pause'], True, False, 0, 5], 2: [True, ['pause'], True, False, 0, 5], 3: [True, ['pause'], True, False, 0, 5], 4: [True, ['pause'], True, False, 0, 5], 5: [True, ['pause'], True, False, 0, 5]}[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
0	`[True, ['pause'], True, False, 0, 3]`	`[True, ['pause'], True, False, 0, 3]`	Passed
1	`[False, ['resume'], False, True, 3, 0]`	`[False, ['resume'], False, True, 3, 0]`	Passed
2	`[False, [], True, False, 0, 4]`	`[False, [], True, False, 0, 4]`	Passed
3	`[True, [], False, True, 4, 0]`	`[True, [], False, True, 4, 0]`	Passed
4	`[False, [], False, False, 3, 1]`	`[False, [], False, False, 3, 1]`	Passed
5	`[False, [], False, False, 1, 2]`	`[False, [], False, False, 1, 2]`	Passed
6	`[False, ['resume'], False, True, 4, 0]`	`[False, ['resume'], False, True, 4, 0]`	Passed
7	`[True, ['pause'], True, False, 0, 5]`	`[True, ['pause'], True, False, 0, 5]`	Passed

SHA-256 / b13ba957da5a5b080a055843a0651f082dfd204d40cd1e9825d77609620abcc9

Verification & scope

Offline finite deterministic model; no claim of production implementation or concurrent memory-model conformance. 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:44:38.907962+00:00.

Case digest / 854b4e80f58090fb922283034e948109495c28449fb25d6cda2894baa3741a3e