FUGC, Fil's Unbelievable Garbage Collector, is what reclaims memory in Fil-C. It marks and sweeps on its own threads, in parallel, while the program runs, and never moves an object. It never stops the world: it asks each thread for work, such as scanning its stack, by a soft handshake, which the thread answers at its next pollcheckpoll Fil-CA safepoint is a point where the thread may run signal handlers and answer the collector. The collector frees nothing the program can name there, but a handler the program installed may free an object under the rest of the program. A pollcheck is a safepoint on an edge: a jump target poll(L), a poll edge, runs one before going to L. Calls, allocations and some helpers are safepoints too (ir:evidence_preserving/1, ir:polls_every_cycle/1).. While it marks, a store barrier marks the target of every pointer stored to the heap. It finds pointers exactly: on stacks through the rootsroot Fil-CA root is a frame word the collector scans for live capabilities: an entry of the Pizderson frame's lowers[] (the record each function keeps on the stack: a parent link, an origin and the lowers), a local's stack aux, or a jmpbuf root (filc_abi:lower_function/5, amd64_regs_check:valid_map/3). Every live lower is in one at every safepoint, so registers never hold the only copy. the compiler keeps, and in objects only in their auxaux Fil-CAn object's aux allocation, as large as its payload: where Fil-C keeps the lowers of the pointers stored in the object, slot for slot, while their intvals sit in the object's bytes. The aux word in the object header points at it; it is null for an object no pointer was ever stored into, which the collector then scans as a leaf. A pointer store must *ensure* it exists, which may call the runtime; a pointer load reads it. allocation.

• free does not wait for it. Free empties the object's bounds and raises its free flag at once, so every later access through any pointer to it panicstrap Fil-CA trap is a Fil-C check failing, which upstream calls a Fil-C panic or safety error (filc_safety_panic): the run ends trap(Reason), terminal and uncatchable. Because nothing follows it, a check is a pure assertion, which is why a check proved never to fail can be deleted without changing behaviour.. FUGC then repoints every lowerlower Fil-CThe lower is how Fil-C represents a capability natively: the address of the first byte of the object a pointer may access, kept beside the pointer's intval in a flight pointer. The object header sits just below it: the upper bound at lower−16 and the aux word at lower−8, whose low 48 bits point at the aux allocation and whose top 16 bits hold the object's flags (free, read-only, global, ...). A null lower accesses nothing, and free sets upper to lower, so every access through any lower of a freed object fails. filc_abi:lower_function/5 keeps each live one in a root. of the freed object at one shared free singleton and reclaims the memory. Use after free and double free are caught even after the memory is reused, and an object never freed is still reclaimed.

• The model has one thread and no collector. What FUGC may do at a safepoint is stated as runtimeruntime Fil-CThe runtime is what Fil-C does around one thread's program, natively libpizlo.so with FUGC: where a new object goes, what free does, and what the collector may change while the program waits at a safepoint. The model does not define it; it states it as one page of axioms, Module Type Runtime (Runtime), each with a native test in tests/c/prog/axiom-*.c. axioms: no region changes (collector_live), so nothing the program can name is reclaimed (rooting, a lemma from it); no object moves (non_moving); and a free changes no byte (retentionretention nanofilRetention is the runtime axiom that free changes no byte and no stored capability: a freed object's memory stays as it was while anything can name it. Only its header changes, so every access through a capability to it traps, but bytes read through a check that passed before the free are the same bytes.).