From bfc0cb9bfd4f4efe6ce8316316cbfcfe9ec84e74 Mon Sep 17 00:00:00 2001 From: Robert Allan James Date: Tue, 4 Aug 2026 00:12:56 -0400 Subject: [PATCH] starkernel: document the mutex stub's concurrency constraint (item 0.9) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit sf_mutex_lock()'s no-op is correct only while nothing in interrupt context mutates the structure a given lock protects. States that explicitly, and states why a real spinlock is the wrong fix if that constraint is ever violated: a single hart would deadlock spinning against its own interrupt handler. The correct fix in that case is disabling interrupts around the critical section. Documentation only, no behaviour change. Punch list §25 item 0.9 complete. Co-Authored-By: Claude Sonnet 5 --- FABRIC.md | 2 +- src/starkernel/vm/host/shim.c | 8 ++++++++ 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/FABRIC.md b/FABRIC.md index baa83f3..d039a95 100644 --- a/FABRIC.md +++ b/FABRIC.md @@ -2150,7 +2150,7 @@ on until there is a tick on all three architectures (§16.1, §16.5).* > DoE run in a later phase or a dedicated look at the warm-up gate. *Refs:* §16.4 (as ruled), §18.4, §21.2, §26. -- [ ] **0.9 — Write the concurrency constraint at the mutex stub.** +- [x] **0.9 — Write the concurrency constraint at the mutex stub.** Add a comment at `src/starkernel/vm/host/shim.c:415` stating that the no-op is correct only while nothing in interrupt context mutates shared structure, and that making it a real spinlock would deadlock a single hart. diff --git a/src/starkernel/vm/host/shim.c b/src/starkernel/vm/host/shim.c index 5cf826c..14e0fb2 100644 --- a/src/starkernel/vm/host/shim.c +++ b/src/starkernel/vm/host/shim.c @@ -410,6 +410,14 @@ void sf_mutex_destroy(sf_mutex_t *mutex) { * Single-threaded kernel: no contention is possible at the VM level, so * acquiring the mutex is always immediate and guaranteed to succeed. * + * This no-op is correct only as long as nothing running in interrupt + * context mutates the structure a given lock protects (FABRIC.md §21.2, + * §25.1 item 0.9). If that ever stops being true, making this a real + * spinlock is not the fix: a single hart taking an interrupt while + * already holding the lock would spin against itself and deadlock. The + * correct fix in that case is disabling interrupts around the critical + * section, not adding a spinlock here. + * * @param mutex Ignored. */ void sf_mutex_lock(sf_mutex_t *mutex) {