protocol_step_order: a role body takes a step its protocol does not allow yet
An @[endpoints] protocol generates one state per step of each role, and a
role body moves from state to state by calling the generated functions:
send_…, recv_…, choose_…, offer_…, close. Each function takes the
state it is the next step from. Calling one with a state the role is not in
yet, or no longer in, is this error. It says what the call tries to do, what
the protocol says the role must do at that point, and points at that step of
the protocol. It also draws the conversation so far: the protocol’s steps up to
that point, the role’s own marked done, the one it must take next, and the
one it tried (inside a loop, drawn as one round; inside a choose, as the
branch taken).
A program that triggers it
mod Main do
needs IO
needs Session.Live
@[endpoints]
protocol Stream do
loop do
Prod -> Cons : Int
choose by Cons:
more -> Cons -> Prod : Bool
done -> Cons -> Prod : Bool
stop
end
end
end
pfn cons(s : Cap(Session.Live), st : Stream_Cons.S_recv_Msg_Prod_Cons_1) : Stream_Cons.Yield do
Stream_Cons.close(s, Stream_Cons.choose_done(s, st, true))
end
fn main(c : Cap(IO)) do () end
end
Cons chooses done before it has received the Int that Prod sends at the
top of each round.
The fix
Take the step the error names first, then go on from the state it gives you:
mod Main do
needs IO
needs Session.Live
@[endpoints]
protocol Stream do
loop do
Prod -> Cons : Int
choose by Cons:
more -> Cons -> Prod : Bool
done -> Cons -> Prod : Bool
stop
end
end
end
pfn cons(s : Cap(Session.Live), st : Stream_Cons.S_recv_Msg_Prod_Cons_1) : Stream_Cons.Yield do
Stream_Cons.recv_Msg_Prod_Cons_1(s, st, fn (_n, st1) ->
Stream_Cons.close(s, Stream_Cons.choose_done(s, st1, true)))
end
fn main(c : Cap(IO)) do () end
end
Inside a loop, the step after the last one of a round is the first one of
the next: after more, a role is back at the top of the loop, so it cannot
close there.
Why the rule exists
The protocol is the contract every role is checked against. A body that takes its steps in another order would send a message its peer is not waiting for, or wait for one that never comes, and both deadlock the session at run time. Typing each state separately turns that into a compile-time error at the call that goes out of order.
See also: writing each role.