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.
##
## Atomic node slots use `ptr NodeObj[T]`, not `ref NodeObj[T]`:
## `Atomic[ref T]` falls back to spinlock-based atomics on arc/orc, which
## silently defeats lock-free guarantees. `retain` / `releaseDestructor`
## from `debra/refptr` bridge a Nim `ref` into a raw pointer with explicit
## GC tracking.

import debra
import debra/atomics
import std/options

type
  NodeObj[T] = object
    value: T
    next: Atomic[ptr NodeObj[T]]

  Node[T] = ref NodeObj[T]

  Stack*[T] = object
    head: Atomic[ptr 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 newNode = retain Node[T](value: value)

  stack.handle.withPin:
    while true:
      let oldHead = stack.head.load(moAcquire)
      newNode.next.store(oldHead, moRelaxed)
      var observed = oldHead
      if stack.head.compareExchangeStrong(observed, newNode, moRelease, moRelaxed):
        break

proc pop*[T](stack: var Stack[T]): Option[T] =
  result = none(T)

  stack.handle.withPin:
    block popLoop:
      while true:
        let oldHead = stack.head.load(moAcquire)
        if oldHead == nil:
          break popLoop

        let next = oldHead.next.load(moRelaxed)
        var observed = oldHead
        if stack.head.compareExchangeStrong(observed, next, moRelease, moRelaxed):
          result = some(oldHead.value)
          # Retire the popped node. The destructor balances the `retain`
          # done by `push` once the epoch is safe.
          it.retire(cast[pointer](../../examples/oldHead), releaseDestructor[NodeObj[T]](../../examples))
          break popLoop

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.
##
## Atomic node slots use `ptr NodeObj[T]`, not `ref NodeObj[T]`:
## `Atomic[ref T]` falls back to spinlock-based atomics on arc/orc, which
## silently defeats lock-free guarantees. `retain` / `releaseDestructor`
## from `debra/refptr` bridge a Nim `ref` into a raw pointer with explicit
## GC tracking.

import debra
import debra/atomics
import std/options

type
  NodeObj[T] = object
    value: T
    next: Atomic[ptr NodeObj[T]]

  Node[T] = ref NodeObj[T]

  Queue*[T] = object
    head: Atomic[ptr NodeObj[T]]
    tail: Atomic[ptr 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. `retain` pins it in the GC and yields a ptr we
  # can store atomically. The sentinel is balanced by the retire path
  # the first time it gets dequeued.
  let sentinel = retain Node[T](../../examples)
  result.head.store(sentinel, moRelaxed)
  result.tail.store(sentinel, moRelaxed)

proc enqueue*[T](queue: var Queue[T], value: T) =
  let newNode = retain Node[T](value: value)

  queue.handle.withPin:
    while true:
      let tail = queue.tail.load(moAcquire)
      let next = tail.next.load(moAcquire)

      if next == nil:
        var expected: ptr NodeObj[T] = nil
        if tail.next.compareExchangeStrong(expected, newNode, moRelease, moRelaxed):
          # Best-effort "help" to swing the tail forward. A spurious weak
          # failure here is fine — another enqueue/dequeue will retry the
          # same swing on its next iteration. Weak avoids the LL/SC retry
          # loop on weakly-ordered architectures.
          var observedTail = tail
          discard
            queue.tail.compareExchangeWeak(observedTail, newNode, moRelease, moRelaxed)
          break
      else:
        # Help-along: another producer enqueued but hasn't yet swung the
        # tail. Weak CAS is sufficient — spurious failure is harmless;
        # the next iteration retries.
        var observedTail = tail
        discard queue.tail.compareExchangeWeak(observedTail, next, moRelease, moRelaxed)

proc dequeue*[T](queue: var Queue[T]): Option[T] =
  result = none(T)

  queue.handle.withPin:
    block dequeueLoop:
      while true:
        let head = queue.head.load(moAcquire)
        let tail = queue.tail.load(moAcquire)
        let next = head.next.load(moAcquire)

        if head == tail:
          if next == nil:
            break dequeueLoop
          # Help-along: same as in `enqueue`'s help branch. Weak is fine
          # because a spurious failure is recovered by the next iteration.
          var observedTail = tail
          discard
            queue.tail.compareExchangeWeak(observedTail, next, moRelease, moRelaxed)
        else:
          let value = next.value
          var observedHead = head
          if queue.head.compareExchangeStrong(observedHead, next, moRelease, moRelaxed):
            # Retire old head (sentinel). The destructor will GC_unref it
            # once the epoch is safe, balancing the `retain` from newQueue
            # or the previous enqueue.
            it.retire(cast[pointer](../../examples/head), releaseDestructor[NodeObj[T]](../../examples))
            result = some(value)
            break dequeueLoop

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

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

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.
##
## Atomic node slots use `ptr NodeObj[T]`, not `ref NodeObj[T]`:
## `Atomic[ref T]` falls back to spinlock-based atomics on arc/orc, which
## silently defeats lock-free guarantees. `retain` / `releaseDestructor`
## from `debra/refptr` bridge a Nim `ref` into a raw pointer with explicit
## GC tracking.

import typestates
import debra
import debra/atomics
import ./item_processing
import std/options

type
  NodeObj[T] = object
    value: T
    next: Atomic[ptr NodeObj[T]]

  Node[T] = ref NodeObj[T]

  StackBase[T] = object
    top: Atomic[ptr 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 = retain 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 = retain Node[T](value: value)

  while true:
    let oldTop = base.top.load(moAcquire)
    newNode.next.store(oldTop, moRelaxed)
    var observed = oldTop
    if base.top.compareExchangeStrong(observed, 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:
      let oldTop = base.top.load(moAcquire)

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

      let next = oldTop.next.load(moRelaxed)

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

        # Retire the node. The destructor balances the `retain` from
        # `push` once the epoch is safe.
        let ready = retireReady(pinned)
        discard ready.retire(cast[pointer](../../examples/oldTop), releaseDestructor[NodeObj[T]](../../examples))

        if next == nil:
          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 with Atomic[ptr NodeObj[T]]:

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

ptr is opaque to Nim's type checker, so the recursive shape resolves without forward-declaration gymnastics. Use retain to GC-pin a ref and hand back a raw pointer for atomic storage; pair it with releaseDestructor[NodeObj[T]]() at retire time. See examples/lockfree_queue.nim for the canonical pattern.

Best Practices

1. Minimize Critical Section Duration

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

# BAD - process inside critical section
let pinned = unpinned(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 = unpinned(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