diff options
| -rw-r--r-- | protocol.txt | 60 |
1 files changed, 36 insertions, 24 deletions
diff --git a/protocol.txt b/protocol.txt index 223f58a..7699e2a 100644 --- a/protocol.txt +++ b/protocol.txt @@ -6,34 +6,46 @@ Types.hs for the data types that JSON serialization instances are derived from. A debug-me session starts with the user sending an Activity Seen -containing some introductory message. This first Activity Seen has -Nothing as its prevActivity. All subsequent Activity sent by either the -user or developer has a prevActivity that points to the Hash of -the previous activity, so a chain of Activity is built up. +containing an introductory message, eg "debug-me session started". +This first Activity Seen has Nothing as its prevActivity. All +subsequent Activity sent by either the user or developer must have a +prevActivity that points to the Hash of the previous activity. +So a chain of Activity is built up. The exact details about how these objects are hashed is not described here; see Hash.hs for the implementation. Note that the JSON strings are *not* directly hashed (to avoid tying hashing to JSON serialization details), instead the values in the data types are hashed. -The user and developer have different points of view; the debug-me protocol -makes sure that both sides agree on what is happening, to avoid -disagreements. For example, the developer could send an Activity Entered -at the same time the user is sending an Activity Seen. In this case, -the developer didn't see something that happened while they were entering -a command. So, when the user receives their Activity Entered, and sees that -its prevActivity does not point to the just sent Activity Seen, the user -will reject that input, sending back a Rejected message to let the -developer know. - -This requirement that the developer always send Activity Entered that points -to the last Activity that the user has sent/accepted is known as the -synchronicity requirement. - -The synchronicity requirement can be problematic when the developer is -entering a command, because each letter they type gets echoed back, and -that echo happens asynchronously. To avoid needing to wait for the letter -to be echoed back before the next letter can be entered, the debug-me -protocol allows the developer to include echoDatta in an Activity Entered. - +The user and developer have different points of view. For example, +the developer could send an Activity Entered at the same time the user +is sending an Activity Seen. It's not clear in which order these two +Activities occurred -- in fact they occurred in different orders in +different places -- and so the user and developer will disagree +about it. + +Since the goal of debug-me is to produce a proof of the sequence of events +that occurred in a session, that is a problem. Perhaps the developer was +entering "y" in response to "Shutdown reactor?" at the same time +that a new "Vent core to atmosphere?" question was being displayed! +So, the debug-me protocol is designed to prevent such conflicts of opinion. + +The user only processes a new Activity Entered when either: + +1. The Activity Entered has as its prevActivity the last Activity + (Entered or Seen) that the user processed. +2. The Activity Entered has as its prevActivity an older Activity + that the user processed, and its echoData matches the concacenation + of every Activity Seen after the prevActivity, up to the most recent + Activity Seen. + + (This allows the developer to enter a command quickly without waiting + for each letter to echo back to them.) + +When an Activity Entered does not meet these rules, the user sends it +back in a Rejected message to let the developer know the input was not +allowed. + +The developer also checks the prevActivity of messages it receives +from the user, to make sure that it's receiving a valid chain of messages. |