|
| 1 | +# Slot Ownership Typestates |
| 2 | + |
| 3 | +## Overview |
| 4 | + |
| 5 | +Slot ownership typestates make data races structurally impossible by tracking slot ownership through the type system. Each state transition enforces critical invariants at compile-time. |
| 6 | + |
| 7 | +## Producer-Side Flow |
| 8 | + |
| 9 | +``` |
| 10 | +tryClaimSlot() |
| 11 | + | |
| 12 | + v |
| 13 | +SlotClaimed ----[writeItem]----> SlotWritten ----[commitSlot]----> SlotCommitted |
| 14 | + | | |
| 15 | + v v |
| 16 | + SegmentFull [data ready] |
| 17 | +``` |
| 18 | + |
| 19 | +### States |
| 20 | + |
| 21 | +- **SlotClaimed**: Exclusive write access after winning CAS |
| 22 | + - Guarantees: This thread owns the slot index |
| 23 | + - Linear type: Can only use once (via `sink` parameter) |
| 24 | + |
| 25 | +- **SlotWritten**: Data written but not visible yet |
| 26 | + - Guarantees: Data in slot, but consumers blocked |
| 27 | + |
| 28 | +- **SlotCommitted**: Data visible to consumers |
| 29 | + - Guarantees: Consumers can now read |
| 30 | + |
| 31 | +### Transitions |
| 32 | + |
| 33 | +```nim |
| 34 | +# Try to claim a slot |
| 35 | +let result = tryClaimSlot(segment) |
| 36 | +
|
| 37 | +case result.kind: |
| 38 | +of ckClaimed: |
| 39 | + # Won CAS - have exclusive access |
| 40 | + let claimed = result.claimed |
| 41 | +
|
| 42 | + # Write data (consumes claimed token) |
| 43 | + let written = writeItem(claimed, myData) |
| 44 | +
|
| 45 | + # Commit (make visible to consumers) |
| 46 | + let committed = commitSlot(written) |
| 47 | +
|
| 48 | +of ckSegmentFull: |
| 49 | + # Allocate new segment and retry |
| 50 | + discard |
| 51 | +
|
| 52 | +of ckRetry: |
| 53 | + # Lost CAS race, try again |
| 54 | + discard |
| 55 | +``` |
| 56 | + |
| 57 | +## Consumer-Side Flow |
| 58 | + |
| 59 | +``` |
| 60 | +tryClaimForRead() |
| 61 | + | |
| 62 | + v |
| 63 | +SlotAvailable ----[readItem]----> T (data) |
| 64 | + | |
| 65 | + v |
| 66 | +SlotPending ----[waitForCommit]----> SlotAvailable |
| 67 | +``` |
| 68 | + |
| 69 | +### States |
| 70 | + |
| 71 | +- **SlotAvailable**: Slot ready to read |
| 72 | + - Guarantees: Producer has committed, data is valid |
| 73 | + |
| 74 | +- **SlotPending**: Claimed but not committed (MPSC only) |
| 75 | + - Need to wait for producer to commit |
| 76 | + |
| 77 | +### Transitions |
| 78 | + |
| 79 | +```nim |
| 80 | +# Try to claim a slot for reading |
| 81 | +let result = tryClaimForRead(segment) |
| 82 | +
|
| 83 | +case result.kind: |
| 84 | +of pkAvailable: |
| 85 | + # Data ready - can read immediately |
| 86 | + let data = readItem(result.available) |
| 87 | +
|
| 88 | +of pkPending: |
| 89 | + # Producer hasn't committed yet - wait |
| 90 | + let available = waitForCommit(result.pending) |
| 91 | + let data = readItem(available) |
| 92 | +
|
| 93 | +of pkExhausted: |
| 94 | + # Segment empty, advance to next |
| 95 | + discard |
| 96 | +
|
| 97 | +of pkEmpty: |
| 98 | + # Queue empty |
| 99 | + discard |
| 100 | +``` |
| 101 | + |
| 102 | +## Safety Guarantees |
| 103 | + |
| 104 | +| Guarantee | How Enforced | |
| 105 | +|-----------|--------------| |
| 106 | +| No write without CAS | `writeItem` requires `SlotClaimed`, only from successful CAS | |
| 107 | +| No double write | `sink` parameter consumes `SlotClaimed` token | |
| 108 | +| No commit without write | `commitSlot` requires `SlotWritten` | |
| 109 | +| No read without CAS | `readItem` requires `SlotAvailable`, only from successful CAS | |
| 110 | +| No read uncommitted data | `SlotAvailable` only when committed flag set (MPSC) | |
| 111 | + |
| 112 | +## Type System Enforcement |
| 113 | + |
| 114 | +The type system makes these errors impossible: |
| 115 | + |
| 116 | +```nim |
| 117 | +# ERROR: Cannot write without claiming |
| 118 | +let written = writeItem(segment, data) # No SlotClaimed token! |
| 119 | +
|
| 120 | +# ERROR: Cannot reuse claimed token |
| 121 | +let claimed = tryClaimSlot(segment).claimed |
| 122 | +let written1 = writeItem(claimed, data1) |
| 123 | +let written2 = writeItem(claimed, data2) # claimed already consumed! |
| 124 | +
|
| 125 | +# ERROR: Cannot commit without writing |
| 126 | +let committed = commitSlot(claimed) # Need SlotWritten, not SlotClaimed! |
| 127 | +
|
| 128 | +# ERROR: Cannot read without claiming |
| 129 | +let data = readItem(segment, 0) # No SlotAvailable token! |
| 130 | +``` |
| 131 | + |
| 132 | +## Integration with DEBRA Typestates |
| 133 | + |
| 134 | +Slot ownership states compose with DEBRA pin/unpin states: |
| 135 | + |
| 136 | +```nim |
| 137 | +type |
| 138 | + MPSCPushContext[T; S, MT: static int] = object |
| 139 | + pinnedHandle: ThreadHandle[MT] |
| 140 | + pinnedEpoch: uint64 |
| 141 | + queue: ptr UnboundedMupsicBase[S, T, MT] |
| 142 | + slotOwnership: SlotClaimed[T, S] # Embedded slot state |
| 143 | +``` |
| 144 | + |
| 145 | +This ensures: |
| 146 | +- Must be pinned to push |
| 147 | +- Must claim slot to write |
| 148 | +- All invariants enforced together |
| 149 | + |
| 150 | +## MPSC Implementation Example |
| 151 | + |
| 152 | +The unbounded MPSC queue uses the following typestate progression: |
| 153 | + |
| 154 | +### Push Operation States |
| 155 | + |
| 156 | +1. **MPSCPushReady**: Initial state with pinned DEBRA context |
| 157 | +2. **MPSCPushSegmentLoaded**: Segment and tail position loaded |
| 158 | +3. **MPSCPushSlotClaimed**: Slot claimed via CAS (or SegmentFull/Retry) |
| 159 | +4. **MPSCPushItemWritten**: Data written to slot |
| 160 | +5. **MPSCPushComplete**: Committed flag set, data visible to consumers |
| 161 | + |
| 162 | +### Example Usage |
| 163 | + |
| 164 | +```nim |
| 165 | +import debra |
| 166 | +import lockfreequeues/typestates/unbounded_mpsc_push |
| 167 | +
|
| 168 | +# Setup |
| 169 | +var manager = initDebraManager[4]() |
| 170 | +let handle = registerThread(manager) |
| 171 | +var queue: UnboundedMupsicBase[64, int, 4] |
| 172 | +# ... initialize queue ... |
| 173 | +
|
| 174 | +# Push operation |
| 175 | +let pinned = unpinned(handle).pin() |
| 176 | +let ready = startPush(pinned, addr queue) |
| 177 | +let loaded = ready.loadSegment() |
| 178 | +
|
| 179 | +let claimResult = loaded.tryClaimSlot() |
| 180 | +case claimResult.kind: |
| 181 | +of mMPSCPushSlotClaimed: |
| 182 | + let claimed = claimResult.mpscpushslotclaimed |
| 183 | + let written = claimed.writeItem(42) |
| 184 | + let complete = written.markCommitted() |
| 185 | + discard complete.extractPinned().unpin() |
| 186 | +
|
| 187 | +of mMPSCPushSegmentFull: |
| 188 | + # Handle segment allocation |
| 189 | + let newSeg = newSegment() |
| 190 | + let ready = claimResult.mpscpushsegmentfull.allocateNewSegment(newSeg) |
| 191 | + # Retry... |
| 192 | +
|
| 193 | +of mMPSCPushReady: |
| 194 | + # CAS failed, retry |
| 195 | + discard |
| 196 | +``` |
| 197 | + |
| 198 | +## Performance |
| 199 | + |
| 200 | +Slot ownership typestates are **zero-cost abstractions**: |
| 201 | + |
| 202 | +- All types are compile-time only |
| 203 | +- No runtime overhead |
| 204 | +- Same assembly as hand-written CAS code |
| 205 | +- Just adds compile-time safety |
| 206 | + |
| 207 | +## Future Extensions |
| 208 | + |
| 209 | +Potential enhancements: |
| 210 | + |
| 211 | +- Batch operations: Claim multiple slots at once |
| 212 | +- Backpressure: SlotClaimFailed -> wait/retry logic |
| 213 | +- Priority: Different claim strategies based on priority |
| 214 | +- Monitoring: Track claim success rates |
0 commit comments