Concurrent separation logic carries ownershipseparation logic IrisSeparation logic is Hoare logic whose assertions describe the part of memory a piece of code owns. ℓ ↦ v owns one cell, P ∗ Q holds of memory that splits into a part where P holds and a disjoint part where Q holds, and the frame rule lets code proved on what it owns run inside any larger memory, which it leaves alone. Aliasing is ruled out by the assertions, not by side conditions. across threads: threads that own disjoint resources run in parallel without interfering, and a lock guards a resource invariant that the thread taking the lock receives and must restore before releasing it. The decade after it produced a logic per sharing pattern (RGSep, CAP, iCAP, TaDA and more), each with its own soundness proof; IrisIris IrisIris is a higher-order concurrent separation logic framework in Rocq. Its propositions describe owned resources, may quantify over propositions, and are shared through invariants; user-defined ghost state expresses protocols. A language joins it by giving its step relation, and adequacy turns a weakest precondition proved in the logic into a fact about every run. reduced them to ghost state and invariants.

• In Fil-C, other threads and signal handlers are what may free an object under a program, and both are the program's own code: 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.'s collector frees nothing at a safepointpoll 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). (collector_live). nanofil's model has one thread and no handler; a concurrent one would verify the handler or thread as program code, owning only what it was handed.

See How Iris works, Concurrent separation logic.