C7 — Kernel concurrency integration (plan and report)

Status: complete 2026-10-25 (plan accepted 2026-10-24; ADR 0009). Acceptance results are below. Roadmap acceptance: effects, SpinLock<T>/Mutex<T> guards, KRef, QuiesceGuard, PerCpu, deferred reclamation; negative effect tests; lockdep clean under QEMU stress; real concurrency rules exercised (roadmap.md). Prompt (cosmoos-native.md C7): investigate and introduce context effects, kernel object borrowing, lock guards, epoch guards, and deferred reclamation compatibility; test against the kernel's real concurrency rules. Stage S0: out of tree, CosmoOS read-only.

Audit (CosmoOS 5cfd1ffe, v1.0.13; read, not copied)

The audits of C4–C6 were at 98040b9b; this one re-reads every interface C7 touches.

Interface	Where	What it says
Spinlocks	kernel/include/kernel/spinlock.h:31-60, kernel/core/spinlock.c:30-120,211-220	spinlock_t is C state (locked, owner_cpu, name, lockdep class; 24 bytes) set up by spinlock_init(lock, name); taking one disables preemption first; lockdep keys the class on the name; re-acquiring on the same CPU panics. spin_lock, spin_unlock, spin_lock_irqsave, spin_unlock_irqrestore (arch_irq_state_t = unsigned long), _nested forms and spin_trylock are exported
Mutexes	kernel/include/kernel/mutex.h:20-44, kernel/scheduler/mutex.c:13-23,243-247	struct mutex embeds a spinlock, a wait queue and a list node; after mutex_init the list heads point to themselves, so an initialised mutex cannot move. mutex_lock sleeps; init, lock, trylock and unlock are exported
Sleeping check	kernel/include/kernel/lockdep.h:233-248	might_sleep() is a macro: it panics when preempt_count or irq_depth is non-zero; with CONFIG_LOCKDEP it reports through lockdep_might_sleep, which is not exported
Preemption	kernel/include/kernel/percpu.h:148-187	preempt_disable is inline; preempt_enable is out of line and not exported; arch_percpu_get and arch_cpu_id are exported (kernel/arch/*/percpu.c, kernel/core/percpu.c:214-215)
Quiescence	kernel/include/kernel/quiesce.h, kernel/core/quiesce.c:405-408	read sections are preemption-disabled regions (every spinlock is one); quiesce_read_lock/unlock are inline and call preempt_enable, so a module cannot use them (KQ-2 still open); synchronize_quiesce sleeps; call_quiesce(head, fn) runs fn in thread context after a grace period, with the embedded quiesce_head owned by the subsystem until then; all of these and the _debug halves are exported
Module unload	kernel/module/module.c:614-660	shutdown(), then one synchronize_quiesce(), then a wait for objects whose release is in the module; pending call_quiesce callbacks are not waited for (KQ-3 still open)
Kernel objects	kernel/include/kernel/object.h, kernel/object/object.c:10-119	struct kobject is embedded in its owner; kobject_init(obj, type) with a mandatory release; get, tryget, put, exported; the final put runs the release, which may block, with no might_sleep
Threads	kernel/include/kernel/thread.h:163-185, wait.h:243-246	thread_create(entry, arg, name, priority), thread_join, thread_sleep_ns: exported
Debug build	build/config.mk:10-17, build/toolchain.mk:42,52-55	BUILD=debug (the default) sets CONFIG_DEBUG=1 and LOCKDEP=1; lockdep reports lockdep: <kind> and panics (kernel/core/lockdep.c:313-328)

Plan

Decisions are in ADR 0009. The increments, each with its own tests and commit:

Increment	Content	Where
C7a context effects	sleep/alloc inferred over the package; @effects bounds and extern declarations; `@context(atomic	irq)` on functions and on guard types; drops count; checked in every profile; negative corpus
C7b embedded C state	imported types by value in Nova structs and embedded in imported structs; C-laid-out, immovable types made in place by Box.createIn; zero-filled imported fields; @placed methods; Ptr.containerOf	type-system.md §33
C7c lock guards	SpinLock<T>, IrqSpinLock<T>, Mutex<T> and their guards over CosmoOS's locks	integrations/cosmoos/c7/sync.nova
C7d kernel objects and quiescence	KRef<T> over an embedded kobject, Quiesce.synchronize, Quiesce.deferDrop (unsafe in modules)	integrations/cosmoos/c7/
C7e the kernel's rules, in the kernel	an out-of-tree module (the C5 pipeline) in CosmoOS's debug build (lockdep on), on both arches in QEMU: kernel threads contending on Nova locks, counted references across threads, grace periods and deferred frees; the results must be exact and lockdep silent; runtime negative controls in separate boots	integrations/cosmoos/c7.py

Out of C7 (ADR 0009 §3–§4): static items, ObjectCache<T>, PerCpu<T>, QuiesceGuard in modules (blocked on KQ-2), Nova lock-order checking.

Acceptance

Roadmap criterion	Evidence	Met
Negative effect tests	check-fail/effects.nova (13), check-fail/effect-attributes.nova (9), and 11 cases against the real bindings (c7/negative/): sleeping, allocating or waiting for a grace period where the context forbids it, a final kobject_put under a spin guard	yes
Lockdep clean under QEMU stress	C7e, CosmoOS's debug build (lockdep on), 4 CPUs, both arches: no lockdep report and no panic, 0 boot modules failed, CosmoOS's 507 selftests pass, clean shutdown	yes
Real concurrency rules exercised	kernel threads overlapping on 4 CPUs, on CosmoOS's own spinlocks, irqsave locks, mutexes (sleeping), kobjects and grace periods; lockdep catches the order inversion Nova does not check; an unlocked counter loses updates while every locked one is exact	yes
Content: effects; SpinLock<T>/Mutex<T> guards; KRef; deferred reclamation	type-system §32–§34; c7/sync.nova, kobject.nova, quiesce.nova	yes
Content: QuiesceGuard	not in modules: quiesce_read_unlock inlines the unexported preempt_enable (KQ-2); spin guards are read sections	blocked (KQ-2)
Content: PerCpu	not done: CosmoOS exports no general per-CPU allocation, and Nova has no statics (ADR 0009 §3–§4)	deferred

Results

C7e — the kernel's rules, in the kernel (2026-10-25)

c7.py's boot stage. CosmoOS is built BUILD=debug (lockdep on, the debug half of might_sleep on); c1.Cosmo now takes a build type. The module nova_c7 is the whole C7 package plus c7/stress.nova, c7/module.c and c7/kernel_glue.c. It is built with the debug build's MODULE_CFLAGS, signed, checked with check-module-elf.py and C4's checks, added to a copy of the boot archive, and booted in QEMU with 4 CPUs.

init runs c7_stress(4, 2000), four kernel threads (thread_create, @callback worker), each doing 2,000 rounds of:

• a spin-locked counter;
• an irqsave-locked counter;
• a Mutex-locked ledger with a SpinLock nested inside it (lockdep learns mutex → spinlock);
• a reference of its own to a shared KRef, dropped outside every guard;
• every 32 rounds a deferDrop, and every 256 rounds a Quiesce.synchronize, so grace periods are waited for while others are being requested.

The threads are then joined and every total checked. A control phase follows: each worker makes 100,000 increments with no lock.

Results (run 2026-10-25, CosmoOS 5cfd1ffe, debug build, QEMU on the Mac, -smp 4):

Check	AArch64	x86-64
threads started and joined	4	4
spin-locked, irqsave-locked, mutex-locked and nested counters	8,000 each (exact)	8,000 each (exact)
KRef count after the workers' 8,000 clones and puts	1	1
deferred frees run after the last grace period	252 of 252	252 of 252
workers inside their loops at once (max) / CPUs used	4 / 4	4 / 4
control: unlocked increments counted	343,552 of 400,000 (lost)	210,705 of 400,000 (lost)
lockdep reports, panics	none	none
boot modules	15 loaded, 0 failed	15 loaded, 0 failed
CosmoOS's own selftests in the same boot	507 of 507	507 of 507
shutdown	clean (QEMU 33)	clean (QEMU 33)
negative control (second boot, -DC7_CONTROL=1): two spinlocks taken in both orders	lockdep: lock-order inversion, naming nova.c7.order.a and nova.c7.order.b, and panics	the same

Findings:

• In Nova's harness, fixed: qemu-run.sh makes the scratch disks only when they are missing, so boots in a reused work directory found the disk a previous boot's selftests had formatted, and CosmoOS's cosmofs-* selftests failed ("an unformatted disk is refused"). c1.boot, which C1–C7 share, now starts every boot with fresh disks. A boot of the same debug image without the Nova module, as a baseline, passed 507 of 507.
• In CosmoOS (reported, not changed): its lockdep class table is near capacity in a debug boot. The baseline warns at 496 of 512 ("raise LOCKDEP_MAX_CLASSES before a boot overflows it"), and the C7e boot, whose module adds 6–7 classes (its five lock names, a mutex's inner spinlock and wait queue), at 502 (AArch64) and 503 (x86-64).
• Not Nova's: one AArch64 run failed one CosmoOS selftest, blk-irq-budget, a scheduler-latency bound ("a default-priority thread went longer than the bound without running"), under emulation. The next AArch64 run and the baseline passed all 507. It is recorded as a timing failure, not attributed to Nova.
• The unlocked control needs a phase of its own. Inside the locked rounds, its increments never collided: the workers fall into lockstep behind the mutex. Overlap is therefore measured directly as well (at most 4 inside at once, on 4 CPUs).

C7d — kernel objects and quiescence (2026-10-25)

Language (type-system.md §34):

• @callback gives a top-level function, generic ones included, a C address without a symbol. Each instance used as a value (release<T>) gets a static C function with the C types. The grammar now reads name<T> before ), ,, ; or ] as generic arguments too (grammar §2; a comparison cannot end there).
• Box.intoRaw(b) gives ownership to a raw pointer, and Box.fromRaw(p) (unsafe; the box type comes from the expected type) takes it back. Both are allowed in freestanding code.
• Imported struct fields may be C function pointers, as kobject_type.release is.
• Ptr.containerOf was not needed. Kernel callbacks receive a pointer to the object's first field, which converts to the object (§34.3, C11 6.7.2.1p15).

Bindings:

• c7/kobject.nova: KObject<T> embeds struct kobject first, then its struct kobject_type (the kernel keeps the type pointer, and with no statics in Nova the type lives in the object), then the data. Its @placed method fills the type with release<T> and calls kobject_init. KRef<T> is an owned counted reference, with create, clone (kobject_get), get (shared), count, and a drop that runs kobject_put with the sleep effect. release<T> rebuilds the box and drops it.
• c7/quiesce.nova: Quiesce.synchronize() (sleep); Deferred<T>, a quiesce_head first and then the value; and unsafe fn deferDrop<T>, which gives the box to call_quiesce, so the box cannot be used or submitted again (it moved). The unsafe carries KQ-3: module unload does not wait for pending callbacks.

c7.py (run 2026-10-25, CosmoOS 5cfd1ffe, macOS host):

Check	Result
5 new negative cases: dropping a KRef under a spin guard (the chain reaches kobject_put), Quiesce.synchronize under a spin guard, deferDrop outside unsafe, using a value after deferDrop, writing through KRef.get	each gives exactly its annotated error (N0295 ×2, N0280, N0250, N0211); the 6 of C7c still pass
Host test against CosmoOS's own kernel/object/object.c (and its spinlock shim and harness), with c7/host_kernel.c providing module hooks and a one-CPU grace period: a KRef with four references, three dropped, then the last; a Deferred value freed by a grace period	PASS: counts 4 then 1, the data dropped exactly once and only at the last put; the deferred value still there after deferDrop, freed at synchronize; no kernel-heap block live after the tests
AArch64 and x86-64 objects under MODULE_CFLAGS with C4's checks	PASS; undefined only kernel exports (now also kobject_init, kobject_get, kobject_put, kobject_refcount, call_quiesce, synchronize_quiesce)

Also ffi/raw-boxes.nova in every C configuration (three instances of one generic callback, each giving its box back once), and check-fail/callbacks.nova (8 misuses).

Not done: @nonblockingRelease, so every final put counts as sleeping, which is conservative. kobject_tryget for table lookups. Module ownership is tested only as far as the host can go; C7e and C8 load the code as a module.

C7c — lock guards (2026-10-24)

integrations/cosmoos/c7/sync.nova, over CosmoOS's own kernel/spinlock.h and kernel/mutex.h (imported, §31):

Type	Holds	lock()	Guard
SpinLock<T>	spinlock_t by value, the lockdep name, T	spin_lock	SpinGuard<T>: @context(atomic); drop spin_unlock
IrqSpinLock<T>	the same	spin_lock_irqsave	IrqSpinGuard<T>: @context(atomic), keeps the IRQ state; drop spin_unlock_irqrestore
Mutex<T>	struct mutex by value (self-pointing once initialised), the name, T	mutex_lock (@effects(sleep))	MutexGuard<T>: drop mutex_unlock

• Each lock is made by create(name, data) in a KernelHeap box. Its @placed method runs spinlock_init or mutex_init at the final address (§33).
• guard.data() is the only way to the data, and its borrow mut T borrows the guard. Every field is private, a rule new in C7c (type-system §12: file-private, as language-spec.md §5 defines private; N0296), so no other file can reach the data, forge a guard, or skip the lock.
• C5's binding now declares kmalloc @effects(alloc) (it never sleeps; KQ-4) and kfree @effects(), so kernel allocation is allowed under a spin guard and forbidden in @context(irq).
• Doc comments now attach to drop blocks, so a drop that uses unsafe can carry its Safety: line.

integrations/cosmoos/c7.py (run 2026-10-24, CosmoOS 5cfd1ffe, macOS host):

Check	Result
6 negative cases (c7/negative/): a mutex under a spin guard and under an irq guard, a sleeping callee under a spin guard (the message names the chain down to mutex_lock), making a lock in @context(irq) (allocation), reaching data or building a guard from another file, moving a guard while its data is borrowed	each gives exactly its annotated error (N0295 ×4, N0296 ×2, N0240)
Host test (c7/host_test.c) with CosmoOS's HOST_CFLAGS (ASan, UBSan, -Werror), its headers, HOST_COMMON_SRCS (harness, spinlock shim) and c7/host_kernel.c (a mutex shim that panics on sleeping with a spinlock held, as might_sleep does, and on a mutex that moved): 100 spin-locked updates with one lock seen held under each guard and none after; two nested irqsave locks; a spinlock under a mutex 50 times	PASS
Negative control: a SpinGuard drop that does not unlock	caught: host spinlock 'nova.c7.stats' re-acquired (deadlock)
AArch64 object under MODULE_CFLAGS, with c4/nova_rt_kernel.c and c7/kernel_glue.c (c7_locks_held from preempt_count): C4's checks	PASS; undefined only kernel exports (spin_lock, spin_lock_irqsave, spin_unlock, spin_unlock_irqrestore, spinlock_init, mutex_init, mutex_lock, mutex_unlock, kmalloc, kfree, arch_percpu_get, panic); largest frame 64 B
x86-64 object, the same	PASS; largest frame 56 B
CosmoOS working tree unchanged	PASS

Not shown here, and left to C7e: the locks under real concurrency (several CPUs and threads) and lockdep, in the kernel. Moving a guard is allowed (it is an ordinary value); nested irqsave guards rely on locals being dropped in reverse order, which a moved guard could break (the C0 design's note); C7e exercises the ordinary use.

C7b — C state embedded by value (2026-10-24)

type-system.md §33 (ADR 0009 §2). Imported types are now allowed by value as struct fields, as embedded members of imported structs (struct emb_dev { lock: emb_lock; link: emb_list; }, checked with _Generic only) and as a box's contents. A type that holds one is C-laid-out:

• generated C defines it with the real member types and asserts nothing about its layout;
• every other by-value use of it is N0294, checked once struct fields are known;
• a new NIR pass, Analysis/InPlaceChecker.cs, run before move checking, accepts a value of it only on the way from its literal into Box.create/createIn, or into an enclosing literal;
• imported fields are left out of literals and zero-filled, through a new NIR operand, NirZero;
• @placed methods run in field order, innermost first, from a generated nvPL_<T> helper right after the value is stored in its box, and their effects count as the box's (§32);
• the interpreter and placement analysis refuse such types instead of guessing a layout.

Ptr.containerOf moved to C7d, whose generated callbacks are its only users. Doc comments before attributes now attach to methods and extern functions too, as they did to top-level items.

Tests (run 2026-10-24, local suite, 1,967 tests):

• ffi/embedded.nova in every C configuration. Two queues with self-pointing C list heads and a lock are nested in a struct with a lock of its own; placement order is checked (1–4), and the rings are checked in C after linking one into the other. Also an all-C-state struct that stays zero-filled, and an imported struct's embedded members passed to C in place;
• check-fail/c-state-types.nova (8 forbidden positions and 6 misused @placed, plus the array case's existing N0259);
• check-fail/c-state-moves.nova (5 moves and misplaced literals, with valid in-place uses in the same file);
• check-fail/effects.nova, which now covers a sleeping @placed method under an atomic context;
• the interpreter fault.

The generated C of every existing program is unchanged (emit-c snapshots), so no guest runs were needed. Kernel flags are exercised with C7c's real CosmoOS types.

C7a — context effects (2026-10-24)

type-system.md §32. @effects(sleep, alloc) and @context(atomic|irq) on functions, methods and impl methods (which may now carry attributes; grammar §2), and @context(atomic) on structs. Analysis/EffectChecker.cs runs on NIR after drop elaboration:

• it infers each compiled function's effects to a fixed point over the package, counting calls, built-ins (table of §32.1) and drops (drop blocks, contents, user deallocators);
• it reports each operation whose effect its context forbids, with the chain of calls that leads to it ('atomicBody' is @context(atomic), but this may sleep: it calls 'slower', which calls 'slow', which calls 'c_block', declared @effects(sleep));
• for @context(atomic) values, a forward may-analysis tracks where a holder local may be live. A guard moved into a callee makes the callee answer for it.

Tests (run 2026-10-24, local suite): check-fail/effects.nova (13 violations: atomic and irq functions, a live guard, a guard live on one branch, a guard held by value in a struct, a guard passed to a callee, a sleeping drop under a guard, @effects bounds, an extern without @effects, recursion, a generic function instantiated three times and reported once), with no other diagnostic and no false positive on the guard-free paths in the same file; check-fail/effect-attributes.nova (9 misuses); run-pass/effects.nova in every C configuration, the interpreter and the fault-injection sweep. The existing corpus needed one change: the placeholder effect names of M8b (may_block, nosleep, noalloc) became sleep and ().