ADR 0009 — C7: context effects, and C state embedded by value

Inherited. ADR 0009 was accepted before CeeSafe's fork (Decision 0006), when the language had its earlier name. In this record, "the reference" is that language and project and "the reference compiler" its compiler: read them as CeeSafe and ceesafec. Links to documents CeeSafe did not keep are given as text.

• Status: Accepted (project owner, 2026-10-24, choosing "embed by value" for kernel locks and objects over out-of-line C state). The rest is the agent's design under that choice, following cosmoos/kernel-memory-and-lifetimes.md §4–§7; the owner may revise it.
• Scope: C7 (cosmoos/c7-report.md). It amends ADR 0008 point 4 (imported types only behind pointers).

Context

C7 wraps CosmoOS's locks, kernel objects and quiescence (audit in cosmoos/c7-report.md). Three facts from the code decide the design:

1. The kernel's synchronisation objects are C state that lives inside the data it protects. spinlock_t is 24 bytes (kernel/include/kernel/spinlock.h:31-37). struct mutex embeds a spinlock, a wait queue and list links (mutex.h:20-35). A struct kobject is embedded in its owner and found again with container_of.
2. Once initialised, some of this state points into itself. mutex_init runs list_init, which sets head->next = head (kernel/scheduler/mutex.c:21-22, list.h:24-28). Moving such a value bitwise corrupts it.
3. Atomic versus sleepable is a runtime property: might_sleep() (lockdep.h:239) panics on sleeping with preemption disabled. Nothing checks it statically, and nothing checks at all that a final kobject_put, whose release may block, is not made under a spinlock (object.c:74-81 has no might_sleep).

Decision

1. Context effects (C7a)

• Two effects: sleep (may block) and alloc (may allocate). A function's effects are those of everything it calls and every value it drops, inferred over the whole package. Built-in operations declare theirs (heap allocation is alloc; hosted I/O is sleep).
• @effects(sleep, alloc) (any subset; @effects() for none) declares them: on an extern function it is what the reference assumes, and on a CeeSafe function it is an upper bound that the inferred set must fit. An extern function without @effects is assumed to have both, the most conservative choice. A call through a C function pointer has both.
• @context(atomic) (no sleep) and @context(irq) (no sleep, no alloc; KQ-1's the reference default) on a function forbid effects in its body. On a struct, @context(atomic) makes every point where a value of it is live (maybe initialised and not yet dropped) atomic: holding a spin-lock guard is an atomic context, with no annotation at the use.
• Effects are checked in every profile. They create obligations only where a context or an @effects bound is declared, so hosted programs without them are unaffected.
• The checker proves only that CeeSafe code respects the declared effects of what it calls. CosmoOS's runtime checks (might_sleep, lockdep) stay the backstop. The reference generates no might_sleep() calls: the debug half of the macro calls lockdep_might_sleep, which modules cannot link to (it is not exported), and every sleeping primitive the reference calls has its own.

2. C state embedded by value (C7b)

• A CeeSafe struct may hold an imported C type by value, and so may an imported struct (an embedded member). Such a type, and every type that contains one by value, is C-laid-out. Like an imported type, it has no The reference layout. Generated C defines it with the real C member types, so the C compiler lays it out, and it gets no layout assertions. The interpreter faults on it.
• C-laid-out values are immovable. They are made in place and never moved:
  • the only way to make one is a struct literal given directly to Box.createIn (or nested in such a literal);
  • imported fields are left out of the literal and zero-filled (C's {0}), which is the only imported value the reference can make;
  • the contents of such a box are never moved out;
  • a C-laid-out type cannot be a local, parameter, result, array element, enum payload, optional or type argument (a reference to one can be). static items come later (§4).
• @placed methods (fn m(borrow mut this)) run C's initialisers at the final address. After Box.createIn places the value, the compiler calls the @placed methods of its fields' types, innermost first in field order, then the type's own. They run before anything else can borrow the value, so code never sees uninitialised C state. A lock's @placed method calls spinlock_init with its name.
• Ptr.containerOf (unsafe) recovers a struct from a pointer to one of its fields, using C's offsetof. Kernel callbacks need it, since they receive the embedded struct kobject * or struct quiesce_head *. (Implementation note, C7b: it moved to C7d, whose release and quiescence callbacks are generated by the compiler and are its only users so far.)

3. CosmoOS bindings (C7c–C7e, integrations/cosmoos/c7/)

• SpinLock<T>, IrqSpinLock<T> and Mutex<T> hold their C lock and their data. lock() returns a guard that borrows the lock and gives borrow mut T access. Spin guards are @context(atomic). Mutex.lock is sleep. Dropping a guard unlocks. Data is reachable only through a guard.
• KRef<T>, a counted reference to a reference-defined kernel object (it embeds kobject). Its drop is kobject_put, with the sleep effect unless the type is @nonblockingRelease. A final put under a spin guard is then a compile error, the hole of fact 3.
• Quiesce.synchronize() (sleep). Quiesce.deferDrop(box) uses call_quiesce with an embedded quiesce_head. It is unsafe in modules, because module unload does not wait for pending callbacks (module.c:627-631; KQ-3). Its contract is that the module stays loaded until the callback has run.
• Not in C7: QuiesceGuard read sections in modules (quiesce_read_unlock inlines the unexported preempt_enable, quiesce.h; KQ-2; spin guards are read sections already), PerCpu<T> (CosmoOS exports no general per-CPU allocation), and statics (§4).

4. Deferred

static items (locks and caches with a lifetime of the module), and with them ObjectCache<T> (C5). Lock-order checking stays lockdep's job.

Consequences

• ADR 0008 point 4 now reads: imported types appear by value only in C-laid-out types, which are immovable and made in place. Everywhere else they appear behind pointers and references.
• type-system.md gains §32 (effects) and §33 (embedded C state). profiles.md §1 changes the effects row to checked everywhere. kernel-memory-and-lifetimes.md §5–§6 point to them.
• The proposals of kernel-memory-and-lifetimes.md that C7 leaves out stay proposals: PerCpu, statics, Unlinked<T>, @scopedOnly, and the irq-state ordering of nested IrqSpinGuards beyond using's LIFO.