f3b1e847e9
Start with machines.dot, which gives the override. Then traverse downwards from wormhole.dot .
36 lines
1.5 KiB
Plaintext
36 lines
1.5 KiB
Plaintext
digraph {
|
|
start [label="Order\nMachine" style="dotted"]
|
|
/* our goal: deliver PAKE before anything else */
|
|
|
|
{rank=same; S0 P0_other}
|
|
{rank=same; S1 P1_other}
|
|
|
|
S0 [label="S0: no pake" color="orange"]
|
|
S1 [label="S1: yes pake" color="green"]
|
|
S0 -> P0_pake [label="got_pake"
|
|
color="orange" fontcolor="orange"]
|
|
P0_pake [shape="box" color="orange"
|
|
label="K.got_pake\ndrain queue:\n[R.got_message]"
|
|
]
|
|
P0_pake -> S1 [color="orange"]
|
|
S0 -> P0_other [label="got_version\ngot_phase" style="dotted"]
|
|
P0_other [shape="box" label="queue" style="dotted"]
|
|
P0_other -> S0 [style="dotted"]
|
|
|
|
S1 -> P1_other [label="got_version\ngot_phase"]
|
|
P1_other [shape="box" label="R.got_message"]
|
|
P1_other -> S1
|
|
|
|
|
|
/* the Mailbox will deliver each message exactly once, but doesn't
|
|
guarantee ordering: if Alice starts the process, then disconnects,
|
|
then Bob starts (reading PAKE, sending both his PAKE and his VERSION
|
|
phase), then Alice will see both PAKE and VERSION on her next
|
|
connect, and might get the VERSION first.
|
|
|
|
The Wormhole will queue inbound messages that it isn't ready for. The
|
|
wormhole shim that lets applications do w.get(phase=) must do
|
|
something similar, queueing inbound messages until it sees one for
|
|
the phase it currently cares about.*/
|
|
}
|