From: Ian Jackson Date: Sun, 28 Jun 2020 14:22:58 +0000 (+0100) Subject: wip new based on update states X-Git-Tag: otter-0.2.0~1515 X-Git-Url: https://www.chiark.greenend.org.uk/ucgi/~ianmdlvl/git?a=commitdiff_plain;h=d552d0dc90fdf7015ae46c49153d94b0f9496101;p=otter.git wip new based on update states --- diff --git a/NOTES b/NOTES index 5cfeb07e..be1cee29 100644 --- a/NOTES +++ b/NOTES @@ -89,52 +89,70 @@ There is a diagraph of updates. Each update specifies the complete state of the piece. The server maintains an authoritative history; the client only maintains the state of the piece. -Updates may be from this client ("client updates") or from another +Updates may be from this client ("Client updates") or from another client or the server. We look at the protocol from a single client's -point of view, and call all the other updates "server updates". +point of view, and call all the other updates "Server updates". -Each update has a single ancestor. Updates may be: +Each update has a single direct ancestor, but this is not recorded in +the message nor by the client. Updates may be some combination of: -From the point of view of the server an update it has seen -may be: Recorded - stored by server. Downbound - on way from server to client. Discarded - received by server and thrown away. - -From the point of view of the client an update that it has seen may -be: - Processed - sent by server, state has been updated. - Upbound - local state has been updated by local action; - update on way from client to server. + Upbound - on way from client to server. + Displayed - seen by client, is most recent state + Superseded - seen by client, is no longer most recent state. Server assigns generation number (strictly increasing but maybe with gaps) to each Recorded update. -Each Upbound update contains the generation of the most recent +Each Upbound update is tagged with the generation of the most recent Processed update. -Actually the most redcent Processed generation stored by the client is +(Actually the most recent Processed generation stored by the client is global across all pieces, and the server's generations are likewise generated globally although recorded separately for each piece. So the update contain s a generation >= the most recently Processed update for that piece, and < any subseuent Processed upate for that piece. The server only compares the incoming update generation for >= -with a recorded value, so this makes no difference. +with a recorded value, so this makes no difference.) + +Desirable properties +-------------------- + +Legal combinations are: + Server + Recorded + Downbound + Server + Recorded + Displayed + Server + Recorded + Superseded + Client + (Displayed / Superseded) + Upbound + Client + (Displayed / Superseded) + Recorded + Client + (Displayed / Superseded) + Discarded + +_linear_: The Recorded updates form a linear sequence (so it is only +ever appended to). + +_forwards_: Each update has at most one Server descendant, and at most +one Client descendant. + +_display_: Exactly one update is Displayed at any one time. It has no +Client child and no Superseded descendants. Each update is only +Displayed at most once, and can only become Superseded after having +been Displayed. + +_discard_: For every Discarded update K there is a Recorded Server +update S which not an ancestor of K; and with S's generation > K's +tag. Invariants ---------- -The Recorded updates form +_record_: Sequence of Recorded updates is as follows. + Recorded Superseded zero or more + Recorded Displayed zero or one + Recorded Downbound zero or more + -Each update was caused by some client, possibly this one. We are not -interested in other clients - we treat those as the server deciding to -put its own updates onto A. So we talk about "client's" updates and -"server's" updates. -(Notation: "=" is any updates; "*" is server's updates; "-" is -client's updates. We speak of "XYZ" to includes Y and Z but not X, -unless X is O; or to put it another way letters indicate "just after" -the update. "!" indicates a nonempty sequence.) Invariants ---------- @@ -163,18 +181,149 @@ they were generated. (U and B must be inferred at the server, when they are needed.) + + + Update generation operations ---------------------------- -Sever may invent a foreign update at any time. This extends A. -The server must send the update. This is clearly OK. +I. Server update + +Server may invent and transmit an update at any time. Its ancestor is +the most recent Recorded update. It is Recorded+Downbound. No other +updates change their state. + +Properties and invariants: _linear_, _forwards_, _record_ are +obvious. _display_ is not affected. + +II. Client update + +Client may invent and transmit an update at any time; it must have the +Displayed update as its parent. That update becomes Superseded. +The new update is Displayed+Upbound. + +_linear_ and _record_ are not affected. _forwardxs_ is honoured +because of _display_. _display_ is preserved. + +Server message reception +------------------------ + +Suppose the server receives a message, Q. It was Client Upbound. + +Let T be the most recent Recorded message. The server finds the most +recent Server Recorded message, U. + +I. Q's generation is >= U's generation. + +The server records Q with T as parent. Q becomes Client Recorded; it +is Displayed or Superseded as before. + +_linear_: We need to show that T really is Q's parent. + +If Q's generation >= U's generation, the ancestry path have been +received by the server. So they must be Recorded or Discarded. + +Suppose one, K, was Discarded. Then by _discard_ there is some +Recorded Server update S which is not an ancestor of Q. S's +generation must be > Q's tag, since Q's tag is >= all of its Recorded +ancestors. So S's generation > U's. But this means that S is a +Server update more recent than U. _|_ + +So everything in is Recorded. Only Q is not Recorded. +Therefore Q's parent is indeed the most recent Recorded update, T. + +_forwards_: We aren't making new messages. _display_: We aren't +changing any of this. _discard_: we aren't discarding anything. + +_record_: Let S be the most recent Recorded Downbound update S. This +must be U. But Q's generation >= U's generation so U can no longer be +Downbound. So there are no Downbound updates. Maybe Q is Displayed; +in any case all older Recorded updates are Superseded. + +II. Q's generation is < U's generation + +The server discards Q. It becomes Discarded. + +_linear_, _forwards_, _display_, _record_: No change. + +_discard_: Q becomes K. Use U as S. U is Recorded. If Q had U as an +ancestor, U's generation would have been visible to the client when it +generated Q, so Q's tag would have been >= U's generation. S's +generation is U's generation and is >= Q's by case assumption. + + +Client message reception +------------------------ + +Suppose the client receives a message Q. + +It displays it. (The currently Displayed update becomes Superseded. +Q becomes Displayed.) + +_linear_, _forwards_, discard_: No change. + +_display_: Q is a Server message because it was Downbound. We have +just received it so it cannot yet have any Client descendant. It +might have Server descendants, but those are also Recorded Downbound, +by _record_. + +_record_: By order of delivery, Q is the most recent Recorded +Downbound. + + +Liveness properties +------------------- + +I. "When things ahve settled, all is consistent." + +If there are no Upbound or Downbound updates, the most recent Recorded +update R is Displayed. + +Suppose some update D is displayed instead. + +D can't be Recorded. If it were, R would have to be Downbound, by +_record_. + +So D can't be Server. Suppose D is Client. It must be Recorded, +Upbound or Discarded. Only Discarded is left. + +If D is Discarded, by _discard_, there is some Recorded Server S which +is not an ancestor of D, with S's generation > D's. S must be +Displayed or Superseded, since there are no Downbound updates. If S +were Displayed it would be equal to D, hence D would be an ancestor of +S. So S must be Superseded. + +If S is Recorded Superseded, at some point it was Displayed. D is now +Displayed. So D was Displayed more recently than S. D is Client so +when it was Displayed it became Upbound, tagged with a generation of +at least S's; i.e. D's generation >= S's. _|_ + + + + + +_live_: In all system states reachable from that system state without +the generation of server updates, either there are Upbound updates or +the most recently Recorded update is the most recently generated +client update. + + + + + + + This extends A. The server +must send the update. This is clearly OK. Client may invent a client's update at any time. It puts in the value of B, which it knows. This extends T. The client must send the update. This is clearly OK. -Server message reception ------------------------- Suppose the server receives a message, Q. Q must be a descendant