PROTOCOL.md

   1 Copyright 2020-2021 Ian Jackson and contributors to Otter
   2 SPDX-License-Identifier: AGPL-3.0-or-later
   3 There is NO WARRANTY.
   4
   5
   6 CONCURRENT UPDATE PROTOCOL AND ANALYSIS
   7 =======================================
   8
   9 (Assumption: our network techniques deliver messages in order in both
  10 directions between a server and a client; failure of the communication
  11 stream is allowed to break things - we treat it as fatal.)
  12
  13 We run the following algorithm / data model separately for each piece.
  14
  15
  16 Model
  17 -----
  18
  19 There is:
  20
  21   * actual committed history, a list of updates
  22   * the history seen so far by the client
  23     this can only advance, which is a prefix of the above
  24   * possibly branch(es) of history made by the client;
  25     this can rewind and be discarded
  26
  27 There is a diagraph of updates.  Each update specifies the complete
  28 state of the piece.  The server maintains an authoritative history;
  29 the client only maintains the state of the piece.
  30
  31 Updates may be from this client ("`Client` updates") or from another
  32 client or made by the server itself.  We look at the protocol from a
  33 single client's point of view, and call all the other updates
  34 "`Server` updates".
  35
  36 Each update has a single direct ancestor, but this is not recorded in
  37 the message nor by the client.  Updates may be some combination of:
  38
  39   * `Recorded` - stored by server.
  40   * `Downbound` - on way from server to client.
  41   * `Discarded` - received by server and thrown away.
  42   * `Upbound` - on way from client to server.
  43   * `Displayed` - seen by client, is most recent state there
  44   * `Superseded` - seen by client, is no longer most recent state.
  45
  46 Server assigns generation number (strictly increasing but maybe with
  47 gaps) to each `Recorded` update.
  48
  49 Each `Upbound` update is tagged with the generation of the most recent
  50 Processed update.
  51
  52 (Actually the most recent Processed generation stored by the client is
  53 global across all pieces, and the server's generations are likewise
  54 generated globally although recorded separately for each piece.  So
  55 the update contain s a generation >= the most recently Processed
  56 update for that piece, and < any subseuent Processed upate for that
  57 piece.  The server only compares the incoming update generation for >=
  58 with a recorded value, so this makes no difference.)
  59
  60 Desirable properties and invariants
  61 -----------------------------------
  62
  63 Legal combinations are:
  64
  65   * `Server` + `Recorded` + `Downbound`
  66   * `Server` + `Recorded` + `Displayed`
  67   * `Server` + `Recorded` + `Superseded`
  68   * `Client` + (`Displayed` / `Superseded`) + `Upbound`
  69   * `Client` + (`Displayed` / `Superseded`) + `Recorded`
  70   * `Client` + (`Displayed` / `Superseded`) + `Discarded`
  71
  72 _linear_: The `Recorded` updates form a linear sequence (so it is only
  73 ever appended to).
  74
  75 _forwards_: Each update has at most one `Server` descendant, and at most
  76 one `Client` descendant.
  77
  78 _display_: Exactly one update is `Displayed` at any one time.  It has no
  79 `Client` child and no `Superseded` descendants.  Each update is only
  80 `Displayed` at most once, and can only become `Superseded` after having
  81 been `Displayed`.
  82
  83 _discard_: For every `Discarded` update K there is a `Recorded` `Server`
  84 update S which not an ancestor of K; and with S's generation > K's
  85 tag.
  86
  87 _record_: Sequence of `Recorded` updates is as follows:
  88
  89   * `Recorded` `Superseded` (zero or more)
  90   * `Recorded` `Displayed` (zero or one)
  91   * `Recorded` `Downbound` (zero or more)
  92
  93
  94 Update generation operations
  95 ----------------------------
  96
  97 ### I. Server update ###
  98
  99 Server may invent and transmit an update at any time.  Its ancestor is
 100 the most recent `Recorded` update.  It is `Recorded`+`Downbound`.  No other
 101 updates change their state.
 102
 103 Properties and invariants: _linear_, _forwards_, _record_ are
 104 obvious.  _display_ is not affected.
 105
 106 ### II. Client update ###
 107
 108 Client may invent and transmit an update at any time; it must have the
 109 `Displayed` update as its parent.  That update becomes `Superseded`.
 110 The new update is `Displayed`+`Upbound`.
 111
 112 _linear_ and _record_ are not affected.  _forwardxs_ is honoured
 113 because of _display_.  _display_ is preserved.
 114
 115 Server message reception
 116 ------------------------
 117
 118 Suppose the server receives a message, Q.  It was `Client` `Upbound`.
 119
 120 Let T be the most recent `Recorded` message.  The server finds the most
 121 recent `Server` `Recorded` message, U.
 122
 123 ### I. Q's generation is >= U's generation. ###
 124
 125 The server records Q with T as parent.  Q becomes `Client` `Recorded`; it
 126 is `Displayed` or `Superseded` as before.
 127
 128 _linear_: We need to show that T really is Q's parent.
 129
 130 If Q's generation >= U's generation, the ancestry path <U..Q] exists
 131 and contains only `Client` updates: if there were some `Server` update S
 132 in U..Q, it would be `Recorded` (since all `Server` messages are) and more
 133 recent than U, contradicting the definition of U.
 134
 135 Because of in-order message delivery, all updates in <U..Q> have been
 136 received by the server.  So they must be `Recorded` or `Discarded`.
 137
 138 Suppose one, K, was `Discarded`.  Then by _discard_ there is some
 139 `Recorded` `Server` update S which is not an ancestor of Q.  S's
 140 generation must be > Q's tag, since Q's tag is >= all of its `Recorded`
 141 ancestors.  So S's generation > U's.  But this means that S is a
 142 `Server` update more recent than U. _|_
 143
 144 So everything in <U..Q> is `Recorded`.  Only Q is not `Recorded`.
 145 Therefore Q's parent is indeed the most recent `Recorded` update, T.
 146
 147 _forwards_: We aren't making new messages.  _display_: We aren't
 148 changing any of this.  _discard_: we aren't discarding anything.
 149
 150 _record_: Let S be the most recent `Recorded` `Downbound` update S.  This
 151 must be U.  But Q's generation >= U's generation so U can no longer be
 152 `Downbound`.  So there are no `Downbound` updates.  Maybe Q is `Displayed`;
 153 in any case all older `Recorded` updates are `Superseded`.
 154
 155 ### II. Q's generation is < U's generation ###
 156
 157 The server discards Q.  It becomes `Discarded`.
 158
 159 _linear_, _forwards_, _display_, _record_: No change.
 160
 161 _discard_: Q becomes K.  Use U as S.  U is `Recorded`.  If Q had U as an
 162 ancestor, U's generation would have been visible to the client when it
 163 generated Q, so Q's tag would have been >= U's generation.  S's
 164 generation is U's generation and is >= Q's by case assumption.
 165
 166
 167 Client message reception
 168 ------------------------
 169
 170 Suppose the client receives a message Q.
 171
 172 It displays it.  (The currently `Displayed` update becomes `Superseded`.
 173 Q becomes `Displayed`.)
 174
 175 _linear_, _forwards_, discard_: No change.
 176
 177 _display_: Q is a `Server` update because it was `Downbound`.  We have
 178 just received it so it cannot yet have any `Client` descendant.  It
 179 might have `Server` descendants, but those are also `Recorded` `Downbound`,
 180 by _record_.
 181
 182 _record_: By order of delivery, Q is the most recent `Recorded`
 183 `Downbound`.
 184
 185
 186 Liveness property
 187 -----------------
 188
 189 "When things ahve settled, all is consistent."
 190
 191 If there are no `Upbound` or `Downbound` updates, the most recent `Recorded`
 192 update R is `Displayed`.
 193
 194 Suppose some update D is displayed instead.
 195
 196 D can't be `Recorded`.  If it were, R would have to be `Downbound`, by
 197 _record_.
 198
 199 So D can't be `Server`.  Suppose D is `Client`.  It must be `Recorded`,
 200 `Upbound` or `Discarded`.  Only `Discarded` is left.
 201
 202 If D is `Discarded`, by _discard_, there is some `Recorded` `Server` S which
 203 is not an ancestor of D, with S's generation > D's.  S must be
 204 `Displayed` or `Superseded`, since there are no `Downbound` updates.  If S
 205 were `Displayed` it would be equal to D, hence D would be an ancestor of
 206 S.  So S must be `Superseded`.
 207
 208 If S is `Recorded` `Superseded`, at some point it was `Displayed`.  D is now
 209 `Displayed`.  So D was `Displayed` more recently than S.  D is `Client` so
 210 when it was `Displayed` it became `Upbound`, tagged with a generation of
 211 at least S's; i.e. D's generation >= S's.  _|_
 212
 213 SERVER ACKS
 214 ===========
 215
 216 Actually, the client wants to know when conflicts occur, so that it
 217 can report to the user, and interrupt drag operations etc.
 218 To this end:
 219
 220 Update messages from the client to the server also contain a client
 221 sequence number (monotonically but not strictly increasing).  When the
 222 client sends an update, it makes a note of the sequence number.  This
 223 is the "outstanding Client updates sequence number note", or the
 224 "oustanding note".
 225
 226 When the server processes a message from the client and Records it, it
 227 puts the client sequence number in the update stream (as a non-update
 228 message).  (This is skipped if it's the same as the last client
 229 sequence number for that client.)
 230
 231 If the echoed sequence number is equal to the client's oustanding
 232 note, the client knows the server is up to date, and deletes the note.
 233
 234 If the client sees a Server update message, and the client has a note,
 235 it knows that there was a conflict.
 236
 237
 238 LEVEL (Z ORDER)
 239 ===============
 240
 241 Each piece has a Z level which is a finite f64, set by the client
 242 which manipulates the piece, according to the protocol above.
 243
 244 Each piece *also* has a Z level generation.  This is set by the
 245 server.  The server guarantees to set it to the server generation, and
 246 guarantees to do so as the result of any client Z level update.
 247
 248 So the client which sends a Z level update can assume that a server
 249 update to the generation will turn up, and with a higher value.
 250
 251 The Z generation is used to disambiguate the Z order for pieces with
 252 identical Z level.  Higher values are closer to the user (ie, occlude
 253 lower values).