Concurrency Models and Verifying Concurrent Code: Shared Memory, Actors, CSP and Model Checking

Version note: The code in this post was built and run with .NET 10 (C# 14); tests use xUnit v3 4.0.3. The model checking examples were run with tla2tools.jar 1.7.4 and Java 21. The outputs were taken on ARM64.

Guess First

In Bookstore, the online bookstore used as the shared example across this site's series, there are 1,000 copies of Dune in stock and eight clients send 500 orders each. Reservations are handled by an actor in which a single thread touches the stock: there is no lock, and only the actor's own loop accesses the stock field. The clients first ask "how many are in stock?", and if the answer is above zero they send a "set the stock to this value" message. There is no data race inside the actor. How many books get sold?

Second question: if each of four threads does a 10-step job, how many different interleavings are there according to the formula from the first post? How many of them does a stress test try? In the previous seven posts of the series we stayed inside the shared memory model. In this last post we look at two things: models that communicate without sharing, and showing the correctness of concurrent code beyond testing.

Models and Shared Memory

A concurrency model is the framework that decides who owns the state of parts running at the same time and how they communicate with each other. You can build the same Bookstore problem (reserving from limited stock) in four different ways:

The first row has been the topic of the series so far. In the Models/ folder I added to the lab project, the same reservation is written with three models. The shared memory version is short:

// Model 1: shared memory + lock. Every caller touches the stock; the lock makes check-and-act one step
public sealed class LockedOrderDesk(int stock) : IOrderDesk
{
    private readonly Lock _gate = new();
    private int _stock = stock;

    public Task<bool> ReserveAsync(int quantity)
    {
        lock (_gate)
        {
            if (_stock < quantity)
                return Task.FromResult(false);
            _stock -= quantity;
            return Task.FromResult(true);
        }
    }
}

The strength of this model is its directness; its weakness is that correctness depends on discipline at every access. Every new method that touches the stock has to take the right lock; the races of the second post, the deadlocks of the fourth and the memory model subtleties of the fifth and sixth are the price of this model.

The Actor Model

The actor model comes from the 1973 work of Carl Hewitt, Peter Bishop and Richard Steiger. The idea: every actor keeps its own state and shares it with nobody. From the outside it only receives messages; the messages pile up in the actor's mailbox and the actor processes them one by one. While processing a message it can send messages to other actors, create new actors and change its own state for the next message.

// Model 2: actor. Only the actor's own loop touches the stock; callers send messages to its mailbox
private async Task LoopAsync()
{
    // one message at a time: inside a handler nothing else can touch _stock
    await foreach (Message message in _mailbox.Reader.ReadAllAsync())
    {
        switch (message)
        {
            case ReserveMessage r when _stock >= r.Quantity:
                _stock -= r.Quantity;
                r.Reply.SetResult(true);
                break;
            case ReserveMessage r:
                r.Reply.SetResult(false);
                break;
            case GetStockMessage g:
                g.Reply.SetResult(_stock);
                break;
            case SetStockMessage s:
                _stock = s.Value;
                break;
        }
    }
}

The mailbox here is a single-reader Channel<T>; replies come back through a TaskCompletionSource. There is no lock on the _stock field, because only this loop touches it. In a real project you would not write this infrastructure yourself. Microsoft Orleans offers actors as "grains" distributed across a cluster; Akka.NET is the .NET counterpart of Akka from the Scala world.

The actor model removes data races but not race conditions. The Orleans documentation gives two examples. In the default mode a grain does not start a new request before it has finished the current one; so two grains calling each other at the same time can get stuck waiting for each other's reply, and the calls end in a timeout. The circular wait of the fourth post, this time with messages. If you mark the grain as reentrant this hang goes away, but at the point where one request awaits, the steps of another request can step in; so a check-then-act split across the two sides of an await breaks again.

CSP: Processes That Talk Over Channels

CSP, Communicating Sequential Processes, comes from Tony Hoare's 1978 paper. It is similar to actors but with a different emphasis: actors have an identity and messages are sent to that identity; in CSP processes are anonymous and communication happens over named channels. Go's goroutines and channels are the best-known implementation of this idea; the upcoming Go backend series will cover them in detail. The .NET counterpart is System.Threading.Channels; we covered its use in the Channels post of the C# Asynchronous Programming series.

// Model 3: CSP. Anonymous stages connected by channels; the reserve stage is the only owner of the stock
private async Task ValidateAsync()
{
    await foreach (OrderRequest request in _incoming.Reader.ReadAllAsync())
    {
        if (request.Quantity is < 1 or > 20)
            request.Reply.SetResult(false);
        else
            await _validated.Writer.WriteAsync(request);
    }
}

private async Task ReserveStageAsync(int stock)
{
    await foreach (OrderRequest request in _validated.Reader.ReadAllAsync())
    {
        bool ok = stock >= request.Quantity;
        if (ok)
            stock -= request.Quantity;
        request.Reply.SetResult(ok);
    }
}

The validation stage never sees the stock; the stock is a local variable of the reserve stage. Thanks to bounded channels, when one stage slows down the previous one starts waiting, so backpressure comes from the model itself. I ran the three models with the same load: 1,000 in stock, 8 clients, 4,000 single-copy orders in total:

dotnet run -c Release --project src/Bookstore.ConcurrencyLab -- models

shared memory + lock  stock=1,000 orders=4,000 accepted=1,000 (4 ms)
actor (mailbox)       stock=1,000 orders=4,000 accepted=1,000 (4 ms)
CSP pipeline          stock=1,000 orders=4,000 accepted=1,000 (4 ms)

All three accepted exactly 1,000 orders. The difference is not in correctness but in where correctness comes from: in the first, from discipline at every access; in the other two, from the state having a single owner.

Immutable Data, the Event Loop and STM

Another way of sharing is to make the shared thing unchangeable. Any number of threads can read an immutable price list; an update means creating a new list and publishing the reference. As we saw in the sixth post, publishing a reference is safe in .NET, and types such as ImmutableDictionary support this model directly. When writes are rare and reads are frequent, this is usually the cheapest model.

A single-threaded event loop keeps concurrency on a single thread: JavaScript in Node.js and the browser runs each callback to completion, then moves on to the next one in the queue. There are no data races, but state can still change between await points; we looked at this order in detail in the event loop post of the Advanced JavaScript series.

STM, Software Transactional Memory, groups memory accesses like database transactions: changes to shared memory happen inside transactions and are retried automatically on conflict. It is built into Haskell's GHC compiler and into Clojure; in .NET, Microsoft's experimental STM.NET work never became a product.

Why Testing Is Not Enough

The answer to the first opening question:

dotnet run -c Release --project src/Bookstore.ConcurrencyLab -- actor-protocol

run 1: stock=1,000 sold with GetStock+SetStock=4,000 stock left=425
run 2: stock=1,000 sold with GetStock+SetStock=4,000 stock left=392
run 3: stock=1,000 sold with GetStock+SetStock=4,000 stock left=457

4,000 books were sold from 1,000 copies of stock, and at the end around 400 books still show as in stock. There is no bug inside the actor; each message is handled correctly on its own. The bug is in the protocol: "read" and "write" are two separate messages, and other clients' messages step in between the two. This is the check-then-act of the second post written with messages. The fix is to move the decision into the actor: the client says "reserve 1 copy", and the actor does the check and the decrement in one message. Changing the model does not mean you can stop thinking.

Why do tests miss bugs like this? In the first post we calculated that two threads doing three steps each can run in 20 different orders. With the same formula, four threads doing ten steps each means about 4.7 × 10^21 different interleavings. A stress test tries a small sample of them, the one the operating system's timing happens to pick, and catches a broken stack like the one in the seventh post in only 63 of 20,000 histories.

There are ways to make stress testing more effective. The first is invariant assertions: putting a rule such as "sold + stock = initial stock" into the code and checking it after every operation catches the bug when it happens, not in its result. The second is deterministic scheduling: during a test a tool controls the order of threads and tasks, tries different orders systematically, and can replay the same order once it finds a bug. The well-known tool for this approach in .NET is Microsoft Coyote. I checked its state on GitHub: the repository is active and support for .NET 10 and .NET 11 was added in November 2026; but the latest version on NuGet is 1.7.11 from March 2024, and its newest target is net8.0. That is why I did not run Coyote in this post; before using it in a .NET 10 project, check whether a new version has been released.

Model Checking: Stock Reservation in TLA+

Model checking means writing a small model of the system and having a tool try all of its possible behaviours. TLA+, developed by Leslie Lamport, is one of the most widely used languages for this; it is built on TLA, the Temporal Logic of Actions, and specs are run with the TLC model checker; I used version 2.19. Here is the model of the if (stock > 0) stock-- code from the second post, in the specs/ folder I added to the project:

------------------------- MODULE StockReservation -------------------------
EXTENDS Integers

CONSTANTS Buyers, InitialStock

VARIABLES stock, sold, pc

vars == <<stock, sold, pc>>

Init ==
    /\ stock = InitialStock
    /\ sold = 0
    /\ pc = [b \in Buyers |-> "check"]

\* if (stock > 0) ...
Check(b) ==
    /\ pc[b] = "check"
    /\ pc' = [pc EXCEPT ![b] = IF stock > 0 THEN "reserve" ELSE "done"]
    /\ UNCHANGED <<stock, sold>>

\* ... stock--;
Reserve(b) ==
    /\ pc[b] = "reserve"
    /\ stock' = stock - 1
    /\ sold' = sold + 1
    /\ pc' = [pc EXCEPT ![b] = "done"]

Finished ==
    /\ \A b \in Buyers : pc[b] = "done"
    /\ UNCHANGED vars

Next == (\E b \in Buyers : Check(b) \/ Reserve(b)) \/ Finished

Spec == Init /\ [][Next]_vars

NoOversell == sold <= InitialStock
=============================================================================

How to read it: pc holds where each buyer is in the code. The Check step only looks at the stock and moves the buyer to "reserve" or "done"; the Reserve step decrements the stock. Next says that at every step any buyer may take any step; we do not write the interleavings, TLC generates all of them itself. NoOversell is the invariant that must hold in every state. The .cfg file with the same name provides two buyers ("ada", "alan") and 1 copy of stock. After downloading tla2tools.jar from the GitHub release page of the TLA+ repository (v1.7.4) into the specs/ folder, the command is the same on every operating system:

java -XX:+UseParallelGC -cp tla2tools.jar tlc2.TLC StockReservation

Error: Invariant NoOversell is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ sold = 0
/\ pc = [ada |-> "check", alan |-> "check"]
/\ stock = 1

State 2: <Check line 17, col 5 to line 19, col 32 of module StockReservation>
/\ sold = 0
/\ pc = [ada |-> "reserve", alan |-> "check"]
/\ stock = 1

State 3: <Check line 17, col 5 to line 19, col 32 of module StockReservation>
/\ sold = 0
/\ pc = [ada |-> "reserve", alan |-> "reserve"]
/\ stock = 1

State 4: <Reserve line 23, col 5 to line 26, col 38 of module StockReservation>
/\ sold = 1
/\ pc = [ada |-> "done", alan |-> "reserve"]
/\ stock = 0

State 5: <Reserve line 23, col 5 to line 26, col 38 of module StockReservation>
/\ sold = 2
/\ pc = [ada |-> "done", alan |-> "done"]
/\ stock = -1

13 states generated, 10 distinct states found, 1 states left on queue.

I removed the version and environment lines at the top; the rest is TLC's output. TLC gives the shortest path that breaks the invariant, step by step: both buyers see the stock as 1, both decrement it, the stock drops to -1 and 2 books are sold from a stock of 1. This is the proof on paper of the overselling we saw in 372 of 2,000 rounds in the second post. For the version that does the check and the decrement in one atomic step (StockReservationLocked, the model of the code inside the lock), the output is different:

java -XX:+UseParallelGC -cp tla2tools.jar tlc2.TLC StockReservationLocked

Model checking completed. No error has been found.
  Estimates of the probability that TLC did not check all reachable states
  because two distinct states had the same fingerprint:
  calculated (optimistic):  val = 4.3E-19
6 states generated, 4 distinct states found, 0 states left on queue.

"No error has been found" here does not mean "I did not see one in my tries", it means "I looked at every reachable state of this model". With three buyers and 2 copies of stock (ThreeBuyers.cfg) the same result comes with 8 distinct states, while the broken version is caught again with a counterexample of 7 states. TLC does not try interleavings one by one; it merges different paths that lead to the same state, which is why the number of states grows much more slowly than the number of interleavings.

Do not forget the limit of the model either: TLC checks the model you wrote, not the C# code. If the model differs from the code (for example, if you assumed stock-- is atomic), the proof only holds up to that difference. That is why model checking is used mostly for protocols and algorithms: lock ordering, two-phase commit, cache invalidation, the message flow of a distributed system.

A Decision Guide: Which Model for Which Problem

These are the rules I arrived at by the end of the series:

• Try not sharing first: each request with its own data, each thread with its own result, merged at the end. State that is not shared needs none of the rules of this series.
• Many reads and few writes: immutable data and reference publishing.
• Short critical sections that protect a few fields together: lock; a single counter or flag: Interlocked.
• An entity (a cart, a stock item, an institutional order) with long-lived state and ordered requests coming to it: an actor; especially when the state is spread across several servers, an infrastructure like Orleans.
• Data flowing from one stage to the next (order validation, reservation, shipping label): a CSP-style channel pipeline.
• A complex protocol with a high cost of failure: a small TLA+ model before writing the code.

In Production

Choose the model as a team and write down its boundaries. In a service where part of the state is written with locks, part with actors and part lock-free, the rules of each model end up being broken inside another. For example, touching a shared dictionary from inside an actor erases every guarantee of the actor model.

Design the message protocol like an API. With actors and channels, races hide in the order and splitting of messages. Instead of "read, then write" messages use "state your intent" messages (reserve, cancel); leave the decision to the owner of the state. Check in the documentation of your infrastructure what it guarantees about message order; make no assumption about the relative order of messages from different clients.

Split verification into layers. For the algorithm itself, model checking or a linearization point argument on paper; for the implementation, stress tests with invariant assertions; for distributed behaviour, patterns such as fencing tokens and idempotency covered in the Distributed Systems Fundamentals series. None of them is enough on its own.

Common Pitfalls

Believing the actor model has no races. In the experiment the inside of the actor was bug-free and still 4,000 books were sold from 1,000 copies. No data race, but a race condition.

Underestimating reentrancy. Making an actor or grain reentrant solves the deadlock but turns every await into an interleaving point. If there is an await between the two steps of a check-then-act, you get the same bug as in lock-free code.

Trying to apply a model checker to the whole system. A team that tries to model a microservice architecture end to end in TLA+ ends up with state explosion and a spec that never gets finished. Limit the model to the riskiest protocol, keep the constants small (two buyers, one book), and grow them only while TLC stays fast.

Counting a green test as proof. Trying a few thousand of 4.7 × 10^21 interleavings says nothing about the rest. A test does not say "this bug does not exist"; it only says "I did not see it in these runs".

A Small Experiment

★☆☆ Fix the client in the actor-protocol command: use ReserveAsync(1) instead of GetStockAsync and SetStock, and check that exactly 1,000 books are sold. Explain why the fix works without adding any code inside the actor.

★★☆ Add a Cancel(b) step to StockReservation.tla: a buyer who has reserved can cancel and increase the stock again. Is the NoOversell invariant still caught in the broken version, and does it still pass in the locked version? Discuss how you need to update the meaning of the sold variable once cancellation exists.

★★★ Model the two-warehouse stock transfer of the fourth post in TLA+: each transfer takes the lock of the source warehouse first, then the target. Write a spec in which TLC's default deadlock check finds the deadlock, then show that the version taking the locks in Id order is deadlock-free.

With this post the Concurrency Theory series ends. We started with interleaving and Amdahl in the first post, separated races from data races, looked at the theory of mutual exclusion and deadlock, the memory models of the hardware and of .NET, lock-free algorithms, and finally at models and verification. The version of the same questions spread across several machines, meaning consistency under message loss, clock differences and network partitions, is the topic of the Distributed Systems Fundamentals series; there you will meet the happens-before, linearizability and deadlock concepts of this series again in a distributed setting.