“Threading Is Simple” — the Lie Too Big to Check

Starting a thread is one line — new Thread(r).start() — and the line looks exactly like every other line of code you've ever written. Same font. Same semicolon. Nothing about it says: you have just changed what your program is.

But you have. A sequential program is a path — one state after another, each line's precondition established by the line before it. Read it top to bottom and you have, in the real and rigorous sense, seen what it does. The moment a second thread touches the same memory, your program stops being a path and becomes a space: the set of every possible interleaving of every instruction of every thread, and your program's correctness is no longer a property of the text — it's a property of every point in that space at once. You didn't add a feature. You changed the mathematical object you're responsible for.

One line to fork, a lifetime to reason

How big is the space? Two threads of just one hundred instructions each can interleave in "200 choose 100" ways — about 9 × 10⁵⁸ distinct executions. Add a third thread: past 10¹⁴⁰. A fourth: past 10²³⁶. For calibration, the observable universe holds around 10⁸⁰ atoms. And the factorial count is actually the optimistic model — it assumes the hardware executes some honest interleaving of your instructions. Modern CPUs don't: store buffers and out-of-order execution produce behaviors that are no interleaving of the program text, which is why memory models exist at all.

What those numbers condemn — and it's important to be precise about this — is sampling. A test suite is a sample. Run a threaded test a million times, a heroic CI budget, and against 10⁵⁹ schedules you have examined a fraction of the behavior with fifty zeros after the decimal point. A race that fires on one schedule in a billion passes every run you will ever afford, then meets a production machine with different timing, different load, a different core count — a machine that samples a different region of the space — and fires. This is why concurrency bugs are the infamous heisenbugs: attach a debugger, add a log line, and the timing shifts enough to move you off the fatal point. The bug doesn't hide from you. You move when you look.

“But nobody verifies by enumeration” — correct. That's the indictment

Here is the rebuttal a sharp reader is already composing: nobody has ever verified anything by enumerating states. A sequential function over two 64-bit inputs has 2¹²⁸ input states — also past the atom count — and we don't blink, because verification has never been enumeration. It's quotienting: you state an invariant, prove the code maintains it, and a billion states collapse into one equivalence class. A mutex is exactly such a move — "all interleavings inside this critical section are equivalent to one" — and a lock-discipline argument is a proof sketch that quotients 10⁵⁹ schedules down to a handful of cases. So the size of the space, alone, condemns testing but not reasoning. Undecidability alone doesn't condemn threading either — "does this sequential program ever divide by zero" is undecidable too, by the same Rice's theorem, and we ship sequential programs anyway.

So why does sequential reasoning survive contact with its enormous space while threaded reasoning drowns in its? Because sequential invariants have three properties that shared-memory threading specifically destroys:

They're local. A sequential invariant about a variable is threatened only by the lines that mention it — you can find them, read them, and be done. Under shared memory, any thread, touching any shared field, from anywhere in the codebase, can invalidate the reasoning you did here. The proof obligation stops being "check this function" and becomes "check this function against everything that runs."

They're compositional. Two correct sequential modules compose into a correct program whenever their interfaces are the whole story — which is precisely the condition a type system can state and check (no hidden aliasing, no shared globals; sequential languages have spent fifty years machine-enforcing exactly this). Two individually correct locking modules can deadlock the moment you call them in the wrong order — and no interface can even express the condition, because lock order is a property of dynamic execution, not of any signature. The one tool civilization has for building large systems out of small verified pieces doesn't survive the fork call.

And nothing checks them. This is the fatal one. Your quotient — the lock ordering, the happens-before edges, the "only touched under lockX" convention — lives in comments and culture. Forget one volatile, acquire two locks in the wrong order in one rarely-taken branch, and the compiler says nothing, the type checker says nothing, the tests (see above) say nothing. Sequential code gets its invariants checked constantly — types, bounds, null analysis, a borrow checker if you have one. Threaded code's invariants are load-bearing and unenforced. The language hands you the largest proof obligation in engineering and grades it on the honor system.

And now look at the lock again, because in this light the mutex — the respectable, textbook, code-reviewed mutex — is revealed as the lie in miniature. A lock makes a seductively local promise: "inside this section, you are alone; sequential reasoning is restored." But whether the promise holds is a global property — it depends on every other lock in the program, acquired in every order, on every path, including the ones written next year by someone who never saw yours. The promise is uncheckable where it's made and breakable from anywhere else; honoring it costs you the very parallelism it exists to permit (a contended lock is a serialization point wearing a concurrency costume); and its failure mode, deadlock, is precisely the liveness property no checker will ever certify. A lock is not a tool for managing shared memory. It's a rental of sequentiality whose terms nobody enforces.

One concession, before the slogan, because every reviewer has seen the counterexample: a single coarse lock in a leaf module — no callouts under it, no second lock in sight, invariant statable in one comment — is honest at that scale; you really can verify it locally. The trouble is that lock honesty doesn't scale, and nothing tells you when you've left the honest regime: each added lock, each callout under a held lock, each new caller multiplies the global obligations, and the language draws no line between "one mutex, verifiable over coffee" and "forty mutexes, unsearchable space." The costume fits perfectly at small n — which is arguably worse than never fitting, because that's how the forty-lock program gets built: one honest lock at a time.

The honest exits

If the disease is invariants that are non-local, non-compositional, and unchecked, an honest cure has to fix at least one of those three — mechanically, not culturally. Three families have seriously tried.

Make the quotient machine-checked. This is Rust: Send/Sync and the borrow checker turn "who may touch this, from where" into types, and a data race into a compile error. By the honesty principle this is the invariant moved from culture into the checker, and it deserves the credit. Note its boundary, though: Rust proves data-race freedom, not liveness — deadlocks remain representable and unchecked — and a race-free execution is still one point in a nondeterministic space. Your bug reproduces if the scheduler feels like it.

Make the composition algebra real. This is software transactional memory, and it deserves a fair hearing precisely because it targets non-compositionality by name: composable atomic blocks, with retry/orElse, restoring the algebra that locks destroy. In Haskell it's real and type-confined. Why isn't it the answer? Because the performance story never materialized at scale; because imperative-language STMs went weakly atomic, reintroducing the footgun at every transactional/non-transactional boundary; and because even a working STM leaves you exactly where Rust does — race-safe inside a nondeterministic schedule, with no journal. Composition was the right target. The execution model underneath it was still the space.

Make the space unrepresentable. This is Erlang's road, and it's ours: SuperJ has no threads. No Thread, no synchronized, no volatile, no memory model — because a memory model is a patch for a construct we declined to admit. A SuperJ process is one thread executing one path: read the code top to bottom and you've seen what it does. Above the runtime, the 10¹⁴⁰ points collapse back into a line, and every invariant you write is local, compositional, and — being sequential — checkable.

Rust, it should be said, sells the first and third exits à la carte — channels and ownership transfer are idiomatic Rust, and a disciplined team can live message-passing-only. The difference is that SuperJ made the third exit mandatory, and the reason is the card none of the other exits holds: not safety but determinism — events sequenced into a recorded order, which is where the payoff of this entire design concentrates.

Where the space still lives — our mea culpa, stated plainly

Let's say the honest version instead of the flattering one. The unsearchable space still exists in our codebase. The claim was never that it can be abolished — hardware is shared memory; something must speak fence. The claim is about where it lives, who is exposed to it, and what shape it's allowed to take. In SuperJ, shared-memory concurrency is sanctioned for exactly one artifact — the lock-free queue — and nothing else. Not "mostly queues." One artifact, and note what makes it the honest one: a lock pretends the shared world is sequential; the queue pretends nothing. It admits the sharing, confines it to a single narrow protocol — a ring of slots, single-writer cursors (so most of it needs no atomics at all), one release store to publish, one acquire load to consume — and exists for one purpose: to move data out of the shared-memory world and into the message world, where reasoning is local again.

It is the airlock between the two models, engineered once, by the people who wrote the memory-model argument down, verified and regression-gated, and it contains not a single lock. Above that layer the space is unrepresentable: no application programmer can re-open it, because the language has no words for it. Java made the expert-layer move too, with java.util.concurrent — and then kept selling raw Thread, synchronized, and shared mutation beside it, to everyone, forever. The difference between the two designs is not the existence of an expert layer. It's whether the footgun is also on the shelf. Every language with concurrency has a priesthood; ours is just not allowed to hand out keys to the reactor.

Order is a topology you draw

What replaces the thread model is not a slogan; it's a specific architecture with its own obligations. A SuperJ system is share-nothing processes connected by queues, and its canonical shape is a star: applications publish commands into per-app queues; a sequencer — the only writer of the event stream — merges them, stamps each with a monotonic sequence number, and publishes a totally ordered journal that every application consumes independently. Within that sequenced domain the guarantee is strict: same journal, same state, every time — restart an application from sequence zero and it reproduces its state bit for bit. Parallelism comes from pipelining stages across cores and from partitioning into independent sequenced domains; flows that need a global order pay the sequencer, flows that don't, don't.

Determinism must be claimed at its true strength, not its flattering one. Across independent domains, cross-domain arrival order varies run to run — so the strong form, "same inputs, same result, every run," holds within a domain, not globally. What holds globally is the property that actually kills the heisenbug: every run, however its cross-domain timing fell out, is replayable, because each domain's journal is the schedule that domain experienced. The "one in a billion" ordering that triggered the failure is not a roll of dice you hope to re-roll — it's a file. You run it again. It happens again. You fix it.

And the surviving bug classes are named, not waved away: message passing makes data races unrepresentable — no shared field to tear — but protocol races remain (independent processes' messages still arrive in some order), a slow consumer can starve a pipeline as surely as priority inversion starved a rover, and queue graphs with cycles and bounded buffers can deadlock through backpressure. Every one of those failures, in this model, arrives with its journal attached.

And the essay's own test must be run against the topology. Is deadlock-freedom of a queue graph local? No — it's a graph property. Compositional? No — two correct pipelines can deadlock when connected. So what, exactly, is different from the lock-ordering convention on the wiki? This: a lock order is a property of dynamic execution, scattered across every call path, undecidable in general — while a queue topology is static, finite, and declarable, which moves the liveness question from Rice's territory into a cycle check you could run on a diagram. That is a categorical improvement in principle — checkable versus uncheckable — and the framework ships a build-time cycle-and-boundedness check that rejects a bounded-queue deadlock and names its queues. The canonical star passes with its cycle recognized and policy-annotated rather than merely drawn.

The receipts

LMAX's single-threaded event-sourced core out-ran the lock-tuned industry. Redis executes commands on one thread to this day (I/O got helper threads in 6.0; the data structures never needed them). Node took over web I/O with one loop. Our own: an 88-nanosecond framework round trip between processes, 10.6 million messages a second, 2.1× the multithreaded JVM system it reimplements, with total ordering and a replayable journal. On hardware where the real costs are cache-line contention and coherence traffic — exactly what sharing maximizes and share-nothing avoids — the queue is not the tax you pay for safety. It's frequently the fast path.

Not a shame

There's a reflex to hear "we removed threads" as a confession of weakness — as if a serious systems language owes you the footgun, and taking it away means we couldn't handle it. Invert that. Every mature engineering field keeps a catalog of designs it refuses to build because they cannot be verified, and the refusal is the maturity. When the analysis says this artifact's failure space cannot be sampled meaningfully, cannot be decided in general, and strips the invariant-reasoning that tames every other large space — the grown-up move is to change the artifact, not to staff the search harder.

It is not a shame to admit that something is not computable. The shame would be knowing it — and shipping the space anyway.