jonnifyfsharp

Dive C4.09.3

The single writer

Many callers, one mailbox. That is the whole reason the queue is safe under concurrency.

This is the chapter's payoff. A queue is hammered by many callers at once — each minting a job or claiming the next one. If they all wrote to the registry directly, two could interleave: both could read the same oldest job and claim it, or two mints could collide on a row. The MailboxProcessor removes the possibility. Every mint and every claim is a message into one mailbox, handled by one loop, one at a time. The transitions serialize: two callers cannot race a claim or mint a colliding id. This dive states why, in the echo_fs broker's own words, and shows the test that proves it.

Run the race, then the mailbox Module hub
C4.09.3 · part 1

The race a shared writer allows

Picture the registry as a mutable cell that any caller may read and write. Two workers each pull the next job. Worker A reads the oldest pending id; before it removes it, worker B reads the same oldest id. Each proceeds as the holder; each runs it. The job is claimed twice. The mirror failure is on the mint side: two callers compute a row for a new id and both write, and one write clobbers the other. Neither bug is in the logic of a claim or a mint — each is correct alone. The bug is that two of them interleaved.

Locks are the usual answer, but a lock is a thing to remember on every path, and a forgotten one is the same race again. The functional answer is to remove the shared write altogether: route every change through a single owner, so there is never more than one writer to interleave.

The hazard is concurrent writes to one structure. With a single writer there are no concurrent writes — every transition is applied by the same loop, in the order the messages arrived.
C4.09.3 · part 2

One mailbox imposes an order

A MailboxProcessor has exactly one inbox and one loop. Many callers may post at once, and the runtime is free to interleave their posting; but the loop pulls messages one at a time, so the transitions run strictly in sequence. Whatever order the mailbox accepts the messages in becomes a total order, and the registry advances through it deterministically. A claim runs against the state the previous claim left; a mint runs against a registry that already holds every prior row. There is no window in which two transitions overlap, because the loop never starts the next message until the current one has produced its new state.

The echo_fs broker states this in its own module comment, naming the same guarantee the Elixir bus relies on:

// echo_fs/EchoMQ/Broker.fs — the module's own words
/// The single-writer broker: a `MailboxProcessor` that owns one queue's state
/// and serializes every transition through its mailbox. This is F#'s actor — the
/// GenServer analog — and it is what makes minting and claiming safe under
/// concurrency: there is only ever one writer, so two callers cannot race a
/// claim or mint a colliding id. The Elixir bus gets this from the single
/// `Portal.Engine` writer; the F# port gets it from the mailbox.
The argument is not F#-specific. Elixir gets serialized writes from one GenServer process; F# gets them from one MailboxProcessor loop. In both, the safety comes from there being a single owner of the write — not from a lock around a shared one.

Four callers, two outcomes

Four callers each post a mint for a distinct branded id, all at once. Choose the model and step it. The shared writer interleaves two unguarded read-modify-write pairs, so a write is lost and the registry ends short. The single writer funnels all four through one mailbox, handles them in order, and keeps every id. The readout names what survived; the count at the end is the proof.

Concurrent mints · shared writer vs single writer

four callers · concurrent mints mint JOB…aZxKq9P mint JOB…b7Lm2Tg mint JOB…c4Rt8Wd mint JOB…d9Yk5Qm shared cell mutable cell · any caller writes applying — rows written 0 registry empty
Pick a model and press step. The shared writer lets two mints interleave and loses one; the single writer serializes all four through the mailbox and keeps every id.

Same four mints, two endings. Direct writes can interleave and drop one; one mailbox imposes an order, so all four land. The safety is structural — it does not depend on remembering a lock.

C4.09.3 · part 3

The test that proves it

The guarantee is not a claim in a comment — it is checked. The echo_fs BrokerTests suite posts two hundred distinct ids to one broker at the same time, with Async.Parallel, and then asks the broker how many are pending. If any two had raced — a lost write, a colliding id — the count would fall short. It is exactly two hundred.

// echo_fs/EchoMQ.Tests/BrokerTests.fs
[<Fact>]
let ``parallel posts are serialized by the mailbox — no lost or colliding ids`` () =
    let b = Broker.Broker()
    let ids = [ for n in 1L..200L -> mint n ]

    ids
    |> List.map (fun id -> b.EnqueueAsync(id, "p"))
    |> Async.Parallel
    |> Async.RunSynchronously
    |> ignore

    Assert.Equal<int>(200, b.PendingSize())

The same shape, run in dotnet fsi against a reduced broker, gives the same result — all two hundred survive the parallel posting:

let b = Broker()
[ for n in 1..200 -> sprintf "JOB%011d" n ]
|> List.map (fun id -> b.EnqueueAsync(id, "p"))
|> Async.Parallel
|> Async.RunSynchronously
|> ignore

b.PendingSize()   // val it: int = 200

Elixir — one GenServer serializes the writes

# Elixir — 200 concurrent calls into one GenServer; none are lost
1..200
|> Task.async_stream(fn id -> GenServer.call(broker, {:enqueue, id}) end)
|> Enum.to_list()
# pending = 200 — the single Portal.Engine writer serialized them

F# — one MailboxProcessor does the same

// F# — 200 concurrent posts into one mailbox; none are lost
// pending = 200 — the single MailboxProcessor loop serialized them

EchoMQ in F#

Status — echo_fs is an in-memory model. The EchoMQ protocol — the Lua transitions executing on a Valkey wire — is not implemented (there is no Lua and no Valkey client in the code); that is the coming-soon transport (EchoMQ.Connector). This block shows how the model uses the structure, not a running bus.

This is the chapter's running example at its conclusion: the registry of C4.09.1, owned by the broker of C4.09.2, made safe by the single-writer property — and the bus proves it holds.

runs today echo_fs/EchoMQ/Broker.fs · EchoMQ.Tests/BrokerTests.fs

EchoMQ.Broker is built and tested, and the single-writer guarantee is one of its tests: "parallel posts are serialized by the mailbox — no lost or colliding ids". Because the broker is the only writer over EchoMQ.Store.Rows, the bus needs no lock around the registry — minting and claiming serialize through the mailbox by construction. This is the property that lets a queue stay correct under load: the part the chapter was built to reach.

coming soon The serialization holds in memory today. When the Valkey transport EchoMQ.Connector lands, the same single-writer discipline carries to the wire — the production bus moves the atomicity into Valkey-side scripts, but the broker's contract, that one writer owns the transitions, is unchanged.

The chapter, closed

Twelve modules built the registry from the ground up: lists and trees, sorting and maps, the HAMT and the CHAMP, the branded id and its persistence. This module folded them into a working store and gave it a single writer — and that writer, the MailboxProcessor, is what makes the queue safe without a lock. The store can later become a branded CHAMP and gain a Valkey wire; the actor over it does not change. That is the shape of a queue: a persistent registry, owned by one loop.

C4.09 · the parts

A branded-keyed persistent registry, an F# MailboxProcessor, and a single-writer discipline.

The result

A queue that stays correct under concurrent mints and claims — no lost work, no colliding ids, no lock.

↑ C4.09 · Branded CHAMP maps & MailboxProcessor C4 · Algorithms & Data Structures Elixir · F4.09 (the GenServer parity)

References

Sources

Related in this course