Software Transactional Memory for Cats Effect with intelligent scheduling.

Bengal STM lets you compose concurrent operations as in-memory transactions: you write the sequence of reads and writes you want, and the library takes care of locking, retries, semantic blocking and scheduling.

• A scheduler that knows what each transaction will touch. Before running a transaction, Bengal computes its footprint — the variables and map keys it will access — and runs only transactions that cannot conflict at the same time. A blindly optimistic STM lets conflicting transactions race and then throws the loser's work away; Bengal mostly avoids the collision. The footprint is more than a throughput device: reads take no locks and are never validated at commit time, so the footprint check is the only thing standing between a transaction and a stale read. See Static analysis and transaction footprints — it also explains the one shape that costs you concurrency, and how to avoid it.

• Transactional maps as a first-class structure. TxnVarMap tracks conflicts per key, so two transactions writing different keys of the same map run concurrently. Wrapping a Map in a TxnVar makes every write conflict with every other. One cost to know about: the map retains an internal id-registry entry for every distinct key it has ever seen — read, written, deleted, or merely probed — for the map's lifetime. Prefer bounded key spaces; a map keyed by an unbounded stream (session ids, request ids) grows without limit.

• Semantic blocking. waitFor parks a transaction until its condition can hold, without blocking a thread. See How waitFor wakes up — the rule there is load-bearing, and getting it wrong parks a transaction permanently.

• Built on Cats Effect, polymorphic in F[_] over Async.

The commit and scheduling protocols are specified in TLA+ and model-checked in CI. That work found eight concurrency defects in the shipped library — several of which no test could have caught — and later proved a whole commit-time check unreachable, so it was deleted. See Correctness.

• Java: 21 or later
• Scala: 2.13.x or 3.x
• Versioning: pre-1.0 (0.x) — minor versions may break source and binary compatibility. Per-release breaks are listed in CHANGELOG.md; MiMa checks binary compatibility within a minor line.

Add the following dependency to your build.sbt:

libraryDependencies += "ai.entrolution" %% "bengal-stm" % "<version>"

See the Maven Central badge above for the latest version.

import ai.entrolution.bengal.stm.STM
import ai.entrolution.bengal.stm.model._
import ai.entrolution.bengal.stm.syntax.all._
import cats.effect.{IO, IOApp}

object QuickStart extends IOApp.Simple {
  def run: IO[Unit] =
    STM.runtime[IO].flatMap { implicit stm =>
      for {
        counter <- TxnVar.of[IO, Int](0)
        _       <- counter.modify(_ + 1).commit
        value   <- counter.get.commit
        _       <- IO.println(s"Counter: $value")
      } yield ()
    }
}

All three imports are needed. syntax.all._ is what brings .get / .set / .modify / .commit into scope; without it .get fails with a cannot be accessed error rather than a missing-import one, because the runtime's own private[stm] members shadow the extension methods.

On STM[F]. and the imports. pure, delay, fromF, unit, abort and waitFor are members of STM[F], not free functions — call them as STM[IO].pure(...). The extension methods (.get, .set, .modify, .commit, and the F-variants) come from import ai.entrolution.bengal.stm.syntax.all._. An implicit STM[F] in scope is not enough on its own; you need the import. (STM[F] also exposes allocateTxnVar and allocateTxnVarMap — direct equivalents of TxnVar.of / TxnVarMap.of for code that holds the runtime instance.)

On effectful arguments. The F-variants (setF, modifyF, handleErrorWithF) and the delay/fromF combinators must not encapsulate side effects — but their evaluation frequencies differ. delay/fromF thunks run in both passes of every executed attempt that reaches them (the analysis pass and the log run), and again on every retry; a flow already terminated at a waitFor retry or abort reaches them in neither pass. The F-variant setter values are not forced during analysis: they run once per executed attempt, plus once per retry. handleErrorWithF's handler runs only on an error. The common rule stands for all of them — a re-run must be harmless.

On by-name arguments. Every => above is load-bearing rather than cosmetic. Whether an expression is evaluated during the analysis pass — and can therefore throw there — depends on exactly this; see Static analysis.

This example demonstrates transactional transfers between accounts with semantic blocking until the bank opens:

import ai.entrolution.bengal.stm.STM
import ai.entrolution.bengal.stm.model._
import ai.entrolution.bengal.stm.syntax.all._
import cats.effect.{IO, IOApp}
import scala.concurrent.duration._

object BankTransfer extends IOApp.Simple {

  def run: IO[Unit] = {
    def createAccount(
        name: String,
        initialBalance: Int,
        accounts: TxnVarMap[IO, String, Int]
    )(implicit stm: STM[IO]): IO[Unit] =
      accounts.set(name, initialBalance).commit

    def transferFunds(
        accounts: TxnVarMap[IO, String, Int],
        bankOpen: TxnVar[IO, Boolean],
        to: String,
        from: String,
        amount: Int
    )(implicit stm: STM[IO]): IO[Unit] =
      (for {
        balance    <- accounts.get(from)
        isBankOpen <- bankOpen.get
        _          <- STM[IO].waitFor(isBankOpen)
        _          <- STM[IO].waitFor(balance.exists(_ >= amount))
        _          <- accounts.modify(from, _ - amount)
        _          <- accounts.modify(to, _ + amount)
      } yield ()).commit

    def openBank(
        bankOpen: TxnVar[IO, Boolean]
    )(implicit stm: STM[IO]): IO[Unit] =
      for {
        _ <- IO.sleep(1000.millis)
        _ <- IO.println("Bank Open!")
        _ <- bankOpen.set(true).commit
      } yield ()

    def printAccounts(
        accounts: TxnVarMap[IO, String, Int]
    )(implicit stm: STM[IO]): IO[Unit] =
      for {
        accounts <- accounts.get.commit
        _ <- IO.println(accounts.toList.map { case (k, v) => s"$k: $v" }.mkString(", "))
      } yield ()

    STM.runtime[IO].flatMap { implicit stm =>
      for {
        bankOpen <- TxnVar.of(false)
        accounts <- TxnVarMap.of[IO, String, Int](Map())
        _        <- createAccount("David", 100, accounts)
        _        <- createAccount("Sasha", 0, accounts)
        _        <- printAccounts(accounts)
        _        <- openBank(bankOpen).start
        _        <- transferFunds(accounts, bankOpen, "Sasha", "David", 100)
        _        <- printAccounts(accounts)
      } yield ()
    }
  }
}

Bengal's scheduler is what makes it different from a blindly optimistic STM: before a transaction runs, it works out that transaction's footprint — the set of variables and map keys it will touch — and uses it to run only transactions that cannot conflict at the same time. That is where the concurrency comes from. (How the footprint machinery, the scheduler, and the commit protocol fit together is narrated in docs/architecture.md.)

To do that, Bengal runs your transaction through a static-analysis pass. It is a real execution: reads happen, so values that later steps depend on are available. But writes are not applied, because the transaction has not been scheduled yet.

That last point has a consequence worth knowing about.

Not everything in your transaction runs during analysis, and the distinction decides whether a given expression can throw there:

Both columns are by-name, so it is not something you can read off the call site — it is a property of the combinator. The value you pass to set is suspended and the analyser never looks at it; the key you pass to set is forced, because the footprint cannot be computed without it.

During the analysis pass, a read of something the transaction itself wrote earlier returns the pre-transaction value, not the written one. If a step in the forced column cannot cope with that, it throws — during analysis only, never at run time:

for {
  _   <- inventory.set(sku, 10)
  qty <- inventory.get(sku)                      // analysis sees None; the real run sees Some(10)
  n   <- STM[IO].delay(qty.get + 1)              // forced: `.get` on None throws, in analysis only
  _   <- restock.set(sku, n)
} yield ()

Note where the .get sits. Written as restock.set(sku, qty.get + 1) this transaction is fine — the value argument is never evaluated by the analyser, so nothing throws and the footprint is complete. Move the same expression into a delay and it becomes the problem case. The hazard follows the combinator, not the expression.

The other way to hit it is a key thunk that throws — for example, computing a map key from a value you read back and .get-ing an Option to do it.

Bengal handles this safely, and the safe answer costs throughput. When analysis cannot determine the whole footprint, the transaction is marked as under-approximated, and an under-approximated footprint is treated as conflicting with everything. The transaction runs alone, and it keeps doing so on every attempt — this is not a one-off cost that a retry recovers.

That is deliberate, and it is not conservatism for its own sake. Reads are not validated at commit time and take no locks, so the scheduler's footprint check is the only thing standing between a transaction and a stale read. A footprint that is missing entries does not make the scheduler slightly less precise — it switches its protection off. Running such a transaction on its own is what keeps it correct. (Before this was fixed, a pair of such transactions produced non-serializable results in 198 of 200 contended runs.)

Measured cost: −34.7% throughput against the same workload before the fix, roughly two-thirds of what a comparable transaction with a fully-known footprint achieves. A data-dependent key (below) is a net gain on the current tree — the coverage check costs what it costs, and the id-registry and fold work that landed since more than pays for it.

Nothing else got slower. The commit path sits inside its own noise against the pre-fix baseline while carrying H6's coverage check on every commit, and a whole-map read plus insert is faster — because the same work that added the coverage check also proved the older commit-time dirty check could never fire, and deleting that (plus the id-registry and fold work) was worth more than the coverage check costs. The numbers live in benchmarks/README.md (re-measured 2026-07-14 on a dedicated Ryzen 9 5950X with the reworked harness); read that README's opening before trusting any number you produce there yourself — it leads with the two ways these measurements have already been got wrong.

Keep the throwing expression out of the forced positions:

// Best: keep the value you are about to write, instead of reading it back.
val qty = 10
for {
  _ <- inventory.set(sku, qty)
  _ <- restock.set(sku, qty + 1)
} yield ()

// Or make the forced expression total, so nothing throws during analysis.
for {
  _   <- inventory.set(sku, 10)
  qty <- inventory.get(sku)
  n   <- STM[IO].delay(qty.getOrElse(0) + 1)   // `.getOrElse`, not `.get`
  _   <- restock.set(sku, n)
} yield ()

The same applies to anything else that can throw in a forced position — partial pattern matches, .head on a possibly-empty collection, and so on. If it throws only because a write has not been applied yet, it costs you concurrency rather than correctness.

A related case: if a map key is computed from a value the transaction reads, the footprint depends on that value — and the analysis pass runs before the transaction is scheduled, so the value can change in between. Bengal detects this at commit time, discards the run before it publishes anything, and re-runs with the correct footprint. It is safe; it costs a retry.

waitFor(predicate) parks the transaction until the predicate can hold. What wakes it is not the predicate — it is the transaction's read set. A parked transaction is woken when another transaction commits a write that its footprint conflicts with; it then re-runs from the top and re-evaluates the predicate against fresh reads.

The rule that follows is short, and getting it wrong parks a transaction permanently:

Everything the predicate depends on must be read from a TxnVar or TxnVarMap inside the same transaction.

// CORRECT — `isOpen` is read inside the transaction, so it is in the read set,
// and a commit to `bankOpen` wakes this.
for {
  isOpen <- bankOpen.get
  _      <- STM[IO].waitFor(isOpen)
  _      <- from.modify(_ - amount)
} yield ()

// WRONG — the read is hoisted out. The transaction's read set is empty, nothing
// can ever conflict with it, and no commit will ever wake it. It parks forever.
val isOpen = bankOpenRef.get.unsafeRunSync()
for {
  _ <- STM[IO].waitFor(isOpen)
  _ <- from.modify(_ - amount)
} yield ()

Two further details:

• A predicate that throws aborts the transaction; it does not retry it.
• handleErrorWith does not absorb a waitFor retry. Wrapping a blocking transaction in an error handler will not make it stop blocking.

Cancelling the F returned by commit — a timeout, a lost race, supervisor shutdown — abandons the transaction. Once the cancellation completes:

• the transaction never begins executing again;
• a parked waitFor transaction is removed from the retry machinery — no later commit can wake it, so it cannot run and publish after its caller has gone;
• all scheduler bookkeeping is released, and transactions queued behind the abandoned one proceed.

One carve-out: the atomic commit window itself is uncancelable. A window already executing when cancellation arrives runs to completion, and its writes may be published — cancellation does not interrupt a window in flight; it prevents every future one, promptly, without waiting on the in-flight one. commit.timeout(d) therefore composes safely with waitFor: the timeout fires, the transaction is abandoned, and nothing leaks.

Every TxnVar and TxnVarMap belongs to the STM runtime in scope when it was created, and all transactions touching it must be committed through that runtime. Sharing a variable across two runtimes is undefined: each scheduler enforces its conflict guarantees only over its own transactions, so two conflicting transactions committed under different runtimes can interleave unchecked — stale reads and lost updates with no error raised. One STM.runtime per application (or per isolated variable set) is the rule.

Bengal's commit and scheduling protocols are specified in TLA+ and model-checked in CI on every change. The specs live in specs/.

That work found eight concurrency defects in the shipped library — a catalogue that runs from a lock-order deadlock and a write skew to two distinct lost wakeups and a data-dependent footprint divergence; the authoritative per-defect table, with verdicts and pinned expectations, is in specs/README.md. Every one is fixed, and every one is pinned by a CI expectation, so its counterexample would come back if the fix regressed.

The part worth knowing, if you are weighing a library like this one:

Several of these cannot be found by running the code at all. A lost wakeup needs a conflicting transaction's entire submit-and-commit to land inside a window a couple of microseconds wide. Randomized testing did not produce one across millions of operations, and neither did a soak built specifically to try. The model finds it in seconds.

That is measured, not asserted: every fix was reverted in turn and the behavioural suites re-run to see which would have caught it. The table is in specs/README.md. The conclusion it points to is worth stating plainly — a green test suite is not evidence that these protocols are correct. The pinned models are.

A JMH suite measures what the correctness work cost. The headline: one deliberate cliff — a transaction whose footprint cannot be fully analysed runs alone, at roughly two-thirds throughput — and nothing else got slower. The numbers, the method, and the two ways these measurements have already been got wrong are in benchmarks/README.md.

For an introduction to STM concepts, see Beautiful Concurrency by Simon Peyton Jones.

Under high contention, a blindly optimistic STM does a lot of work it then throws away. In production that pushed us toward running transactions sequentially, which gives up the point of STM. Bengal's scheduler works out what each transaction will touch before running it, so conflicting transactions are kept apart instead of colliding and retrying.

Bengal also treats Map as a first-class transactional structure, roughly the way a database treats an index. That makes structural updates an interesting scheduling problem — a whole-map read has to conflict with a new-key insert somewhere else in the map, or you get phantoms — and it is worth the trouble in practice.

cats-stm is an excellent STM for Cats Effect. Bengal differs in:

• Scheduling: cats-stm executes optimistically and retries on conflict. Bengal computes each transaction's footprint up front and schedules around conflicts.
• Maps: TxnVarMap tracks conflicts per key, rather than per map.
• Implementation: Free monads with two interpreters — one for the static-analysis pass, one for the transaction log (docs/architecture.md walks the whole runtime).
• API: cats-stm has orElse to bypass a retry; Bengal omits it (see below).
• Verification: Bengal's commit and scheduling protocols are specified in TLA+ and model-checked in CI. See Correctness.

Because Bengal abandons a transaction the instant a waitFor predicate fails, rather than running it to completion and discarding the result. That short-circuit is only sound if nothing downstream could still rescue the transaction — which is exactly what an orElse would be. Adding one would mean checking, on every failed predicate, whether some later branch might recover it. waitFor means block until this holds, and nothing else.

Bengals are a very playful and active cat breed. The name fits a library built on Cats.

Contributions are welcome! Please see CONTRIBUTING.md for guidelines.

For security vulnerabilities, use the process in SECURITY.md rather than a public issue.

Bengal STM is licensed under the Apache License 2.0.

Copyright 2023 Greg von Nessi