Skip to content

Integration

Integrating nim-debra with lock-free data structures.

Overview

This guide shows how to integrate nim-debra into lock-free data structures for safe memory reclamation.

Basic Integration Pattern

  1. Add manager reference to your data structure
  2. Register threads on initialization
  3. Pin during operations
  4. Retire removed nodes
  5. Periodically reclaim

Lock-Free Stack

A complete Treiber stack implementation with DEBRA+ reclamation:

# examples/lockfree_stack.nim
## Lock-free Treiber stack with DEBRA reclamation.

import debra
import std/[atomics, options]

type
  NodeObj[T] = object
    value: T
    next: Atomic[Managed[ref NodeObj[T]]]
  Node[T] = ref NodeObj[T]

  Stack*[T] = object
    head: Atomic[Managed[ref NodeObj[T]]]
    manager: ptr DebraManager[64]
    handle: ThreadHandle[64]

proc newStack*[T](manager: ptr DebraManager[64]): Stack[T] =
  result.manager = manager
  result.handle = registerThread(manager[])

proc push*[T](stack: var Stack[T], value: T) =
  let pinned = unpinned(stack.handle).pin()

  let newNode = managed Node[T](value: value)

  while true:
    var oldHead = stack.head.load(moAcquire)
    newNode.inner.next.store(oldHead, moRelaxed)
    if stack.head.compareExchange(oldHead, newNode, moRelease, moRelaxed):
      break

  discard pinned.unpin()

proc pop*[T](stack: var Stack[T]): Option[T] =
  let pinned = unpinned(stack.handle).pin()

  while true:
    var oldHead = stack.head.load(moAcquire)
    if oldHead.isNil:
      discard pinned.unpin()
      return none(T)

    let next = oldHead.inner.next.load(moRelaxed)
    if stack.head.compareExchange(oldHead, next, moRelease, moRelaxed):
      result = some(oldHead.value)

      # Retire the popped node
      let ready = retireReady(pinned)
      discard ready.retire(oldHead)

      discard pinned.unpin()
      return

proc main() =
  var manager = initDebraManager[64](../../examples)
  setGlobalManager(addr manager)

  var stack = newStack[int](../../examples/addr manager)

  echo "Pushing 1, 2, 3..."
  stack.push(1)
  stack.push(2)
  stack.push(3)

  echo "Popping..."
  while true:
    let item = stack.pop()
    if item.isNone:
      break
    echo "  Popped: ", item.get

  # Reclaim
  for _ in 0..3:
    manager.advance()

  let reclaimResult = reclaimStart(addr manager).loadEpochs().checkSafe()
  case reclaimResult.kind:
  of rReclaimReady:
    let count = reclaimResult.reclaimready.tryReclaim()
    echo "Reclaimed ", count, " nodes"
  of rReclaimBlocked:
    echo "Reclamation blocked"

  echo "Lock-free stack example completed"

when isMainModule:
  main()

View full source

Lock-Free Queue

A complete Michael-Scott queue implementation with DEBRA+ reclamation:

# examples/lockfree_queue.nim
## Lock-free Michael-Scott queue with DEBRA reclamation.

import debra
import std/[atomics, options]

type
  NodeObj[T] = object
    value: T
    next: Atomic[Managed[ref NodeObj[T]]]
  Node[T] = ref NodeObj[T]

  Queue*[T] = object
    head: Atomic[Managed[ref NodeObj[T]]]
    tail: Atomic[Managed[ref NodeObj[T]]]
    manager: ptr DebraManager[64]
    handle: ThreadHandle[64]

proc newQueue*[T](manager: ptr DebraManager[64]): Queue[T] =
  result.manager = manager
  result.handle = registerThread(manager[])

  # Create sentinel node
  let sentinel = managed Node[T](../../examples)
  result.head.store(sentinel, moRelaxed)
  result.tail.store(sentinel, moRelaxed)

proc enqueue*[T](queue: var Queue[T], value: T) =
  let pinned = unpinned(queue.handle).pin()

  let newNode = managed Node[T](value: value)

  while true:
    var tail = queue.tail.load(moAcquire)
    let next = tail.inner.next.load(moAcquire)

    if next.isNil:
      var expected: Managed[Node[T]]
      if tail.inner.next.compareExchange(expected, newNode, moRelease, moRelaxed):
        discard queue.tail.compareExchange(tail, newNode, moRelease, moRelaxed)
        break
    else:
      discard queue.tail.compareExchange(tail, next, moRelease, moRelaxed)

  discard pinned.unpin()

proc dequeue*[T](queue: var Queue[T]): Option[T] =
  let pinned = unpinned(queue.handle).pin()

  while true:
    var head = queue.head.load(moAcquire)
    var tail = queue.tail.load(moAcquire)
    let next = head.inner.next.load(moAcquire)

    if head == tail:
      if next.isNil:
        discard pinned.unpin()
        return none(T)
      discard queue.tail.compareExchange(tail, next, moRelease, moRelaxed)
    else:
      let value = next.value
      if queue.head.compareExchange(head, next, moRelease, moRelaxed):
        # Retire old head (sentinel)
        let ready = retireReady(pinned)
        discard ready.retire(head)

        discard pinned.unpin()
        return some(value)

proc main() =
  var manager = initDebraManager[64](../../examples)
  setGlobalManager(addr manager)

  var queue = newQueue[int](../../examples/addr manager)

  echo "Enqueueing 1, 2, 3..."
  queue.enqueue(1)
  queue.enqueue(2)
  queue.enqueue(3)

  echo "Dequeueing..."
  while true:
    let item = queue.dequeue()
    if item.isNone:
      break
    echo "  Dequeued: ", item.get

  # Reclaim
  for _ in 0..3:
    manager.advance()

  let reclaimResult = reclaimStart(addr manager).loadEpochs().checkSafe()
  case reclaimResult.kind:
  of rReclaimReady:
    let count = reclaimResult.reclaimready.tryReclaim()
    echo "Reclaimed ", count, " nodes"
  of rReclaimBlocked:
    echo "Reclamation blocked"

  echo "Lock-free queue example completed"

when isMainModule:
  main()

View full source

Typestate Composition

DEBRA is implemented using nim-typestates. This means you can compose DEBRA's memory safety guarantees with your own application-level typestates.

This enables "correct by design" algorithms:

  1. Your algorithm's states - Enforced at compile time (e.g., Empty/NonEmpty stack)
  2. DEBRA's protocol - Pin/unpin/retire sequence enforced at compile time
  3. Bridges - Connect your states to other typestates (e.g., popped items enter a processing pipeline)

Library Typestates Are Pluggable

When you import debra, you get access to DEBRA's typestates:

  • Unpinned[N] / Pinned[N] / Neutralized[N] - Epoch guard states
  • RetireReady[N] / Retired[N] - Retirement states
  • ReclaimStart[N] / EpochsLoaded[N] / ReclaimReady[N] / ReclaimBlocked[N] - Reclamation states

Your code uses these directly. The compiler verifies you follow the protocol.

Example: Item Processing Pipeline

Item Processing Typestate

Define a typestate for processing items after they leave the data structure:

# examples/item_processing.nim
## Item lifecycle typestate for demonstrating typestate composition.
##
## This module defines a simple processing pipeline:
##   Unprocessed -> Processing -> Completed | Failed
##
## Use with lockfree_stack_typestates.nim to see how popped items
## bridge into this processing pipeline.

import typestates

type
  Item*[T] = object
    ## Base type for items in the processing pipeline.
    value*: T

  Unprocessed*[T] = distinct Item[T]
    ## Item just received, not yet being processed.

  Processing*[T] = distinct Item[T]
    ## Item currently being worked on.

  Completed*[T] = distinct Item[T]
    ## Item successfully processed (terminal state).

  Failed*[T] = distinct Item[T]
    ## Item processing failed (terminal state).

typestate Item[T]:
  consumeOnTransition = false
  states Unprocessed[T], Processing[T], Completed[T], Failed[T]
  initial Unprocessed[T]
  terminal Completed[T], Failed[T]
  transitions:
    Unprocessed[T] -> Processing[T]
    Processing[T] -> Completed[T] | Failed[T] as ProcessingResult[T]

# Transition: begin processing an item
proc startProcessing*[T](item: Unprocessed[T]): Processing[T] {.transition.} =
  ## Begin processing an unprocessed item.
  Processing[T](../../examples/Item[T](item))

# Transition: finish processing with success or failure
proc finish*[T](item: Processing[T], success: bool): ProcessingResult[T] {.transition.} =
  ## Complete processing. Returns Completed on success, Failed otherwise.
  if success:
    ProcessingResult[T] -> Completed[T](../../examples/Item[T](item))
  else:
    ProcessingResult[T] -> Failed[T](../../examples/Item[T](item))

# Convenience procs for terminal states
proc complete*[T](item: Processing[T]): Completed[T] {.transition.} =
  ## Mark item as successfully completed.
  Completed[T](../../examples/Item[T](item))

proc fail*[T](item: Processing[T]): Failed[T] {.transition.} =
  ## Mark item as failed.
  Failed[T](../../examples/Item[T](item))

when isMainModule:
  # Demonstrate the item processing pipeline
  echo "Item Processing Typestate Demo"
  echo "=============================="
  echo ""

  # Create an unprocessed item
  let raw = Unprocessed[int](../../examples/Item[int](value: 42))
  echo "1. Created item in Unprocessed state"

  # Start processing
  let inProgress = raw.startProcessing()
  echo "2. Transitioned to Processing state"

  # Finish with success
  let successResult = inProgress.finish(success = true)
  echo "3. Finished processing with success"
  case successResult.kind:
  of pCompleted:
    echo "   -> Result: Completed state"
  of pFailed:
    echo "   -> Result: Failed state (unexpected)"

  echo ""

  # Demo failure path
  let raw2 = Unprocessed[int](../../examples/Item[int](value: 99))
  let inProgress2 = raw2.startProcessing()
  let failResult = inProgress2.finish(success = false)
  echo "4. Alternative path: finish with failure"
  case failResult.kind:
  of pCompleted:
    echo "   -> Result: Completed state (unexpected)"
  of pFailed:
    echo "   -> Result: Failed state"

  echo ""
  echo "Item processing typestate example completed successfully"

View source

Example: Stack with Typestate Composition

Lock-Free Stack Typestate

Combine stack states, DEBRA states, and bridges to the item processing pipeline:

# examples/lockfree_stack_typestates.nim
## Lock-free stack with full typestate composition.
##
## Demonstrates:
## 1. Stack states (Empty, NonEmpty) enforced at compile time
## 2. DEBRA's pin/unpin/retire typestates used internally
## 3. Manual bridge from stack to item processing typestate
##
## This is a "correct by design" lock-free data structure.

import typestates
import debra
import ./item_processing
import std/[atomics, options]

type
  NodeObj[T] = object
    value: T
    next: Atomic[Managed[ref NodeObj[T]]]
  Node[T] = ref NodeObj[T]

  StackBase[T] = object
    top: Atomic[Managed[ref NodeObj[T]]]
    manager: ptr DebraManager[64]
    handle: ThreadHandle[64]

  Empty*[T] = distinct StackBase[T]
    ## Stack with no elements.

  NonEmpty*[T] = distinct StackBase[T]
    ## Stack with at least one element.

typestate StackBase[T]:
  consumeOnTransition = false
  states Empty[T], NonEmpty[T]
  transitions:
    Empty[T] -> NonEmpty[T]
    NonEmpty[T] -> Empty[T] | NonEmpty[T] as PopResult[T]

proc initStack*[T](manager: ptr DebraManager[64]): Empty[T] =
  ## Create a new empty stack.
  var base: StackBase[T]
  base.manager = manager
  base.handle = registerThread(manager[])
  Empty[T](../../examples/base)

proc push*[T](stack: Empty[T], value: T): NonEmpty[T] {.transition.} =
  ## Push onto empty stack, returns NonEmpty.
  var base = StackBase[T](../../examples/stack)

  let pinned = unpinned(base.handle).pin()

  let newNode = managed Node[T](value: value)
  base.top.store(newNode, moRelease)

  let unpinResult = pinned.unpin()
  case unpinResult.kind:
  of uUnpinned: discard
  of uNeutralized: discard unpinResult.neutralized.acknowledge()

  NonEmpty[T](../../examples/base)

proc push*[T](stack: NonEmpty[T], value: T): NonEmpty[T] {.transition.} =
  ## Push onto non-empty stack, returns NonEmpty.
  var base = StackBase[T](../../examples/stack)

  let pinned = unpinned(base.handle).pin()

  let newNode = managed Node[T](value: value)

  while true:
    var oldTop = base.top.load(moAcquire)
    newNode.inner.next.store(oldTop, moRelaxed)
    if base.top.compareExchange(oldTop, newNode, moRelease, moRelaxed):
      break

  let unpinResult = pinned.unpin()
  case unpinResult.kind:
  of uUnpinned: discard
  of uNeutralized: discard unpinResult.neutralized.acknowledge()

  NonEmpty[T](../../examples/base)

proc pop*[T](stack: NonEmpty[T]): (PopResult[T], Option[Unprocessed[T]]) =
  ## Pop from non-empty stack.
  ## Returns (new stack state, optional item in Unprocessed state).
  var base = StackBase[T](../../examples/stack)

  let pinned = unpinned(base.handle).pin()

  var resultStack: PopResult[T]
  var item: Option[Unprocessed[T]]

  block popLoop:
    while true:
      var oldTop = base.top.load(moAcquire)

      if oldTop.isNil:
        resultStack = PopResult[T](kind: pEmpty, empty: Empty[T](base))
        item = none(Unprocessed[T])
        break popLoop

      let next = oldTop.inner.next.load(moRelaxed)

      if base.top.compareExchange(oldTop, next, moRelease, moRelaxed):
        item = some(Unprocessed[T](../../examples/Item[T](value: oldTop.value)))

        # Retire the node
        let ready = retireReady(pinned)
        discard ready.retire(oldTop)

        if next.isNil:
          resultStack = PopResult[T](kind: pEmpty, empty: Empty[T](base))
        else:
          resultStack = PopResult[T](kind: pNonempty, nonempty: NonEmpty[T](base))
        break popLoop

  let unpinResult = pinned.unpin()
  case unpinResult.kind:
  of uUnpinned: discard
  of uNeutralized: discard unpinResult.neutralized.acknowledge()

  (resultStack, item)

when isMainModule:
  echo "Lock-Free Stack with Typestate Composition"
  echo "==========================================="
  echo ""

  var manager = initDebraManager[64](../../examples)
  setGlobalManager(addr manager)

  var stack = initStack[int](../../examples/addr manager)
  echo "Created empty stack"

  var nonEmptyStack = stack.push(10)
  echo "Pushed 10 (stack is now NonEmpty)"

  nonEmptyStack = nonEmptyStack.push(20)
  nonEmptyStack = nonEmptyStack.push(30)
  echo "Pushed 20, 30"
  echo ""

  echo "Popping and processing items:"
  var currentStack = nonEmptyStack

  while true:
    let (popResult, itemOpt) = currentStack.pop()

    if itemOpt.isSome:
      let item = itemOpt.get
      let processing = item.startProcessing()
      let processResult = processing.finish(success = true)

      case processResult.kind:
      of pCompleted:
        echo "  Popped and completed: ", Item[int](../../examples/processResult.completed).value
      of pFailed:
        echo "  Popped but failed: ", Item[int](../../examples/processResult.failed).value
    else:
      echo "  Race condition: another thread popped the item first"

    case popResult.kind:
    of pEmpty:
      echo "  Stack is now empty"
      break
    of pNonempty:
      currentStack = popResult.nonempty

  echo ""

  for _ in 0..3:
    manager.advance()

  let reclaimResult = reclaimStart(addr manager).loadEpochs().checkSafe()

  case reclaimResult.kind:
  of rReclaimReady:
    let count = reclaimResult.reclaimready.tryReclaim()
    echo "Reclaimed ", count, " nodes"
  of rReclaimBlocked:
    echo "Reclamation blocked (threads still active)"

  echo ""
  echo "Lock-free stack with typestate composition completed successfully"

View source

Key Points

  • Nested enforcement: DEBRA's pin()/unpin() happens inside your push()/pop() - both are type-checked
  • Bridges connect state machines: Popped items flow from stack states into processing states
  • Zero runtime cost: All validation is compile-time
  • Module-qualified syntax: Use module.Typestate.State in bridges for clarity

Self-Referential Types Pattern

For types that reference themselves (linked lists, trees), use the ref Obj pattern:

# The ref Obj pattern for self-referential Managed types
type
  NodeObj[T] = object
    value: T
    next: Atomic[Managed[ref NodeObj[T]]]
  Node[T] = ref NodeObj[T]

This pattern is required because Nim's type system cannot resolve Managed[Node] inside Node's definition when Node = ref object.

Best Practices

1. Minimize Critical Section Duration

# GOOD - process outside critical section
let pinned = handle.pin()
let data = loadSharedData()
discard pinned.unpin()
processData(data)

# BAD - process inside critical section
let pinned = handle.pin()
let data = loadSharedData()
processData(data)
discard pinned.unpin()

2. Batch Retirements

Retire multiple objects in a single critical section when possible.

3. Handle Neutralization

Always handle the uNeutralized case from unpin(). This is a required pattern - neutralization occurs when the epoch advances during a critical section, and you must acknowledge it before re-pinning.

let unpinResult = pinned.unpin()
case unpinResult.kind:
of uUnpinned:
  # Normal unpin - continue
  discard
of uNeutralized:
  # Was neutralized - must acknowledge before re-pinning
  discard unpinResult.neutralized.acknowledge()

4. Periodic Reclamation

Don't reclaim after every operation - amortize the cost.

Common Pitfalls

Forgetting to Pin

# WRONG - accessing shared data without pinning
let value = queue.head.load(moAcquire).value

# RIGHT - pin before access
let pinned = handle.pin()
let value = queue.head.load(moAcquire).value
discard pinned.unpin()

Retiring Too Early

# WRONG - retire before unlinking
discard ready.retire(oldHead)
queue.head.store(newHead, moRelease)

# RIGHT - retire after unlinking
queue.head.store(newHead, moRelease)
discard ready.retire(oldHead)

Sharing Handles

# WRONG - sharing handle between threads
var sharedHandle: ThreadHandle[64]

# RIGHT - each thread has own handle
proc workerThread() {.thread.} =
  let handle = registerThread(manager)

Performance Tips

  1. Batch operations: Pin once for multiple operations
  2. Amortize reclamation: Reclaim every N operations
  3. Dedicated reclaimer: Use background thread for reclamation
  4. Minimize pinning: Only pin when accessing shared data
  5. Avoid blocking: Don't block while pinned

Next Steps

  • Review API reference
  • Study the complete examples in the repository
  • Benchmark your integration