A 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 pollL, a poll edge, runs one before going to L. Calls, allocations and some helpers are safepoints too (ir:evidence_preserving/1ir.plevidence_preserving+InstsemidetInst reaches no safepoint and cannot free an object or change its bounds or rights: pure arithmetic, comparison and conversion, pure pointer construction, a heap check, a scalar raw access (object headers lie outside every object's bounds) and a raw pointer load (aux and box reads, no helper). Calls, alloc, getters, setjmp, va_arg, pointer stores and the res…, ir:polls_every_cycle/1ir.plpolls_every_cycle+BlockssemidetEvery cycle of the control-flow graph of Blocks, unreachable blocks included, has a poll edge: without them the graph is acyclic. A call does not count, since the callee need not poll. Depth-first search, with each label gray while on the path and done after.).

• Upstream puts a pollcheck on every back edge of the control-flow graph, not only on loops. A thread about to block in a system call first exits, and the collector does its handshake work for it (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.).

• Every cycle of a checked function has a poll edge, so a loop cannot keep the collector waiting (polls_every_cycle).

• No live factlive fact nanofilA live fact live(Q, P, Lo, Hi, Rights, Align) is the validator's record that the proof Q came from a check of P over [Lo, Hi) that still holds: no safepoint since, and neither Q nor P redefined. A later raw access through Q that the fact covers needs no check of its own. crosses a safepoint, with three exceptions, covered by 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., which every runtime meets (spares_any).

• Rocq: the target Poll; 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. acts only before an instruction where at_safepoint holds or before a poll edge (safepoint_due), as its axiom safepoints says, and there it changes no region (collector_live). The model has no handler: installing one is a call to an external with no contract, which ends the run.