FA-90786 / Garbage collector invariants / Open access
TAMS: watermark aliases the live allocation top · case 01
TAMS moves with allocation, so objects allocated during marking must be marked or are freed.
ROOT CAUSE
The TAMS table is the same dict as the allocation tops.
VERIFIED REPAIR
Snapshot the tops when marking starts.
Unsuccessful approach: Capturing the snapshot only once reuses the first cycle's TAMS forever.
Case contract
Concurrent marking with per-region top-at-mark-start (TAMS). alloc r size bump-allocates in region r (addresses r*region_size onward; None if it would pass the region end). start snapshots every region's current top as its TAMS (regions never allocated in have TAMS at their bottom) and clears marks. mark addr marks an object. end frees, in address order, every object below its region's TAMS that is not marked; objects at or above TAMS were allocated during marking and are live. Return allocation addresses and the freed list of each end.
Why this case matters
Snapshot collectors treat objects allocated during marking as live using a per-region watermark.
1 / The failure
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(region_size, events):
top = {}
tams = {}
marked = set()
objs = {}
out = []
for ev in events:
op = ev[0]
if op == 'alloc':
r = ev[1]
a = top.get(r, r * region_size)
if a + ev[2] > (r + 1) * region_size:
out.append(None)
continue
objs[a] = ev[2]
top[r] = a + ev[2]
out.append(a)
elif op == 'start':
tams = top
marked = set()
elif op == 'mark':
marked.add(ev[1])
else:
dead = []
for a in sorted(objs):
r = a // region_size
if a < tams.get(r, r * region_size) and a not in marked:
dead.append(a)
for a in dead:
del objs[a]
out.append(dead)
return out
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = [[('regression: objects above TAMS are implicitly live',
(100,
[['alloc', 0, 30],
['alloc', 0, 21],
['alloc', 1, 40],
['start'],
['alloc', 0, 10],
['alloc', 2, 10],
['mark', 0],
['end']]),
[0, 30, 100, 51, 200, [30, 100]]),
('first object allocated after marking started',
(100, [['alloc', 0, 30], ['alloc', 0, 21], ['alloc', 1, 40], ['start'], ['alloc', 1, 6], ['end']]),
[0, 30, 100, 140, [0, 30, 100]]),
('region untouched when marking started',
(100,
[['alloc', 0, 30],
['alloc', 0, 21],
['alloc', 1, 40],
['start'],
['alloc', 3, 20],
['alloc', 3, 5],
['end']]),
[0, 30, 100, 300, 320, [0, 30, 100]]),
('second cycle uses fresh TAMS and marks',
(100,
[['alloc', 0, 30],
['alloc', 0, 21],
['alloc', 1, 40],
['start'],
['mark', 0],
['alloc', 0, 5],
['end'],
['start'],
['mark', 30],
['end']]),
[0, 30, 100, 51, [30, 100], [0, 51]]),
('marks from the previous cycle are discarded',
(100,
[['alloc', 0, 30],
['alloc', 0, 21],
['alloc', 1, 40],
['start'],
['mark', 0],
['mark', 100],
['end'],
['start'],
['end']]),
[0, 30, 100, [30], [0, 100]]),
('control: allocation beyond the region',
(100, [['alloc', 0, 90], ['alloc', 0, 21], ['start'], ['end']]),
[0, None, [0]])],
[('regression: objects above TAMS are implicitly live',
(100,
[['alloc', 0, 30],
['alloc', 0, 22],
['alloc', 1, 40],
['start'],
['alloc', 0, 10],
['alloc', 2, 10],
['mark', 0],
['end']]),
[0, 30, 100, 52, 200, [30, 100]]),
('first object allocated after marking started',
(100, [['alloc', 0, 30], ['alloc', 0, 22], ['alloc', 1, 40], ['start'], ['alloc', 1, 7], ['end']]),
[0, 30, 100, 140, [0, 30, 100]]),
('region untouched when marking started',
(100,
[['alloc', 0, 30],
['alloc', 0, 22],
['alloc', 1, 40],
['start'],
['alloc', 3, 20],
['alloc', 3, 5],
['end']]),
[0, 30, 100, 300, 320, [0, 30, 100]]),
('second cycle uses fresh TAMS and marks',
(100,
[['alloc', 0, 30],
['alloc', 0, 22],
['alloc', 1, 40],
['start'],
['mark', 0],
['alloc', 0, 5],
['end'],
['start'],
['mark', 30],
['end']]),
[0, 30, 100, 52, [30, 100], [0, 52]]),
('marks from the previous cycle are discarded',
(100,
[['alloc', 0, 30],
['alloc', 0, 22],
['alloc', 1, 40],
['start'],
['mark', 0],
['mark', 100],
['end'],
['start'],
['end']]),
[0, 30, 100, [30], [0, 100]]),
('control: allocation beyond the region',
(100, [['alloc', 0, 90], ['alloc', 0, 22], ['start'], ['end']]),
[0, None, [0]])],
[('regression: objects above TAMS are implicitly live',
(100,
[['alloc', 0, 30],
['alloc', 0, 23],
['alloc', 1, 40],
['start'],
['alloc', 0, 10],
['alloc', 2, 10],
['mark', 0],
['end']]),
[0, 30, 100, 53, 200, [30, 100]]),
('first object allocated after marking started',
(100, [['alloc', 0, 30], ['alloc', 0, 23], ['alloc', 1, 40], ['start'], ['alloc', 1, 8], ['end']]),
[0, 30, 100, 140, [0, 30, 100]]),
('region untouched when marking started',
(100,
[['alloc', 0, 30],
['alloc', 0, 23],
['alloc', 1, 40],
['start'],
['alloc', 3, 20],
['alloc', 3, 5],
['end']]),
[0, 30, 100, 300, 320, [0, 30, 100]]),
('second cycle uses fresh TAMS and marks',
(100,
[['alloc', 0, 30],
['alloc', 0, 23],
['alloc', 1, 40],
['start'],
['mark', 0],
['alloc', 0, 5],
['end'],
['start'],
['mark', 30],
['end']]),
[0, 30, 100, 53, [30, 100], [0, 53]]),
('marks from the previous cycle are discarded',
(100,
[['alloc', 0, 30],
['alloc', 0, 23],
['alloc', 1, 40],
['start'],
['mark', 0],
['mark', 100],
['end'],
['start'],
['end']]),
[0, 30, 100, [30], [0, 100]]),
('control: allocation beyond the region',
(100, [['alloc', 0, 90], ['alloc', 0, 23], ['start'], ['end']]),
[0, None, [0]])],
[('regression: objects above TAMS are implicitly live',
(100,
[['alloc', 0, 30],
['alloc', 0, 24],
['alloc', 1, 40],
['start'],
['alloc', 0, 10],
['alloc', 2, 10],
['mark', 0],
['end']]),
[0, 30, 100, 54, 200, [30, 100]]),
('first object allocated after marking started',
(100, [['alloc', 0, 30], ['alloc', 0, 24], ['alloc', 1, 40], ['start'], ['alloc', 1, 9], ['end']]),
[0, 30, 100, 140, [0, 30, 100]]),
('region untouched when marking started',
(100,
[['alloc', 0, 30],
['alloc', 0, 24],
['alloc', 1, 40],
['start'],
['alloc', 3, 20],
['alloc', 3, 5],
['end']]),
[0, 30, 100, 300, 320, [0, 30, 100]]),
('second cycle uses fresh TAMS and marks',
(100,
[['alloc', 0, 30],
['alloc', 0, 24],
['alloc', 1, 40],
['start'],
['mark', 0],
['alloc', 0, 5],
['end'],
['start'],
['mark', 30],
['end']]),
[0, 30, 100, 54, [30, 100], [0, 54]]),
('marks from the previous cycle are discarded',
(100,
[['alloc', 0, 30],
['alloc', 0, 24],
['alloc', 1, 40],
['start'],
['mark', 0],
['mark', 100],
['end'],
['start'],
['end']]),
[0, 30, 100, [30], [0, 100]]),
('control: allocation beyond the region',
(100, [['alloc', 0, 90], ['alloc', 0, 24], ['start'], ['end']]),
[0, None, [0]])],
[('regression: objects above TAMS are implicitly live',
(100,
[['alloc', 0, 30],
['alloc', 0, 25],
['alloc', 1, 40],
['start'],
['alloc', 0, 10],
['alloc', 2, 10],
['mark', 0],
['end']]),
[0, 30, 100, 55, 200, [30, 100]]),
('first object allocated after marking started',
(100, [['alloc', 0, 30], ['alloc', 0, 25], ['alloc', 1, 40], ['start'], ['alloc', 1, 10], ['end']]),
[0, 30, 100, 140, [0, 30, 100]]),
('region untouched when marking started',
(100,
[['alloc', 0, 30],
['alloc', 0, 25],
['alloc', 1, 40],
['start'],
['alloc', 3, 20],
['alloc', 3, 5],
['end']]),
[0, 30, 100, 300, 320, [0, 30, 100]]),
('second cycle uses fresh TAMS and marks',
(100,
[['alloc', 0, 30],
['alloc', 0, 25],
['alloc', 1, 40],
['start'],
['mark', 0],
['alloc', 0, 5],
['end'],
['start'],
['mark', 30],
['end']]),
[0, 30, 100, 55, [30, 100], [0, 55]]),
('marks from the previous cycle are discarded',
(100,
[['alloc', 0, 30],
['alloc', 0, 25],
['alloc', 1, 40],
['start'],
['mark', 0],
['mark', 100],
['end'],
['start'],
['end']]),
[0, 30, 100, [30], [0, 100]]),
('control: allocation beyond the region',
(100, [['alloc', 0, 90], ['alloc', 0, 25], ['start'], ['end']]),
[0, None, [0]])]]
for label, args, expected in cases[N - 1]:
check(label, solve(*args), expected)
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 |
|---|---|---|---|
| regression: objects above TAMS are implicitly live | [0, 30, 100, 51, 200, [30, 51, 100, 200]] | [0, 30, 100, 51, 200, [30, 100]] | Failed |
| first object allocated after marking started | [0, 30, 100, 140, [0, 30, 100, 140]] | [0, 30, 100, 140, [0, 30, 100]] | Failed |
| region untouched when marking started | [0, 30, 100, 300, 320, [0, 30, 100, 300, 320]] | [0, 30, 100, 300, 320, [0, 30, 100]] | Failed |
| second cycle uses fresh TAMS and marks | [0, 30, 100, 51, [30, 51, 100], [0]] | [0, 30, 100, 51, [30, 100], [0, 51]] | Failed |
| marks from the previous cycle are discarded | [0, 30, 100, [30], [0, 100]] | [0, 30, 100, [30], [0, 100]] | Passed |
| control: allocation beyond the region | [0, None, [0]] | [0, None, [0]] | Passed |
SHA-256 / c7d0ef384be28741ca19de5fe9ce81a2672d73788d76ec670f553986e8f2f68e
2 / The unsuccessful fix
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(region_size, events):
top = {}
tams = {}
marked = set()
objs = {}
out = []
for ev in events:
op = ev[0]
if op == 'alloc':
r = ev[1]
a = top.get(r, r * region_size)
if a + ev[2] > (r + 1) * region_size:
out.append(None)
continue
objs[a] = ev[2]
top[r] = a + ev[2]
out.append(a)
elif op == 'start':
tams = dict(top) if not tams else tams
marked = set()
elif op == 'mark':
marked.add(ev[1])
else:
dead = []
for a in sorted(objs):
r = a // region_size
if a < tams.get(r, r * region_size) and a not in marked:
dead.append(a)
for a in dead:
del objs[a]
out.append(dead)
return out
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = [[('regression: objects above TAMS are implicitly live',
(100,
[['alloc', 0, 30],
['alloc', 0, 21],
['alloc', 1, 40],
['start'],
['alloc', 0, 10],
['alloc', 2, 10],
['mark', 0],
['end']]),
[0, 30, 100, 51, 200, [30, 100]]),
('first object allocated after marking started',
(100, [['alloc', 0, 30], ['alloc', 0, 21], ['alloc', 1, 40], ['start'], ['alloc', 1, 6], ['end']]),
[0, 30, 100, 140, [0, 30, 100]]),
('region untouched when marking started',
(100,
[['alloc', 0, 30],
['alloc', 0, 21],
['alloc', 1, 40],
['start'],
['alloc', 3, 20],
['alloc', 3, 5],
['end']]),
[0, 30, 100, 300, 320, [0, 30, 100]]),
('second cycle uses fresh TAMS and marks',
(100,
[['alloc', 0, 30],
['alloc', 0, 21],
['alloc', 1, 40],
['start'],
['mark', 0],
['alloc', 0, 5],
['end'],
['start'],
['mark', 30],
['end']]),
[0, 30, 100, 51, [30, 100], [0, 51]]),
('marks from the previous cycle are discarded',
(100,
[['alloc', 0, 30],
['alloc', 0, 21],
['alloc', 1, 40],
['start'],
['mark', 0],
['mark', 100],
['end'],
['start'],
['end']]),
[0, 30, 100, [30], [0, 100]]),
('control: allocation beyond the region',
(100, [['alloc', 0, 90], ['alloc', 0, 21], ['start'], ['end']]),
[0, None, [0]])],
[('regression: objects above TAMS are implicitly live',
(100,
[['alloc', 0, 30],
['alloc', 0, 22],
['alloc', 1, 40],
['start'],
['alloc', 0, 10],
['alloc', 2, 10],
['mark', 0],
['end']]),
[0, 30, 100, 52, 200, [30, 100]]),
('first object allocated after marking started',
(100, [['alloc', 0, 30], ['alloc', 0, 22], ['alloc', 1, 40], ['start'], ['alloc', 1, 7], ['end']]),
[0, 30, 100, 140, [0, 30, 100]]),
('region untouched when marking started',
(100,
[['alloc', 0, 30],
['alloc', 0, 22],
['alloc', 1, 40],
['start'],
['alloc', 3, 20],
['alloc', 3, 5],
['end']]),
[0, 30, 100, 300, 320, [0, 30, 100]]),
('second cycle uses fresh TAMS and marks',
(100,
[['alloc', 0, 30],
['alloc', 0, 22],
['alloc', 1, 40],
['start'],
['mark', 0],
['alloc', 0, 5],
['end'],
['start'],
['mark', 30],
['end']]),
[0, 30, 100, 52, [30, 100], [0, 52]]),
('marks from the previous cycle are discarded',
(100,
[['alloc', 0, 30],
['alloc', 0, 22],
['alloc', 1, 40],
['start'],
['mark', 0],
['mark', 100],
['end'],
['start'],
['end']]),
[0, 30, 100, [30], [0, 100]]),
('control: allocation beyond the region',
(100, [['alloc', 0, 90], ['alloc', 0, 22], ['start'], ['end']]),
[0, None, [0]])],
[('regression: objects above TAMS are implicitly live',
(100,
[['alloc', 0, 30],
['alloc', 0, 23],
['alloc', 1, 40],
['start'],
['alloc', 0, 10],
['alloc', 2, 10],
['mark', 0],
['end']]),
[0, 30, 100, 53, 200, [30, 100]]),
('first object allocated after marking started',
(100, [['alloc', 0, 30], ['alloc', 0, 23], ['alloc', 1, 40], ['start'], ['alloc', 1, 8], ['end']]),
[0, 30, 100, 140, [0, 30, 100]]),
('region untouched when marking started',
(100,
[['alloc', 0, 30],
['alloc', 0, 23],
['alloc', 1, 40],
['start'],
['alloc', 3, 20],
['alloc', 3, 5],
['end']]),
[0, 30, 100, 300, 320, [0, 30, 100]]),
('second cycle uses fresh TAMS and marks',
(100,
[['alloc', 0, 30],
['alloc', 0, 23],
['alloc', 1, 40],
['start'],
['mark', 0],
['alloc', 0, 5],
['end'],
['start'],
['mark', 30],
['end']]),
[0, 30, 100, 53, [30, 100], [0, 53]]),
('marks from the previous cycle are discarded',
(100,
[['alloc', 0, 30],
['alloc', 0, 23],
['alloc', 1, 40],
['start'],
['mark', 0],
['mark', 100],
['end'],
['start'],
['end']]),
[0, 30, 100, [30], [0, 100]]),
('control: allocation beyond the region',
(100, [['alloc', 0, 90], ['alloc', 0, 23], ['start'], ['end']]),
[0, None, [0]])],
[('regression: objects above TAMS are implicitly live',
(100,
[['alloc', 0, 30],
['alloc', 0, 24],
['alloc', 1, 40],
['start'],
['alloc', 0, 10],
['alloc', 2, 10],
['mark', 0],
['end']]),
[0, 30, 100, 54, 200, [30, 100]]),
('first object allocated after marking started',
(100, [['alloc', 0, 30], ['alloc', 0, 24], ['alloc', 1, 40], ['start'], ['alloc', 1, 9], ['end']]),
[0, 30, 100, 140, [0, 30, 100]]),
('region untouched when marking started',
(100,
[['alloc', 0, 30],
['alloc', 0, 24],
['alloc', 1, 40],
['start'],
['alloc', 3, 20],
['alloc', 3, 5],
['end']]),
[0, 30, 100, 300, 320, [0, 30, 100]]),
('second cycle uses fresh TAMS and marks',
(100,
[['alloc', 0, 30],
['alloc', 0, 24],
['alloc', 1, 40],
['start'],
['mark', 0],
['alloc', 0, 5],
['end'],
['start'],
['mark', 30],
['end']]),
[0, 30, 100, 54, [30, 100], [0, 54]]),
('marks from the previous cycle are discarded',
(100,
[['alloc', 0, 30],
['alloc', 0, 24],
['alloc', 1, 40],
['start'],
['mark', 0],
['mark', 100],
['end'],
['start'],
['end']]),
[0, 30, 100, [30], [0, 100]]),
('control: allocation beyond the region',
(100, [['alloc', 0, 90], ['alloc', 0, 24], ['start'], ['end']]),
[0, None, [0]])],
[('regression: objects above TAMS are implicitly live',
(100,
[['alloc', 0, 30],
['alloc', 0, 25],
['alloc', 1, 40],
['start'],
['alloc', 0, 10],
['alloc', 2, 10],
['mark', 0],
['end']]),
[0, 30, 100, 55, 200, [30, 100]]),
('first object allocated after marking started',
(100, [['alloc', 0, 30], ['alloc', 0, 25], ['alloc', 1, 40], ['start'], ['alloc', 1, 10], ['end']]),
[0, 30, 100, 140, [0, 30, 100]]),
('region untouched when marking started',
(100,
[['alloc', 0, 30],
['alloc', 0, 25],
['alloc', 1, 40],
['start'],
['alloc', 3, 20],
['alloc', 3, 5],
['end']]),
[0, 30, 100, 300, 320, [0, 30, 100]]),
('second cycle uses fresh TAMS and marks',
(100,
[['alloc', 0, 30],
['alloc', 0, 25],
['alloc', 1, 40],
['start'],
['mark', 0],
['alloc', 0, 5],
['end'],
['start'],
['mark', 30],
['end']]),
[0, 30, 100, 55, [30, 100], [0, 55]]),
('marks from the previous cycle are discarded',
(100,
[['alloc', 0, 30],
['alloc', 0, 25],
['alloc', 1, 40],
['start'],
['mark', 0],
['mark', 100],
['end'],
['start'],
['end']]),
[0, 30, 100, [30], [0, 100]]),
('control: allocation beyond the region',
(100, [['alloc', 0, 90], ['alloc', 0, 25], ['start'], ['end']]),
[0, None, [0]])]]
for label, args, expected in cases[N - 1]:
check(label, solve(*args), expected)
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 |
|---|---|---|---|
| regression: objects above TAMS are implicitly live | [0, 30, 100, 51, 200, [30, 100]] | [0, 30, 100, 51, 200, [30, 100]] | Passed |
| first object allocated after marking started | [0, 30, 100, 140, [0, 30, 100]] | [0, 30, 100, 140, [0, 30, 100]] | Passed |
| region untouched when marking started | [0, 30, 100, 300, 320, [0, 30, 100]] | [0, 30, 100, 300, 320, [0, 30, 100]] | Passed |
| second cycle uses fresh TAMS and marks | [0, 30, 100, 51, [30, 100], [0]] | [0, 30, 100, 51, [30, 100], [0, 51]] | Failed |
| marks from the previous cycle are discarded | [0, 30, 100, [30], [0, 100]] | [0, 30, 100, [30], [0, 100]] | Passed |
| control: allocation beyond the region | [0, None, [0]] | [0, None, [0]] | Passed |
SHA-256 / 9cbfd6951967bc467bbd4f7493e6d775a89d386a6b11b6a00e2ac876b71d327d
3 / The verified repair
Exit 0"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(region_size, events):
top = {}
tams = {}
marked = set()
objs = {}
out = []
for ev in events:
op = ev[0]
if op == 'alloc':
r = ev[1]
a = top.get(r, r * region_size)
if a + ev[2] > (r + 1) * region_size:
out.append(None)
continue
objs[a] = ev[2]
top[r] = a + ev[2]
out.append(a)
elif op == 'start':
tams = dict(top)
marked = set()
elif op == 'mark':
marked.add(ev[1])
else:
dead = []
for a in sorted(objs):
r = a // region_size
if a < tams.get(r, r * region_size) and a not in marked:
dead.append(a)
for a in dead:
del objs[a]
out.append(dead)
return out
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = [[('regression: objects above TAMS are implicitly live',
(100,
[['alloc', 0, 30],
['alloc', 0, 21],
['alloc', 1, 40],
['start'],
['alloc', 0, 10],
['alloc', 2, 10],
['mark', 0],
['end']]),
[0, 30, 100, 51, 200, [30, 100]]),
('first object allocated after marking started',
(100, [['alloc', 0, 30], ['alloc', 0, 21], ['alloc', 1, 40], ['start'], ['alloc', 1, 6], ['end']]),
[0, 30, 100, 140, [0, 30, 100]]),
('region untouched when marking started',
(100,
[['alloc', 0, 30],
['alloc', 0, 21],
['alloc', 1, 40],
['start'],
['alloc', 3, 20],
['alloc', 3, 5],
['end']]),
[0, 30, 100, 300, 320, [0, 30, 100]]),
('second cycle uses fresh TAMS and marks',
(100,
[['alloc', 0, 30],
['alloc', 0, 21],
['alloc', 1, 40],
['start'],
['mark', 0],
['alloc', 0, 5],
['end'],
['start'],
['mark', 30],
['end']]),
[0, 30, 100, 51, [30, 100], [0, 51]]),
('marks from the previous cycle are discarded',
(100,
[['alloc', 0, 30],
['alloc', 0, 21],
['alloc', 1, 40],
['start'],
['mark', 0],
['mark', 100],
['end'],
['start'],
['end']]),
[0, 30, 100, [30], [0, 100]]),
('control: allocation beyond the region',
(100, [['alloc', 0, 90], ['alloc', 0, 21], ['start'], ['end']]),
[0, None, [0]])],
[('regression: objects above TAMS are implicitly live',
(100,
[['alloc', 0, 30],
['alloc', 0, 22],
['alloc', 1, 40],
['start'],
['alloc', 0, 10],
['alloc', 2, 10],
['mark', 0],
['end']]),
[0, 30, 100, 52, 200, [30, 100]]),
('first object allocated after marking started',
(100, [['alloc', 0, 30], ['alloc', 0, 22], ['alloc', 1, 40], ['start'], ['alloc', 1, 7], ['end']]),
[0, 30, 100, 140, [0, 30, 100]]),
('region untouched when marking started',
(100,
[['alloc', 0, 30],
['alloc', 0, 22],
['alloc', 1, 40],
['start'],
['alloc', 3, 20],
['alloc', 3, 5],
['end']]),
[0, 30, 100, 300, 320, [0, 30, 100]]),
('second cycle uses fresh TAMS and marks',
(100,
[['alloc', 0, 30],
['alloc', 0, 22],
['alloc', 1, 40],
['start'],
['mark', 0],
['alloc', 0, 5],
['end'],
['start'],
['mark', 30],
['end']]),
[0, 30, 100, 52, [30, 100], [0, 52]]),
('marks from the previous cycle are discarded',
(100,
[['alloc', 0, 30],
['alloc', 0, 22],
['alloc', 1, 40],
['start'],
['mark', 0],
['mark', 100],
['end'],
['start'],
['end']]),
[0, 30, 100, [30], [0, 100]]),
('control: allocation beyond the region',
(100, [['alloc', 0, 90], ['alloc', 0, 22], ['start'], ['end']]),
[0, None, [0]])],
[('regression: objects above TAMS are implicitly live',
(100,
[['alloc', 0, 30],
['alloc', 0, 23],
['alloc', 1, 40],
['start'],
['alloc', 0, 10],
['alloc', 2, 10],
['mark', 0],
['end']]),
[0, 30, 100, 53, 200, [30, 100]]),
('first object allocated after marking started',
(100, [['alloc', 0, 30], ['alloc', 0, 23], ['alloc', 1, 40], ['start'], ['alloc', 1, 8], ['end']]),
[0, 30, 100, 140, [0, 30, 100]]),
('region untouched when marking started',
(100,
[['alloc', 0, 30],
['alloc', 0, 23],
['alloc', 1, 40],
['start'],
['alloc', 3, 20],
['alloc', 3, 5],
['end']]),
[0, 30, 100, 300, 320, [0, 30, 100]]),
('second cycle uses fresh TAMS and marks',
(100,
[['alloc', 0, 30],
['alloc', 0, 23],
['alloc', 1, 40],
['start'],
['mark', 0],
['alloc', 0, 5],
['end'],
['start'],
['mark', 30],
['end']]),
[0, 30, 100, 53, [30, 100], [0, 53]]),
('marks from the previous cycle are discarded',
(100,
[['alloc', 0, 30],
['alloc', 0, 23],
['alloc', 1, 40],
['start'],
['mark', 0],
['mark', 100],
['end'],
['start'],
['end']]),
[0, 30, 100, [30], [0, 100]]),
('control: allocation beyond the region',
(100, [['alloc', 0, 90], ['alloc', 0, 23], ['start'], ['end']]),
[0, None, [0]])],
[('regression: objects above TAMS are implicitly live',
(100,
[['alloc', 0, 30],
['alloc', 0, 24],
['alloc', 1, 40],
['start'],
['alloc', 0, 10],
['alloc', 2, 10],
['mark', 0],
['end']]),
[0, 30, 100, 54, 200, [30, 100]]),
('first object allocated after marking started',
(100, [['alloc', 0, 30], ['alloc', 0, 24], ['alloc', 1, 40], ['start'], ['alloc', 1, 9], ['end']]),
[0, 30, 100, 140, [0, 30, 100]]),
('region untouched when marking started',
(100,
[['alloc', 0, 30],
['alloc', 0, 24],
['alloc', 1, 40],
['start'],
['alloc', 3, 20],
['alloc', 3, 5],
['end']]),
[0, 30, 100, 300, 320, [0, 30, 100]]),
('second cycle uses fresh TAMS and marks',
(100,
[['alloc', 0, 30],
['alloc', 0, 24],
['alloc', 1, 40],
['start'],
['mark', 0],
['alloc', 0, 5],
['end'],
['start'],
['mark', 30],
['end']]),
[0, 30, 100, 54, [30, 100], [0, 54]]),
('marks from the previous cycle are discarded',
(100,
[['alloc', 0, 30],
['alloc', 0, 24],
['alloc', 1, 40],
['start'],
['mark', 0],
['mark', 100],
['end'],
['start'],
['end']]),
[0, 30, 100, [30], [0, 100]]),
('control: allocation beyond the region',
(100, [['alloc', 0, 90], ['alloc', 0, 24], ['start'], ['end']]),
[0, None, [0]])],
[('regression: objects above TAMS are implicitly live',
(100,
[['alloc', 0, 30],
['alloc', 0, 25],
['alloc', 1, 40],
['start'],
['alloc', 0, 10],
['alloc', 2, 10],
['mark', 0],
['end']]),
[0, 30, 100, 55, 200, [30, 100]]),
('first object allocated after marking started',
(100, [['alloc', 0, 30], ['alloc', 0, 25], ['alloc', 1, 40], ['start'], ['alloc', 1, 10], ['end']]),
[0, 30, 100, 140, [0, 30, 100]]),
('region untouched when marking started',
(100,
[['alloc', 0, 30],
['alloc', 0, 25],
['alloc', 1, 40],
['start'],
['alloc', 3, 20],
['alloc', 3, 5],
['end']]),
[0, 30, 100, 300, 320, [0, 30, 100]]),
('second cycle uses fresh TAMS and marks',
(100,
[['alloc', 0, 30],
['alloc', 0, 25],
['alloc', 1, 40],
['start'],
['mark', 0],
['alloc', 0, 5],
['end'],
['start'],
['mark', 30],
['end']]),
[0, 30, 100, 55, [30, 100], [0, 55]]),
('marks from the previous cycle are discarded',
(100,
[['alloc', 0, 30],
['alloc', 0, 25],
['alloc', 1, 40],
['start'],
['mark', 0],
['mark', 100],
['end'],
['start'],
['end']]),
[0, 30, 100, [30], [0, 100]]),
('control: allocation beyond the region',
(100, [['alloc', 0, 90], ['alloc', 0, 25], ['start'], ['end']]),
[0, None, [0]])]]
for label, args, expected in cases[N - 1]:
check(label, solve(*args), expected)
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 |
|---|---|---|---|
| regression: objects above TAMS are implicitly live | [0, 30, 100, 51, 200, [30, 100]] | [0, 30, 100, 51, 200, [30, 100]] | Passed |
| first object allocated after marking started | [0, 30, 100, 140, [0, 30, 100]] | [0, 30, 100, 140, [0, 30, 100]] | Passed |
| region untouched when marking started | [0, 30, 100, 300, 320, [0, 30, 100]] | [0, 30, 100, 300, 320, [0, 30, 100]] | Passed |
| second cycle uses fresh TAMS and marks | [0, 30, 100, 51, [30, 100], [0, 51]] | [0, 30, 100, 51, [30, 100], [0, 51]] | Passed |
| marks from the previous cycle are discarded | [0, 30, 100, [30], [0, 100]] | [0, 30, 100, [30], [0, 100]] | Passed |
| control: allocation beyond the region | [0, None, [0]] | [0, None, [0]] | Passed |
SHA-256 / 08733f1667198471e1e446d147e2172eea74560fe0cd79ca20982aef24699465
Verification & scope
A deterministic, bounded teaching model of one garbage-collector mechanism with stipulated rules; it is not a production collector and claims no conformance to any particular runtime. 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:51:29.869109+00:00.
Case digest / 09f705eb76b94420bf3884a912793f1c6deb245669a5e38fa0981024995c893d