retention
nanofil
In Fil-C free changes only the header; FUGCFUGC Fil-CFUGC, 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 pollcheck. While it marks, a store barrier marks the target of every pointer stored to the heap. It finds pointers exactly: on stacks through the roots the compiler keeps, and in objects only in their aux allocation. reclaims the memory once no 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. names it (FUGC)
Retention is the 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. 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.
Runtime.v's retention, proved for the interpreter by free_res_retention; natively free_impl writes only the header. Native test: axiom-retention.c (another thread frees the object a loop reads and churns the allocator; the loop reads retained bytes or traps, never other values).
With non_moving it makes another thread's free between a check and its access harmless natively: the access reads retained bytes, and the next check traps. The one-threaded model has no such free; its safepoint changes no region (collector_live).
It is also why a pointer store stays safe natively when its 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. exit runs a handler the program installed that frees the object: the store lands in retained memory, as Fil-C's own argument at that exit says. The model leaves such handlers out, so every runtime meets sparesspares nanofilspares says that at a safepoint just before an instruction the evidence pass keeps facts across, the runtime changes no region. Every runtime meets it, so the generic soundness theorem, once stated under it, no longer takes it as a hypothesis..
See runtime-axioms.md, The axioms.