Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

STM – Software Transactional Memory

Lean: Hale.STM | Haskell: stm

Pessimistic STM with global mutex serialization. Provides TVar, TMVar, and TQueue for concurrent programming.

Key Types

TypeDescription
STM αTransactional computation
TVar αMutable variable (IO.Ref α)
TMVar αSynchronization variable (empty or full)
TQueue αUnbounded FIFO queue (two-list amortized)

API

FunctionDescription
atomicallyExecute STM transaction
retryBlock and retry transaction
orElseAlternative transaction
newTVarIO / readTVar / writeTVarTVar operations
newTMVar / takeTMVar / putTMVarTMVar operations
newTQueue / readTQueue / writeTQueueTQueue operations

Files

  • Hale/STM/Control/Monad/STM.lean – STM monad, atomically, retry, orElse
  • Hale/STM/Control/Concurrent/STM/TVar.lean – Transactional variables
  • Hale/STM/Control/Concurrent/STM/TMVar.lean – Transactional MVars
  • Hale/STM/Control/Concurrent/STM/TQueue.lean – Transactional queues