d4f8045c4a4f5478ecd2b06ec4f94fcbcd65f631
1 \documentclass[11pt]{article}\r
2 \newcommand{\tuple}{\ensuremath \langle #1 \rangle}\r
3 \usepackage{color}\r
4 \usepackage{amsthm}\r
5 \usepackage{amsmath}\r
6 \usepackage{graphicx}\r
7 \usepackage{mathrsfs}\r
8 \usepackage{algpseudocode}% http://ctan.org/pkg/algorithmicx\r
9 \newtheorem{theorem}{Theorem}\r
10 \newtheorem{prop}{Proposition}\r
11 \newtheorem{lem}{Lemma}\r
12 \newtheorem{defn}{Definition}\r
13 \newcommand{\note}{{\color{red} \bf [[#1]]}}\r
14 \newcommand{\push}{\hskip\dimexpr #1\algorithmicindent\relax}\r
15 \begin{document}\r
16 \section{Approach}\r
17 \r
18 \subsection{Keys}\r
19 \r
20 Each device has: user id + password\r
21 \r
22 Server login is:\r
23 hash1(user id), hash1(password)\r
24 \r
25 Symmetric Crypto keys is:\r
26 hash2(user id | password)\r
27 \r
28 Server has finite length queue of entries + max\_entry\_identifier +\r
29 server login key\r
30 \r
31 \subsection{Entry layout}\r
32 Each entry has:\r
33 \begin{enumerate}\r
34 \item Sequence identifier\r
35 \item Random IV (if needed by crypto algorithm)\r
36 \item Encrypted payload\r
37 \end{enumerate}\r
38 \r
40 \begin{enumerate}\r
41 \item Sequence identifier\r
42 \item Machine id (most probably something like a 64-bit random number \r
43 that is self-generated by client)\r
44 \item HMAC of previous slot\r
45 \item Data entries\r
46 \item HMAC of current slot\r
47 \end{enumerate}\r
48 \r
49 A data entry can be one of these:\r
50 \begin{enumerate}\r
51 \item All or part of a Key-value entry\r
52 \item Slot sequence entry: Machine id + last message identifier \r
53 \newline {The purpose of this is to keep the record of the last slot \r
54 from a certain client if a client's update has to expunge that other \r
55 client's last entry from the queue. This is kept in the slot until \r
56 the entry owner inserts a newer update into the queue.}\r
57 \item Queue state entry: Includes queue size \newline {The purpose \r
58 of this is for the client to tell if the server lies about the number \r
59 of slots in the queue, e.g. if there are 2 queue state entry in the queue, \r
60 e.g. 50 and 70, the client knows that when it sees 50, it should expect \r
61 at most 50 slots in the queue and after it sees 70, it should expect \r
62 50 slots before that queue state entry slot 50 and at most 70 slots. \r
63 The queue state entry slot 70 is counted as slot number 51 in the queue.}\r
64 \item Collision resolution entry: message identifier + machine id of a\r
65 collision winner\r
66 \newline {The purpose of this is to keep keep track of the winner of \r
67 all the collisions until all clients have seen the particular entry.}\r
68 \end{enumerate}\r
69 \r
70 \subsection{Live status}\r
71 \r
72 Live status of entries:\r
73 \begin{enumerate}\r
74 \item Key-Value Entry is dead if either (a) there is a newer key-value pair or (b) it is incomplete.\r
75         \r
76 \item Slot sequence number (of either a message version data\r
77 or user-level data) is dead if there is a newer slot from the same machine.\r
78 \r
79 \item Queue state entry is dead if there is a newer queue state entry.\r
80 {In the case of queue state entries 50 and 70, this means that queue state \r
81 entry 50 is dead and 70 is live. However, not until the number of slots reaches \r
82 70 that queue state entry 50 will be expunged from the queue.}\r
83 \r
84 \item Collision resolution entry is dead if this entry has been seen\r
85 by all clients after a collision happens.\r
86 \end{enumerate}\r
87 \r
88 When data is at the end of the queue ready to expunge, if:\r
89 \begin{enumerate}\r
90 \item The key-value entry is not dead, it must be reinserted at the\r
91 beginning of the queue.\r
92 \r
93 \item If the slot sequence number is not dead, then a message sequence\r
94 entry must be inserted.\r
95 \r
96 \item If the queue state entry is not dead, it must be reinserted at the\r
97 beginning of the queue.\r
98 \end{enumerate}\r
99 \r
100 \r
102 Client sends a sequence number.  Server replies with either: all data\r
103 entries or all newer data entries.\r
104 \r
105 \paragraph{Writes:}\r
106 Client sends slot, server verifies that sequence number is valid,\r
107 checks entry hash, and replies with an accept message if all checks\r
108 pass.  On success, client updates its sequence number.  On failure,\r
109 server sends updates slots to client and client validates those slots.\r
110 \r
111 \paragraph{Local state on each client:}\r
112 A list of machines and the corresponding latest sequence numbers.\r
113 \r
114 \paragraph{Validation procedure on client:}\r
115 \begin{enumerate}\r
116 \item Decrypt each new slot in order.\r
117 \item For each slot:\r
118     (a) check its HMAC, and\r
119     (b) check that the previous entry HMAC field matches the previous\r
120     entry.\r
121 \item Check that the last message version for our machine matches our\r
122 last message sent.\r
123 \item For all other machines, check that the latest sequence number is\r
124 at least as large (never goes backwards).\r
125 \item That the queue has a current queue state entry.\r
126 \item That the number of entries received is consistent with the size\r
127 specified in the queue state entry.\r
128 \end{enumerate}\r
129 \r
130 Key-value entries can span multiple slots.  They aren't valid until\r
131 they are complete.\r
132 \r
133 \subsection{Resizing Queue}\r
134 Client can make a request to resize the queue. This is done as a write that combines:\r
135   (a) a slot with the message, and\r
136         (b) a request to the server\r
137 \r
138 \subsection{Server Algorithm}\r
139 $s \in SN$ is a sequence number set\\\r
140 $sv \in SV$ is a slot's value\\\r
141 $slot_s = \tuple{s, sv} \in SL \subseteq SN \times SV$ \\ \\\r
142 \textbf{State} \\\r
143 \textit{SL = set of live slots on server} \\\r
144 \textit{max = maximum number of slots (input only for resize message)} \\\r
145 \textit{n = number of slots} \\ \\\r
146 \textbf{Helper Function} \\\r
147 $MaxSlot(SL_s)= \tuple{s, sv} \mid \tuple{s, sv}\r 148 \in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s \geq s_s$ \\\r
149 $MinSlot(SL_s)= \tuple{s, sv} \mid \tuple{s, sv} \r 150 \in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s \leq s_s$ \\\r
151 $SeqN(\tuple{s, sv})=s$ \\\r
152 $SlotVal(\tuple{s, sv})=sv$ \\\r
153 \r
154 \begin{algorithmic}\r
155 \Function{GetSlot}{$s_g$}\r
156 \State \Return{$\{\tuple{s, sv} \in SL \mid s \geq s_g\}$}\r
157 \EndFunction\r
158 \end{algorithmic}\r
159 \r
160 \begin{algorithmic}\r
161 \Function{PutSlot}{$s_p,sv_p,max'$}\r
162 \If{$(max' \neq \emptyset)$}\Comment{Resize}\r
163 \State $max \gets max'$\r
164 \EndIf\r
165 \State $\tuple{s_n,sv_n} \gets MaxSlot(SL)$\Comment{Last sv}\r
166 \State $s_n \gets SeqN(\tuple{s_n,sv_n})$\r
167 \If{$(s_p = s_n + 1)$}\r
168         \If{$n = max$}\r
169         \State $\tuple{s_m,sv_m} \gets MinSlot(SL)$\Comment{First sv}\r
170                 \State $SL \gets SL - \{\tuple{s_m,sv_m}\}$\r
171         \Else \Comment{$n < max$}\r
172                 \State $n \gets n + 1$\r
173         \EndIf\r
174     \State $SL \gets SL \cup \{\tuple{s_p,sv_p}\}$\r
175         \State \Return{$(true,\emptyset)$}\r
176 \Else\r
177         \State \Return{$(false,\{\tuple{s,sv}\in SL \mid \r 178 s \geq s_p\})$}\r
179 \EndIf\r
180 \EndFunction\r
181 \end{algorithmic}\r
182 \r
183 \subsection{Client Algorithm}\r
185 \textbf{Data Entry} \\\r
186 $de$ is a data entry \\\r
187 $k$ is key of entry \\\r
188 $v$ is value of entry \\\r
189 $kv$ is a key-value entry $\tuple{k,v}$, $kv \in D$ \\\r
190 $ss$ is a slot sequence entry $\tuple{id,s_{last}}$, \r
191 id + last s of a machine, $ss \in D$ \\\r
192 $qs$ is a queue state entry (contains $max$ size of queue), $qs \in D$ \\\r
193 $cr$ is a collision resolution entry $\tuple{s_{col},id_{col}}$, \r
194 s + id of a machine that wins a collision, $cr \in D$ \\\r
195 $D = \{kv,ss,qs,cr\}$ \\\r
196 $DE = \{de \mid de \in D\}$ \\ \\\r
197 $s \in SN$ is a sequence number set\\\r
198 $id$ is a machine ID\\\r
199 $hmac_p$ is the HMAC value of the previous slot \\\r
200 $hmac_c$ is the HMAC value of the current slot \\\r
201 $Dat_s = \tuple{s,id,hmac_p,DE,hmac_c}$ \\\r
202 $sv_s = \tuple{s, E(Dat_s)} = \r 203 \tuple{s, E(\tuple{s,id,hmac_p,DE,hmac_c})}$ \\ \\\r
204 \textbf{States} \\\r
205 \textit{$hmac_{p_g}$ = the HMAC value of the previous slot \r
206 ($hmac_{p_g} = \emptyset$ for the first slot)} \\\r
207 \textit{$id_{self}$ = machine Id of this client} \\\r
208 \textit{$max_g$ = maximum number of slots (initially $max_g > 0$)} \\\r
209 \textit{m = number of slots on client (initially $m = 0$ and $m \leq n$)} \\\r
210 \textit{$sl_{last}$ = info of last slot in queue = \r
211         $\tuple{s_{last},sv_{last},id_{last}}$ (initially $\emptyset$)} \\\r
212 \textit{DT = set of $\tuple{k,v}$ on client} \\\r
213 \textit{MS = set of $\tuple{id, s_{last}}$ of all clients on client \r
214 (initially empty)} \\\r
215 \textit{$MS_g$ = set MS to save all $\tuple{id, s_{last}}$ pairs while\r
216 traversing DT after a request to server (initially empty)} \\\r
217 \textit{SK = Secret Key} \\\r
218 \textit{$SM$ = set of $\tuple{s, id}$ of all slots in a previous read\r
219 (initially empty)} \\ \\\r
220 \textbf{Helper Functions} \\\r
221 $MaxSlot(SL_s)= \tuple{s, sv}$ \textit{such that} $\tuple{s, sv}\r 222 \in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s \geq s_s$ \\\r
223 $MinSlot(SL_s)= \tuple{s, sv}$ \textit{such that} $\tuple{s, sv} \r 224 \in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s \leq s_s$ \\\r
225 $Slot(SL_s,s_s)= \tuple{s, sv}$ \textit{such that} $\tuple{s, sv} \r 226 \in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s = s_s$ \\\r
227 $SeqN(\tuple{s, sv})=s$ \\\r
228 $SlotVal(\tuple{s, sv})=sv$ \\\r
229 $CreateLastSL(s,sv,id)=\tuple{s,sv,id}=sl_{last}$ \\\r
230 $Decrypt(SK_s,sv_s)=Dat_s=\tuple{s,id,hmac_p,DE,hmac_c}$ \\\r
231 $GetSeqN(Dat_s = \tuple{s,id,hmac_p,DE,hmac_c})=s$ \\\r
232 $GetMacId(Dat_s = \tuple{s,id,hmac_p,DE,hmac_c})=id$ \\\r
233 $GetPrevHmac(Dat_s = \tuple{s,id,hmac_p,DE,hmac_c})=hmac_p$ \\\r
234 $GetCurrHmac(Dat_s = \tuple{s,id,hmac_p,DE,hmac_c})=hmac_c$ \\\r
235 $GetDatEnt(Dat_s = \tuple{s,id,hmac_p,DE,hmac_c})=DE$ \\\r
236 $GetKV(de_s$ \textit{such that} $de_s \in D \land de_s = kv)=\tuple{k_s,v_s}$ \\\r
237 $GetSS(de_s$ \textit{such that} $de_s \in D \land de_s = ss)=\tuple{id,s_{last}}$ \\\r
238 $GetQS(de_s$ \textit{such that} $de_s \in D \land de_s = qs)=qs_s$ \\\r
239 $GetCR(de_s$ \textit{such that} $de_s \in D \land de_s = cr)=\tuple{s_s,id_s}$ \\\r
240 $GetLastSeqN(MS_s,id_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}}\r 241 \in MS_s \wedge \forall \tuple{id_s, s_{s_{last}}} \in MS_s, id = id_s$ \\\r
242 $GetMachineId(SM_s,s_s)= id$ \textit{such that} $\tuple{s, id}\r 243 \in SM_s \wedge \forall \tuple{s_s, id_s} \in SM_s, s = s_s$ \\\r
244 $GetS(\tuple{s, id})=s$ \\\r
245 $GetId(\tuple{s, id})=id$ \\\r
246 $GetKey(\tuple{k, v})=k$ \\\r
247 $GetVal(\tuple{k, v})=v$ \\\r
248 $GetKeyVal(DT_s,k_s)= \tuple{k, v}$ \textit{such that} $\tuple{k, v} \r 249 \in DT_s \wedge \forall \tuple{k_s, v_s} \in DT_s, k = k_s$ \\\r
250 $MaxLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s \r 251 \wedge \forall \tuple{id_s, s_{s_{last}}} \in MS_s, s_{last} \geq s_{s_{last}}$ \\\r
252 $MinLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s \r 253 \wedge \forall \tuple{id_s, s_{s_{last}}} \in MS_s, s_{last} \leq s_{s_{last}}$ \\\r
254 \r
255 \begin{algorithmic}\r
256 \Procedure{ReportError}{$msg$}\r
257 \State $Print(msg)$\r
258 \State $Halt()$\r
259 \EndProcedure\r
260 \end{algorithmic}\r
261 \r
262 \note{Don't include such that'' in the argument of a function...}\r
263 \r
264 \begin{algorithmic}\r
265 \Function{ValidHmac}{$DE_s,SK_s,hmac_{stored}$}\r
266 \State $hmac_{computed} \gets Hmac(DE_s,SK_s)$\r
267 \State \Return {$hmac_{stored} = hmac_{computed}$}\r
268 \EndFunction\r
269 \end{algorithmic}\r
270 \r
271 \begin{algorithmic}\r
272 \Function{ValidPrevHmac}{$DE_s,hmac_{p_s},hmac_{p_{sto}}$}\r
273 \If{$hmac_{p_s} = \emptyset$}\Comment{First slot - no previous HMAC}\r
274         \State \Return $true$\r
275 \Else\r
276         \State \Return {$hmac_{p_{sto}} = hmac_{p_s}$}\r
277 \EndIf\r
278 \EndFunction\r
279 \end{algorithmic}\r
280 \r
281 \note{So if a slot has a null previous hmac, everything is fine?  What if it isn't the first slot?}\r
282 \r
283 \begin{algorithmic}\r
284 \Function{GetQueSta}{$Dat_s$}\r
285 \State $DE_s \gets GetDatEnt(DE_s)$\r
286 \State $de_{qs} \gets de_s$ \textit{such that} $de_s \in DE_s, \r 287 de_s \in D \land de_s = qs$\r
288 \If{$de_{qs} \neq \emptyset$}\r
289         \State $qs_{ret} \gets GetQS(de_{qs})$\r
290 \Else\r
291         \State $qs_{ret} \gets \emptyset$\r
292 \EndIf\r
293 \State \Return{$qs_{ret}$}\r
294 \EndFunction\r
295 \end{algorithmic}\r
296 \r
297 \begin{algorithmic}\r
298 \Function{GetSlotSeq}{$Dat_s$}\r
299 \State $DE_s \gets GetDatEnt(Dat_s)$\r
300 \State $de_{ss} \gets de_s$ \textit{such that} $de_s \in DE_s, \r 301 de_s \in D \land de_s = ss$\r
302 \If{$de_{ss} \neq \emptyset$}\r
303         \State $\tuple{id_{ret},s_{last_{ret}}} \gets GetSS(de_{ss})$\r
304 \Else\r
305         \State $\tuple{id_{ret},s_{last_{ret}}} \gets \emptyset$\r
306 \EndIf\r
307 \State \Return{$\tuple{id_{ret},s_{last_{ret}}}$}\r
308 \EndFunction\r
309 \end{algorithmic}\r
310 \r
311 \begin{algorithmic}\r
312 \Function{GetColRes}{$Dat_s$}\Comment{At most 2 $cr$ entries in a slot}\r
313 \State $DE_s \gets GetDatEnt(Dat_s)$\r
314 \State $de_{cr} \gets de_s$ \textit{such that} $de_s \in DE_s, \r 315 de_s \in D \land de_s = cr$\r
316 \If{$de_{cr} \neq \emptyset$}\r
317         \State $\tuple{s_{ret},id_{ret}} \gets GetCR(de_{cr})$\r
318 \Else\r
319         \State $\tuple{s_{ret},id_{ret}} \r 320 \gets \emptyset$\r
321 \EndIf\r
322 \State $de_{r_{cr}} \gets de_s$ \textit{such that} $de_s \in DE_s, \r 323 de_s \in D \land de_s = cr \land de_s \neq de_{cr}$\r
324 \If{$de_{r_{cr}} \neq \emptyset$}\r
325         \State $\tuple{s_{r_{ret}},id_{r_{ret}}} \gets GetCR(de_{r_{cr}})$\r
326 \Else\r
327         \State $\tuple{s_{r_{ret}},id_{r_{ret}}} \r 328 \gets \emptyset$\r
329 \EndIf\r
330 \State \Return{$\{\tuple{s_{ret},id_{ret}},\tuple{s_{r_{ret}},id_{r_{ret}}}\}$}\r
331 \EndFunction\r
332 \end{algorithmic}\r
333 \r
334 \begin{algorithmic}\r
335 \Function{UpdateLastSeqN}{$id_s,s_s,MS_s$}\r
336 \State $s_t \gets GetLastSeqN(MS_s,id_s)$\r
337 \If{$s_t = \emptyset$}\r
338         \State $MS_s \gets MS_s \cup \{\tuple{id_s,s_s}\}$\Comment{First occurrence}\r
339 \Else\r
340         \If{$s_s > s_t$}\Comment{Update entry with a later s}\r
341         \State $MS_s \gets (MS_s - \{\tuple{id_s,s_t}\}) \cup \r 342 \{\tuple{id_s,s_s}\}$\r
343     \EndIf\r
344 \EndIf\r
345 \State \Return{$MS_s$}\r
346 \EndFunction\r
347 \end{algorithmic}\r
348 \r
349 \begin{algorithmic}\r
350 \Procedure{CheckLastSeqN}{$MS_s,MS_t$}\Comment{Check $MS_t$ based on $MS_s$}\r
351 \ForAll{$\tuple{id_t,s_{t_{last}}} \in MS_t$}\r
352         \State $s_{s_{last}} \gets GetLastSeqN(MS_s,id_t)$\r
353         \If{$s_{s_{last}} \neq \emptyset$}\r
354                 \If{$id_t = id_{self}$}\r
355                 \If{$s_{s_{last}} \neq s_{t_{last}}$}\r
356                                 \State \Call{ReportError}{'Invalid last $s$ for this machine'}\r
357                         \EndIf\r
358                 \Else\r
359                         \If{$s_{s_{last}} \geq s_{t_{last}}$}\r
360                                 \State $MS_s \gets (MS_s - \{\tuple{id_t,s_{t_{last}}}\}) \cup \r 361 \{\tuple{id_t,s_{s_{last}}}\}$\r
362                         \Else\r
363                                 \State \Call{ReportError}{'Invalid last $s$ for machine $id_t$'}\r
364                         \EndIf\r
365                 \EndIf\r
366         \EndIf\r
367 \EndFor\r
368 \EndProcedure\r
369 \end{algorithmic}\r
370 \r
371 \begin{algorithmic}\r
372 \Procedure{CheckCollision}{$MS_s,SM_s,\tuple{s_s,id_s}$}\r
373 \If{$\tuple{s_s,id_s} \neq \emptyset$}\r
374         \State $s_s \gets GetS(\tuple{s_s,id_s})$\r
375         \State $id_s \gets GetId(\tuple{s_s,id_s})$\r
376         \State $s_{s_{last}} \gets GetLastSeqN(MS_s,id_s)$\r
377         \If{$s_{s_{last}} < s_s$}\r
378                 \State $\Call{CheckColRes}{SM_s,\tuple{s_s,id_s}}$\r
379         \EndIf\r
380 \EndIf\r
381 \EndProcedure\r
382 \end{algorithmic}\r
383 \r
384 \begin{algorithmic}\r
385 \Procedure{CheckColRes}{$SM_s,\tuple{s_t,id_t}$}\Comment{Check $id_s$ in $SM_s$}\r
386 \State $s_t \gets GetS(\tuple{s_t,id_t})$\r
387 \State $id_t \gets GetId(\tuple{s_t,id_t})$\r
388 \State $id_s \gets GetMachineId(SM_s,s_t)$\r
389 \If{$id_s \neq id_t$}\r
390         \State \Call{ReportError}{'Invalid $id_s$ for this slot update'}\r
391 \EndIf\r
392 \EndProcedure\r
393 \end{algorithmic}\r
394 \r
395 \begin{algorithmic}\r
396 \Function{StoreLastSlot}{$MS_s,sl_l,s_s,sv_s,id_s$}\r
397 \State $s_{min} \gets MinLastSeqN(MS_s)$\r
398 \If{$s_{min} \neq \emptyset \land s_{min} = s_s$}\Comment{$MS$ initially empty}\r
399         \State $sl_l \gets CreateLastSL(s_s,sv_s,id_s)$\r
400 \EndIf\r
401 \State \Return{$sl_l$}\r
402 \EndFunction\r
403 \end{algorithmic}\r
404 \r
405 \begin{algorithmic}\r
406 \Function{UpdateDT}{$DT_s,Dat_s$}\r
407 \State $DE_s \gets GetDatEnt(Dat_s)$\r
408 \ForAll{$de_s \in DE_s$}\r
409         \If{$de_s$ \textit{such that} $de_s \in D \land de_s = kv$}\r
410                 \State $\tuple{k_s,v_s} \gets GetKV(de_s)$\r
411                 \State $\tuple{k_s,v_t} \gets GetKeyVal(DT_s,k_s)$\r
412                 \If{$\tuple{k_s,v_t} = \emptyset$}\r
413                         \State $DT_s \gets DT_s \cup \{\tuple{k_s,v_s}\}$\r
414                 \Else\r
415                 \State $DT_s \gets (DT_s - \{\tuple{k_s,v_t}\}) \cup \r 416 \{\tuple{k_s,v_s}\}$\r
417                 \EndIf\r
418     \EndIf\r
419 \EndFor\r
420 \State \Return{$DT_s$}\r
421 \EndFunction\r
422 \end{algorithmic}\r
423 \r
424 \begin{algorithmic}\r
425 \Procedure{ProcessSL}{$SL_g$}\r
426 \State $MS_g \gets \emptyset$\r
427 \State $SM_{curr} \gets \emptyset$\r
428 \State $\tuple{s_{g_{max}},sv_{g_{max}}} \gets MaxSlot(SL_g)$\r
429 \State $s_{g_{max}} \gets SeqN(\tuple{s_{g_{max}},sv_{g_{max}}})$\r
430 \State $\tuple{s_{g_{min}},sv_{g_{min}}} \gets MinSlot(SL_g)$\r
431 \State $s_{g_{min}} \gets SeqN(\tuple{s_{g_{min}},sv_{g_{min}}})$\r
432 \For{$s_g \gets s_{g_{min}}$ \textbf{to} $s_{g_{max}}$}\Comment{Process slots \r
433         in $SL_g$ in order}\r
434         \State $\tuple{s_g,sv_g} \gets Slot(SL_g,s_g)$\r
435         \State $SM_{curr} \gets SM_{curr} \cup \{\tuple{s_g,sv_g}\}$\r
436     \State $s_g \gets SeqN(\tuple{s_g,sv_g})$\r
437         \State $sv_g \gets SlotVal(\tuple{s_g,sv_g})$\r
438         \State $Dat_g \gets Decrypt(SK,sv_g)$\r
439         \State $s_{g_{in}} \gets GetSeqN(Dat_g)$\r
440     \If{$s_g \neq s_{g_{in}}$}\r
441                 \State \Call{ReportError}{'Invalid sequence number'}\r
442         \EndIf\r
443         \State $DE_g \gets GetDatEnt(Dat_g)$\r
444         \State $hmac_{p_{stored}} \gets GetPrevHmac(Dat_g)$\r
445         \If{$\neg \Call{ValidPrevHmac}{DE_g,hmac_{p_g},hmac_{p_{stored}}}$}\r
446                 \State \Call{ReportError}{'Invalid previous HMAC value'}\r
447         \EndIf\r
448         \State $hmac_{c_g} \gets GetCurrHmac(Dat_g)$\r
449         \If{$\neg \Call{ValidHmac}{DE_g,SK,hmac_{c_g}}$}\r
450                 \State \Call{ReportError}{'Invalid current HMAC value'}\r
451         \EndIf\r
452         \State $hmac_{p_g} \gets Hmac(DE_g,SK)$\Comment{Update $hmac_{p_g}$ for next check}\r
453         \State $qs_g \gets \Call{GetQueSta}{Dat_g}$\Comment{Handle qs}\r
454         \If{$qs_g \neq \emptyset \land qs_g > max_g$}\r
455                 \State $max_g \gets qs_g$\r
456         \EndIf\r
457     %Check for last s in Dat\r
458         \State $id_g \gets GetMacId(Dat_g)$\Comment{Handle last s}\r
459         \State $MS_g \gets \Call{UpdateLastSeqN}{id_g,s_g,MS_g}$\r
460     %Check for last s in DE in Dat\r
461     \State $\tuple{id_d,s_{d_{last}}} \gets \Call{GetSlotSeq}{Dat_g}$\Comment{Handle ss}\r
462         \If{$\tuple{id_d,s_{d_{last}}} \neq \emptyset$}\r
463         \State $MS_g \gets \Call{UpdateLastSeqN}{id_d,s_{d_{last}},MS_g}$\r
464         \EndIf\r
465         \State $\{\tuple{s_e,id_e},\tuple{s_f,id_f}\} \gets \r 466 \Call{GetColRes}{Dat_g}$\Comment{Handle cr}\r
467         \State $\Call{CheckCollision}{MS,SM,\tuple{s_e,id_e}}$\Comment{From normal slot}\r
468         \State $\Call{CheckCollision}{MS,SM,\tuple{s_f,id_f}}$\Comment{From reinsertion}\r
469         \State $sl_{last} \gets \Call{StoreLastSlot}{MS,sl_{last},s_g,sv_g,id_g}$\r
470         \State $DT \gets \Call{UpdateDT}{DT,Dat_g}$\r
471 \EndFor\r
472 \State $SM \gets SM_{curr}$\r
473 \If{$m + |SL_g| \leq max_g$}\Comment{Check actual size against $max_g$}\r
474         \State $m \gets m + |SL_g|$\r
475 \Else\r
476         \State \Call{ReportError}{'Actual queue size exceeds $max_g$'}\r
477 \EndIf\r
478 \State $\Call{CheckLastSeqN}{MS_g,MS}$\r
479 \EndProcedure\r
480 \end{algorithmic}\r
481 \r
482 \begin{algorithmic}\r
483 \Procedure{GetKVPairs}{}\r
484 \State $s_g \gets GetLastSeqN(MS,id_{self}) + 1$\r
485 \State $SL_c \gets \Call{GetSlot}{s_g}$\r
486 \State $\Call{ProcessSL}{SL_c}$\Comment{Process slots and update DT}\r
487 \EndProcedure\r
488 \end{algorithmic}\r
489 \r
490 \begin{algorithmic}\r
491 \Function{GetValFromKey}{$k_g$}\r
492 \State $\tuple{k_s,v_s} \gets \tuple{k,v}$ \textit{such that} $\tuple{k,v} \r 493 \in DT \land k = k_g$\r
494 \State \Return{$v_s$}\r
495 \EndFunction\r
496 \end{algorithmic}\r
497 \r
498 \subsubsection{Writing Slots}\r
499 \textbf{Data Entry} \\\r
500 $k$ is key of entry \\\r
501 $v$ is value of entry \\\r
502 $kv$ is a key-value entry $\tuple{k,v}$\\\r
503 $D = \{kv,ss,qs,cr\}$ \\\r
504 $DE = \{de \mid de \in D\}$ \\\r
505 $Dat_s = \tuple{s,id,hmac_p,DE,hmac_c}$ \\\r
506 $sv_s = \tuple{s, E(Dat_s)} = \r 507 \tuple{s, E(\tuple{s,id,hmac_p,DE,hmac_c})}$ \\ \\\r
508 \textbf{States} \\\r
509 \textit{$cp$ = data entry $DE$ maximum size/capacity} \\\r
510 \textit{$cr_p$ = saved cr entry $\tuple{s,id}$ on client if there is a collision\r
511 (sent in the following slot)} \\\r
512 \textit{$cr_{p_{last}}$ = saved cr entry $\tuple{s,id}$ on client if there is a \r
513 collision in reinserting the last slot (sent in the following slot)} \\\r
514 \textit{$ck_p$ = counter of $kv \in KV$ for putting pairs (initially 0)} \\\r
515 \textit{$ck_g$ = counter of $kv \in KV$ for getting pairs (initially 0)} \\\r
516 \textit{$hmac_{c_p}$ = the HMAC value of the current slot} \\\r
517 \textit{$hmac_{p_p}$ = the HMAC value of the previous slot \r
518 ($hmac_{p_p} = \emptyset$ for the first slot)} \\\r
519 \textit{$id_{self}$ = machine Id of this client} \\\r
520 \textit{$sl_{last}$ = info of last slot in queue = \r
521         $\tuple{s_{last},sv_{last},id_{last}}$ (initially $\emptyset$)} \\\r
522 \textit{$th_p$ = threshold number of dead slots for a resize to happen} \\\r
523 \textit{$m'_p$ = offset added to $max$ for resize} \\\r
524 \textit{$KV$ = set of $\tuple{ck, \tuple{k,v}}$ of kv entries on client} \\\r
525 \textit{$SL_p$ = set of returned slots on client} \\\r
526 \textit{SK = Secret Key} \\ \\\r
527 \textbf{Helper Functions} \\\r
528 $CreateDat(s,id,hmac_p,DE,hmac_c)=Dat_s=\tuple{s,id,hmac_p,DE,hmac_c}$ \\\r
529 $CreateCR(s,id)=\tuple{s,id}$ \\\r
530 $CreateQS(max')=qs$ \\\r
531 $CreateSS(id,s_{last})=\tuple{id,s_{last}}$ \\\r
532 $Encrypt(Dat_s,SK_s)=sv_s$ \\\r
533 $GetStatus(\tuple{status,SL})=status$ \\\r
534 $GetSL(\tuple{status,SL})=SL$ \\\r
535 $GetLastS(sl = \tuple{s,sv,id})=s$ \\\r
536 $GetSV(sl = \tuple{s,sv,id})=sv$ \\\r
537 $GetID(sl = \tuple{s,sv,id})=id$ \\\r
538 $GetColSeqN(SL_s,s_s)= \tuple{s, sv}$ \textit{such that} $\tuple{s, sv}\r 539 \in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s = s_s$ \\\r
540 $GetKV(KV_s,k_s)= \tuple{ck,\tuple{k, v}}$ \textit{such that} \r
541 $\tuple{ck,\tuple{k, v}} \in KV_s \wedge\r 542 \forall \tuple{ck_s,\tuple{k_s, v_s}} \in KV_s, k = k_s$ \\\r
543 \r
544 \begin{algorithmic}\r
545 \Function{PutKVPair}{$KV_s,\tuple{k_s,v_s}$}\r
546 \State $\tuple{ck_s,\tuple{k_s,v_t}} \gets GetKV(KV_s,k_s)$\r
547 \If{$\tuple{ck_s,\tuple{k_s,v_t}} = \emptyset$}\r
548         \State $KV_s \gets KV_s \cup \{\tuple{ck_p, \tuple{k_s,v_s}}\}$\r
549         \State $ck_p \gets ck_p + 1$\r
550 \Else\r
551         \State $KV_s \gets (KV_s - \{\tuple{ck_s, \tuple{k_s,v_t}}\}) \cup \r 552 \{\tuple{ck_s, \tuple{k_s,v_s}}\}$\r
553 \EndIf\r
554 \State \Return{$KV_s$}\r
555 \EndFunction\r
556 \end{algorithmic}\r
557 \r
558 \begin{algorithmic}\r
559 \Function{CheckResize}{$MS_s,th_s,max'_t,m'_s$}\r
560 \State $s_{last_{min}} \gets MinLastSeqN(MS_s)$\r
561 \State $s_{last_{max}} \gets MaxLastSeqN(MS_s)$\r
562 \State $n_{live} \gets s_{last_{max}} - s_{last_{min}}$\Comment{Number of live slots}\r
563 \State $n_{dead} \gets max'_t - n_{live}$\r
564 \If{$n_{dead} \leq th_s$}\r
565         \State $max'_s \gets max'_t + m'_s$\r
566 \Else\r
567         \State $max'_s \gets \emptyset$\r
568 \EndIf\r
569 \State \Return{$max'_s$}\r
570 \EndFunction\r
571 \end{algorithmic}\r
572 \r
573 \begin{algorithmic}\r
574 \Function{CheckNeedSS}{$MS_s,max'_t$}\Comment{Check if $ss$ is needed}\r
575 \State $s_{last_{min}} \gets MinLastSeqN(MS_s)$\r
576 \State $s_{last_{max}} \gets MaxLastSeqN(MS_s)$\r
577 \State $n_{live} \gets s_{last_{max}} - s_{last_{min}}$\Comment{Number of live slots}\r
578 \State $n_{dead} \gets max'_t - n_{live}$\r
579 \State \Return {$n_{dead} = 0$}\r
580 \EndFunction\r
581 \end{algorithmic}\r
582 \r
583 \begin{algorithmic}\r
584 \Function{HandleCollision}{$\tuple{stat_s,SL_s}$}\r
585 \State $stat_s \gets GetStatus(\tuple{stat_s,SL_s})$\r
586 \State $SL_s \gets GetSL(\tuple{stat_s,SL_s})$\r
587 \If{$\neg stat_s$}\Comment{Handle collision}\r
588         \State $\tuple{s_{col},sv_{col}} \gets GetColSeqN(SL_s,s_s)$\r
589         \State $s_{col} \gets SeqN(\tuple{s_{col},sv_{col}})$\r
590         \State $sv_{col} \gets SlotVal(\tuple{s_{col},sv_{col}})$\r
591         \State $Dat_{col} \gets Decrypt(SK,sv_{col})$\r
592         \State $id_{col} \gets GetMacId(Dat_{col})$\r
593         \State $\tuple{s_{col},id_{col}} \gets CreateCR(s_{col},id_{col})$\r
594         \State $cr_s \gets \tuple{s_{col},id_{col}}$\r
595 \Else\r
596         \State $cr_s \gets \emptyset$\r
597 \EndIf\r
598 \State $\Call{ProcessSL}{SL_s}$\r
599 \State \Return{$cr_s$}\r
600 \EndFunction\r
601 \end{algorithmic}\r
602 \r
603 \begin{algorithmic}\r
604 \Function{ReinsertLastSlot}{$need_s,sl_{s_{last}},max'_s$}\r
605 \If{$need_s$}\r
606         \State $s_s \gets GetLastS(sl_{s_{last}})$\r
607         \State $sv_s \gets GetSV(sl_{s_{last}})$\r
608         \State $\tuple{stat_s,SL_s} \gets \Call{PutSlot}{s_s,sv_s,max'_s}$\r
609         \State $cr_s \gets \Call{HandleCollision}{\tuple{stat_s,SL_s}}$\r
610 \EndIf\r
611 \State \Return{$cr_s$}\r
612 \EndFunction\r
613 \end{algorithmic}\r
614 \note{Shouldn't this function do something pretty sophisticated about seeing what data we actually need to keep from the last slot and not just insert the entire thing?}\r
615 \r
616 \note{Probably best to just not call this function is $need_s$ is false and not pass in such parameters.  It makes it harder to read.}\r
617 \r
618 \r
619 \begin{algorithmic}\r
620 \Function{GetDEPairs}{$KV_s,max'_s,need_s,sl_s$}\r
621 \State $DE_{ret} \gets \emptyset$\r
622 \State $cp_s \gets cp$\r
623 \If{$cr_p \neq \emptyset$}\Comment{Check and insert a $cr$}\r
624         \State $DE_{ret} \gets DE_{ret} \cup cr_p$\r
625         \State $cp_s \gets cp_s - 1$\r
626 \EndIf\r
627 \If{$cr_{p_{last}} \neq \emptyset$}\Comment{Check and insert a $cr$}\r
628         \State $DE_{ret} \gets DE_{ret} \cup cr_{p_{last}}$\r
629         \State $cp_s \gets cp_s - 1$\r
630 \EndIf\r
631 \If{$max'_s \neq \emptyset$}\Comment{Check and insert a $qs$}\r
632         \State $qs_s \gets max'_s$\r
633         \State $DE_{ret} \gets DE_{ret} \cup qs_s$\r
634         \State $cp_s \gets cp_s - 1$\r
635 \EndIf\r
636 \If{$need_s$}\Comment{Check and insert a $ss$}\r
637         \State $id_s \gets GetID(sl_s)$\r
638         \State $s_{s_{last}} \gets GetLastS(sl_s)$\r
639         \State $ss_s \gets CreateSS(id_s,s_{s_{last}})$\r
640         \State $DE_{ret} \gets DE_{ret} \cup ss_s$\r
641         \State $cp_s \gets cp_s - 1$\r
642 \EndIf\r
643 \If{$|KV_s| \leq cp$}\Comment{$KV$ set can extend multiple slots}\r
644         \State $DE_{ret} \gets DE_{ret} \cup\r 645 \{\tuple{k_s,v_s} \mid \tuple{ck_s,\tuple{k_s,v_s}} \in KV_s\}$\r
646 \Else\r
647         \State $DE_{ret} \gets DE_{ret} \cup\r 648 \{\tuple{k_s,v_s} \mid \tuple{ck_s,\tuple{k_s,v_s}} \in KV_s,\r 649 ck_g \leq ck_s < ck_g + cp_s\}$\r
650         \If{$|DE_{ret}| = cp$}\r
651                 \State $ck_g \gets ck_g + cp_s$\Comment{Middle of KV set}\r
652         \Else\r
653                 \State $ck_g \gets 0$\Comment{End of KV set}\r
654         \EndIf\r
655 \EndIf\r
656 \State \Return{$DE_{ret}$}\r
657 \EndFunction\r
658 \end{algorithmic}\r
659 \r
660 \begin{algorithmic}\r
661 \Procedure{PutDataEntries}{$th_p,m'_p$}\r
662 \State $s_p \gets MaxLastSeqN(MS)$\r
663 \State $max'_p \gets \Call{CheckResize}{MS,th_p,max'_g,m'_p}$\r
664 \State $need_p \gets \Call{CheckNeedSS}{MS,max'_g}$\r
665 \State $DE_p \gets \Call{GetDEPairs}{KV,max'_p,need_p,sl_{last}}$\r
666 \State $hmac_{c_p} \gets Hmac(DE_p,SK)$\r
667 \State $Dat_p \gets CreateDat(s_p,id_{self},hmac_{p_p},DE_p,hmac_{c_p})$\r
668 \State $hmac_{p_p} \gets hmac_{c_p}$\r
669 \State $sv_p \gets Encrypt(Dat_p,SK)$\r
670 \State $\tuple{stat_p,SL_p} \gets \Call{PutSlot}{s_p,sv_p,max'_p}$\r
671 \State $cr_p \gets \Call{HandleCollision}{\tuple{stat_p,SL_p}}$\r
672 \State $cr_{p_{last}} \gets \Call{ReinsertLastSlot}{need_p,sl_{last},max'_p}$\r
673 \EndProcedure\r
674 \end{algorithmic}\r
675 \r
676 \note{Lots of problems with PutDataEntries: (1) What happens if lose network connectivity after adding the key value pair, but before reinserting the last slot?  You probably need to create space first and then insert your data entry...  (2) What if reinsertlastslot kicks something else important out?  What if the server rejects our update because it is out of date?  At the very least, any putdataentries function w/o a loop is wrong!}\r
677 \r
678 \note{General comments...  Work on structuring things to improve\r
679   readability...  This include names of functions/variables, how\r
680   things are partitioned into functions, adding useful comments,...}\r
681 \r
682 \r
683 \subsection{Definitions for Formal Guarantees}\r
684 \r
685 \begin{enumerate}\r
686 \item Equality: Two messages $t$ and $u$ are equal if their sequence numbers, senders, and contents are exactly the same.\r
687 \item Message: A message $t$, is the tuple $t = (i(t), s(t), contents(t))$ containing the sequence number, machine ID of the sender, and contents of $t$ respectively.\r
688 \item Parent: A parent of a message $t$ is the message $A(t)$, unique by the correctness of HMACs, such that $HMAC_C(t) = HMAC_P(A(t))$.\r
689 \item Chain: A chain of messages with length $n \ge 1$ is a message sequence $(t_i, t_{i+1}, ..., t_{i+n-1})$ such that for every index $i < k \le i+n-1$, $t_k$ has sequence number $k$ and is the parent of $t_{k-1}$. Note that no two entries in a chain can have the same sequence number.\note{This definition is never used, instead you refer to paths..}\r
690 \item Partial message sequence: A partial message sequence is a sequence of messages, no two with the same sequence number, that can be divided into disjoint chains.\r
691 \item Total message sequence: A total message sequence $T$ with length $n$ is a chain of messages that starts at $i = 1$. The path of a message $t$ is the total message sequence whose last message is $t$.\r
692 \item Consistency: A partial message sequence $P$ is consistent with a total message sequence $T$ of length $n$ if for every message $p \in P$ with $i(p) < n$, $T_{i(p)} = p$. This implies that $\{p \in P | i(p) \le n\}$ is a subsequence of T.\r
693 \item Transitive closure set at index $i$: A set $\mathscr{S}$ of clients comprising a connected component of an undirected graph, where two clients are connected by an edge if they both received the same message $t$ with index $i(t) > i$.\note{Confusing to reuse i}\r
694 \r
695 \end{enumerate}\r
696 \r
697 \subsection{Formal Guarantee}\r
698 \r
699 \begin{prop} Every client $J$ who sends a message $t$ has $A(t)$ as its latest stored message, and $i(t) = i(A(t)) + 1$. \end{prop}\r
700 \begin{proof} True by definition, because $J$ sets $HMAC_P(t) = HMAC_C(A(t))$ and $i(t) = i(A(t)) + 1$ when a message is sent. \end{proof}\r
701 \r
702 \begin{prop} If a rejected message entry is added to the RML at index $i$, the message will remain in the RML until every client has seen it. \end{prop}\r
703 \begin{proof} Every RML entry $e$ remains in the queue until it reaches the tail, and is refreshed by the next sender $J$ at that time if $min(MS) > i(e)$; that is, until every client has sent a message with sequence number greater than $i(e)$. Because every client who sends a message with index $i$ has the state of the queue at $i - 1$, this client will have seen the message at $i(e)$. \end{proof}\r
704 \r
705 \begin{lem} If two packets $t$ and $u$, with $i(t) \le i(u)$, are received without errors by a client $C$, then $t$ is in the path of $u$. \note{path never defined}\end{lem}\r
706 \begin{proof}\r
707 Assume that $t$ is not in the path of $u$. Take $u$ to be the packet of smallest index for which this occurs, and $t$ be the packet with largest index for this $u$. We will prove that an error occurs upon receipt of $u$.\r
708 \r
709 Let $R_1$ be the earliest member of the path of $t$ that is not in the path of $u$, and $q$ be its parent. $q$, the last common ancestor of $t$ and $u$, must exist, since all clients and the server were initialized with the same state. Let $S_1$ be the successor of $q$ that is in the path of $u$; we know $S_1 \neq R_1$. Let $R = (R_1, R_2, \dots, R_m = t)$ be the distinct portion of the path of $t$, and similarly let $S$ be the distinct portion of the path of $S_n = u$.\r
710 \r
711 Let $J = s(R_1)$, and $K = s(S_1)$. Because no client can send two messages with the same index, and $i(R_1) = i(S_1) = i(q) + 1$, we know that $J \neq K$.\r
712 \r
713 There are two cases:\r
714 \r
715 \begin{itemize}\r
716 \item Case 1: $J$ did not send a message in $S$. Then $v_J(t) > v_J(q) = v_J(u)$. $C$ will throw an error, because the latest index of $J$ changes in the opposite direction of the sequence number: $v_J(u) < v_J(t)$ but $i(u) > i(t)$.\note{Need more contet as to why C would throw an error...You are assuming that it reads two disjoint windows...one with u and the other with t...other case is that they are contiguous, in which case the hashes can't match...}\r
717 \item Case 2: $J$ sent at least one message in $S$. Call the first one $p$. We know that $i(p) > i(S_1)$, since $J \neq K$. $R_1$ must be sent either before or after $p$.\r
718 \begin{itemize}\r
719 \item Case 2.1: Client $J$ sends $p$, and then $R_1$. When $p$ was sent, whether it was accepted or rejected, $i(J, p) \geq i(p)$. Since $i(p) > i(S_1)$, $i(J, p) > q$. So $i(q) < i(J, p)$, which would cause $J$ to fail to send $R_1$, a contradiction.\note{Never defined i(J,p).  don't you mean i(q)+1 instead of q?}\r
720 \item Case 2.2: Client $J$ sends $R_1$, and then $p$. Let $X = (R_1, \dots )$ be the list of messages $J$ sends starting before $R_1$ and ending before $p$.\r
721 \begin{itemize}\r
722 \item Case 2.2.1: Some message in $X$ was accepted. In this case, before sending $p$, $J$'s value for its own latest index would be strictly greater than $v_J(q)$. ($J$ could not have sent a message with index less than $i(q)$ after receiving $q$). When preparing to send $p$, $J$ would have received its own latest index as at most $v_J(q)$. $J$ throws an error before sending $p$, because its own latest index decreases.\r
723 \item Case 2.2.2: All messages in $X$ were rejected. Client $J$ will always add the latest rejected message to the rejected-message list in the next update; so for every $i$, $1 \leq i < |X|$, the $i$th element of $X$ will be recorded in the RML of all further elements of $X$; and every element of $X$ will be recorded in $RML(p)$. Since every rejected message in $RML(p)$ will be in $RML(C, u)$, and $u$ is the first message that $C$ sees which does not have $t$ in its path, $R_1$ will be recorded in $RML(C, p)$. When $C$ receives $u$, $C$ will throw an error from the match $(J, iq+1)$ in $RML(C, p)$.\note{Missing case...what if C switches branches before J? It will see a version rollback...Also need more context...disjoint reads...etc...}\r
724 \end{itemize}\r
725 \end{itemize}\r
726 \end{itemize}\r
727 \end{proof}\r
728 \r
729 \begin{theorem}\r
730 Suppose that there is a transitive closure set $\mathscr{S}$ of clients, at index $n$. Then there is some total message sequence $T$ of length $n$ such that every client $C$ in $\mathscr{S}$ sees a partial sequence $P_C$ consistent with $T$. \end{theorem}\r
731 \r
732 \begin{proof}\r
733 The definition of consistency of $P_C$ with $T$ is that every message $p \in P_C$ with index $i(p) \le n$ is equal to the message in that slot in $T$. Let $C_1$ be some client in the transitive closure set, with partial message sequence $P_{C_1}$, and let $u$ be some message with $i(u) > i$ that $C_1$ shares with another client. Then let $T$ be the portion of the path of $u$ ending at index $i$ and $t$ be the message at that index. Clearly, by Lemma 1, $P_{C_1}$ is consistent with $T$, and furthermore. \note{typo in previous sentence?} We will show that, for every other client $D$ with partial sequence $P_D$, $P_D$ has some message whose path includes $t$. Because $D$ is in the transitive closure, there is a sequence of edges from $C_1$ to $D$. Call this $\mathscr{C} = (C_1, C_2, ..., D)$. I will prove by induction that $D$ has a message whose path includes $t$.\r
734 \r
735 For the base case, $P_{C_1}$ includes $u$, whose path includes $t$. For the inductive step, suppose $P_{C_k}$ has an message $w$ with a path that includes $t$, and shares message $x$ with $P_{C_{k+1}}$ such that $i(x) > i$. If $i(w) = i(x)$, then $w = x$. If $i(w) < i(x)$, then, by Lemma 1, $w$ is in the path of $x$. If $i(w) > i(x)$, $x$ is in the path of $w$; note again that its index is greater than $i$. In any case, $t$ is in the path of $u_k+1$.\r
736 \r
737 Let $w$ the message of $D$ whose path includes $t$. By Lemma 1, every message in $P_D$ with index smaller than $i(w)$ is in the path of $w$. Since $t$ is in the path of $w$, every message in $P_D$ with smaller index than $i(t)$ is in $T$. Therefore, $P_D$ is consistent with $T$.\r
738 \end{proof}\r
739 \r
740 \note{General comments...some diagrams could help...theorem 1 is pretty hard to follow...}\r
741 \r
742 \subsection{Future Work}\r
743 \paragraph{Support Messages}\r
744   A message is dead once receiving machine sends an entry with a newer\r
745   sequence identifier\r
746 \r
747 \paragraph{Persistent data structures}\r
748         Root object w/ fields\r
749         Other objects can be reachable from root\r
750         Each object has its own entries\r
751         Dead objects correspond to dead \r
752 \r
753 \paragraph{Multiple App Sharing}\r
754 \r
755 Idea is to separate subspace of entries...  Shared with other cloud...\r
756 \end{document}\r
757 \r