README.md

Garbage collection, the recovery log and the server GC primitive (formal verification effort)

Three Quint models.

• gc.qnt models mkit gc as specified in SPEC-GC: retention roots, the fail-closed requirement, recording to and expiring the recovery log, the expire → collect roots → prune sequence, the object grace window, and writers that do not hold gc's locks ("Concurrent writers and the grace window"). Locking follows SPEC-CONCURRENCY §3.1, §3.2 and §4. It is aligned with rust/crates/mkit-core/src/ops/gc.rs (collect_roots, live_objects, run_gc), ops/recovery.rs (record, expire, is_retained), store.rs (ObjectStore::write, BulkWriter::write, object_metadata, prune_if_old) and rust/crates/mkit-cli/src/commands/gc.rs, tag.rs, attest.rs.
• sweepRace.qnt refines the atomic sweep in gc.qnt: it separates the initial metadata read, exclusive lock, final metadata read, unlink and lock release. A writer holds a shared lock across its read and refresh or write. It covers process death before and after unlink, and cached-object reuse.
• contentIndex.qnt models the server-side GC primitive, rust/crates/mkit-server/src/store/content_index.rs ("GC ordering (R-64)", steps 1 to 4), against an upload of the same blob (mkit-server/src/fs/blob.rs). There is no normative text for it yet (SPEC-SERVER's server-GC section is WP-5.1a) and nothing calls collectable/commit_collect yet (the driver is WP-5.3a/b), so this model states the contract a future caller must meet rather than checking a shipped path.

Tool pins (verification toolchain)

Host for the timings below: macOS arm64, 15 cores, 24 GB, shared with five other verification jobs (load average 9 to 15). TLC ran with -Xmx4g and 2 workers, Apalache with -Xmx4g; one JVM at a time.

check.sh finds the tools at ${FV_HOME:-$HOME/.local/share/mkit-fv}/apalache-0.62.2/ (APALACHE_MC, TLA2TOOLS override), and Java at $JAVA_HOME, else /usr/libexec/java_home -v 21, else Homebrew's openjdk@21.

gc.qnt

Model

• gc runs through GcLock, GcExpireRead, GcExpireWrite, GcMark, GcSweep(o) (one listed object per step) and GcDone. GcLock takes worktrees.lock plus every worktree.lock (SPEC-CONCURRENCY §4), then reads now (commands/gc.rs reads the clock after the locks and before expire, as SPEC-GC now requires). Expire is split into a read step and a rewrite step because expire reads, filters and then atomically rewrites the log; the log is rewritten only when the snapshot dropped entries (pruned == 0). is_retained is "age ≤ grace or among the last keep_last", as in recovery.rs. GcMark runs the strict collect_roots plus the closure: an unreadable root source, or a closure object missing from the store (ObjectNotFound), aborts before anything is deleted. Each sweep step reads that object's mtime and deletes it if it is unreachable and now - mtime >= GRACE.
• Producer (amend/reset/rebase on main): ProdBegin, ProdRecord, ProdMove under its tree's worktree.lock. It writes the new tip's objects, records the superseded tip (record is durable, so one step), then moves the ref.
• Writer outside gc's lock set (PushWrite then PushPublish, or PushAbort): writes all of the tip's objects into the store gc sweeps and later publishes a root. It takes none of gc's locks. On this branch that writer is the import phase of mkit git import/fetch/pull (BulkWriter under git-<remote>.lock only). See "Which writers race gc" below for why file-transport and served pushes are not.
• Later root publish under the lock (TagPublish, TAG_CHECK): one step under this tree's worktree.lock that re-verifies its target and publishes a root, as tag <name> <hash>, attest and update-ref do (#267).
• Environment: Tick(d); Corrupt(s)/Repair(s) for the root sources main, tag, pushed and rlog.
• Objects: 8 objects in a fixed DAG. Objects 5 and 7 start as old orphans; 5 is in the writer's closure, 7 is garbage nobody writes, so a gc can delete something while a writer is in flight. Writes are content-addressed: a dedup hit leaves the existing mtime unchanged unless FRESHEN is set. The model's writer is the one outside gc's lock set, git import. FRESHEN = true is the implementation since MKIT-55: BulkWriter::write (byte-equal existing file), the writer git import uses, sets the existing file's mtime to now on a dedup hit, and rewrites the object if it cannot. FRESHEN = false is the implementation before MKIT-55. ObjectStore::write and WriteBatch do not refresh mtime; their callers hold worktree.lock, which gc also takes, so they are not the model's writer.

Bounds: 8 objects, 3 refs plus the recovery log, 1 producer, 1 writer, 1 tag publisher, clock 0..6, GRACE = 2 (0 in gcGrace0), RETAIN = 2, KEEP_LAST = 1, at most 3 recovery records. quint run: 20000 samples of up to 30 steps, seed 0x1. Apalache: safe instances to length 8, mutants and canaries at (or above) the length of their shortest counterexample. TLC: every reachable state of the instance under the stated CONSTRAINT (see Results).

The TLC runs use a VIEW that drops only state no guard and no Safety or Progress conjunct reads (counters, lastAction, gc scratch outside the phase that reads it, mtimes of absent objects, pushStart outside "wrote"). This is sound for Safety, Progress and their conjuncts, not for the canaries, which are checked with quint run and Apalache.

Invariants

Safety is the conjunction of the first five, Progress of the last two, and All = Safety and Progress. Progress is stated as invariants because TLC's deadlock check (-deadlock/CHECK_DEADLOCK FALSE) would be vacuous here in any case: Corrupt/Repair are always enabled. gc and producer steps are guarded by their phase alone, so the non-trivial stuck states are a leaked lock and a writer with no enabled step.

Canaries (each must be violated): CanaryNoPrune, CanaryNoAbort, CanaryNoExpire, CanaryNoPrunedRecord, CanaryNoPushPublished, CanaryNoPruneDuringPush, CanaryNoPrunedPushPublished (gc deletes an object while a writer is in flight and that writer then publishes; pinned by prunedDuringSafePushTest), CanaryNoYoungOverPruned (gc keeps a young object and deletes an old one in its closure), CanaryNoTagPublished.

GC vs. a writer outside gc's lock set (SPEC-GC "Concurrent writers and the grace window")

Safety condition. A publish at instant T by a writer outside gc's lock set cannot lose an object iff every object it makes newly reachable (not reachable from roots that stay unchanged during the gc run) is present at T with on-disk mtime > T - GRACE. gcPushBounded checks sufficiency of exactly this form; necessity is shown by counterexamples (mutBoundedLax at the boundary, gcPushFast, gcPushRaw*), not proved in general. It works because gc reads now before its mark, so a gc whose mark precedes the publish has now ≤ T, and the other roots are frozen during a gc run (producers are excluded, expire precedes mark). The writer's duration bounds this only when a dedup hit refreshes mtime (gcPushFastFreshen). The root model's GcSweep(o) reads o's mtime and deletes o in one step. sweepRace.qnt checks the refinement to the implementation's separate metadata reads and unlink: a final re-stat under an exclusive store lock excludes the writer's shared lock across refresh or write. The initial unlocked metadata read only selects candidates. --grace-secs 0 is never safe against such a writer. This is the condition SPEC-GC now states as normative.

Split metadata read and unlink (sweepRace.qnt)

The focused model starts with one old unreferenced loose object. Gc records now and whether the object is live, reads its mtime without the store lock, and selects a candidate. It then takes the exclusive store lock, re-reads mtime and unlinks only if the object is still old. A single writer takes the shared lock across the existing-file read and refresh (including map-cache reuse), or across an atomic new-object write. Ref publication occurs after the shared lock is released. A busy lock or failed final metadata read keeps the candidate. The one-writer bound abstracts exclusion between gc and any shared holder; it does not establish writer throughput or fairness.

refreshBetweenReadAndUnlinkTest and staleReadLossTest run the same interleaving against the fix and the stale-check mutant. The missing-lock mutant refreshes after the final check. crashBeforeUnlinkTest releases the kernel lock with the canonical object present; crashAfterUnlinkTest releases it after an old unmarked object was removed and a later writer recreates the object. No trash path or recovery namespace exists. Writer process death likewise releases its shared lock. Filesystem power-loss semantics, lock API portability and fsync ordering require the Rust tests and code review; this model checks process death and interleaving only.

NoRecentPruned forbids a deletion within GRACE of the actual on-disk mtime at deletion time. NoLivePruned, NoDangling and NoLeakedLock complete All. Canaries require pruning, publication after pruning (with a later rewrite), and crashes on both sides of unlink to remain reachable. Bounds: one object, one import run, arbitrarily repeated gc runs, clock 0..5, GRACE = 2 except the zero-grace instance. This refines the object-level step in gc.qnt; it does not add the full root DAG to the small race model.

Later root publish under the lock (gcTagRoot, gcTagClosure)

The grace window is per object, not per closure. A young unreachable object survives a gc while an old object in its closure is deleted (Git, by contrast, keeps objects reachable from recent unreachable objects). CanaryNoYoungOverPruned shows the state is reachable in the supported deployment: a writer that wrote a tip and its closure and never published (a crash, an error, or the abandoned import in PushAbort) leaves the young tip 6 over the old dedup-hit 5. A later mkit tag <name> <hash> (or attest, update-ref) takes its lock, so no gc runs concurrently, but re-verifies only the target itself (store.contains). gcTagRoot publishes a root whose closure is incomplete (tagAfterGraceTest, NoDangling violated). Checking the closure under the lock (gcTagClosure) is safe: the lock excludes gc, so a closure present under the lock stays present until the publish.

Which writers race gc (server-era review)

• git-bridge import: mkit git import/fetch/pull writes loose objects through BulkWriter and publishes tags and remote-tracking refs under git-<remote>.lock only (git_import.rs), outside gc's lock set. BulkWriter::write refreshes the mtime of a byte-equal existing object; map-cache reuse now refreshes through the same path, once per object per import run. The final locked gc re-stat closes the read/unlink race. With a write-or-refresh-to-publish interval strictly shorter than GRACE, this is gcPushFastFreshen, refined by sweepFixed. A run that exceeds that interval still has the gcPushRawFreshen residue; zero grace is unsafe against an import even when no time passes. Refreshing once per run does not extend the grace window throughout a long import.
• File-transport and served pushes do not race mkit gc on this branch. FileTransport and mkit serve/mkit-server (FsBlobStore, FsLayoutStore) store <root>/packs/<64-hex> and <root>/refs/.... mkit gc sweeps only loose objects in <root>/.mkit/objects/<2>/<62> (iter_object_hashes) and collects roots only under <root>/.mkit (RepoLayout has no bare form). The sets are disjoint, so gc cannot delete a pushed object, and a pushed ref is not one of its roots. SPEC-GC's "Concurrent writers" section and SPEC-CONCURRENCY §3.1 now say so.
• mkit serve's startup sweep (FsBlobStore::sweep_stale_uploads, under an exclusive non-blocking serve.lock, SPEC-CONCURRENCY §2, §3.1) removes only regular files named exactly .<64-hex>.tmp.<pid>.<seq> in packs/ with mtime at least 1 h old. It never removes a blob or a ref, so it cannot make a published object dangle. Its only effect on a concurrent writer is on liveness: a FileTransport upload (no serve.lock) whose temp file is older than 1 h at its rename gets ENOENT and fails before it publishes anything. mkit serve's doc says FileTransport writes "each temp file in one go" (true: write_atomic is create, write_all, fsync, rename), so this needs a writer stalled for an hour inside that sequence. Not modelled.
• pack::rewrite_excluding (WP-5.7a) is a pure function over pack bytes with no I/O and no callers outside tests. It cannot delete anything; the takedown flow that would publish its output is WP-5.7b. Not modelled.
• ContentIndex GC (R-64) can delete bytes a concurrent upload relies on, depending on the caller's ordering: modelled in contentIndex.qnt below.

contentIndex.qnt

One object, one upload, one GC. The upload takes a hold (add_hold, refused while deleting), writes or dedups the bytes (AlreadyPresent/Created), applies the ref-shard write with NotAfter = hold time + APPLY_WINDOW or gives up and releases the hold; the relay records the holder row and releases the hold within RELAY_LAG of the apply (an assumption on time). GC runs collectable (no holders, no live hold, now - changed >= GRACE), commit_collect (guarded by Equals on the state row), the blob delete and finish_collect; it may crash after the mark and resume at the delete. Every index mutation bumps seq, sets changed = max(changed, now) and prunes an expired hold, as mutate does. Bounds: clock 0..7, GRACE = 2, TTL = 3, APPLY_WINDOW = 1, RELAY_LAG = 1 unless stated.

Canaries (violated): CanaryNoDelete, CanaryNoPublish, CanaryNoHolder, CanaryNoDeleteThenPublish (GC deletes the old blob and the upload still publishes, after its refused hold is retried: gcFirstTest).

Contract for a caller of the R-64 primitive (checked, bounded):

1. Take the hold before relying on the bytes, that is before the AlreadyPresent dedup or the blob write. With the bytes first (ciBytesFirst, dedupThenCollectTest), a whole GC cycle (plan, mark, delete, clear) fits between the dedup and the hold, the hold then succeeds, and the apply publishes a lost object. add_hold's doc says only "taken before the ref-shard apply", which permits this order.
2. From the hold, GC is kept off the object until max(hold expiry, last change + GRACE); the apply is a ref-shard write and does not touch the state row. So APPLY_WINDOW + RELAY_LAG < max(TTL, GRACE) is needed: ciShortTtl (TTL = GRACE = 2 = window + lag) loses the object; ciShortTtlGrace (GRACE = 3) and ciHoldFirst (TTL = 3) are safe. The add_hold doc states the TTL half ("TTL must exceed MAX_APPLY_WINDOW plus the relay-lag bound").
3. The primitive's own guards are load-bearing: without the deleting refusal (ciMutNoDeletingGuard) or the Equals guard on the plan (ciMutNoSeqGuard) the object is lost even with the right ordering.

The R-64 driver's root re-check and relay watermark wait are not modelled (not implemented yet).

Results

Split-sweep refinement (2026-10-18). The default ./check.sh run exits 0: every existing root-model and ContentIndex check, all six focused scenario modules, the fixed invariant and four focused canaries match their expected outcomes. ONLY=sweep TLC=1 ./check.sh also exits 0. TLC exhausts 4,832 distinct states for sweepFixed::All with no violation; all six unsafe variants/checks produce the expected named violations. The fixed model uses one object, one writer, clock 0..5 and GRACE = 2.

Apalache 0.62.2 checks sweepFixed::All through length 12 successfully. It finds the expected violations for sweepSplit::NoDangling, sweepNoLock::NoRecentPruned, sweepNoRefresh::NoDangling, sweepSlow::NoDangling and sweepGrace0::NoDangling at respective bounds 12, 11, 12, 12 and 10. These are bounded results, not an unbounded proof. The zero-grace and long-import counterexamples retain the narrower operator restriction in SPEC-GC; they do not expose a new split-sweep residue.

Historical results for the unchanged root and ContentIndex models follow.

All results below are from the final state of gc.qnt, contentIndex.qnt and check.sh on 2026-09-26. Times are wall clock on the shared host.

quint (./check.sh): all 13 quint test scenarios pass and all 48 quint run checks come out as expected (gc model 2 min 23 s, ContentIndex model under 30 s).

TLC (TLC=1), exhaustive, no state left on the queue, -Xmx4g, 2 workers:

The state counts for gc, gcGrace0, gcPushBounded and gcPushFastFreshen equal the earlier tla2tools runs: the new actor and invariants are disabled or read-only in those instances. The constraint on the writer instances is what keeps them inside 4 GB; unconstrained they were OOM-killed at about 40M states. Bounded ≠ proved: the constrained runs cover every state with at most two producer rewrites and no corrupt source.

Apalache 0.62.2 (APALACHE=1), -Xmx4g:

MKIT-55 re-run (2026-09-27), after BulkWriter began refreshing mtime on a dedup hit (the model is unchanged; this confirms the instance the code now matches): ONLY=gc SEL='^gcPushFast' APALACHE=1 ./check.sh exits 0. All 8 gc quint test scenarios pass; quint run gcPushFastFreshen::All and ::NoLivePruned ok, gcPushFast::NoDangling/::NoLivePruned and the gcPushFastFreshen canaries CanaryNoPruneDuringPush/CanaryNoPrunedPushPublished violated as expected; Apalache gcPushFastFreshen::All length 8 ok (450 s), gcPushFast::NoDangling / ::NoLivePruned length 8 violated (174 s / 67 s), gcPushFastFreshen::CanaryNoPrunedPushPublished length 9 violated (41 s). Bounded, not proved.

gcTagRoot::NoDangling is not run under Apalache: its shortest counterexample is 16 steps (gc must sweep all seven objects and finish before the tag can take the lock), and a length-12 run found nothing in 19 minutes, as expected. TLC, quint run and tagAfterGraceTest cover it. The safe gc instances were checked to length 10 with Apalache 0.47.2 in the previous revision; with 0.62.2 they are checked to length 8 to stay under 30 minutes per check on the shared host (GC_DEPTH=10 restores the old bound).

Commands

./check.sh                  # quint typecheck/test/run, all models
APALACHE=1 ./check.sh       # + Apalache 0.62.2 (~2 h on the shared host)
TLC=1 ./check.sh            # + TLC from the Apalache jar (~50 min)
ONLY=ci TLC=1 APALACHE=1 ./check.sh   # ContentIndex model only (~2 min)
SEL='^gc::All$' TLC=1 ONLY=gc ./check.sh   # one check

Not modelled

MAX_REACHABLE truncation (same abort as ObjectNotFound), crash durability of record, several producers in different linked worktrees appending to the shared recovery log concurrently (each holds only its own tree's lock; O_APPEND appends are not modelled), the R-64 driver, relay watermark and root re-check, and the blocklist.