typestates/slot_state¶
slot_state defines the slot-level ownership typestate machine
shared across all bounded BQueue shapes and the unbounded Queue's
segment cells. It encodes the Vyukov per-slot seq protocol's
allowed transitions (empty → producer-owned → committed → consumed →
next-empty) as a typestate so that violations are statically
detectable in the queue body code.
Downstream code does not normally interact with slot_state directly;
it is documented here to make the umbrella's internal safety
contracts visible.
See also¶
Slot-state predicates for v0.1.0 lockfree umbrella.
Two predicate families plus an MPSC committed-segment predicate in
sibling segment_state.nim.
Module-layout choice:
shared slot_state.nim for Families A and B. Family-A symbols use the B
suffix (seqIsClosedB, etc.); Family-B uses no suffix (seqIsClosed,
etc.) because LCRQ-integration is the live consumer in v0.1.0 (4 call
sites in queue.nim). The two families intentionally do NOT share a
seqIsClosed symbol so that a silent uint64 ↔ uint width punning
across the substrates cannot occur (orthogonality rationale).
Three substrates → two slot-state predicate families plus one
segment-state predicate (the MPSC committed[i] predicate lives in
the sibling segment_state.nim module):
Family A — Bounded-Vyukov:
Substrate: MPMCCell[T] with payload.seq: Atomic[uint64].
Close sentinel: ClosedBitB = high(uint64) shr 1 (64-bit wide).
Current call sites: NONE (placeholder for future bounded
close-on-empty; consumed by later phases).
Family B — LCRQ-integration:
Substrate: LCRQCell[T] = Atomic[Pair[uint, T]].
Close sentinel: CLOSED_BIT, platform-uint wide.
Live consumer in queue.nim.
Import-cycle note: this module is a substrate for queue.nim (queue.nim
imports it), so it MUST NOT import queue.nim. For Family B that means
seqIsClosed(s: uint) takes a plain uint and uses a locally-defined
LCRQClosedBit constant whose value is computed by the same formula as
queue.nim's CLOSED_BIT* = 1'u shl (sizeof(uint) * 8 - 1).
Drift guard (honest scope): the import cycle (queue.nim imports THIS
module) makes it impossible to import CLOSED_BIT here, so a true
cross-module pin (static: doAssert LCRQClosedBit == CLOSED_BIT)
CANNOT exist. Instead the two constants are kept equal by using the
IDENTICAL formula, and a LOCAL static-assert at the bottom of this
file pins this module's LCRQClosedBit to that canonical formula
(1'u shl (sizeof(uint) * 8 - 1)). That tripwire fires if someone
edits THIS module's constant away from the canonical formula.
RESIDUAL RISK (explicit, not guarded): if someone edits queue.nim's
CLOSED_BIT formula, the divergence is NOT caught here — the local
assert only pins this module's side. Keeping both on the same literal
formula is the only mitigation available without breaking the cycle.
const ClosedBitB = high(uint64) shr 1
Family-A close sentinel. 64-bit wide because the Vyukov
substrate is Atomic[uint64]. Distinct from Family-B's
platform-uint CLOSED_BIT so the two substrates remain lexically
separable (orthogonality rationale).
seqIsEmptyB inline ¶
proc seqIsEmptyB(s: uint64; pos: uint64): bool
Family A. Vyukov empty: seq == pos.
Parameters
-
s(uint64) -
pos(uint64)
Returns
bool
seqIsFilledB inline ¶
proc seqIsFilledB(s: uint64; pos: uint64): bool
Family A. Vyukov filled: seq == pos + 1.
Parameters
-
s(uint64) -
pos(uint64)
Returns
bool
seqIsClosedB inline ¶
proc seqIsClosedB(s: uint64): bool
Family A. Placeholder for future bounded close-on-empty;
zero call sites in v0.1.0.
Parameters
-
s(uint64)
Returns
bool
seqIsClaimedB inline ¶
proc seqIsClaimedB(s: uint64; pos: uint64): bool
Family A. Bounded destructor walk: a slot is "claimed" when
its seq has advanced past the filled epoch but has not been closed.
Parameters
-
s(uint64) -
pos(uint64)
Returns
bool
seqIsLiveB inline ¶
proc seqIsLiveB(slot: var MPMCCell[T]; pos: uint64): bool
Family A. Loads payload.seq with moRelaxed and reports
whether the slot is filled at epoch pos and not closed.
Parameters
-
slot(var MPMCCell[T]) -
pos(uint64)
Returns
bool
seqIsClosed inline ¶
proc seqIsClosed(s: uint): bool
Family B. LCRQ-integration close test. Replaces the inline
(<seq> and CLOSED_BIT) != 0'u literals in queue.nim.
Parameters
-
s(uint)
Returns
bool