Concurrency Models

Lead Summary

Concurrency—the ability of a system to make progress on multiple tasks whose execution overlaps in time—has been a central challenge in computing since long before multi-core processors made it unavoidable. The difficulty is not merely engineering; it is foundational. Shared mutable state, race conditions, deadlocks, and resource leaks are not bugs in individual programs but predictable consequences of reasoning models ill-suited to simultaneous execution.

Over six decades, researchers and practitioners have developed a layered set of concurrency models: abstract mathematical frameworks that define what concurrent execution means, programming language primitives that expose those abstractions to developers, and runtime systems that implement them efficiently. The field has repeatedly discovered that the same problems—how to coordinate access to shared resources, how to propagate errors across concurrent tasks, how to reason about what a concurrent program does—reappear at every level of abstraction, from hardware synchronization primitives to distributed databases.

This article traces those models from their formal origins through their language implementations and into the practical systems that run in production today.

Historical Development

The Formal Foundations: CSP and the 1970s

The modern field of concurrency theory traces a clear origin point: Tony Hoare's 1978 paper introducing Communicating Sequential Processes. CSP defined concurrent systems as independent sequential processes that coordinate exclusively through synchronous message passing on named channels. Two processes communicate only when both are ready to exchange a message—a rendezvous that eliminates the need for shared memory.

The original formulation was algebraic, providing notation and laws for composing processes. By 1984, Brookes, Hoare, and Roscoe had given CSP three mutually consistent denotational semantic models:

• The traces model, recording observable communication sequences
• The stable failures model, adding information about blocked communication
• The failures-divergences model, accounting for nondeterminism and infinite loops

These models provided a sound mathematical foundation for proving process equivalence and refinement—properties that could be mechanically checked using tools like FDR (Failures-Divergence Refinement).

Hardware Takes CSP Seriously: The Transputer Era

In the 1980s, Inmos manufactured the transputer—a microprocessor architecture that integrated CPU cores with multiple serial communication links, enabling efficient concurrent programming without shared memory. The Occam language, designed for transputers, mapped CSP processes directly to transputer cores and channel communications to inter-processor links.

This tight alignment between formal model, language, and hardware demonstrated the practical viability of synchronous message-passing architectures for scalable concurrent systems—a proof of concept whose lessons outlasted the transputer hardware itself.

Actors and the Erlang Lineage

The actor model, independently developed by Carl Hewitt in the early 1970s, offered a different decomposition: actors are independent entities with private state, communicating through asynchronous messages placed in buffered mailboxes. Where CSP requires synchronous rendezvous, the actor model decouples senders from receivers, making it more natural for distributed systems where latency and partial failure are unavoidable.

Erlang, developed at Ericsson in the 1980s, brought the actor model into production in telecom infrastructure. The BEAM virtual machine was designed specifically to optimize for concurrent execution and fault-tolerant systems rather than raw throughput. BEAM processes require approximately 2.5KB of memory—not OS-level threads but lightweight scheduled entities. A single Erlang system can manage millions of concurrent processes, with each process having its own heap and garbage collector.

Core Concepts

The Shared-State Problem

The root difficulty in concurrent programming is shared mutable state. When two threads can simultaneously read and write the same memory location, the result depends on timing—an outcome invisible to either thread alone. Immutable data structures eliminate this class of bugs entirely: because immutable values cannot change, there is no race to observe. Functional languages like Haskell demonstrated that the attack surface for a single-core program can be identical to that of a multi-core program when immutability is enforced by design.

For programs that do require mutable state, two main strategies dominate: shared-memory concurrency (using locks, compare-and-swap, and other synchronization primitives) and message-passing concurrency (using channels or mailboxes to transfer ownership of data rather than sharing it).

Message Passing vs. Shared Memory

The actor model and CSP represent different points in the design space of message-passing:

Actors use asynchronous messaging with buffered mailboxes that decouple senders from receivers. CSP uses synchronous rendezvous requiring simultaneous alignment. The actor model is more general and suitable for distributed systems; CSP's synchrony enables tighter resource control and simpler reasoning.

Bartosz Milewski's analysis makes the tradeoff precise: asynchronous messaging enables systems to scale across distributed machines where simultaneous process alignment is impossible, but adds complexity in buffer management and failure handling. Synchronous CSP simplifies reasoning about process coordination at the cost of making distributed deployment harder.

BEAM processes communicate exclusively through message passing, not shared memory. This design prevents classical data races: multiple processes cannot simultaneously access and modify shared state. Concurrency issues are limited to application logic bugs (incorrect messages sent), not memory corruption or low-level synchronization failures.

Hardware Primitives: Compare-and-Swap

Not all concurrency can be managed through message passing. Shared-memory systems require synchronization primitives. The most powerful of these is Compare-and-Swap (CAS), a hardware instruction that atomically reads a memory location, compares it to an expected value, and conditionally updates it.

Maurice Herlihy proved that CAS has an infinite consensus number—it can be used to solve consensus among any number of processes. This makes CAS a universal primitive: any concurrent object that can be defined by a sequential specification can be implemented in a wait-free, linearizable manner using CAS and read-write registers.

Classification & Taxonomy

By Coordination Mechanism

Concurrency models cluster around their fundamental coordination strategy:

Shared-memory models — threads share an address space and coordinate through mutual exclusion (locks, semaphores) or lock-free data structures (CAS-based queues, atomic references). Correctness requires careful discipline from programmers; the type system typically offers little assistance.

Message-passing models — processes or actors communicate through channels (CSP) or mailboxes (actors). The absence of shared state provides a natural isolation boundary. BEAM's per-process GC is a direct consequence: each process has its own heap, so GC pauses affect only one process at a time.

Event-loop models — a single thread runs an event loop that dispatches callbacks or resumes coroutines when I/O completes. Python's asyncio uses platform-specific I/O multiplexing mechanisms (epoll on Linux, kqueue on macOS, IOCP on Windows) to monitor multiple I/O operations without blocking. Asyncio coroutines are substantially more lightweight than OS threads, enabling thousands of concurrent coroutines within a single thread.

Software transactional memory (STM) — transactions on shared memory are retried on conflict, analogous to database transactions. Offers composability that locks do not, but at the cost of runtime overhead and potential livelock.

By Fault Tolerance Architecture

Defensive programming — checks at every call site to prevent errors upfront. Increases code complexity and execution overhead; individual functions must reason about all possible failure modes.

Supervision trees (let it crash) — accepts that unanticipated failures will occur and builds recovery into the system's structure. Erlang's OTP supervision framework allows supervisors to restart failing actors, escalate failures up a tree, or ignore them entirely. This operates at the architectural level, enabling simpler business logic in individual processes.

Structured Concurrency

Structured concurrency is the most significant conceptual development in concurrency models since the actor model, and its adoption across language ecosystems in the 2010s–2020s reflects a broad recognition of a recurring design mistake.

The goto Analogy

NJ Smith's 2018 essay Notes on Structured Concurrency drew an explicit analogy between unstructured task spawning and Dijkstra's 1968 critique of goto statements. Just as goto created implicit, hard-to-reason-about control flow, fire-and-forget task spawning creates implicit, hard-to-reason-about concurrency. In both cases, execution can jump to an arbitrary point outside the current function's context—violating the abstraction boundary that makes code composable.

In unstructured models (bare goroutines in Go, Task.detached in Swift), a task can be spawned and continue executing after the spawning function returns. The spawning function has no way to observe whether the task succeeded or failed, and no obligation to wait for it.

Nurseries and Task Groups

Structured concurrency solves this by introducing nurseries (Trio's term) or task groups (asyncio, Java): constructs that manage a set of child tasks and enforce that no task can be spawned without being assigned to an explicit scope.

The key semantic guarantees are:

These guarantees eliminate entire classes of bugs: orphaned tasks, leaked resources, silently dropped errors, and the inability to reason about what concurrent work is in flight.

Cross-Language Convergence

Structured concurrency has been adopted across independent language ecosystems as a standard pattern:

Language	Implementation	Year
Python	Trio	2017
Python	asyncio.TaskGroup (Python 3.11)	2022
Kotlin	Coroutines structured concurrency	2018
Swift	SE-0304 (Swift 5.5)	2021
Java	JEP 453/480 (JDK 21+)	2023
Rust	Experimental (async_nursery, Tokio discussions)	ongoing
OCaml	Eio 1.0 (effects-based)	2024

This convergence across dynamic, static, systems, and platform languages suggests that the pattern addresses a fundamental design flaw rather than a language-specific limitation.

Type Systems and Concurrency Safety

Ownership and Deadlock Freedom

Rust's ownership system applies a different approach: the type checker tracks which code has the right to access data, and those rules are strong enough to statically prevent data races. Object ownership can also guarantee deadlock freedom: when concurrent objects are organized into hierarchies where lock acquisition respects the ownership structure, circular waiting cannot form. This eliminates both data races and data-based deadlock through static type checking rather than runtime mechanisms.

Reference Capabilities in Pony

Pony takes the ownership approach further with reference capabilities: a type-system annotation on every reference that describes the aliasing and mutability constraints that hold for that reference. The six capability types (iso, trn, ref, val, box, tag) cover all possible combinations of read/write access and aliasing, and the type checker verifies that capability constraints are respected at every operation.

The consequences are substantial:

• Deadlock freedom: Pony's type system prevents circular wait conditions through careful management of message ordering and access patterns. If a Pony program compiles, the concurrent actor system cannot deadlock.
• Data-race freedom: the ORCA (Ownership and Reference Counting-based Garbage Collection in the Actor World) protocol leverages the data-race-freedom guarantees from reference capabilities to eliminate read/write barriers, allowing individual actors to garbage collect independently between message handlers—with no stop-the-world pauses.

Session Types

Session types apply type theory directly to the structure of communication protocols. A channel's type describes the sequence of messages that must be exchanged over it—who sends what, in what order, with what types. Session type systems have foundations in linear logic, a resource-aware logic that naturally captures structured interactions.

Session types provide two correctness properties through static type checking:

• Session fidelity: messages follow the protocol
• Deadlock freedom: the communication structure cannot produce circular waiting

This represents a direct extension of type safety from data to communication—shifting protocol conformance from a runtime property (enforced by tests and assertions) to a compile-time property.

Formal Verification

TLA+ in Production

TLA+ is a formal specification language that integrates with two categories of model checkers: TLC (explicit-state enumeration) and APALACHE (symbolic model checking using SMT solvers). The symbolic approach translates the transition relation into quantifier-free SMT constraints, addressing the state-space explosion problem that makes explicit enumeration impractical for large systems.

TLA+ is not an academic exercise. Multiple AWS teams including S3, DynamoDB, EBS, Aurora, and EC2 have used TLA+ since 2011 to verify critical distributed systems. Lightweight formal methods applied to Amazon S3's ShardStore storage node prevented 16 issues from reaching production, including subtle crash consistency and concurrency problems that traditional testing would miss.

Formal Fault Models

Formal verification of distributed systems requires explicitly stating the fault model—what failures are assumed possible. The Verdi framework implements different network semantics as separate computational models within the Coq proof assistant: message loss, crashes, Byzantine behavior. This explicit approach clarifies what guarantees hold under what assumptions—a distinction often left implicit in informal protocol descriptions.

Standards and Regulation

Formal methods are increasingly mandated by safety and certification standards. DO-178C for aviation explicitly recognizes formal methods as a way to satisfy safety assurance levels (DAL A, B), requiring formal specification and proof techniques for critical properties. The trend indicates that mathematical rigor in concurrent system design is transitioning from academic research to engineering practice in regulated domains.

Consistency in Distributed Concurrent Systems

When concurrent execution spans multiple machines, the question of concurrency models intersects with the question of consistency models. Consistency levels form a well-defined hierarchy:

1. Linearizability (atomic consistency) — the strongest; operations appear instantaneous
2. Sequential consistency — operations appear in some total order consistent with program order
3. Causal consistency — causally related operations are observed in causal order everywhere; concurrent operations may be observed in different orders
4. Eventual consistency — replicas converge given sufficient time without updates

Causal consistency, defined by Hutto and Ahamad in 1990, is particularly significant: it guarantees that cause precedes effect across all processes while remaining available during network partitions (AP in the CAP theorem). This makes it practically implementable in distributed systems that cannot afford the coordination costs of linearizability.

CRDTs: Convergence Without Coordination

Conflict-free Replicated Data Types (CRDTs) provide strong eventual consistency by designing data structures whose operations commute. If two replicas receive the same set of operations in different orders, they deterministically converge to the same state. This commutativity property is formalized through lattice theory: the state space forms a partial order, and merge operations are commutative, associative, and idempotent.

CRDTs eliminate a coordination bottleneck: replicas do not need to negotiate ordering before accepting writes. They accept all writes immediately and converge after the fact. This makes them directly applicable to local-first software that must work offline and sync later.

Language Ecosystem Perspectives

Python's Concurrency Stack

Python's concurrency story is shaped by the Global Interpreter Lock (GIL), a design choice that prevents multiple threads from executing Python bytecode simultaneously. The GIL simplifies memory management through reference counting but makes threading ineffective for CPU-bound workloads.

Python's concurrency options form a three-layer stack with distinct tradeoffs:

• Threading: effective for I/O-bound work (threads release the GIL during I/O); ineffective for CPU-bound work
• Multiprocessing: achieves true parallelism by spawning independent processes, each with its own interpreter and GIL. Data must be serialized (pickled) for inter-process transfer—a significant overhead
• Asyncio: cooperative multitasking via an event loop. Coroutines are substantially more lightweight than OS threads, enabling thousands of concurrent operations within a single thread

Python 3.11 introduced asyncio.TaskGroup, which provides structured concurrency for asyncio: when any task raises an exception, the TaskGroup cancels all remaining tasks and propagates exceptions in an ExceptionGroup. PEP 684 introduced a per-interpreter GIL, enabling true parallelism across subinterpreters within a single process.

The JVM: From Threads to Virtual Threads

Java's Project Loom represents a significant rethinking of JVM concurrency. Virtual threads, proposed in JEP 425 (JDK 19 preview) and finalized in JEP 444 (JDK 21), are lightweight threads scheduled by the JVM rather than the OS, enabling millions of concurrent threads with minimal overhead. JEP 453's Structured Concurrency API — still in preview through JEP 480 and JEP 505 — builds on this foundation, treating groups of related virtual-thread tasks as a single unit of work with defined lifetime, coordinated error handling, and automatic cancellation propagation.

Kotlin's coroutines established the same principles earlier and more completely, making structured concurrency the default in Kotlin's ecosystem. Java's adoption represents convergence toward patterns that other JVM languages had already demonstrated.

BEAM Languages: Gleam's Static Types

The BEAM ecosystem (Erlang, Elixir) is characterized by its "let it crash" fault tolerance architecture: rather than trying to prevent all errors, the system builds recovery into its structure through supervision trees. Gleam extends this tradition with Hindley-Milner type inference: a statically-typed functional language that targets BEAM and preserves the full supervision tree architecture while adding compile-time type safety guarantees.

ECS: Data-Oriented Concurrency

The Entity-Component-System architecture used in game engines takes a data-oriented approach to concurrency. Systems operating on disjoint sets of components can run in parallel without synchronization—if two systems access entirely different component types, their reads and writes cannot conflict. The explicit data dependency graph established by component queries makes parallelism opportunities visible to the scheduler, enabling automatic parallelization that would be opaque in traditional OOP designs.

Controversies & Debates

Async/Await as "Function Coloring"

The async/await pattern, adopted in Python, JavaScript, Rust, C#, and Swift, has attracted sustained criticism under the "function coloring" framing: async functions can only be called directly from other async functions, creating a viral annotation that propagates throughout a codebase. Critics argue this creates a second-class version of every abstraction in the language.

Structured concurrency is complementary to this debate rather than a resolution: it can be applied within async code to handle fault tolerance properly, but does not address the annotation propagation problem. OCaml's effect handlers (via Eio 1.0) represent one approach to direct-style concurrency without monadic transformation: concurrent programming without requiring async annotations to propagate.

Go's Concurrency: Channels vs. Goroutines

Go adopted CSP's channel concept but exposed goroutines as a lower-level primitive that can be spawned without structured lifetime management. A goroutine can run indefinitely after the spawning function returns. Critics argue this recreates the goto problem: implicit, hard-to-reason-about concurrency. Go's channels provide the communication mechanism but not the lifetime discipline. NJ Smith's essay specifically addresses the go statement as the problematic construct.

Current Status

The field is in a period of convergence on structured concurrency as a baseline pattern, with active research and standardization work on stronger static guarantees:

• Session types remain primarily in research languages but are beginning to appear in library form in mainstream languages
• Ownership-based concurrency (Rust's model) is expanding to new domains, including async Rust where structured concurrency semantics are being developed by the Tokio and async-std ecosystems
• Effect handlers (OCaml 5, Koka, Frank) offer a generalization that subsumes both async/await and exceptions, potentially providing a unified abstraction for all forms of non-local control flow including concurrency
• Formal verification is moving from specialist tooling toward integrated development workflows, driven by AWS's public evidence of practical returns on investment

The consistent theme across these directions is that concurrency safety should be enforced by the language or type system rather than relying on programmer discipline—the same lesson that structured programming drew from the goto era.