Execution counters, MR3 to depth 3, MR9 retired

Three times a path has looked tested and never executed: a corpus that never
reached a second attention split, a chunk-size row that never chunked, and an
admission check that made the eviction path unreachable. Each was caught by
noticing afterwards. engine/audit/counters.py makes it a mechanism: 26 declared
paths, incremented by the engine, and require_fired() turns a relation that
passes without firing its own mechanism into a failure. It generalizes what MR3
and MR4 were already doing by hand.

The counters are also the fuzzer's coverage substrate, so the coverage report
and the vacuity guards read the same numbers rather than two parallel sets.

MR3 now sweeps two dimensions: the preemption point across every decode step at
depth 1, and depths 2 and 3 explicitly. Depth matters because preempt-resume-
preempt is where allocator state gets interesting, a block freed by the first
preemption can be handed to another request and then be needed again by the
second. Depth 3 never being reached fails the relation.

MR9 is retired in the architecture doc with its reasoning rather than left
listed as pending: it assumes an explicit pad region and this engine packs
sequences, so there is nothing to mask. MR5 covers the occupancy intent.

Author: u7k4rs6

docs/02-technical-architecture.md

@@ -144,14 +144,14 @@ The alphabet in section 2, constrained by feasibility rules (cannot resume a req
 
 Three components, all reported. Coverage is what proves exploration rather than sampling the easy middle.
 
-1. **Lifecycle n-grams.** All feasible 2-grams and 3-grams of per-request events, reported as a percentage of the feasible set
+1. **Lifecycle n-grams.** All feasible 2-grams and 3-grams of per-request events, reported as a percentage of the feasible set. The feasible set is *derived* in `engine/sched/lifecycle.py` by search over a declared transition relation, never hand-listed: a hand-written set can reach 100 percent by having omitted the hard transitions and nothing in the number would show it. Every n-gram a real run produces is checked against the derived set, so a transition the table forgot fails loudly rather than being silently dropped
 2. **Boundary predicates**, each required at value, value minus 1, and value plus 1:
    - chunk end versus block size
    - cache-hit length versus block size (the live SGLang bug is literally `prefix_len == block_size`; make this the poster child)
    - split boundary versus KV length
    - batch size transitions across {1, 2, 3, 4, 8, 16, 31, 32}
    - free-block count in {0, 1, low}
-3. **Preemption depth** per request, up to 3
+3. **Preemption depth** per request, up to 3. MR3 sweeps the preemption point across every decode step at depth 1, and drives depths 2 and 3 explicitly, because preempt-resume-preempt is where allocator state gets interesting: a block freed by the first preemption can be reallocated to another request and then be needed again by the second
 
 ### 8.3 Generation strategy
 
@@ -173,9 +173,9 @@ ddmin (Zeller and Hildebrandt, IEEE TSE 2002) applied in three staged passes: re
 | MR6 | Replay. Identical inputs twice, identical trajectory hash |
 | MR7 | RNG isolation. Deleting request A leaves request B's tokens unchanged |
 | MR8 | Temperature-0 tie-break. Argmax stable under logit-preserving permutations of the batch |
-| MR9 | Mask no-op, fidelity-side. A fully-masked pad region changes nothing within tolerance |
+| MR9 | ~~Mask no-op, fidelity-side~~. **Retired.** The relation assumes an explicit pad region, and this engine packs sequences rather than padding them, so there is no masked region to be a no-op over. MR5 covers the occupancy intent: a cohabitant that only shifts where the packed token count lands against the GEMM tile must leave other requests bitwise unchanged |
 
-MR1 through MR8 run both in-process and black-box. MR9 is in-process only.
+MR1 through MR8 run both in-process and black-box. MR9 is retired; see its row.
 
 ## 10. Mutation testing
 

engine/audit/counters.py

@@ -0,0 +1,125 @@
+"""Execution counters over every path under claim.
+
+Three times now a path has looked tested and never executed: a corpus that never
+reached a second attention split, a chunk-size row that never chunked, and an
+admission check that made the eviction path unreachable. Each was caught by
+noticing afterwards. This makes it a mechanism.
+
+Every relation asserts not only its outcome but that the paths it exists to
+exercise had nonzero counts. A relation that passes without firing its own
+mechanism is a failure, not a pass.
+
+The counters are also the fuzzer's coverage substrate, so the coverage report and
+the vacuity guards read the same numbers. A coverage denominator derived from
+somewhere else than the thing being counted is how a coverage number ends up
+describing a denominator someone chose.
+
+Counters are observation only. They are incremented after a decision is taken,
+never read by one, and nothing in a kernel config path can see them: a counter
+that fed back into a decision would be a batch-derived quantity by another name.
+"""
+
+from __future__ import annotations
+
+from collections import Counter as _Counter
+from dataclasses import dataclass, field
+
+# Every path under claim, with the one-line statement of what firing it means.
+# The fuzzer's coverage report enumerates this dict rather than a hand-written
+# list, so a path added here is covered by both without a second edit.
+PATHS: dict[str, str] = {
+    # admission and lifecycle
+    "admit": "a waiting request was admitted",
+    "admit_refused": "the policy declined to admit a waiting request",
+    "finish": "a request reached its limit or an EOS and released its blocks",
+    # prefill and chunking
+    "prefill_chunk": "a partial prefill chunk was computed",
+    "prefill_complete": "a prefill finished and the request began decoding",
+    "decode_step": "a single-token decode step was computed",
+    "chunk_boundary_mid_block": "a chunk ended part-way through a KV block",
+    "chunk_boundary_mid_split": "a chunk ended part-way through an attention split",
+    "chunk_boundary_on_block": "a chunk ended exactly on a block boundary",
+    # attention shape
+    "attention_multi_split": "attention ran with two or more splits",
+    "attention_single_split": "attention ran within one split",
+    # preemption
+    "preempt_fired": "a running request was preempted for recompute",
+    "preempt_depth_2": "a request was preempted for the second time",
+    "preempt_depth_3_plus": "a request was preempted a third time or beyond",
+    "resume": "a preempted request was re-admitted and recomputed",
+    # prefix cache
+    "cache_hit": "a prefix hit was found and honoured",
+    "cache_hit_refused": "a prefix hit was found and the policy declined it",
+    "cache_miss": "a lookup found no usable prefix",
+    "cache_insert": "whole blocks were indexed after a request finished",
+    "cache_full_prompt_trimmed": "a whole-prompt hit gave its last block back",
+    # allocator
+    "eviction_taken": "a cached block was reclaimed under pressure",
+    "eviction_pass": "one pass of the reserve-with-eviction loop",
+    "cow_performed": "a shared block was copied on write",
+    "block_reclaimed_at_zero": "a block's last reference went away and it was freed",
+    "out_of_blocks": "the pool could not satisfy a reservation",
+}
+
+
+@dataclass
+class Counters:
+    """Per-run execution counts. Created by the Scheduler, shared with the pool.
+
+    Not a module global: a global would make one test's counts visible to the
+    next and would not survive the cross-process replay, where two interpreters
+    must produce identical trajectories.
+    """
+
+    counts: _Counter = field(default_factory=_Counter)
+
+    def hit(self, path: str, amount: int = 1) -> None:
+        if path not in PATHS:
+            raise KeyError(
+                f"{path!r} is not a declared path. Add it to PATHS with a "
+                "one-line statement of what firing it means, so the coverage "
+                "report enumerates it too."
+            )
+        self.counts[path] += amount
+
+    def __getitem__(self, path: str) -> int:
+        return self.counts.get(path, 0)
+
+    def fired(self, *paths: str) -> bool:
+        return all(self.counts.get(path, 0) > 0 for path in paths)
+
+    def missing(self, *paths: str) -> list[str]:
+        """Which of `paths` never fired. What a vacuity guard reports."""
+        return [path for path in paths if self.counts.get(path, 0) == 0]
+
+    def merge(self, other: "Counters") -> None:
+        self.counts.update(other.counts)
+
+    def as_dict(self) -> dict[str, int]:
+        return {path: self.counts.get(path, 0) for path in PATHS if self.counts.get(path, 0)}
+
+    def summary(self) -> str:
+        live = self.as_dict()
+        if not live:
+            return "no paths fired"
+        width = max(len(path) for path in live)
+        return "\n".join(f"  {path:<{width}}  {count}" for path, count in sorted(live.items()))
+
+
+class VacuousRun(AssertionError):
+    """A relation passed without firing the paths it exists to exercise."""
+
+
+def require_fired(counters: Counters, *paths: str, what: str = "this relation") -> None:
+    """Assert the mechanism actually ran. The generalization of the hand checks.
+
+    MR3 reported "7 of 10 actually preempted" and MR4 reported "12 of 12
+    registering real hits" by hand. This is that, for every relation.
+    """
+    missing = counters.missing(*paths)
+    if missing:
+        raise VacuousRun(
+            f"{what} passed without firing: {', '.join(missing)}. "
+            "A relation that never executes its own mechanism is not evidence. "
+            f"Paths that did fire: {sorted(counters.as_dict())}"
+        )

engine/cache/prefix.py

@@ -63,6 +63,7 @@ class PrefixCache:
     """
 
     block_size: int
+    counters: object = None
     entries: dict[bytes, CacheEntry] = field(default_factory=dict)
     stats: dict = field(
         default_factory=lambda: {"lookups": 0, "hit_blocks": 0, "inserts": 0, "evictions": 0}
@@ -102,6 +103,8 @@ def lookup(self, tokens: list[int]) -> tuple[int, list[int]]:
             entry.hits += 1
             blocks.append(entry.physical_block)
         self.stats["hit_blocks"] += len(blocks)
+        if self.counters is not None:
+            self.counters.hit("cache_hit" if blocks else "cache_miss")
         return len(blocks) * self.block_size, blocks
 
     def insert(self, tokens: list[int], block_ids: list[int], pool) -> int:
@@ -122,6 +125,8 @@ def insert(self, tokens: list[int], block_ids: list[int], pool) -> int:
             pool.pin(physical)
             created += 1
         self.stats["inserts"] += created
+        if created and self.counters is not None:
+            self.counters.hit("cache_insert", created)
         return created
 
     def evictable_blocks(self, pool) -> list[int]:
@@ -145,6 +150,8 @@ def evict(self, physical_block: int, pool) -> bool:
                 del self.entries[key]
                 pool.unpin(physical_block)
                 self.stats["evictions"] += 1
+                if self.counters is not None:
+                    self.counters.hit("eviction_taken")
                 return True
         return False
 

engine/kv/paged.py

@@ -35,6 +35,7 @@
 
 import torch
 
+from engine.audit.counters import Counters
 from engine.kernels import registry
 
 # Block size is configuration, not a constant, and it is parameterized now while
@@ -98,7 +99,9 @@ def __init__(
         dtype: torch.dtype = torch.float16,
         poison_on_free: bool = True,
         block_size: int = DEFAULT_BLOCK_SIZE,
+        counters: Counters | None = None,
     ):
+        self.counters = counters if counters is not None else Counters()
         if registry.KV_TILE % block_size != 0:
             raise ValueError(
                 f"block_size {block_size} does not divide the KV tile "
@@ -138,6 +141,7 @@ def free_blocks(self) -> int:
 
     def _take_block(self) -> int:
         if not self._free:
+            self.counters.hit("out_of_blocks")
             raise OutOfBlocks(
                 f"all {self.num_blocks} blocks are held; the policy must evict or "
                 "preempt before asking for more"
@@ -158,6 +162,7 @@ def _release_block(self, block: int) -> None:
                     self.v[layer][block].fill_(POISON)
             heapq.heappush(self._free, block)
             self.stats["freed"] += 1
+            self.counters.hit("block_reclaimed_at_zero")
 
     # -- sequences -----------------------------------------------------------
 
@@ -246,6 +251,7 @@ def ensure_writable(self, uid: str, logical_block: int) -> int:
         sequence.block_ids[logical_block] = new
         self.refcount[old] -= 1
         self.stats["cow_copies"] += 1
+        self.counters.hit("cow_performed")
         return new
 
     # -- views ---------------------------------------------------------------

engine/sched/policy.py

@@ -258,6 +258,31 @@ def should_preempt(self, state: SchedulerState, uid: str) -> bool:
         return True
 
 
+class PreemptAtStepsPolicy(DefaultPolicy):
+    """Preempt one request at several named steps, for depth sweeps.
+
+    Preemption depth is a coverage dimension in architecture doc 8.2, up to 3.
+    Depth matters because preempt-resume-preempt is where allocator state gets
+    interesting: a block freed by the first preemption can be reallocated to
+    another request and then be needed again by the second.
+    """
+
+    def __init__(self, uid: str, at_steps: tuple[int, ...], max_running: int = 32):
+        super().__init__(max_running=max_running)
+        self.uid = uid
+        self.at_steps = set(at_steps)
+        self.fired_at: list[int] = []
+        self.name = f"preempt({uid}@{sorted(at_steps)})"
+
+    def should_preempt(self, state: SchedulerState, uid: str) -> bool:
+        if uid != self.uid or state.step not in self.at_steps:
+            return False
+        if state.step in self.fired_at:
+            return False
+        self.fired_at.append(state.step)
+        return True
+
+
 class NoCacheHitPolicy(DefaultPolicy):
     """Refuse every prefix hit. The cold half of MR4."""