{"abstract":"Objects marked in an earlier cycle survive later cycles without being reached.","category":"Garbage collector invariants","checks":6,"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.","evaluation_group":"w2-garbage-collector-invariants-top-at-mark-start","failed_approach":"Dropping marks only of freed objects still keeps stale marks of survivors.","family":"w2-garbage-collector-invariants-top-at-mark-start-mark-reset","id":"FA-90791","implementations":{"attempt":{"sha256":"d248fa33eb818c5d7cf155c39dffa2085724796dffc5fdbd573319b1bcef052d","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(region_size, events):\n    top = {}\n    tams = {}\n    marked = set()\n    objs = {}\n    out = []\n    for ev in events:\n        op = ev[0]\n        if op == 'alloc':\n            r = ev[1]\n            a = top.get(r, r * region_size)\n            if a + ev[2] > (r + 1) * region_size:\n                out.append(None)\n                continue\n            objs[a] = ev[2]\n            top[r] = a + ev[2]\n            out.append(a)\n        elif op == 'start':\n            tams = dict(top)\n            marked = {a for a in marked if a in objs}\n        elif op == 'mark':\n            marked.add(ev[1])\n        else:\n            dead = []\n            for a in sorted(objs):\n                r = a // region_size\n                if a < tams.get(r, r * region_size) and a not in marked:\n                    dead.append(a)\n            for a in dead:\n                del objs[a]\n            out.append(dead)\n    return out\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncases = [[('regression: objects above TAMS are implicitly live',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 21],\n     ['alloc', 1, 40],\n     ['start'],\n     ['alloc', 0, 10],\n     ['alloc', 2, 10],\n     ['mark', 0],\n     ['end']]),\n   [0, 30, 100, 51, 200, [30, 100]]),\n  ('first object allocated after marking started',\n   (100, [['alloc', 0, 30], ['alloc', 0, 21], ['alloc', 1, 40], ['start'], ['alloc', 1, 6], ['end']]),\n   [0, 30, 100, 140, [0, 30, 100]]),\n  ('region untouched when marking started',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 21],\n     ['alloc', 1, 40],\n     ['start'],\n     ['alloc', 3, 20],\n     ['alloc', 3, 5],\n     ['end']]),\n   [0, 30, 100, 300, 320, [0, 30, 100]]),\n  ('second cycle uses fresh TAMS and marks',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 21],\n     ['alloc', 1, 40],\n     ['start'],\n     ['mark', 0],\n     ['alloc', 0, 5],\n     ['end'],\n     ['start'],\n     ['mark', 30],\n     ['end']]),\n   [0, 30, 100, 51, [30, 100], [0, 51]]),\n  ('marks from the previous cycle are discarded',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 21],\n     ['alloc', 1, 40],\n     ['start'],\n     ['mark', 0],\n     ['mark', 100],\n     ['end'],\n     ['start'],\n     ['end']]),\n   [0, 30, 100, [30], [0, 100]]),\n  ('control: allocation beyond the region',\n   (100, [['alloc', 0, 90], ['alloc', 0, 21], ['start'], ['end']]),\n   [0, None, [0]])],\n [('regression: objects above TAMS are implicitly live',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 22],\n     ['alloc', 1, 40],\n     ['start'],\n     ['alloc', 0, 10],\n     ['alloc', 2, 10],\n     ['mark', 0],\n     ['end']]),\n   [0, 30, 100, 52, 200, [30, 100]]),\n  ('first object allocated after marking started',\n   (100, [['alloc', 0, 30], ['alloc', 0, 22], ['alloc', 1, 40], ['start'], ['alloc', 1, 7], ['end']]),\n   [0, 30, 100, 140, [0, 30, 100]]),\n  ('region untouched when marking started',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 22],\n     ['alloc', 1, 40],\n     ['start'],\n     ['alloc', 3, 20],\n     ['alloc', 3, 5],\n     ['end']]),\n   [0, 30, 100, 300, 320, [0, 30, 100]]),\n  ('second cycle uses fresh TAMS and marks',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 22],\n     ['alloc', 1, 40],\n     ['start'],\n     ['mark', 0],\n     ['alloc', 0, 5],\n     ['end'],\n     ['start'],\n     ['mark', 30],\n     ['end']]),\n   [0, 30, 100, 52, [30, 100], [0, 52]]),\n  ('marks from the previous cycle are discarded',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 22],\n     ['alloc', 1, 40],\n     ['start'],\n     ['mark', 0],\n     ['mark', 100],\n     ['end'],\n     ['start'],\n     ['end']]),\n   [0, 30, 100, [30], [0, 100]]),\n  ('control: allocation beyond the region',\n   (100, [['alloc', 0, 90], ['alloc', 0, 22], ['start'], ['end']]),\n   [0, None, [0]])],\n [('regression: objects above TAMS are implicitly live',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 23],\n     ['alloc', 1, 40],\n     ['start'],\n     ['alloc', 0, 10],\n     ['alloc', 2, 10],\n     ['mark', 0],\n     ['end']]),\n   [0, 30, 100, 53, 200, [30, 100]]),\n  ('first object allocated after marking started',\n   (100, [['alloc', 0, 30], ['alloc', 0, 23], ['alloc', 1, 40], ['start'], ['alloc', 1, 8], ['end']]),\n   [0, 30, 100, 140, [0, 30, 100]]),\n  ('region untouched when marking started',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 23],\n     ['alloc', 1, 40],\n     ['start'],\n     ['alloc', 3, 20],\n     ['alloc', 3, 5],\n     ['end']]),\n   [0, 30, 100, 300, 320, [0, 30, 100]]),\n  ('second cycle uses fresh TAMS and marks',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 23],\n     ['alloc', 1, 40],\n     ['start'],\n     ['mark', 0],\n     ['alloc', 0, 5],\n     ['end'],\n     ['start'],\n     ['mark', 30],\n     ['end']]),\n   [0, 30, 100, 53, [30, 100], [0, 53]]),\n  ('marks from the previous cycle are discarded',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 23],\n     ['alloc', 1, 40],\n     ['start'],\n     ['mark', 0],\n     ['mark', 100],\n     ['end'],\n     ['start'],\n     ['end']]),\n   [0, 30, 100, [30], [0, 100]]),\n  ('control: allocation beyond the region',\n   (100, [['alloc', 0, 90], ['alloc', 0, 23], ['start'], ['end']]),\n   [0, None, [0]])],\n [('regression: objects above TAMS are implicitly live',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 24],\n     ['alloc', 1, 40],\n     ['start'],\n     ['alloc', 0, 10],\n     ['alloc', 2, 10],\n     ['mark', 0],\n     ['end']]),\n   [0, 30, 100, 54, 200, [30, 100]]),\n  ('first object allocated after marking started',\n   (100, [['alloc', 0, 30], ['alloc', 0, 24], ['alloc', 1, 40], ['start'], ['alloc', 1, 9], ['end']]),\n   [0, 30, 100, 140, [0, 30, 100]]),\n  ('region untouched when marking started',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 24],\n     ['alloc', 1, 40],\n     ['start'],\n     ['alloc', 3, 20],\n     ['alloc', 3, 5],\n     ['end']]),\n   [0, 30, 100, 300, 320, [0, 30, 100]]),\n  ('second cycle uses fresh TAMS and marks',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 24],\n     ['alloc', 1, 40],\n     ['start'],\n     ['mark', 0],\n     ['alloc', 0, 5],\n     ['end'],\n     ['start'],\n     ['mark', 30],\n     ['end']]),\n   [0, 30, 100, 54, [30, 100], [0, 54]]),\n  ('marks from the previous cycle are discarded',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 24],\n     ['alloc', 1, 40],\n     ['start'],\n     ['mark', 0],\n     ['mark', 100],\n     ['end'],\n     ['start'],\n     ['end']]),\n   [0, 30, 100, [30], [0, 100]]),\n  ('control: allocation beyond the region',\n   (100, [['alloc', 0, 90], ['alloc', 0, 24], ['start'], ['end']]),\n   [0, None, [0]])],\n [('regression: objects above TAMS are implicitly live',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 25],\n     ['alloc', 1, 40],\n     ['start'],\n     ['alloc', 0, 10],\n     ['alloc', 2, 10],\n     ['mark', 0],\n     ['end']]),\n   [0, 30, 100, 55, 200, [30, 100]]),\n  ('first object allocated after marking started',\n   (100, [['alloc', 0, 30], ['alloc', 0, 25], ['alloc', 1, 40], ['start'], ['alloc', 1, 10], ['end']]),\n   [0, 30, 100, 140, [0, 30, 100]]),\n  ('region untouched when marking started',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 25],\n     ['alloc', 1, 40],\n     ['start'],\n     ['alloc', 3, 20],\n     ['alloc', 3, 5],\n     ['end']]),\n   [0, 30, 100, 300, 320, [0, 30, 100]]),\n  ('second cycle uses fresh TAMS and marks',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 25],\n     ['alloc', 1, 40],\n     ['start'],\n     ['mark', 0],\n     ['alloc', 0, 5],\n     ['end'],\n     ['start'],\n     ['mark', 30],\n     ['end']]),\n   [0, 30, 100, 55, [30, 100], [0, 55]]),\n  ('marks from the previous cycle are discarded',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 25],\n     ['alloc', 1, 40],\n     ['start'],\n     ['mark', 0],\n     ['mark', 100],\n     ['end'],\n     ['start'],\n     ['end']]),\n   [0, 30, 100, [30], [0, 100]]),\n  ('control: allocation beyond the region',\n   (100, [['alloc', 0, 90], ['alloc', 0, 25], ['start'], ['end']]),\n   [0, None, [0]])]]\nfor label, args, expected in cases[N - 1]:\n    check(label, solve(*args), expected)\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":"9794a229a0c3539e7bd7e315daada1f184e2d7104165993268a069c3716aea85","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(region_size, events):\n    top = {}\n    tams = {}\n    marked = set()\n    objs = {}\n    out = []\n    for ev in events:\n        op = ev[0]\n        if op == 'alloc':\n            r = ev[1]\n            a = top.get(r, r * region_size)\n            if a + ev[2] > (r + 1) * region_size:\n                out.append(None)\n                continue\n            objs[a] = ev[2]\n            top[r] = a + ev[2]\n            out.append(a)\n        elif op == 'start':\n            tams = dict(top)\n            marked = set(marked)\n        elif op == 'mark':\n            marked.add(ev[1])\n        else:\n            dead = []\n            for a in sorted(objs):\n                r = a // region_size\n                if a < tams.get(r, r * region_size) and a not in marked:\n                    dead.append(a)\n            for a in dead:\n                del objs[a]\n            out.append(dead)\n    return out\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncases = [[('regression: objects above TAMS are implicitly live',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 21],\n     ['alloc', 1, 40],\n     ['start'],\n     ['alloc', 0, 10],\n     ['alloc', 2, 10],\n     ['mark', 0],\n     ['end']]),\n   [0, 30, 100, 51, 200, [30, 100]]),\n  ('first object allocated after marking started',\n   (100, [['alloc', 0, 30], ['alloc', 0, 21], ['alloc', 1, 40], ['start'], ['alloc', 1, 6], ['end']]),\n   [0, 30, 100, 140, [0, 30, 100]]),\n  ('region untouched when marking started',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 21],\n     ['alloc', 1, 40],\n     ['start'],\n     ['alloc', 3, 20],\n     ['alloc', 3, 5],\n     ['end']]),\n   [0, 30, 100, 300, 320, [0, 30, 100]]),\n  ('second cycle uses fresh TAMS and marks',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 21],\n     ['alloc', 1, 40],\n     ['start'],\n     ['mark', 0],\n     ['alloc', 0, 5],\n     ['end'],\n     ['start'],\n     ['mark', 30],\n     ['end']]),\n   [0, 30, 100, 51, [30, 100], [0, 51]]),\n  ('marks from the previous cycle are discarded',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 21],\n     ['alloc', 1, 40],\n     ['start'],\n     ['mark', 0],\n     ['mark', 100],\n     ['end'],\n     ['start'],\n     ['end']]),\n   [0, 30, 100, [30], [0, 100]]),\n  ('control: allocation beyond the region',\n   (100, [['alloc', 0, 90], ['alloc', 0, 21], ['start'], ['end']]),\n   [0, None, [0]])],\n [('regression: objects above TAMS are implicitly live',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 22],\n     ['alloc', 1, 40],\n     ['start'],\n     ['alloc', 0, 10],\n     ['alloc', 2, 10],\n     ['mark', 0],\n     ['end']]),\n   [0, 30, 100, 52, 200, [30, 100]]),\n  ('first object allocated after marking started',\n   (100, [['alloc', 0, 30], ['alloc', 0, 22], ['alloc', 1, 40], ['start'], ['alloc', 1, 7], ['end']]),\n   [0, 30, 100, 140, [0, 30, 100]]),\n  ('region untouched when marking started',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 22],\n     ['alloc', 1, 40],\n     ['start'],\n     ['alloc', 3, 20],\n     ['alloc', 3, 5],\n     ['end']]),\n   [0, 30, 100, 300, 320, [0, 30, 100]]),\n  ('second cycle uses fresh TAMS and marks',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 22],\n     ['alloc', 1, 40],\n     ['start'],\n     ['mark', 0],\n     ['alloc', 0, 5],\n     ['end'],\n     ['start'],\n     ['mark', 30],\n     ['end']]),\n   [0, 30, 100, 52, [30, 100], [0, 52]]),\n  ('marks from the previous cycle are discarded',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 22],\n     ['alloc', 1, 40],\n     ['start'],\n     ['mark', 0],\n     ['mark', 100],\n     ['end'],\n     ['start'],\n     ['end']]),\n   [0, 30, 100, [30], [0, 100]]),\n  ('control: allocation beyond the region',\n   (100, [['alloc', 0, 90], ['alloc', 0, 22], ['start'], ['end']]),\n   [0, None, [0]])],\n [('regression: objects above TAMS are implicitly live',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 23],\n     ['alloc', 1, 40],\n     ['start'],\n     ['alloc', 0, 10],\n     ['alloc', 2, 10],\n     ['mark', 0],\n     ['end']]),\n   [0, 30, 100, 53, 200, [30, 100]]),\n  ('first object allocated after marking started',\n   (100, [['alloc', 0, 30], ['alloc', 0, 23], ['alloc', 1, 40], ['start'], ['alloc', 1, 8], ['end']]),\n   [0, 30, 100, 140, [0, 30, 100]]),\n  ('region untouched when marking started',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 23],\n     ['alloc', 1, 40],\n     ['start'],\n     ['alloc', 3, 20],\n     ['alloc', 3, 5],\n     ['end']]),\n   [0, 30, 100, 300, 320, [0, 30, 100]]),\n  ('second cycle uses fresh TAMS and marks',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 23],\n     ['alloc', 1, 40],\n     ['start'],\n     ['mark', 0],\n     ['alloc', 0, 5],\n     ['end'],\n     ['start'],\n     ['mark', 30],\n     ['end']]),\n   [0, 30, 100, 53, [30, 100], [0, 53]]),\n  ('marks from the previous cycle are discarded',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 23],\n     ['alloc', 1, 40],\n     ['start'],\n     ['mark', 0],\n     ['mark', 100],\n     ['end'],\n     ['start'],\n     ['end']]),\n   [0, 30, 100, [30], [0, 100]]),\n  ('control: allocation beyond the region',\n   (100, [['alloc', 0, 90], ['alloc', 0, 23], ['start'], ['end']]),\n   [0, None, [0]])],\n [('regression: objects above TAMS are implicitly live',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 24],\n     ['alloc', 1, 40],\n     ['start'],\n     ['alloc', 0, 10],\n     ['alloc', 2, 10],\n     ['mark', 0],\n     ['end']]),\n   [0, 30, 100, 54, 200, [30, 100]]),\n  ('first object allocated after marking started',\n   (100, [['alloc', 0, 30], ['alloc', 0, 24], ['alloc', 1, 40], ['start'], ['alloc', 1, 9], ['end']]),\n   [0, 30, 100, 140, [0, 30, 100]]),\n  ('region untouched when marking started',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 24],\n     ['alloc', 1, 40],\n     ['start'],\n     ['alloc', 3, 20],\n     ['alloc', 3, 5],\n     ['end']]),\n   [0, 30, 100, 300, 320, [0, 30, 100]]),\n  ('second cycle uses fresh TAMS and marks',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 24],\n     ['alloc', 1, 40],\n     ['start'],\n     ['mark', 0],\n     ['alloc', 0, 5],\n     ['end'],\n     ['start'],\n     ['mark', 30],\n     ['end']]),\n   [0, 30, 100, 54, [30, 100], [0, 54]]),\n  ('marks from the previous cycle are discarded',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 24],\n     ['alloc', 1, 40],\n     ['start'],\n     ['mark', 0],\n     ['mark', 100],\n     ['end'],\n     ['start'],\n     ['end']]),\n   [0, 30, 100, [30], [0, 100]]),\n  ('control: allocation beyond the region',\n   (100, [['alloc', 0, 90], ['alloc', 0, 24], ['start'], ['end']]),\n   [0, None, [0]])],\n [('regression: objects above TAMS are implicitly live',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 25],\n     ['alloc', 1, 40],\n     ['start'],\n     ['alloc', 0, 10],\n     ['alloc', 2, 10],\n     ['mark', 0],\n     ['end']]),\n   [0, 30, 100, 55, 200, [30, 100]]),\n  ('first object allocated after marking started',\n   (100, [['alloc', 0, 30], ['alloc', 0, 25], ['alloc', 1, 40], ['start'], ['alloc', 1, 10], ['end']]),\n   [0, 30, 100, 140, [0, 30, 100]]),\n  ('region untouched when marking started',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 25],\n     ['alloc', 1, 40],\n     ['start'],\n     ['alloc', 3, 20],\n     ['alloc', 3, 5],\n     ['end']]),\n   [0, 30, 100, 300, 320, [0, 30, 100]]),\n  ('second cycle uses fresh TAMS and marks',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 25],\n     ['alloc', 1, 40],\n     ['start'],\n     ['mark', 0],\n     ['alloc', 0, 5],\n     ['end'],\n     ['start'],\n     ['mark', 30],\n     ['end']]),\n   [0, 30, 100, 55, [30, 100], [0, 55]]),\n  ('marks from the previous cycle are discarded',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 25],\n     ['alloc', 1, 40],\n     ['start'],\n     ['mark', 0],\n     ['mark', 100],\n     ['end'],\n     ['start'],\n     ['end']]),\n   [0, 30, 100, [30], [0, 100]]),\n  ('control: allocation beyond the region',\n   (100, [['alloc', 0, 90], ['alloc', 0, 25], ['start'], ['end']]),\n   [0, None, [0]])]]\nfor label, args, expected in cases[N - 1]:\n    check(label, solve(*args), expected)\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"},"fixed":{"sha256":"08733f1667198471e1e446d147e2172eea74560fe0cd79ca20982aef24699465","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(region_size, events):\n    top = {}\n    tams = {}\n    marked = set()\n    objs = {}\n    out = []\n    for ev in events:\n        op = ev[0]\n        if op == 'alloc':\n            r = ev[1]\n            a = top.get(r, r * region_size)\n            if a + ev[2] > (r + 1) * region_size:\n                out.append(None)\n                continue\n            objs[a] = ev[2]\n            top[r] = a + ev[2]\n            out.append(a)\n        elif op == 'start':\n            tams = dict(top)\n            marked = set()\n        elif op == 'mark':\n            marked.add(ev[1])\n        else:\n            dead = []\n            for a in sorted(objs):\n                r = a // region_size\n                if a < tams.get(r, r * region_size) and a not in marked:\n                    dead.append(a)\n            for a in dead:\n                del objs[a]\n            out.append(dead)\n    return out\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncases = [[('regression: objects above TAMS are implicitly live',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 21],\n     ['alloc', 1, 40],\n     ['start'],\n     ['alloc', 0, 10],\n     ['alloc', 2, 10],\n     ['mark', 0],\n     ['end']]),\n   [0, 30, 100, 51, 200, [30, 100]]),\n  ('first object allocated after marking started',\n   (100, [['alloc', 0, 30], ['alloc', 0, 21], ['alloc', 1, 40], ['start'], ['alloc', 1, 6], ['end']]),\n   [0, 30, 100, 140, [0, 30, 100]]),\n  ('region untouched when marking started',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 21],\n     ['alloc', 1, 40],\n     ['start'],\n     ['alloc', 3, 20],\n     ['alloc', 3, 5],\n     ['end']]),\n   [0, 30, 100, 300, 320, [0, 30, 100]]),\n  ('second cycle uses fresh TAMS and marks',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 21],\n     ['alloc', 1, 40],\n     ['start'],\n     ['mark', 0],\n     ['alloc', 0, 5],\n     ['end'],\n     ['start'],\n     ['mark', 30],\n     ['end']]),\n   [0, 30, 100, 51, [30, 100], [0, 51]]),\n  ('marks from the previous cycle are discarded',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 21],\n     ['alloc', 1, 40],\n     ['start'],\n     ['mark', 0],\n     ['mark', 100],\n     ['end'],\n     ['start'],\n     ['end']]),\n   [0, 30, 100, [30], [0, 100]]),\n  ('control: allocation beyond the region',\n   (100, [['alloc', 0, 90], ['alloc', 0, 21], ['start'], ['end']]),\n   [0, None, [0]])],\n [('regression: objects above TAMS are implicitly live',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 22],\n     ['alloc', 1, 40],\n     ['start'],\n     ['alloc', 0, 10],\n     ['alloc', 2, 10],\n     ['mark', 0],\n     ['end']]),\n   [0, 30, 100, 52, 200, [30, 100]]),\n  ('first object allocated after marking started',\n   (100, [['alloc', 0, 30], ['alloc', 0, 22], ['alloc', 1, 40], ['start'], ['alloc', 1, 7], ['end']]),\n   [0, 30, 100, 140, [0, 30, 100]]),\n  ('region untouched when marking started',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 22],\n     ['alloc', 1, 40],\n     ['start'],\n     ['alloc', 3, 20],\n     ['alloc', 3, 5],\n     ['end']]),\n   [0, 30, 100, 300, 320, [0, 30, 100]]),\n  ('second cycle uses fresh TAMS and marks',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 22],\n     ['alloc', 1, 40],\n     ['start'],\n     ['mark', 0],\n     ['alloc', 0, 5],\n     ['end'],\n     ['start'],\n     ['mark', 30],\n     ['end']]),\n   [0, 30, 100, 52, [30, 100], [0, 52]]),\n  ('marks from the previous cycle are discarded',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 22],\n     ['alloc', 1, 40],\n     ['start'],\n     ['mark', 0],\n     ['mark', 100],\n     ['end'],\n     ['start'],\n     ['end']]),\n   [0, 30, 100, [30], [0, 100]]),\n  ('control: allocation beyond the region',\n   (100, [['alloc', 0, 90], ['alloc', 0, 22], ['start'], ['end']]),\n   [0, None, [0]])],\n [('regression: objects above TAMS are implicitly live',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 23],\n     ['alloc', 1, 40],\n     ['start'],\n     ['alloc', 0, 10],\n     ['alloc', 2, 10],\n     ['mark', 0],\n     ['end']]),\n   [0, 30, 100, 53, 200, [30, 100]]),\n  ('first object allocated after marking started',\n   (100, [['alloc', 0, 30], ['alloc', 0, 23], ['alloc', 1, 40], ['start'], ['alloc', 1, 8], ['end']]),\n   [0, 30, 100, 140, [0, 30, 100]]),\n  ('region untouched when marking started',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 23],\n     ['alloc', 1, 40],\n     ['start'],\n     ['alloc', 3, 20],\n     ['alloc', 3, 5],\n     ['end']]),\n   [0, 30, 100, 300, 320, [0, 30, 100]]),\n  ('second cycle uses fresh TAMS and marks',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 23],\n     ['alloc', 1, 40],\n     ['start'],\n     ['mark', 0],\n     ['alloc', 0, 5],\n     ['end'],\n     ['start'],\n     ['mark', 30],\n     ['end']]),\n   [0, 30, 100, 53, [30, 100], [0, 53]]),\n  ('marks from the previous cycle are discarded',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 23],\n     ['alloc', 1, 40],\n     ['start'],\n     ['mark', 0],\n     ['mark', 100],\n     ['end'],\n     ['start'],\n     ['end']]),\n   [0, 30, 100, [30], [0, 100]]),\n  ('control: allocation beyond the region',\n   (100, [['alloc', 0, 90], ['alloc', 0, 23], ['start'], ['end']]),\n   [0, None, [0]])],\n [('regression: objects above TAMS are implicitly live',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 24],\n     ['alloc', 1, 40],\n     ['start'],\n     ['alloc', 0, 10],\n     ['alloc', 2, 10],\n     ['mark', 0],\n     ['end']]),\n   [0, 30, 100, 54, 200, [30, 100]]),\n  ('first object allocated after marking started',\n   (100, [['alloc', 0, 30], ['alloc', 0, 24], ['alloc', 1, 40], ['start'], ['alloc', 1, 9], ['end']]),\n   [0, 30, 100, 140, [0, 30, 100]]),\n  ('region untouched when marking started',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 24],\n     ['alloc', 1, 40],\n     ['start'],\n     ['alloc', 3, 20],\n     ['alloc', 3, 5],\n     ['end']]),\n   [0, 30, 100, 300, 320, [0, 30, 100]]),\n  ('second cycle uses fresh TAMS and marks',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 24],\n     ['alloc', 1, 40],\n     ['start'],\n     ['mark', 0],\n     ['alloc', 0, 5],\n     ['end'],\n     ['start'],\n     ['mark', 30],\n     ['end']]),\n   [0, 30, 100, 54, [30, 100], [0, 54]]),\n  ('marks from the previous cycle are discarded',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 24],\n     ['alloc', 1, 40],\n     ['start'],\n     ['mark', 0],\n     ['mark', 100],\n     ['end'],\n     ['start'],\n     ['end']]),\n   [0, 30, 100, [30], [0, 100]]),\n  ('control: allocation beyond the region',\n   (100, [['alloc', 0, 90], ['alloc', 0, 24], ['start'], ['end']]),\n   [0, None, [0]])],\n [('regression: objects above TAMS are implicitly live',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 25],\n     ['alloc', 1, 40],\n     ['start'],\n     ['alloc', 0, 10],\n     ['alloc', 2, 10],\n     ['mark', 0],\n     ['end']]),\n   [0, 30, 100, 55, 200, [30, 100]]),\n  ('first object allocated after marking started',\n   (100, [['alloc', 0, 30], ['alloc', 0, 25], ['alloc', 1, 40], ['start'], ['alloc', 1, 10], ['end']]),\n   [0, 30, 100, 140, [0, 30, 100]]),\n  ('region untouched when marking started',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 25],\n     ['alloc', 1, 40],\n     ['start'],\n     ['alloc', 3, 20],\n     ['alloc', 3, 5],\n     ['end']]),\n   [0, 30, 100, 300, 320, [0, 30, 100]]),\n  ('second cycle uses fresh TAMS and marks',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 25],\n     ['alloc', 1, 40],\n     ['start'],\n     ['mark', 0],\n     ['alloc', 0, 5],\n     ['end'],\n     ['start'],\n     ['mark', 30],\n     ['end']]),\n   [0, 30, 100, 55, [30, 100], [0, 55]]),\n  ('marks from the previous cycle are discarded',\n   (100,\n    [['alloc', 0, 30],\n     ['alloc', 0, 25],\n     ['alloc', 1, 40],\n     ['start'],\n     ['mark', 0],\n     ['mark', 100],\n     ['end'],\n     ['start'],\n     ['end']]),\n   [0, 30, 100, [30], [0, 100]]),\n  ('control: allocation beyond the region',\n   (100, [['alloc', 0, 90], ['alloc', 0, 25], ['start'], ['end']]),\n   [0, None, [0]])]]\nfor label, args, expected in cases[N - 1]:\n    check(label, solve(*args), expected)\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":"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.","method":"Deterministic executable model with adversarial boundary fixtures.","provenance":{"created_by":"Failure Map","dependencies":"Python standard library","family":"w2-garbage-collector-invariants-top-at-mark-start-mark-reset","generated_at":"2026-09-29T14:51:29.912245+00:00","license":"CC0-1.0","python":"3.12.14","seed":1,"split":"open-access"},"relevance":"Snapshot collectors treat objects allocated during marking as live using a per-region watermark.","repair":"Clear all marks when a marking cycle starts.","root_cause":"Starting a cycle copies the previous mark set instead of clearing it.","sha256":"a5d88b83b1c6b7d5f35d076a47abcf2cdcd12e1602ecdfcde24de010158f443c","title":"TAMS: marks carried over into the next cycle · case 01","variant":1,"variant_policy":"Five numbered records share a model and may reuse boundary fixtures.","verification":{"attempt":{"elapsed_ms":41.086,"exit_code":1,"observations":[{"actual":[0,30,100,51,200,[30,100]],"check":"regression: objects above TAMS are implicitly live","expected":[0,30,100,51,200,[30,100]],"passed":true},{"actual":[0,30,100,140,[0,30,100]],"check":"first object allocated after marking started","expected":[0,30,100,140,[0,30,100]],"passed":true},{"actual":[0,30,100,300,320,[0,30,100]],"check":"region untouched when marking started","expected":[0,30,100,300,320,[0,30,100]],"passed":true},{"actual":[0,30,100,51,[30,100],[51]],"check":"second cycle uses fresh TAMS and marks","expected":[0,30,100,51,[30,100],[0,51]],"passed":false},{"actual":[0,30,100,[30],[]],"check":"marks from the previous cycle are discarded","expected":[0,30,100,[30],[0,100]],"passed":false},{"actual":[0,null,[0]],"check":"control: allocation beyond the region","expected":[0,null,[0]],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"regression: objects above TAMS are implicitly live\", \"actual\": [0, 30, 100, 51, 200, [30, 100]], \"expected\": [0, 30, 100, 51, 200, [30, 100]], \"passed\": true}, {\"check\": \"first object allocated after marking started\", \"actual\": [0, 30, 100, 140, [0, 30, 100]], \"expected\": [0, 30, 100, 140, [0, 30, 100]], \"passed\": true}, {\"check\": \"region untouched when marking started\", \"actual\": [0, 30, 100, 300, 320, [0, 30, 100]], \"expected\": [0, 30, 100, 300, 320, [0, 30, 100]], \"passed\": true}, {\"check\": \"second cycle uses fresh TAMS and marks\", \"actual\": [0, 30, 100, 51, [30, 100], [51]], \"expected\": [0, 30, 100, 51, [30, 100], [0, 51]], \"passed\": false}, {\"check\": \"marks from the previous cycle are discarded\", \"actual\": [0, 30, 100, [30], []], \"expected\": [0, 30, 100, [30], [0, 100]], \"passed\": false}, {\"check\": \"control: allocation beyond the region\", \"actual\": [0, null, [0]], \"expected\": [0, null, [0]], \"passed\": true}], \"passed\": false}\n"},"broken":{"elapsed_ms":39.263,"exit_code":1,"observations":[{"actual":[0,30,100,51,200,[30,100]],"check":"regression: objects above TAMS are implicitly live","expected":[0,30,100,51,200,[30,100]],"passed":true},{"actual":[0,30,100,140,[0,30,100]],"check":"first object allocated after marking started","expected":[0,30,100,140,[0,30,100]],"passed":true},{"actual":[0,30,100,300,320,[0,30,100]],"check":"region untouched when marking started","expected":[0,30,100,300,320,[0,30,100]],"passed":true},{"actual":[0,30,100,51,[30,100],[51]],"check":"second cycle uses fresh TAMS and marks","expected":[0,30,100,51,[30,100],[0,51]],"passed":false},{"actual":[0,30,100,[30],[]],"check":"marks from the previous cycle are discarded","expected":[0,30,100,[30],[0,100]],"passed":false},{"actual":[0,null,[0]],"check":"control: allocation beyond the region","expected":[0,null,[0]],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"regression: objects above TAMS are implicitly live\", \"actual\": [0, 30, 100, 51, 200, [30, 100]], \"expected\": [0, 30, 100, 51, 200, [30, 100]], \"passed\": true}, {\"check\": \"first object allocated after marking started\", \"actual\": [0, 30, 100, 140, [0, 30, 100]], \"expected\": [0, 30, 100, 140, [0, 30, 100]], \"passed\": true}, {\"check\": \"region untouched when marking started\", \"actual\": [0, 30, 100, 300, 320, [0, 30, 100]], \"expected\": [0, 30, 100, 300, 320, [0, 30, 100]], \"passed\": true}, {\"check\": \"second cycle uses fresh TAMS and marks\", \"actual\": [0, 30, 100, 51, [30, 100], [51]], \"expected\": [0, 30, 100, 51, [30, 100], [0, 51]], \"passed\": false}, {\"check\": \"marks from the previous cycle are discarded\", \"actual\": [0, 30, 100, [30], []], \"expected\": [0, 30, 100, [30], [0, 100]], \"passed\": false}, {\"check\": \"control: allocation beyond the region\", \"actual\": [0, null, [0]], \"expected\": [0, null, [0]], \"passed\": true}], \"passed\": false}\n"},"fixed":{"elapsed_ms":40.846,"exit_code":0,"observations":[{"actual":[0,30,100,51,200,[30,100]],"check":"regression: objects above TAMS are implicitly live","expected":[0,30,100,51,200,[30,100]],"passed":true},{"actual":[0,30,100,140,[0,30,100]],"check":"first object allocated after marking started","expected":[0,30,100,140,[0,30,100]],"passed":true},{"actual":[0,30,100,300,320,[0,30,100]],"check":"region untouched when marking started","expected":[0,30,100,300,320,[0,30,100]],"passed":true},{"actual":[0,30,100,51,[30,100],[0,51]],"check":"second cycle uses fresh TAMS and marks","expected":[0,30,100,51,[30,100],[0,51]],"passed":true},{"actual":[0,30,100,[30],[0,100]],"check":"marks from the previous cycle are discarded","expected":[0,30,100,[30],[0,100]],"passed":true},{"actual":[0,null,[0]],"check":"control: allocation beyond the region","expected":[0,null,[0]],"passed":true}],"passed":true,"stderr":"","stdout":"{\"observations\": [{\"check\": \"regression: objects above TAMS are implicitly live\", \"actual\": [0, 30, 100, 51, 200, [30, 100]], \"expected\": [0, 30, 100, 51, 200, [30, 100]], \"passed\": true}, {\"check\": \"first object allocated after marking started\", \"actual\": [0, 30, 100, 140, [0, 30, 100]], \"expected\": [0, 30, 100, 140, [0, 30, 100]], \"passed\": true}, {\"check\": \"region untouched when marking started\", \"actual\": [0, 30, 100, 300, 320, [0, 30, 100]], \"expected\": [0, 30, 100, 300, 320, [0, 30, 100]], \"passed\": true}, {\"check\": \"second cycle uses fresh TAMS and marks\", \"actual\": [0, 30, 100, 51, [30, 100], [0, 51]], \"expected\": [0, 30, 100, 51, [30, 100], [0, 51]], \"passed\": true}, {\"check\": \"marks from the previous cycle are discarded\", \"actual\": [0, 30, 100, [30], [0, 100]], \"expected\": [0, 30, 100, [30], [0, 100]], \"passed\": true}, {\"check\": \"control: allocation beyond the region\", \"actual\": [0, null, [0]], \"expected\": [0, null, [0]], \"passed\": true}], \"passed\": true}\n"}},"verified":true,"visibility":"public"}