From f3b1e847e9e9f47a52a0512a6a479fa2709fc91e Mon Sep 17 00:00:00 2001 From: Brian Warner Date: Tue, 21 Feb 2017 17:56:32 -0800 Subject: [PATCH] fix everything: should now be consistent and correct Start with machines.dot, which gives the override. Then traverse downwards from wormhole.dot . --- docs/code.dot | 4 +-- docs/key.dot | 57 +++++------------------------ docs/machines.dot | 43 +++++++++++++++------- docs/mailbox.dot | 9 ++--- docs/order.dot | 35 ++++++++++++++++++ docs/receive.dot | 48 ++++++++++--------------- docs/send.dot | 11 +++--- docs/wormhole.dot | 92 ++++++++++++++++------------------------------- 8 files changed, 138 insertions(+), 161 deletions(-) create mode 100644 docs/order.dot diff --git a/docs/code.dot b/docs/code.dot index f19c956..864d757 100644 --- a/docs/code.dot +++ b/docs/code.dot @@ -24,7 +24,7 @@ digraph { S2 -> P2_got_nameplates [label="got_nameplates"] P2_got_nameplates [shape="box" label="stash nameplates\nfor completion"] P2_got_nameplates -> S2 - S2 -> P2_finish [label="" color="orange" fontcolor="orange"] + S2 -> P2_finish [label="" color="orange" fontcolor="orange"] P2_finish [shape="box" label="lookup wordlist\nfor completion"] P2_finish -> S3 S3 [label="S3: typing\ncode"] @@ -33,7 +33,7 @@ digraph { P3_completion -> S3 S3 -> P0_set_code [label="" - color="orange" fontcolor="orange"] + color="orange" fontcolor="orange"] S0 -> P0_allocate [label="allocate"] P0_allocate [shape="box" label="C.tx_allocate"] diff --git a/docs/key.dot b/docs/key.dot index b342475..de75c2b 100644 --- a/docs/key.dot +++ b/docs/key.dot @@ -13,7 +13,7 @@ digraph { S0 [label="S0: know\nnothing"] S0 -> P0_build [label="set_code"] - P0_build [shape="box" label="build_pake\nM.set_nameplate\nM.add_message(pake)"] + P0_build [shape="box" label="build_pake\nM.add_message(pake)"] P0_build -> S1 S1 [label="S1: know\ncode"] @@ -28,55 +28,16 @@ digraph { something similar, queueing inbound messages until it sees one for the phase it currently cares about.*/ - S1 -> P_mood_scary [label="got_message(pake)\npake bad"] - S1 -> P1_compute [label="got_message(pake)\npake good"] - S1 -> P1_queue_inbound [label="got_message(data)" style="dashed"] - P1_queue_inbound [shape="box" style="dotted" label="queue"] - P1_queue_inbound -> S1 [style="dashed"] - S1 -> P1_queue_version [label="got_message(version)"] - P1_queue_version [label="queue\nversion??"] - P1_queue_version -> S1 - S1 -> P_mood_lonely [label="close"] + S1 -> P_mood_scary [label="got_pake\npake bad"] + P_mood_scary [shape="box" color="red" label="W.scared"] + P_mood_scary -> S3 [color="red"] + S3 [label="S3:\nscared" color="red"] + S1 -> P1_compute [label="got_pake\npake good"] + #S1 -> P_mood_lonely [label="close"] - P1_compute [label="compute_key\nM.add_message(version)\nA.got_verifier" shape="box"] + P1_compute [label="compute_key\nM.add_message(version)\nW.got_verifier\nR.got_key" shape="box"] P1_compute -> S2 - P_mood_scary [shape="box" label="M.close\nmood=scary"] - P_mood_scary -> P_notify_failure + S2 [label="S2: know_key" color="green"] - P_notify_failure [shape="box" label="(record failure)" color="red"] - P_notify_failure -> S_closing - - S2 [label="S2: know_key\n(unverified)" color="orange"] - S2 -> P2_queue_inbound [label="got_message(data)" style="dashed"] - P2_queue_inbound [shape="box" style="dotted" label="queue"] - P2_queue_inbound -> S2 - S2 -> P2_verified [label="got_message(version)\ngood"] - S2 -> P_mood_scary [label="got_message(version)\nbad"] - S2 -> P_mood_lonely [label="close"] /* more like impatient */ - - P2_verified [label="D.got_message(queued)\nA.received(msg)\nencrypt queued\nM.add_message(queued)" - shape="box"] - P2_verified -> S3 - - S3 [label="S3: know_key\n(verified)" color="green"] - S3 -> P3_accept [label="got_message(data)"] /* probably phase */ - S3 -> P_mood_happy [label="close"] - S3 -> P_notify_failure [label="scary"] - - P3_accept [shape="box" label="decrypt\nR.got_message(good,bad)"] - P3_accept -> S3 - P_mood_happy [shape="box" label="M.close\nmood=happy"] - P_mood_happy -> S_closing - - P_mood_lonely [shape="box" label="M.close\nmood=lonely"] - P_mood_lonely -> S_closing - - S_closing [label="closing"] - S_closing -> P_closed [label="closed"] - S_closing -> S_closing [label="got_message"] - - P_closed [shape="box" label="A.closed"] - P_closed -> S_closed - S_closed [label="closed"] } diff --git a/docs/machines.dot b/docs/machines.dot index 89dc10e..7e2ecd3 100644 --- a/docs/machines.dot +++ b/docs/machines.dot @@ -4,29 +4,46 @@ digraph { color="blue" fontcolor="blue"] Mailbox [shape="box" color="blue" fontcolor="blue"] Connection [label="Rendezvous\nConnector" - shape="oval" color="blue" fontcolor="blue"] - websocket [shape="oval" color="blue" fontcolor="blue"] + shape="box" color="blue" fontcolor="blue"] + websocket [color="blue" fontcolor="blue"] + Order [shape="box" label="Ordering" color="blue" fontcolor="blue"] + Key [shape="box" label="Key" color="blue" fontcolor="blue"] + Send [shape="box" label="Send" color="blue" fontcolor="blue"] + Receive [shape="box" label="Receive" color="blue" fontcolor="blue"] Code [shape="box" label="Code" color="blue" fontcolor="blue"] Nameplates [shape="box" label="Nameplate\nLister" color="blue" fontcolor="blue" ] - {rank=same; Nameplates Code} Connection -> websocket [color="blue"] + #Connection -> Order [color="blue"] App -> Wormhole [style="dashed" label="set_code\nsend\nclose\n(once)"] - App -> Wormhole [color="blue"] + #App -> Wormhole [color="blue"] Wormhole -> App [style="dashed" label="got_verifier\nreceived\nclosed\n(once)"] - Wormhole -> Connection [color="blue"] + #Wormhole -> Connection [color="blue"] + + Wormhole -> Send [style="dashed" label="send"] Wormhole -> Mailbox [style="dashed" - label="set_nameplate\nadd_message\nclose\n(once)" - ] - Wormhole -> Mailbox [color="blue"] - Mailbox -> Wormhole [style="dashed" - label="got_message\nclosed\n(once)" + label="set_nameplate\nclose\n(once)" ] + #Wormhole -> Mailbox [color="blue"] + Mailbox -> Wormhole [style="dashed" label="closed\n(once)"] + Mailbox -> Order [style="dashed" label="got_message (once)"] + Wormhole -> Key [style="dashed" label="set_code"] + Key -> Wormhole [style="dashed" label="got_verifier\nscared"] + Order -> Key [style="dashed" label="got_pake"] + Order -> Receive [style="dashed" label="got_message"] + #Wormhole -> Key [color="blue"] + Key -> Mailbox [style="dashed" label="add_message (pake)\nadd_message (version)"] + Receive -> Send [style="dashed" label="got_verified_key"] + Send -> Mailbox [style="dashed" label="add_message (phase)"] + + Key -> Receive [style="dashed" label="got_key"] + Receive -> Wormhole [style="dashed" + label="happy\nscared\ngot_message"] Mailbox -> Connection [style="dashed" label="tx_claim\ntx_open\ntx_add\ntx_release\ntx_close\nstop" @@ -41,7 +58,7 @@ digraph { label="tx_list" ] - Wormhole -> Code [color="blue"] + #Wormhole -> Code [color="blue"] Code -> Connection [style="dashed" label="tx_allocate" ] @@ -50,10 +67,12 @@ digraph { Nameplates -> Code [style="dashed" label="got_nameplates" ] - Code -> Nameplates [color="blue"] + #Code -> Nameplates [color="blue"] Code -> Nameplates [style="dashed" label="refresh_nameplates" ] + Code -> Wormhole [style="dashed" + label="set_code"] diff --git a/docs/mailbox.dot b/docs/mailbox.dot index 65fb17d..51afafc 100644 --- a/docs/mailbox.dot +++ b/docs/mailbox.dot @@ -86,8 +86,9 @@ digraph { P3_process_ours -> S3B S3B -> P3_process_theirs [label="rx_message\n(theirs)" color="orange" fontcolor="orange"] - P3_process_theirs [shape="box" label="C.tx_release\nW.got_message" - color="orange"] + P3_process_theirs [shape="box" color="orange" + label="C.tx_release\nO.got_message if new\nrecord" + ] /* pay attention to the race here: this process_message() will deliver msg_pake to the WormholeMachine, which will compute_key() and send(version), and we're in between S1A (where send gets @@ -116,7 +117,7 @@ digraph { P4_process_ours [shape="box" label="dequeue"] P4_process_ours -> S4B S4B -> P4_process_theirs [label="rx_message\n(theirs)"] - P4_process_theirs [shape="box" label="W.got_message"] + P4_process_theirs [shape="box" label="O.got_message if new\nrecord"] P4_process_theirs -> S4B S4A -> S5A [label="(none)" style="invis"] @@ -145,7 +146,7 @@ digraph { P5_process_ours [shape="box" label="dequeue"] P5_process_ours -> S5B S5B -> P5_process_theirs [label="rx_message\n(theirs)"] - P5_process_theirs [shape="box" label="W.got_message"] + P5_process_theirs [shape="box" label="O.got_message if new\nrecord"] P5_process_theirs -> S5B foo5 [label="" style="invis"] diff --git a/docs/order.dot b/docs/order.dot new file mode 100644 index 0000000..202bc10 --- /dev/null +++ b/docs/order.dot @@ -0,0 +1,35 @@ +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.*/ +} diff --git a/docs/receive.dot b/docs/receive.dot index 1f26604..3761350 100644 --- a/docs/receive.dot +++ b/docs/receive.dot @@ -10,40 +10,30 @@ digraph { start [label="Receive\nMachine" style="dotted"] - S0 [label="S0: unknown\ncode"] - S0 -> P0_got_key [label="got_verified_key"] + S0 [label="S0:\nunknown key" color="orange"] + S0 -> P0_got_key [label="got_key" color="orange"] - P0_got_key [shape="box" label="record key"] - P0_got_key -> S1 + P0_got_key [shape="box" label="record key" color="orange"] + P0_got_key -> S1 [color="orange"] - S0 -> P_mood_lonely [label="close"] + S1 [label="S1:\nunverified key" color="orange"] + S1 -> P_mood_scary [label="got_message\n(bad)"] + S1 -> P1_accept_msg [label="got_message\n(good)" color="orange"] + P1_accept_msg [shape="box" label="S.got_verified_key\nW.happy\nW.got_message" + color="orange"] + P1_accept_msg -> S2 [color="orange"] - S1 [label="S1: verified\nkey" color="green"] + S2 [label="S2:\nverified key" color="green"] - S1 -> P_mood_scary [label="got_message(bad)"] - S1 -> P1_accept_msg [label="got_message(good)"] - S1 -> P_mood_happy [label="close"] + S2 -> P2_accept_msg [label="got_message\n(good)" color="orange"] + S2 -> P_mood_scary [label="got_message(bad)"] - P1_accept_msg [label="A.received(msg)" shape="box"] - P1_accept_msg -> S1 + P2_accept_msg [label="W.got_message" shape="box" color="orange"] + P2_accept_msg -> S2 [color="orange"] - P_mood_scary [shape="box" label="K.scary"] - P_mood_scary -> S_closed + P_mood_scary [shape="box" label="W.scared" color="red"] + P_mood_scary -> S3 [color="red"] - P_notify_failure [shape="box" label="(record failure)" color="red"] - P_notify_failure -> S_closing - - P_mood_happy [shape="box" label="M.close\nmood=happy"] - P_mood_happy -> S_closing - - P_mood_lonely [shape="box" label="M.close\nmood=lonely"] - P_mood_lonely -> S_closing - - S_closing [label="closing"] - S_closing -> P_closed [label="closed"] - S_closing -> S_closing [label="got_message"] - - P_closed [shape="box" label="A.closed"] - P_closed -> S_closed - S_closed [label="closed"] + S3 [label="S3:\nscared" color="red"] + S3 -> S3 [label="got_message"] } diff --git a/docs/send.dot b/docs/send.dot index 6f4ad6b..91ed067 100644 --- a/docs/send.dot +++ b/docs/send.dot @@ -1,11 +1,14 @@ digraph { start [label="Send\nMachine" style="dotted"] + {rank=same; S0 P0_queue} + {rank=same; S1 P1_send} + S0 [label="S0: unknown\nkey"] - S0 -> P0_queue [label="send" style="dashed"] - P0_queue [shape="box" label="queue" style="dashed"] - P0_queue -> S0 [style="dashed"] - S0 -> P0_got_key [label="set_verified_key"] + S0 -> P0_queue [label="send" style="dotted"] + P0_queue [shape="box" label="queue" style="dotted"] + P0_queue -> S0 [style="dotted"] + S0 -> P0_got_key [label="got_verified_key"] P0_got_key [shape="box" label="drain queue:\n[encrypt\n M.add_message]"] P0_got_key -> S1 diff --git a/docs/wormhole.dot b/docs/wormhole.dot index 83744dd..317ef59 100644 --- a/docs/wormhole.dot +++ b/docs/wormhole.dot @@ -10,80 +10,48 @@ digraph { start [label="Wormhole\nMachine" style="dotted"] - S0 [label="S0: know\nnothing"] - S0 -> P0_queue [label="send" style="dotted"] - P0_queue [shape="box" style="dotted" label="queue"] - P0_queue -> S0 [style="dotted"] + {rank=same; P0_code S0} + P0_code [shape="box" style="dashed" + label="Code.input\n or Code.allocate\n or Code.set"] + P0_code -> S0 + S0 [label="S0: empty"] S0 -> P0_build [label="set_code"] - P0_build [shape="box" label="build_pake\nM.set_nameplate\nM.add_message(pake)"] + P0_build [shape="box" label="M.set_nameplate\nK.set_code"] P0_build -> S1 - S1 [label="S1: know\ncode"] - S1 -> P1_queue [label="send" style="dotted"] - P1_queue [shape="box" style="dotted" label="queue"] - P1_queue -> S1 [style="dotted"] + S1 [label="S1: lonely" color="orange"] - /* 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. + S1 -> S2 [label="happy"] - 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.*/ + S1 -> P_close_scary [label="scared" color="red"] + S1 -> P_close_lonely [label="close"] + P_close_lonely [shape="box" label="M.close(lonely)"] + P_close_lonely -> S_closing - S1 -> P_mood_scary [label="got_message(pake)\npake bad"] - S1 -> P1_compute [label="got_message(pake)\npake good"] - S1 -> P1_queue_inbound [label="got_message(other)"] - P1_queue_inbound [shape="box" style="dotted" label="queue\ninbound"] - P1_queue_inbound -> S1 - S1 -> P_mood_lonely [label="close"] + P_close_scary [shape="box" label="M.close(scary)" color="red"] + P_close_scary -> S_closing [color="red"] - P1_compute [label="compute_key\nM.add_message(version)\nA.got_verifier\nschedule process inbound queue?" shape="box"] - P1_compute -> S2 + S2 [label="S2: happy" color="green"] + S2 -> P2_close [label="close"] + P2_close [shape="box" label="M.close(happy)"] + P2_close -> S_closing - P_mood_scary [shape="box" label="M.close\nmood=scary"] - P_mood_scary -> P_notify_failure - - P_notify_failure [shape="box" label="(record failure)" color="red"] - P_notify_failure -> S_closing - - S2 [label="S2: know_key\n(unverified)" color="orange"] - S2 -> P_queue3 [label="send" style="dotted"] - P_queue3 [shape="box" style="dotted" label="queue"] - P_queue3 -> S2 [style="dotted"] - S2 -> P_verify [label="got_message"] /* version or phase */ - S2 -> P_mood_lonely [label="close"] /* more like impatient */ - - P_verify [label="verify(msg)" shape="box"] - P_verify -> P_accept_msg [label="(good)"] - P_verify -> P_mood_scary [label="(bad)"] - - P_accept_msg [label="A.received(msg)\nencrypt queued\nM.add_message(queued)" - shape="box"] - P_accept_msg -> S3 - - S3 [label="S3: know_key\n(verified)" color="green"] - S3 -> P_verify [label="got_message"] /* probably phase */ - S3 -> P_mood_happy [label="close"] - S3 -> P_send [label="send"] - - P_mood_happy [shape="box" label="M.close\nmood=happy"] - P_mood_happy -> S_closing - - P_mood_lonely [shape="box" label="M.close\nmood=lonely"] - P_mood_lonely -> S_closing - - P_send [shape="box" label="encrypt\nM.add_message(msg)"] - P_send -> S3 + S2 -> P2_got_message [label="got_message"] + P2_got_message [shape="box" label="A.received"] + P2_got_message -> S2 S_closing [label="closing"] S_closing -> P_closed [label="closed"] - S_closing -> S_closing [label="got_message"] + S_closing -> S_closing [label="got_message\nhappy\nscared\nclose"] - P_closed [shape="box" label="A.closed"] + P_closed [shape="box" label="A.closed(reason)"] P_closed -> S_closed S_closed [label="closed"] + + {rank=same; Other S_closed} + Other [shape="box" style="dashed" + label="send -> S.send\ngot_verifier -> A.got_verifier" + ] + + }