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) {