From a Protocol to a Cluster

protocol Order names a conversation and describes it from above, once, for everyone in it.

@[endpoints] asks the compiler to generate the code each participant runs.

There are three roles: Shop, Stock and Ledger. A role exists because a step mentions it.

These two lines say what a role's code may do besides talk. Stock may use shared mutable state, and Ledger may print. Shop is granted nothing.

The conversation repeats. One session carries order after order until a branch says stop.

The top of the loop is also where a running session can be ended cleanly when new code is deployed.

A step: Shop sends Stock an Int, the item it wants.

The label want names the message on the wire and the functions generated for it, send_Want and recv_Want.

A decision, and whose it is. Only Stock may choose. The other two have to be ready for either answer.

If Stock has the item, it tells Shop so and tells Ledger to book it, and Ledger confirms to Shop. Then the loop goes round.

A branch must open with a message from the chooser. That message is how the others learn which way the choice went.

If Stock is out, it tells Shop, tells Ledger there is nothing to book, and stop ends the conversation for all three.

Ledger is told either way, so it never waits for a booking that is not coming.

That is the whole agreement. There are no sockets in it, no retries, no message formats and no state machines, and nothing about which machine runs which role.

Those come from the compiler, the runtime and a separate topology file.

Here is every combination: 60 cells, one for each way the three positions can line up. Blocks are Shop's position, columns are Stock's, rows are Ledger's.

Nothing stops ordinary networked programs from reaching any of them, including the ones where one side waits for a message the other will never send, or both sides wait.

The protocol reaches 14 of them. They light in the order the protocol can first reach them, counting a role as moved once it has sent, even if its peer has not received yet.

The other 46 cannot happen. A program that would get there does not compile.

Stock has the order and must now choose have or out. This version skips the choice and tells Ledger to book.

-- Stock tells Ledger to book before it has chosen `have` or `out`.
pfn stock(s : Cap(Session.Live), _m : Cap(IO.Mut), st : Order_Stock.Entry) : Order_Stock.Yield do
  Order_Stock.recv_Want(s, st, fn (n, st1) ->
    stock(s, _m, Order_Stock.send_Book(s, st1, n)))
end

Role `Stock` tries to send an `Int` to `Ledger` here, but at this point protocol `Order` says it must choose `have` or `out`. [protocol_step_order]

-- PROTOCOL ----------------------------- skip_step.march

Role `Stock` tries to send an `Int` to `Ledger` here, but at this point protocol `Order` says it must choose `have` or `out`. [protocol_step_order]

25 |       stock(s, _m, Order_Stock.send_Book(s, st1, n)))
                                                 ^^^

    Take that step with `Order_Stock.choose_have` first.
    The conversation so far, in protocol `Order`:

      loop do                         (repeats)
        want: Shop -> Stock : Int     done
        choose by Stock: have | out   <- `Stock` must do this next

    `Stock` is here: it must choose `have` or `out`:

11 |       choose by Stock:
                     ^^^^^

    `st1` is the state bound here:

24 |     Order_Stock.recv_Want(s, st, fn (n, st1) ->
                                             ^^^
    run `march --explain protocol_step_order`

Stock may answer out. This Shop handles have and nothing else.

-- Shop handles the `have` answer and has nothing for `out`.
pfn shop(s : Cap(Session.Live), st : Order_Shop.Entry) : Order_Shop.Yield do
  let st1 = Order_Shop.send_Want(s, st, 1)
  Order_Shop.offer_have_out(s, st1,
    fn (_v, st2) -> Order_Shop.recv_Booked(s, st2, fn (_b, st3) -> shop(s, st3)))
end

`Order_Shop.offer_have_out` takes one callback for each branch `Stock` can choose in protocol `Order` (`have` and `out`), but this call leaves out `out`. [session_offer_nonexhaustive]

-- PROTOCOL ------------------- offer_misses_branch.march

`Order_Shop.offer_have_out` takes one callback for each branch `Stock` can choose in protocol `Order` (`have` and `out`), but this call leaves out `out`. [session_offer_nonexhaustive]

25 |     Order_Shop.offer_have_out(s, st1,
         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

    After `out` the conversation ends, so the fix closes it; put any other work for that branch before the `close`.

    the choice is declared here:

11 |       choose by Stock:
                     ^^^^^

    fix (`forge fix` applies it):

26 -       fn (_v, st2) -> Order_Shop.recv_Booked(s, st2, fn (_b, st3) -> shop(s, st3)))
26 +       fn (_v, st2) -> Order_Shop.recv_Booked(s, st2, fn (_b, st3) -> shop(s, st3)), fn (_v, st) -> Order_Shop.close(s, st))

    run `march --explain session_offer_nonexhaustive`

Ledger confirms a booking before anyone has asked for one.

-- Ledger confirms a booking nobody has asked it to make.
pfn ledger(s : Cap(Session.Live), c : Cap(IO.Console), st : Order_Ledger.Entry) : Order_Ledger.Yield do
  ledger(s, c, Order_Ledger.send_Booked(s, st, "booked"))
end

Role `Ledger` tries to send a `String` to `Shop` here, but at this point protocol `Order` says it must wait for `Stock` to choose `have` or `out`. [protocol_step_order]

-- PROTOCOL ---------------------- send_out_of_turn.march

Role `Ledger` tries to send a `String` to `Shop` here, but at this point protocol `Order` says it must wait for `Stock` to choose `have` or `out`. [protocol_step_order]

24 |     ledger(s, c, Order_Ledger.send_Booked(s, st, "booked"))
                                                  ^^

    Take that step with `Order_Ledger.offer_have_out` first.
    The conversation so far, in protocol `Order`:

      loop do                         (repeats)
        want: Shop -> Stock : Int
        choose by Stock: have | out   <- `Ledger` must do this next

    `Ledger` is here: it must wait for `Stock` to choose `have` or `out`:

11 |       choose by Stock:
                     ^^^^^

    `st` is the state bound here:

23 |   pfn ledger(s : Cap(Session.Live), c : Cap(IO.Console), st : Order_Ledger.Entry) : Order_Ledger.Yield do
                                                              ^^
    run `march --explain protocol_step_order`

Each message is in the protocol's own terms: the role, what it tried, and what it must do at that point. The marked cell is where the program stood.

Parse. The protocol block is a declaration like a function or a type. @[endpoints] asks for typed code to be generated from it.

Each bar is one of its 16 lines, at its real length.

Project. Each role gets its own view: only the steps it takes. Shop's view has 4 steps, Stock's 5 and Ledger's 3.

The views are checked against each other before any role is written: every message one role sends must be one its peer is waiting to receive (lib/typecheck/typecheck_session.ml).

Generate. While desugaring, the compiler writes 5 modules of ordinary March beside yours: one for the messages and their wire encoding, one for each role, and one that runs a role on a node (lib/desugar/desugar_endpoints.ml).

Every step of a role's view becomes its own linear type: a value that must be used exactly once. There are 12 of them, and 3 more for a session parked inside an actor.

Every move is a function that consumes one state and returns the next. In all, 152 functions come out of the 16 lines.

Typecheck, as usual. Stock holds a value of type S_choose_have_out. The only steps forward from it are choose_have and choose_out. send_Book wants an S_send_Book, and only choose_have returns one.

So order is enforced by an ordinary type mismatch, and exactly-once use by linearity. A table kept beside the types (lib/ast/protocol_states.ml) lets the error name roles and steps instead of generated types.

The line role Stock needs IO.Mut becomes a parameter. Stock's body is handed a capability for exactly that, and the compiler checks that everything the body reaches fits under it.

fn stock(env : Env, s : Cap(Session.Live), m : Cap(IO.Mut), st : Order_Stock.Entry) : Order_Stock.Yield

A role with no needs line is handed its session and nothing else.

Generate main. The lab app has none. A topology file says which pool of machines runs which role, and from it the compiler writes the entry point: start the node, narrow each pool's capabilities, open an offer for each role (lib/desugar/desugar_topology.ml).

Compile. From here it is the normal back half: typed IR, reference counting, LLVM, a native binary. Pools that share a build run the same binary, and each machine is told which pool it is.

The build also records the protocol's fingerprint, fbc92492…, a digest of its roles, steps and payload types. Two nodes compare fingerprints before they exchange a message.

An actor is a mailbox, a piece of state and a set of handlers. Messages for the Ledger queue in the order they arrive.

It handles one message at a time, to the end, and the handler returns the next state. Nothing else can touch total, so there is no lock to take and no race to reason about.

Other actors on the node run in parallel with it.

Every open session's state lives inside this one actor, parked in a map keyed by session. A delivery takes its session out, takes the next step of the protocol, and parks it again.

The parked state is a linear type, the same kind as in the last section. The actor cannot drop a session or use one twice by accident.

If a handler hits a bug, the actor crashes. It does not try to repair itself.

Its mailbox and its state are gone, and the sessions parked in it are cancelled. Messages sent to it meanwhile are dropped.

The node's generated main watches the actors that host roles. When one dies it opens the offer again with a fresh actor, and the next session finds it. No other node is involved.

The fresh actor starts from init, so the total is back at 0. The same happens when the Ledger moves to another machine; the app's own comment says so.

State that must outlive its actor has to be stored outside it. March does not do that for you.

A dot is a session being set up or finishing. A filled square is a session in progress: one square on the host playing Stock for it, and one on the Ledger.

The caller tries the hosts in turn, so the work spreads without a load balancer.

An offer has a capacity. Past it, the host answers "full" and the caller tries the next offer.

Here the load is raised until the Ledger's 64 slots run out. There is one Ledger, so there is no next offer, and the caller gets NoOffer with what each offer said. It does not wait for a timeout.

lab-2 crashes. Its connections close, so the sessions it was serving are cancelled at once.

They are not resumed. A cancelled session is discarded and the caller starts another, which the two remaining hosts take. A reply the dead host had already sent is still delivered.

A machine that hangs is harder, because nothing closes. The cluster node is the failure detector. It probes each peer every 1 second and waits 500 ms for the answer. A peer that misses one is suspected, and has 3 seconds to show it is alive.

Meanwhile lab-2's sessions are frozen and a caller that tries it moves on to the next host. When the time is up it is declared dead and its sessions are cancelled, with that as the cause: at most about 4.5 seconds after it hung.

The host holding the Ledger stops. The topology asks for one Ledger on a host labelled books, so the other such host opens the offer once membership has given up on the first. Sessions are refused in between.

The Ledger keeps a running total in memory, and the total does not move with the role. The new Ledger starts from 0.

The stopped host comes back as a new incarnation, so nothing can reach it through an old session. It offers Stock again, and no other node had to coordinate that.

It does not take the Ledger back at once. A node that rejoins counts for placement only after a settle period of 15 seconds, so a host that keeps dropping out cannot pull a role back and forth. After that, if it still ranks first, the role returns to it, and the total starts from 0 a second time.

Both books hosts are down. Nothing can play Ledger, so every caller gets NoOffer naming that role.

Stock is still on offer, but a session needs every role before it starts. None runs half-formed.