FABRIC.md §22.3: free lists are per-VM, not shared
Review item REVIEW-A2. §22.3 specified that cells are drawn from a shared free list. That undercut the row that decided §21: its SMP discriminator claims messages are the only boundary-crossers, so no shared memory and no locks, permanently. A shared free list is shared mutable state touched by every VM on every admission and reap, and would need a lock or atomics under SMP. §22.3's defence -- that VMs never touch each other's cells -- does not cover it, because the free list is nobody's cell and allocation touches it. Each VM now holds its own free-list head index into the global array. Hera hands over cells when she grants quota; a VM allocates and frees only within what it holds. One index space, one datatype and §13 are all unaffected, and disjointness becomes total rather than nearly total. Capacity transfer remains arithmetic plus a list splice, arbitrated at a known point per §22.5 #2. The layout choice itself is unchanged -- one global array, one index space remains correct for §13. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This commit is contained in:
co-authored by
Claude Opus 5
parent
055e944a73
commit
518334abef
@@ -1535,8 +1535,33 @@ settle that.
|
||||
|
||||
**Chosen: one global array of cells, one global index space.** Nesting becomes a
|
||||
*partition* of that index set rather than separate allocations. A VM's quota is a **count,
|
||||
not a contiguous range**, so cells are drawn from a shared free list, there is no adjacency
|
||||
requirement, no fragmentation, and index links keep working because indices are global.
|
||||
not a contiguous range**, so there is no adjacency requirement, no fragmentation, and index
|
||||
links keep working because indices are global.
|
||||
|
||||
#### Free lists are per-VM, not shared
|
||||
|
||||
An earlier draft of this section said cells are drawn from a **shared free list**. That was
|
||||
wrong, and it quietly undercut the argument that decided §21.
|
||||
|
||||
§21.3's decisive discriminator is the SMP row: *messages are the only boundary-crossers, so
|
||||
no shared memory and still no locks.* A shared free list is shared mutable state, touched by
|
||||
every VM on every admission and every reap. Under SMP it would need a lock or atomics —
|
||||
exactly what that row claims nesting avoids permanently. The defence offered there, that
|
||||
"VMs never touch each other's cells," does not reach it: **the free list is nobody's cell,
|
||||
and allocation touches it.**
|
||||
|
||||
The fix costs essentially nothing:
|
||||
|
||||
> **Each VM holds its own free-list head index into the global array.** Hera hands a VM its
|
||||
> cells when she grants quota; the VM allocates and frees only within what it holds.
|
||||
|
||||
One head index per VM instead of one global head. One index space is preserved, one datatype
|
||||
is preserved, §13 is unaffected — and disjointness becomes **total** rather than nearly
|
||||
total. No mutable structure is shared between VMs at all, which is what §21.3 actually
|
||||
promised.
|
||||
|
||||
Transfer of capacity is then Hera moving cells from one VM's free list to another's, which
|
||||
is still arithmetic plus a list splice, and still arbitrated at a known point (§22.5 #2).
|
||||
|
||||
Two reasons this is the right trade:
|
||||
|
||||
|
||||
Reference in New Issue
Block a user