starkernel: document the mutex stub's concurrency constraint (item 0.9)

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 <noreply@anthropic.com>
This commit is contained in:
Robert Allan James
2026-08-04 00:12:56 -04:00
co-authored by Claude Sonnet 5
parent 3699be964d
commit bfc0cb9bfd
2 changed files with 9 additions and 1 deletions
+1 -1
View File
@@ -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.
+8
View File
@@ -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) {