Skip to content
lockfree

lockfree/typestates/spsc_push

SPSC Push operation lifecycle typestate.

Enforces correct sequencing for single-producer push: Start -> LoadPointers -> CheckFull -> WriteData -> Complete

Key invariant: Once data is written, tail MUST be advanced.

Uses N+1 slot arithmetic (no committed flags needed for SPSC).

Types

Section titled “Types”

SPSCPushStart

Section titled “SPSCPushStart”
SPSCPushStart[N] = object

Entry point. No data yet.

SPSCPushPointersLoaded

Section titled “SPSCPushPointersLoaded”
SPSCPushPointersLoaded[N] = object
  head*: WrappedValueN1[N]
  tail*: WrappedValueN1[N]

Loaded head and tail.

SPSCPushNotFull

Section titled “SPSCPushNotFull”
SPSCPushNotFull[N] = object
  tail*: WrappedValueN1[N]
  slot*: PhysicalSlotN1[N]

Confirmed queue has space.

SPSCPushDataWritten

Section titled “SPSCPushDataWritten”
SPSCPushDataWritten[N] = object
  newTail*: WrappedValueN1[N]

Data written to slot. MUST advance tail.

SPSCPushFull

Section titled “SPSCPushFull”
SPSCPushFull[N] = object

Terminal: queue was full.

SPSCPushOpState

Section titled “SPSCPushOpState”
SPSCPushOpState = enum
  fsSPSCPushNotFull, fsSPSCPushFull, fsSPSCPushStart, fsSPSCPushDataWritten,
  fsSPSCPushPointersLoaded

SPSCPushOpStates

Section titled “SPSCPushOpStates”
SPSCPushOpStates[N] = SPSCPushNotFull[N] | SPSCPushFull[N] | SPSCPushStart[N] |
    SPSCPushDataWritten[N] |
    SPSCPushPointersLoaded[N]

SPSCFullCheckKind

Section titled “SPSCFullCheckKind”
SPSCFullCheckKind = enum
  sSPSCPushNotFull, sSPSCPushFull

SPSCFullCheck

Section titled “SPSCFullCheck”
SPSCFullCheck[N] = object
  case kind*: SPSCFullCheckKind
  of sSPSCPushNotFull:
    spscpushnotfull*: SPSCPushNotFull[N]
  of sSPSCPushFull:
    spscpushfull*: SPSCPushFull[N]

SpscBase

Section titled “SpscBase”
SpscBase[N; T] = object
  head* {.align: 128.}: Atomic[int]
  tail* {.align: 128.}: Atomic[int]
  storage*: StorageN1[N, T]

Procedures & Functions

Section titled “Procedures & Functions”

state

Section titled “state”
proc state[N: static int](f: SPSCPushNotFull[N]): SPSCPushOpState

Runtime state inspection for SPSCPushNotFull. Returns the enum value for pattern matching in case expressions.

state

Section titled “state”
proc state[N: static int](f: SPSCPushFull[N]): SPSCPushOpState

Runtime state inspection for SPSCPushFull. Returns the enum value for pattern matching in case expressions.

state

Section titled “state”
proc state[N: static int](f: SPSCPushStart[N]): SPSCPushOpState

Runtime state inspection for SPSCPushStart. Returns the enum value for pattern matching in case expressions.

state

Section titled “state”
proc state[N: static int](f: SPSCPushDataWritten[N]): SPSCPushOpState

Runtime state inspection for SPSCPushDataWritten. Returns the enum value for pattern matching in case expressions.

state

Section titled “state”
proc state[N: static int](f: SPSCPushPointersLoaded[N]): SPSCPushOpState

Runtime state inspection for SPSCPushPointersLoaded. Returns the enum value for pattern matching in case expressions.

$

proc `$`[N: static int](s: SPSCPushNotFull[N]): string

String representation for state ‘SPSCPushNotFull’. Returns the bare state name (no fs prefix).

$

Section titled “$”
proc `$`[N: static int](s: SPSCPushFull[N]): string

String representation for state ‘SPSCPushFull’. Returns the bare state name (no fs prefix).

$

Section titled “$”
proc `$`[N: static int](s: SPSCPushStart[N]): string

String representation for state ‘SPSCPushStart’. Returns the bare state name (no fs prefix).

$

Section titled “$”
proc `$`[N: static int](s: SPSCPushDataWritten[N]): string

String representation for state ‘SPSCPushDataWritten’. Returns the bare state name (no fs prefix).

$

Section titled “$”
proc `$`[N: static int](s: SPSCPushPointersLoaded[N]): string

String representation for state ‘SPSCPushPointersLoaded’. Returns the bare state name (no fs prefix).

$

Section titled “$”
proc `$`(s: SPSCPushOpState): string {.raises: [], tags: [], forbids: [].}

String representation of SPSCPushOpState enum. Strips the fs prefix for human-friendly output.

toSPSCFullCheck

Section titled “toSPSCFullCheck”
proc toSPSCFullCheck[N: static int](s: sink SPSCPushNotFull[N]): SPSCFullCheck[N]

toSPSCFullCheck

Section titled “toSPSCFullCheck”
proc toSPSCFullCheck[N: static int](s: sink SPSCPushFull[N]): SPSCFullCheck[N]

$

Section titled “$”
proc `$`[N: static int](r: SPSCFullCheck[N]): string

String representation of branching union ‘SPSCFullCheckN’. Returns the active branch’s bare state name.

start

Section titled “start”
proc start[N: static int](): SPSCPushStart[N] {.inline.}

Begin a push operation.

loadPointers

Section titled “loadPointers”
proc loadPointers[N: static int; T](op: sink SPSCPushStart[N];
                                    queue: var SpscBase[N, T]): SPSCPushPointersLoaded[
    N] {.inline, raises: [], tags: [TypestateOp, RootEffect].}

Load head and tail atomically.

checkFull

Section titled “checkFull”
proc checkFull[N: static int](op: sink SPSCPushPointersLoaded[N]): SPSCFullCheck[
    N] {.inline, raises: [], tags: [TypestateOp, RootEffect].}

Check if queue is full. Returns branch type.

writeData

Section titled “writeData”
proc writeData[N: static int; T](op: sink SPSCPushNotFull[N];
                                 queue: var SpscBase[N, T]; item: sink T): SPSCPushDataWritten[
    N] {.inline, raises: [], tags: [TypestateOp, RootEffect].}

Write item to the slot.

complete

Section titled “complete”
proc complete[N: static int; T](op: SPSCPushDataWritten[N];
                                queue: var SpscBase[N, T]): bool {.inline,
    notATransition.}

Advance tail and return success.

extractFalse

Section titled “extractFalse”
proc extractFalse[N: static int](op: SPSCPushFull[N]): bool {.notATransition.}

Terminal: extract false result (queue was full).

Templates

Section titled “Templates”

->

Section titled “->”
template `->`[N: static int](_: typedesc[SPSCFullCheck[N]];
                             s: sink SPSCPushNotFull[N]): SPSCFullCheck[N]

->

Section titled “->”
template `->`[N: static int](_: typedesc[SPSCFullCheck[N]];
                             s: sink SPSCPushFull[N]): SPSCFullCheck[N]

Macros

Section titled “Macros”

match

Section titled “match”
macro match[N: static int](value: SPSCFullCheck[N]; arms: untyped): untyped

Pattern-match on a branching union; rewrites into a case over the kind discriminator. The value being matched must be a var binding. Branch fields are extracted with move(), which requires a mutable binding. Syntax is StateName(bind):, not of StateName as bind:.

match

Section titled “match”
macro match[N: static int](value: SPSCPushOpStates[N]; arms: untyped): untyped

Single-target pattern match on states of typestate ‘SPSCPushOp’; rewrites to block: let bind = move(value); body. Syntax is <StateName>(bind):, with exactly one arm.

SPSCPushOp

Section titled “SPSCPushOp”
macro SPSCPushOp(initial`gensym0: untyped; typeDef`gensym0: untyped): untyped

Typestate-attachment pragma (auto-generated; see §3.7 of the v0.9.0 design doc). Apply to a type declaration to bind the type to this typestate with initial as the starting state. Validates TA-002..TA-004 at compile time and populates typestateAttachments.