FA-90346 / Garbage collector invariants / Open access
Insertion barrier: objects allocated during marking start white · case 01
Freshly allocated objects are swept at the end of the cycle in which they were created.
ROOT CAUSE
Allocation ignores the marking phase and always colours new objects white.
VERIFIED REPAIR
Allocate black while a marking cycle is active.
Unsuccessful approach: Testing whether the worklist is non-empty misses allocations after the worklist has drained but before finish.
Case contract
Incremental tri-colour mark-sweep with a Dijkstra insertion barrier. start: every object white, roots shaded grey. mark k: up to k worklist steps (pop a grey object, shade its white children, blacken it). store src i dst: while marking, shade dst before writing. alloc id k: new object with k null fields, black while marking (allocate-black), otherwise white. root id: add a root, shaded if marking. unroot id removes a root. finish: drain the worklist, free all white objects, stop marking. Return the freed ids per finish and the surviving ids.
Why this case matters
Incremental collectors are only safe if barriers and allocation colour preserve the tri-colour invariant.
1 / The failure
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(heap, roots, events):
heap = {k: list(v) for k, v in heap.items()}
roots = list(roots)
color = {}
grey = []
marking = False
log = []
def shade(o):
if o is not None and color.get(o, 'white') == 'white':
color[o] = 'grey'
grey.append(o)
def step():
o = grey.pop()
for c in heap[o]:
shade(c)
color[o] = 'black'
for ev in events:
op = ev[0]
if op == 'start':
color = {o: 'white' for o in heap}
grey.clear()
marking = True
for r in roots:
shade(r)
elif op == 'mark':
for _ in range(ev[1]):
if grey:
step()
elif op == 'store':
if marking:
shade(ev[3])
heap[ev[1]][ev[2]] = ev[3]
elif op == 'alloc':
heap[ev[1]] = [None] * ev[2]
color[ev[1]] = 'white'
elif op == 'root':
roots.append(ev[1])
if marking:
shade(ev[1])
elif op == 'unroot':
roots.remove(ev[1])
else:
while grey:
step()
dead = sorted(o for o in heap if color.get(o, 'white') == 'white')
for o in dead:
del heap[o]
marking = False
log.append(dead)
return {'freed': log, 'live': sorted(heap)}
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = [[('regression: pointer stored into a black object',
({11: [12, None], 12: [13], 13: [], 14: [15], 15: [], 16: [11]},
[11],
[['start'], ['mark', 1], ['store', 11, 1, 14], ['finish']]),
{'freed': [[16]], 'live': [11, 12, 13, 14, 15]}),
('allocation after the worklist drained',
({11: [12, None], 12: [13], 13: [], 14: [15], 15: [], 16: [11]},
[11],
[['start'], ['mark', 10], ['alloc', 17, 1], ['finish']]),
{'freed': [[14, 15, 16]], 'live': [11, 12, 13, 17]}),
('second cycle starts from all-white',
({11: [12, None], 12: [13], 13: [], 14: [15], 15: [], 16: [11]},
[11],
[['start'], ['finish'], ['unroot', 11], ['start'], ['finish']]),
{'freed': [[14, 15, 16], [11, 12, 13]], 'live': []}),
('finish drains outstanding grey objects',
({11: [12, None], 12: [13], 13: [], 14: [15], 15: [], 16: [11]}, [11], [['start'], ['finish']]),
{'freed': [[14, 15, 16]], 'live': [11, 12, 13]}),
('root registered while marking',
({11: [12, None], 12: [13], 13: [], 14: [15], 15: [], 16: [11]},
[11],
[['start'], ['mark', 10], ['root', 16], ['finish']]),
{'freed': [[14, 15]], 'live': [11, 12, 13, 16]}),
('store before marking needs no barrier',
({11: [12, None], 12: [13], 13: [], 14: [15], 15: [], 16: [11]},
[11],
[['alloc', 18, 1], ['store', 18, 0, 14], ['root', 18], ['start'], ['finish']]),
{'freed': [[16]], 'live': [11, 12, 13, 14, 15, 18]}),
('control: unreachable cycle is freed',
({11: [12], 12: [11], 13: []}, [13], [['start'], ['mark', 1], ['finish']]),
{'freed': [[11, 12]], 'live': [13]})],
[('regression: pointer stored into a black object',
({21: [22, None], 22: [23], 23: [], 24: [25], 25: [], 26: [21]},
[21],
[['start'], ['mark', 1], ['store', 21, 1, 24], ['finish']]),
{'freed': [[26]], 'live': [21, 22, 23, 24, 25]}),
('allocation after the worklist drained',
({21: [22, None], 22: [23], 23: [], 24: [25], 25: [], 26: [21]},
[21],
[['start'], ['mark', 10], ['alloc', 27, 1], ['finish']]),
{'freed': [[24, 25, 26]], 'live': [21, 22, 23, 27]}),
('second cycle starts from all-white',
({21: [22, None], 22: [23], 23: [], 24: [25], 25: [], 26: [21]},
[21],
[['start'], ['finish'], ['unroot', 21], ['start'], ['finish']]),
{'freed': [[24, 25, 26], [21, 22, 23]], 'live': []}),
('finish drains outstanding grey objects',
({21: [22, None], 22: [23], 23: [], 24: [25], 25: [], 26: [21]}, [21], [['start'], ['finish']]),
{'freed': [[24, 25, 26]], 'live': [21, 22, 23]}),
('root registered while marking',
({21: [22, None], 22: [23], 23: [], 24: [25], 25: [], 26: [21]},
[21],
[['start'], ['mark', 10], ['root', 26], ['finish']]),
{'freed': [[24, 25]], 'live': [21, 22, 23, 26]}),
('store before marking needs no barrier',
({21: [22, None], 22: [23], 23: [], 24: [25], 25: [], 26: [21]},
[21],
[['alloc', 28, 1], ['store', 28, 0, 24], ['root', 28], ['start'], ['finish']]),
{'freed': [[26]], 'live': [21, 22, 23, 24, 25, 28]}),
('control: unreachable cycle is freed',
({21: [22], 22: [21], 23: []}, [23], [['start'], ['mark', 1], ['finish']]),
{'freed': [[21, 22]], 'live': [23]})],
[('regression: pointer stored into a black object',
({31: [32, None], 32: [33], 33: [], 34: [35], 35: [], 36: [31]},
[31],
[['start'], ['mark', 1], ['store', 31, 1, 34], ['finish']]),
{'freed': [[36]], 'live': [31, 32, 33, 34, 35]}),
('allocation after the worklist drained',
({31: [32, None], 32: [33], 33: [], 34: [35], 35: [], 36: [31]},
[31],
[['start'], ['mark', 10], ['alloc', 37, 1], ['finish']]),
{'freed': [[34, 35, 36]], 'live': [31, 32, 33, 37]}),
('second cycle starts from all-white',
({31: [32, None], 32: [33], 33: [], 34: [35], 35: [], 36: [31]},
[31],
[['start'], ['finish'], ['unroot', 31], ['start'], ['finish']]),
{'freed': [[34, 35, 36], [31, 32, 33]], 'live': []}),
('finish drains outstanding grey objects',
({31: [32, None], 32: [33], 33: [], 34: [35], 35: [], 36: [31]}, [31], [['start'], ['finish']]),
{'freed': [[34, 35, 36]], 'live': [31, 32, 33]}),
('root registered while marking',
({31: [32, None], 32: [33], 33: [], 34: [35], 35: [], 36: [31]},
[31],
[['start'], ['mark', 10], ['root', 36], ['finish']]),
{'freed': [[34, 35]], 'live': [31, 32, 33, 36]}),
('store before marking needs no barrier',
({31: [32, None], 32: [33], 33: [], 34: [35], 35: [], 36: [31]},
[31],
[['alloc', 38, 1], ['store', 38, 0, 34], ['root', 38], ['start'], ['finish']]),
{'freed': [[36]], 'live': [31, 32, 33, 34, 35, 38]}),
('control: unreachable cycle is freed',
({31: [32], 32: [31], 33: []}, [33], [['start'], ['mark', 1], ['finish']]),
{'freed': [[31, 32]], 'live': [33]})],
[('regression: pointer stored into a black object',
({41: [42, None], 42: [43], 43: [], 44: [45], 45: [], 46: [41]},
[41],
[['start'], ['mark', 1], ['store', 41, 1, 44], ['finish']]),
{'freed': [[46]], 'live': [41, 42, 43, 44, 45]}),
('allocation after the worklist drained',
({41: [42, None], 42: [43], 43: [], 44: [45], 45: [], 46: [41]},
[41],
[['start'], ['mark', 10], ['alloc', 47, 1], ['finish']]),
{'freed': [[44, 45, 46]], 'live': [41, 42, 43, 47]}),
('second cycle starts from all-white',
({41: [42, None], 42: [43], 43: [], 44: [45], 45: [], 46: [41]},
[41],
[['start'], ['finish'], ['unroot', 41], ['start'], ['finish']]),
{'freed': [[44, 45, 46], [41, 42, 43]], 'live': []}),
('finish drains outstanding grey objects',
({41: [42, None], 42: [43], 43: [], 44: [45], 45: [], 46: [41]}, [41], [['start'], ['finish']]),
{'freed': [[44, 45, 46]], 'live': [41, 42, 43]}),
('root registered while marking',
({41: [42, None], 42: [43], 43: [], 44: [45], 45: [], 46: [41]},
[41],
[['start'], ['mark', 10], ['root', 46], ['finish']]),
{'freed': [[44, 45]], 'live': [41, 42, 43, 46]}),
('store before marking needs no barrier',
({41: [42, None], 42: [43], 43: [], 44: [45], 45: [], 46: [41]},
[41],
[['alloc', 48, 1], ['store', 48, 0, 44], ['root', 48], ['start'], ['finish']]),
{'freed': [[46]], 'live': [41, 42, 43, 44, 45, 48]}),
('control: unreachable cycle is freed',
({41: [42], 42: [41], 43: []}, [43], [['start'], ['mark', 1], ['finish']]),
{'freed': [[41, 42]], 'live': [43]})],
[('regression: pointer stored into a black object',
({51: [52, None], 52: [53], 53: [], 54: [55], 55: [], 56: [51]},
[51],
[['start'], ['mark', 1], ['store', 51, 1, 54], ['finish']]),
{'freed': [[56]], 'live': [51, 52, 53, 54, 55]}),
('allocation after the worklist drained',
({51: [52, None], 52: [53], 53: [], 54: [55], 55: [], 56: [51]},
[51],
[['start'], ['mark', 10], ['alloc', 57, 1], ['finish']]),
{'freed': [[54, 55, 56]], 'live': [51, 52, 53, 57]}),
('second cycle starts from all-white',
({51: [52, None], 52: [53], 53: [], 54: [55], 55: [], 56: [51]},
[51],
[['start'], ['finish'], ['unroot', 51], ['start'], ['finish']]),
{'freed': [[54, 55, 56], [51, 52, 53]], 'live': []}),
('finish drains outstanding grey objects',
({51: [52, None], 52: [53], 53: [], 54: [55], 55: [], 56: [51]}, [51], [['start'], ['finish']]),
{'freed': [[54, 55, 56]], 'live': [51, 52, 53]}),
('root registered while marking',
({51: [52, None], 52: [53], 53: [], 54: [55], 55: [], 56: [51]},
[51],
[['start'], ['mark', 10], ['root', 56], ['finish']]),
{'freed': [[54, 55]], 'live': [51, 52, 53, 56]}),
('store before marking needs no barrier',
({51: [52, None], 52: [53], 53: [], 54: [55], 55: [], 56: [51]},
[51],
[['alloc', 58, 1], ['store', 58, 0, 54], ['root', 58], ['start'], ['finish']]),
{'freed': [[56]], 'live': [51, 52, 53, 54, 55, 58]}),
('control: unreachable cycle is freed',
({51: [52], 52: [51], 53: []}, [53], [['start'], ['mark', 1], ['finish']]),
{'freed': [[51, 52]], 'live': [53]})]]
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: pointer stored into a black object | {'freed': [[16]], 'live': [11, 12, 13, 14, 15]} | {'freed': [[16]], 'live': [11, 12, 13, 14, 15]} | Passed |
| allocation after the worklist drained | {'freed': [[14, 15, 16, 17]], 'live': [11, 12, 13]} | {'freed': [[14, 15, 16]], 'live': [11, 12, 13, 17]} | Failed |
| second cycle starts from all-white | {'freed': [[14, 15, 16], [11, 12, 13]], 'live': []} | {'freed': [[14, 15, 16], [11, 12, 13]], 'live': []} | Passed |
| finish drains outstanding grey objects | {'freed': [[14, 15, 16]], 'live': [11, 12, 13]} | {'freed': [[14, 15, 16]], 'live': [11, 12, 13]} | Passed |
| root registered while marking | {'freed': [[14, 15]], 'live': [11, 12, 13, 16]} | {'freed': [[14, 15]], 'live': [11, 12, 13, 16]} | Passed |
| store before marking needs no barrier | {'freed': [[16]], 'live': [11, 12, 13, 14, 15, 18]} | {'freed': [[16]], 'live': [11, 12, 13, 14, 15, 18]} | Passed |
| control: unreachable cycle is freed | {'freed': [[11, 12]], 'live': [13]} | {'freed': [[11, 12]], 'live': [13]} | Passed |
SHA-256 / 1f23e7706926af511c2f845e4c43d115e09ed0186a4698cebcb7f4c86346b59b
2 / The unsuccessful fix
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(heap, roots, events):
heap = {k: list(v) for k, v in heap.items()}
roots = list(roots)
color = {}
grey = []
marking = False
log = []
def shade(o):
if o is not None and color.get(o, 'white') == 'white':
color[o] = 'grey'
grey.append(o)
def step():
o = grey.pop()
for c in heap[o]:
shade(c)
color[o] = 'black'
for ev in events:
op = ev[0]
if op == 'start':
color = {o: 'white' for o in heap}
grey.clear()
marking = True
for r in roots:
shade(r)
elif op == 'mark':
for _ in range(ev[1]):
if grey:
step()
elif op == 'store':
if marking:
shade(ev[3])
heap[ev[1]][ev[2]] = ev[3]
elif op == 'alloc':
heap[ev[1]] = [None] * ev[2]
color[ev[1]] = 'black' if grey else 'white'
elif op == 'root':
roots.append(ev[1])
if marking:
shade(ev[1])
elif op == 'unroot':
roots.remove(ev[1])
else:
while grey:
step()
dead = sorted(o for o in heap if color.get(o, 'white') == 'white')
for o in dead:
del heap[o]
marking = False
log.append(dead)
return {'freed': log, 'live': sorted(heap)}
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = [[('regression: pointer stored into a black object',
({11: [12, None], 12: [13], 13: [], 14: [15], 15: [], 16: [11]},
[11],
[['start'], ['mark', 1], ['store', 11, 1, 14], ['finish']]),
{'freed': [[16]], 'live': [11, 12, 13, 14, 15]}),
('allocation after the worklist drained',
({11: [12, None], 12: [13], 13: [], 14: [15], 15: [], 16: [11]},
[11],
[['start'], ['mark', 10], ['alloc', 17, 1], ['finish']]),
{'freed': [[14, 15, 16]], 'live': [11, 12, 13, 17]}),
('second cycle starts from all-white',
({11: [12, None], 12: [13], 13: [], 14: [15], 15: [], 16: [11]},
[11],
[['start'], ['finish'], ['unroot', 11], ['start'], ['finish']]),
{'freed': [[14, 15, 16], [11, 12, 13]], 'live': []}),
('finish drains outstanding grey objects',
({11: [12, None], 12: [13], 13: [], 14: [15], 15: [], 16: [11]}, [11], [['start'], ['finish']]),
{'freed': [[14, 15, 16]], 'live': [11, 12, 13]}),
('root registered while marking',
({11: [12, None], 12: [13], 13: [], 14: [15], 15: [], 16: [11]},
[11],
[['start'], ['mark', 10], ['root', 16], ['finish']]),
{'freed': [[14, 15]], 'live': [11, 12, 13, 16]}),
('store before marking needs no barrier',
({11: [12, None], 12: [13], 13: [], 14: [15], 15: [], 16: [11]},
[11],
[['alloc', 18, 1], ['store', 18, 0, 14], ['root', 18], ['start'], ['finish']]),
{'freed': [[16]], 'live': [11, 12, 13, 14, 15, 18]}),
('control: unreachable cycle is freed',
({11: [12], 12: [11], 13: []}, [13], [['start'], ['mark', 1], ['finish']]),
{'freed': [[11, 12]], 'live': [13]})],
[('regression: pointer stored into a black object',
({21: [22, None], 22: [23], 23: [], 24: [25], 25: [], 26: [21]},
[21],
[['start'], ['mark', 1], ['store', 21, 1, 24], ['finish']]),
{'freed': [[26]], 'live': [21, 22, 23, 24, 25]}),
('allocation after the worklist drained',
({21: [22, None], 22: [23], 23: [], 24: [25], 25: [], 26: [21]},
[21],
[['start'], ['mark', 10], ['alloc', 27, 1], ['finish']]),
{'freed': [[24, 25, 26]], 'live': [21, 22, 23, 27]}),
('second cycle starts from all-white',
({21: [22, None], 22: [23], 23: [], 24: [25], 25: [], 26: [21]},
[21],
[['start'], ['finish'], ['unroot', 21], ['start'], ['finish']]),
{'freed': [[24, 25, 26], [21, 22, 23]], 'live': []}),
('finish drains outstanding grey objects',
({21: [22, None], 22: [23], 23: [], 24: [25], 25: [], 26: [21]}, [21], [['start'], ['finish']]),
{'freed': [[24, 25, 26]], 'live': [21, 22, 23]}),
('root registered while marking',
({21: [22, None], 22: [23], 23: [], 24: [25], 25: [], 26: [21]},
[21],
[['start'], ['mark', 10], ['root', 26], ['finish']]),
{'freed': [[24, 25]], 'live': [21, 22, 23, 26]}),
('store before marking needs no barrier',
({21: [22, None], 22: [23], 23: [], 24: [25], 25: [], 26: [21]},
[21],
[['alloc', 28, 1], ['store', 28, 0, 24], ['root', 28], ['start'], ['finish']]),
{'freed': [[26]], 'live': [21, 22, 23, 24, 25, 28]}),
('control: unreachable cycle is freed',
({21: [22], 22: [21], 23: []}, [23], [['start'], ['mark', 1], ['finish']]),
{'freed': [[21, 22]], 'live': [23]})],
[('regression: pointer stored into a black object',
({31: [32, None], 32: [33], 33: [], 34: [35], 35: [], 36: [31]},
[31],
[['start'], ['mark', 1], ['store', 31, 1, 34], ['finish']]),
{'freed': [[36]], 'live': [31, 32, 33, 34, 35]}),
('allocation after the worklist drained',
({31: [32, None], 32: [33], 33: [], 34: [35], 35: [], 36: [31]},
[31],
[['start'], ['mark', 10], ['alloc', 37, 1], ['finish']]),
{'freed': [[34, 35, 36]], 'live': [31, 32, 33, 37]}),
('second cycle starts from all-white',
({31: [32, None], 32: [33], 33: [], 34: [35], 35: [], 36: [31]},
[31],
[['start'], ['finish'], ['unroot', 31], ['start'], ['finish']]),
{'freed': [[34, 35, 36], [31, 32, 33]], 'live': []}),
('finish drains outstanding grey objects',
({31: [32, None], 32: [33], 33: [], 34: [35], 35: [], 36: [31]}, [31], [['start'], ['finish']]),
{'freed': [[34, 35, 36]], 'live': [31, 32, 33]}),
('root registered while marking',
({31: [32, None], 32: [33], 33: [], 34: [35], 35: [], 36: [31]},
[31],
[['start'], ['mark', 10], ['root', 36], ['finish']]),
{'freed': [[34, 35]], 'live': [31, 32, 33, 36]}),
('store before marking needs no barrier',
({31: [32, None], 32: [33], 33: [], 34: [35], 35: [], 36: [31]},
[31],
[['alloc', 38, 1], ['store', 38, 0, 34], ['root', 38], ['start'], ['finish']]),
{'freed': [[36]], 'live': [31, 32, 33, 34, 35, 38]}),
('control: unreachable cycle is freed',
({31: [32], 32: [31], 33: []}, [33], [['start'], ['mark', 1], ['finish']]),
{'freed': [[31, 32]], 'live': [33]})],
[('regression: pointer stored into a black object',
({41: [42, None], 42: [43], 43: [], 44: [45], 45: [], 46: [41]},
[41],
[['start'], ['mark', 1], ['store', 41, 1, 44], ['finish']]),
{'freed': [[46]], 'live': [41, 42, 43, 44, 45]}),
('allocation after the worklist drained',
({41: [42, None], 42: [43], 43: [], 44: [45], 45: [], 46: [41]},
[41],
[['start'], ['mark', 10], ['alloc', 47, 1], ['finish']]),
{'freed': [[44, 45, 46]], 'live': [41, 42, 43, 47]}),
('second cycle starts from all-white',
({41: [42, None], 42: [43], 43: [], 44: [45], 45: [], 46: [41]},
[41],
[['start'], ['finish'], ['unroot', 41], ['start'], ['finish']]),
{'freed': [[44, 45, 46], [41, 42, 43]], 'live': []}),
('finish drains outstanding grey objects',
({41: [42, None], 42: [43], 43: [], 44: [45], 45: [], 46: [41]}, [41], [['start'], ['finish']]),
{'freed': [[44, 45, 46]], 'live': [41, 42, 43]}),
('root registered while marking',
({41: [42, None], 42: [43], 43: [], 44: [45], 45: [], 46: [41]},
[41],
[['start'], ['mark', 10], ['root', 46], ['finish']]),
{'freed': [[44, 45]], 'live': [41, 42, 43, 46]}),
('store before marking needs no barrier',
({41: [42, None], 42: [43], 43: [], 44: [45], 45: [], 46: [41]},
[41],
[['alloc', 48, 1], ['store', 48, 0, 44], ['root', 48], ['start'], ['finish']]),
{'freed': [[46]], 'live': [41, 42, 43, 44, 45, 48]}),
('control: unreachable cycle is freed',
({41: [42], 42: [41], 43: []}, [43], [['start'], ['mark', 1], ['finish']]),
{'freed': [[41, 42]], 'live': [43]})],
[('regression: pointer stored into a black object',
({51: [52, None], 52: [53], 53: [], 54: [55], 55: [], 56: [51]},
[51],
[['start'], ['mark', 1], ['store', 51, 1, 54], ['finish']]),
{'freed': [[56]], 'live': [51, 52, 53, 54, 55]}),
('allocation after the worklist drained',
({51: [52, None], 52: [53], 53: [], 54: [55], 55: [], 56: [51]},
[51],
[['start'], ['mark', 10], ['alloc', 57, 1], ['finish']]),
{'freed': [[54, 55, 56]], 'live': [51, 52, 53, 57]}),
('second cycle starts from all-white',
({51: [52, None], 52: [53], 53: [], 54: [55], 55: [], 56: [51]},
[51],
[['start'], ['finish'], ['unroot', 51], ['start'], ['finish']]),
{'freed': [[54, 55, 56], [51, 52, 53]], 'live': []}),
('finish drains outstanding grey objects',
({51: [52, None], 52: [53], 53: [], 54: [55], 55: [], 56: [51]}, [51], [['start'], ['finish']]),
{'freed': [[54, 55, 56]], 'live': [51, 52, 53]}),
('root registered while marking',
({51: [52, None], 52: [53], 53: [], 54: [55], 55: [], 56: [51]},
[51],
[['start'], ['mark', 10], ['root', 56], ['finish']]),
{'freed': [[54, 55]], 'live': [51, 52, 53, 56]}),
('store before marking needs no barrier',
({51: [52, None], 52: [53], 53: [], 54: [55], 55: [], 56: [51]},
[51],
[['alloc', 58, 1], ['store', 58, 0, 54], ['root', 58], ['start'], ['finish']]),
{'freed': [[56]], 'live': [51, 52, 53, 54, 55, 58]}),
('control: unreachable cycle is freed',
({51: [52], 52: [51], 53: []}, [53], [['start'], ['mark', 1], ['finish']]),
{'freed': [[51, 52]], 'live': [53]})]]
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: pointer stored into a black object | {'freed': [[16]], 'live': [11, 12, 13, 14, 15]} | {'freed': [[16]], 'live': [11, 12, 13, 14, 15]} | Passed |
| allocation after the worklist drained | {'freed': [[14, 15, 16, 17]], 'live': [11, 12, 13]} | {'freed': [[14, 15, 16]], 'live': [11, 12, 13, 17]} | Failed |
| second cycle starts from all-white | {'freed': [[14, 15, 16], [11, 12, 13]], 'live': []} | {'freed': [[14, 15, 16], [11, 12, 13]], 'live': []} | Passed |
| finish drains outstanding grey objects | {'freed': [[14, 15, 16]], 'live': [11, 12, 13]} | {'freed': [[14, 15, 16]], 'live': [11, 12, 13]} | Passed |
| root registered while marking | {'freed': [[14, 15]], 'live': [11, 12, 13, 16]} | {'freed': [[14, 15]], 'live': [11, 12, 13, 16]} | Passed |
| store before marking needs no barrier | {'freed': [[16]], 'live': [11, 12, 13, 14, 15, 18]} | {'freed': [[16]], 'live': [11, 12, 13, 14, 15, 18]} | Passed |
| control: unreachable cycle is freed | {'freed': [[11, 12]], 'live': [13]} | {'freed': [[11, 12]], 'live': [13]} | Passed |
SHA-256 / dcf7bb62852b95208265ba833e34feeeb38ea7a566f3276ebc9a1beb26336740
3 / The verified repair
Exit 0"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(heap, roots, events):
heap = {k: list(v) for k, v in heap.items()}
roots = list(roots)
color = {}
grey = []
marking = False
log = []
def shade(o):
if o is not None and color.get(o, 'white') == 'white':
color[o] = 'grey'
grey.append(o)
def step():
o = grey.pop()
for c in heap[o]:
shade(c)
color[o] = 'black'
for ev in events:
op = ev[0]
if op == 'start':
color = {o: 'white' for o in heap}
grey.clear()
marking = True
for r in roots:
shade(r)
elif op == 'mark':
for _ in range(ev[1]):
if grey:
step()
elif op == 'store':
if marking:
shade(ev[3])
heap[ev[1]][ev[2]] = ev[3]
elif op == 'alloc':
heap[ev[1]] = [None] * ev[2]
color[ev[1]] = 'black' if marking else 'white'
elif op == 'root':
roots.append(ev[1])
if marking:
shade(ev[1])
elif op == 'unroot':
roots.remove(ev[1])
else:
while grey:
step()
dead = sorted(o for o in heap if color.get(o, 'white') == 'white')
for o in dead:
del heap[o]
marking = False
log.append(dead)
return {'freed': log, 'live': sorted(heap)}
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = [[('regression: pointer stored into a black object',
({11: [12, None], 12: [13], 13: [], 14: [15], 15: [], 16: [11]},
[11],
[['start'], ['mark', 1], ['store', 11, 1, 14], ['finish']]),
{'freed': [[16]], 'live': [11, 12, 13, 14, 15]}),
('allocation after the worklist drained',
({11: [12, None], 12: [13], 13: [], 14: [15], 15: [], 16: [11]},
[11],
[['start'], ['mark', 10], ['alloc', 17, 1], ['finish']]),
{'freed': [[14, 15, 16]], 'live': [11, 12, 13, 17]}),
('second cycle starts from all-white',
({11: [12, None], 12: [13], 13: [], 14: [15], 15: [], 16: [11]},
[11],
[['start'], ['finish'], ['unroot', 11], ['start'], ['finish']]),
{'freed': [[14, 15, 16], [11, 12, 13]], 'live': []}),
('finish drains outstanding grey objects',
({11: [12, None], 12: [13], 13: [], 14: [15], 15: [], 16: [11]}, [11], [['start'], ['finish']]),
{'freed': [[14, 15, 16]], 'live': [11, 12, 13]}),
('root registered while marking',
({11: [12, None], 12: [13], 13: [], 14: [15], 15: [], 16: [11]},
[11],
[['start'], ['mark', 10], ['root', 16], ['finish']]),
{'freed': [[14, 15]], 'live': [11, 12, 13, 16]}),
('store before marking needs no barrier',
({11: [12, None], 12: [13], 13: [], 14: [15], 15: [], 16: [11]},
[11],
[['alloc', 18, 1], ['store', 18, 0, 14], ['root', 18], ['start'], ['finish']]),
{'freed': [[16]], 'live': [11, 12, 13, 14, 15, 18]}),
('control: unreachable cycle is freed',
({11: [12], 12: [11], 13: []}, [13], [['start'], ['mark', 1], ['finish']]),
{'freed': [[11, 12]], 'live': [13]})],
[('regression: pointer stored into a black object',
({21: [22, None], 22: [23], 23: [], 24: [25], 25: [], 26: [21]},
[21],
[['start'], ['mark', 1], ['store', 21, 1, 24], ['finish']]),
{'freed': [[26]], 'live': [21, 22, 23, 24, 25]}),
('allocation after the worklist drained',
({21: [22, None], 22: [23], 23: [], 24: [25], 25: [], 26: [21]},
[21],
[['start'], ['mark', 10], ['alloc', 27, 1], ['finish']]),
{'freed': [[24, 25, 26]], 'live': [21, 22, 23, 27]}),
('second cycle starts from all-white',
({21: [22, None], 22: [23], 23: [], 24: [25], 25: [], 26: [21]},
[21],
[['start'], ['finish'], ['unroot', 21], ['start'], ['finish']]),
{'freed': [[24, 25, 26], [21, 22, 23]], 'live': []}),
('finish drains outstanding grey objects',
({21: [22, None], 22: [23], 23: [], 24: [25], 25: [], 26: [21]}, [21], [['start'], ['finish']]),
{'freed': [[24, 25, 26]], 'live': [21, 22, 23]}),
('root registered while marking',
({21: [22, None], 22: [23], 23: [], 24: [25], 25: [], 26: [21]},
[21],
[['start'], ['mark', 10], ['root', 26], ['finish']]),
{'freed': [[24, 25]], 'live': [21, 22, 23, 26]}),
('store before marking needs no barrier',
({21: [22, None], 22: [23], 23: [], 24: [25], 25: [], 26: [21]},
[21],
[['alloc', 28, 1], ['store', 28, 0, 24], ['root', 28], ['start'], ['finish']]),
{'freed': [[26]], 'live': [21, 22, 23, 24, 25, 28]}),
('control: unreachable cycle is freed',
({21: [22], 22: [21], 23: []}, [23], [['start'], ['mark', 1], ['finish']]),
{'freed': [[21, 22]], 'live': [23]})],
[('regression: pointer stored into a black object',
({31: [32, None], 32: [33], 33: [], 34: [35], 35: [], 36: [31]},
[31],
[['start'], ['mark', 1], ['store', 31, 1, 34], ['finish']]),
{'freed': [[36]], 'live': [31, 32, 33, 34, 35]}),
('allocation after the worklist drained',
({31: [32, None], 32: [33], 33: [], 34: [35], 35: [], 36: [31]},
[31],
[['start'], ['mark', 10], ['alloc', 37, 1], ['finish']]),
{'freed': [[34, 35, 36]], 'live': [31, 32, 33, 37]}),
('second cycle starts from all-white',
({31: [32, None], 32: [33], 33: [], 34: [35], 35: [], 36: [31]},
[31],
[['start'], ['finish'], ['unroot', 31], ['start'], ['finish']]),
{'freed': [[34, 35, 36], [31, 32, 33]], 'live': []}),
('finish drains outstanding grey objects',
({31: [32, None], 32: [33], 33: [], 34: [35], 35: [], 36: [31]}, [31], [['start'], ['finish']]),
{'freed': [[34, 35, 36]], 'live': [31, 32, 33]}),
('root registered while marking',
({31: [32, None], 32: [33], 33: [], 34: [35], 35: [], 36: [31]},
[31],
[['start'], ['mark', 10], ['root', 36], ['finish']]),
{'freed': [[34, 35]], 'live': [31, 32, 33, 36]}),
('store before marking needs no barrier',
({31: [32, None], 32: [33], 33: [], 34: [35], 35: [], 36: [31]},
[31],
[['alloc', 38, 1], ['store', 38, 0, 34], ['root', 38], ['start'], ['finish']]),
{'freed': [[36]], 'live': [31, 32, 33, 34, 35, 38]}),
('control: unreachable cycle is freed',
({31: [32], 32: [31], 33: []}, [33], [['start'], ['mark', 1], ['finish']]),
{'freed': [[31, 32]], 'live': [33]})],
[('regression: pointer stored into a black object',
({41: [42, None], 42: [43], 43: [], 44: [45], 45: [], 46: [41]},
[41],
[['start'], ['mark', 1], ['store', 41, 1, 44], ['finish']]),
{'freed': [[46]], 'live': [41, 42, 43, 44, 45]}),
('allocation after the worklist drained',
({41: [42, None], 42: [43], 43: [], 44: [45], 45: [], 46: [41]},
[41],
[['start'], ['mark', 10], ['alloc', 47, 1], ['finish']]),
{'freed': [[44, 45, 46]], 'live': [41, 42, 43, 47]}),
('second cycle starts from all-white',
({41: [42, None], 42: [43], 43: [], 44: [45], 45: [], 46: [41]},
[41],
[['start'], ['finish'], ['unroot', 41], ['start'], ['finish']]),
{'freed': [[44, 45, 46], [41, 42, 43]], 'live': []}),
('finish drains outstanding grey objects',
({41: [42, None], 42: [43], 43: [], 44: [45], 45: [], 46: [41]}, [41], [['start'], ['finish']]),
{'freed': [[44, 45, 46]], 'live': [41, 42, 43]}),
('root registered while marking',
({41: [42, None], 42: [43], 43: [], 44: [45], 45: [], 46: [41]},
[41],
[['start'], ['mark', 10], ['root', 46], ['finish']]),
{'freed': [[44, 45]], 'live': [41, 42, 43, 46]}),
('store before marking needs no barrier',
({41: [42, None], 42: [43], 43: [], 44: [45], 45: [], 46: [41]},
[41],
[['alloc', 48, 1], ['store', 48, 0, 44], ['root', 48], ['start'], ['finish']]),
{'freed': [[46]], 'live': [41, 42, 43, 44, 45, 48]}),
('control: unreachable cycle is freed',
({41: [42], 42: [41], 43: []}, [43], [['start'], ['mark', 1], ['finish']]),
{'freed': [[41, 42]], 'live': [43]})],
[('regression: pointer stored into a black object',
({51: [52, None], 52: [53], 53: [], 54: [55], 55: [], 56: [51]},
[51],
[['start'], ['mark', 1], ['store', 51, 1, 54], ['finish']]),
{'freed': [[56]], 'live': [51, 52, 53, 54, 55]}),
('allocation after the worklist drained',
({51: [52, None], 52: [53], 53: [], 54: [55], 55: [], 56: [51]},
[51],
[['start'], ['mark', 10], ['alloc', 57, 1], ['finish']]),
{'freed': [[54, 55, 56]], 'live': [51, 52, 53, 57]}),
('second cycle starts from all-white',
({51: [52, None], 52: [53], 53: [], 54: [55], 55: [], 56: [51]},
[51],
[['start'], ['finish'], ['unroot', 51], ['start'], ['finish']]),
{'freed': [[54, 55, 56], [51, 52, 53]], 'live': []}),
('finish drains outstanding grey objects',
({51: [52, None], 52: [53], 53: [], 54: [55], 55: [], 56: [51]}, [51], [['start'], ['finish']]),
{'freed': [[54, 55, 56]], 'live': [51, 52, 53]}),
('root registered while marking',
({51: [52, None], 52: [53], 53: [], 54: [55], 55: [], 56: [51]},
[51],
[['start'], ['mark', 10], ['root', 56], ['finish']]),
{'freed': [[54, 55]], 'live': [51, 52, 53, 56]}),
('store before marking needs no barrier',
({51: [52, None], 52: [53], 53: [], 54: [55], 55: [], 56: [51]},
[51],
[['alloc', 58, 1], ['store', 58, 0, 54], ['root', 58], ['start'], ['finish']]),
{'freed': [[56]], 'live': [51, 52, 53, 54, 55, 58]}),
('control: unreachable cycle is freed',
({51: [52], 52: [51], 53: []}, [53], [['start'], ['mark', 1], ['finish']]),
{'freed': [[51, 52]], 'live': [53]})]]
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: pointer stored into a black object | {'freed': [[16]], 'live': [11, 12, 13, 14, 15]} | {'freed': [[16]], 'live': [11, 12, 13, 14, 15]} | Passed |
| allocation after the worklist drained | {'freed': [[14, 15, 16]], 'live': [11, 12, 13, 17]} | {'freed': [[14, 15, 16]], 'live': [11, 12, 13, 17]} | Passed |
| second cycle starts from all-white | {'freed': [[14, 15, 16], [11, 12, 13]], 'live': []} | {'freed': [[14, 15, 16], [11, 12, 13]], 'live': []} | Passed |
| finish drains outstanding grey objects | {'freed': [[14, 15, 16]], 'live': [11, 12, 13]} | {'freed': [[14, 15, 16]], 'live': [11, 12, 13]} | Passed |
| root registered while marking | {'freed': [[14, 15]], 'live': [11, 12, 13, 16]} | {'freed': [[14, 15]], 'live': [11, 12, 13, 16]} | Passed |
| store before marking needs no barrier | {'freed': [[16]], 'live': [11, 12, 13, 14, 15, 18]} | {'freed': [[16]], 'live': [11, 12, 13, 14, 15, 18]} | Passed |
| control: unreachable cycle is freed | {'freed': [[11, 12]], 'live': [13]} | {'freed': [[11, 12]], 'live': [13]} | Passed |
SHA-256 / 8f3efc50d5ba915d8b6b33558f8a86076df02688e86989e23ba494a82a0a2883
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:25.821494+00:00.
Case digest / 054ce6bf0b2c454bf94b15393b57f4c52b363e4a28b42198dd12d5bc02daf765