🔒 Software Transactional Memory (STM)

Overview

Software Transactional Memory replaces locks with transactions. Each transaction reads a consistent snapshot of shared state. At commit time, the runtime validates that no read variables were modified by other transactions. On conflict, it rolls back and retries automatically.

This is a faithful single-threaded simulation that models STM semantics (snapshots, validation, retry, orElse) without requiring threads — focusing on the algorithm, not OS plumbing.

Concepts Demonstrated

• Optimistic concurrency control — reads are cheap, conflicts detected at commit
• Transaction isolation — each transaction sees a consistent snapshot
• Composability — two STM actions combine into one atomic block (unlike locks)
• Retry & orElse — blocking and choice combinators for conditional synchronization
• Monadic composition — STM actions form a monad for sequencing effects
• Mutable state management — controlled mutation via transactional variables

Core Abstractions

(* TVar: a versioned mutable cell *)
type 'a tvar = {
  mutable value   : 'a;
  mutable version : int;   (* bumped on every write *)
  id              : int;
}

(* STM monad: sequence reads/writes in a transaction *)
(* read_tvar  — record read + version in transaction log *)
(* write_tvar — buffer write locally until commit *)

(* atomically: run transaction, validate reads, commit or retry *)
(* retry: block until a read variable changes *)
(* orElse: try first action; if it retries, try the alternative *)

How Commit Works

1. Transaction executes against a snapshot (reads logged with versions)
2. At commit: validate every read — has the TVar's version changed?
3. If all reads still valid → apply buffered writes atomically
4. If any read is stale → roll back and retry the entire transaction

STM vs Locks vs CRDTs

Key Takeaways

• STM eliminates deadlocks by removing lock ordering requirements
• Composability is the killer feature — combine any two STM actions into one atomic block
• Optimistic approach means high throughput under low contention
• OCaml's type system makes the transaction boundary explicit and safe