X-Git-Url: http://plrg.eecs.uci.edu/git/?p=iotcloud.git;a=blobdiff_plain;f=doc%2Fiotcloud.tex;h=4d0c9f491dbc12085ed551a060fe60188663992b;hp=b85fc026001afb8b9d70b2254acc0547a33e5d6c;hb=f498aec54ac8672e6b7c5d813f6487b4a57ed5a6;hpb=fd4dfb7fb1099d8617c86398c5ca349e5e583643 diff --git a/doc/iotcloud.tex b/doc/iotcloud.tex index b85fc02..4d0c9f4 100644 --- a/doc/iotcloud.tex +++ b/doc/iotcloud.tex @@ -200,6 +200,7 @@ $Dat_s = \tuple{s,id,hmac_p,DE,hmac_c}$ \\ $slot_s = \tuple{s, E(Dat_s)} = \tuple{s, E(\tuple{s,id,hmac_p,DE,hmac_c})}$ \\ \\ \textbf{States} \\ +\textit{$d$ = delta between the last $s$ recorded and the first $s$ received} \\ \textit{$id_{self}$ = machine Id of this client} \\ \textit{$max_g$ = maximum number of slots (initially $max_g > 0$)} \\ \textit{m = number of slots stored on client (initially $m = 0$)} \\ @@ -258,6 +259,8 @@ $MinLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s \wedge \forall \tuple{id_s, s_{s_{last}}} \in MS_s, s_{last} \leq s_{s_{last}}$ \\ $MinCRSeqN(CR_s)= s$ \textit{such that} $\tuple{s, id} \in CR_s \wedge \forall \tuple{s_s, id_s} \in CR_s, s \leq s_s$ \\ +$MaxSMSeqN(SM_s)= s$ \textit{such that} $\tuple{s, id} \in SM_s + \wedge \forall \tuple{s_s, id_s} \in SM_s, s \geq s_s$ \\ \begin{algorithmic}[1] \Procedure{Error}{$msg$} @@ -266,27 +269,10 @@ $MinCRSeqN(CR_s)= s$ \textit{such that} $\tuple{s, id} \in CR_s \EndProcedure \end{algorithmic} -\begin{algorithmic}[1] -\Function{ValidHmac}{$DE_s,SK_s,hmac_{stored}$} -\State $hmac_{computed} \gets Hmac(DE_s,SK_s)$ -\State \Return {$hmac_{stored} = hmac_{computed}$} -\EndFunction -\end{algorithmic} - -\begin{algorithmic}[1] -\Function{ValidPrevHmac}{$s_s,DE_s,hmac_{p_s},hmac_{p_{sto}}$} -\If{$s_s = 0 \land hmac_{p_s} = \emptyset$}\Comment{First slot - no previous HMAC} - \State \Return $true$ -\Else - \State \Return {$hmac_{p_{sto}} = hmac_{p_s}$} -\EndIf -\EndFunction -\end{algorithmic} - \begin{algorithmic}[1] \Function{GetQueSta}{$DE_s$} -\State $de_{qs} \gets de_s$ \textit{such that} $de_s \in DE_s, - de_s \in D \land de_s = qs$ +\State $de_{qs} \gets ss$ \textit{such that} $ss \in DE_s, + de_s \in D \land type(de_s) = "qs"$ \If{$de_{qs} \neq \emptyset$} \State $qs_{ret} \gets GetQS(de_{qs})$ \Else @@ -298,14 +284,14 @@ $MinCRSeqN(CR_s)= s$ \textit{such that} $\tuple{s, id} \in CR_s \begin{algorithmic}[1] \Function{GetSlotSeq}{$DE_s$} -\State $DE_{ss} \gets \{de_s | de_s \in DE_s, de_s = ss\}$ +\State $DE_{ss} \gets \{de | de \in DE_s \land type(de) = "ss"\}$ \State \Return{$DE_{ss}$} \EndFunction \end{algorithmic} \begin{algorithmic}[1] \Function{GetColRes}{$DE_s$} -\State $DE_{cr} \gets \{de_s | de_s \in DE_s, de_s = cr\}$ +\State $DE_{cr} \gets \{de | de \in DE_s \land type(de) = "cr"\}$ \State \Return{$DE_{cr}$} \EndFunction \end{algorithmic} @@ -394,13 +380,13 @@ $MinCRSeqN(CR_s)= s$ \textit{such that} $\tuple{s, id} \in CR_s \end{algorithmic} \begin{algorithmic}[1] -\Procedure{CheckLastSeqN}{$MS_s,MS_t$} +\Procedure{CheckLastSeqN}{$MS_s,MS_t,d$} \For {$\tuple{id, s_t}$ in $MS_t$}\Comment{Check $MS_t$ based on the newer $MS_s$} \State $s_s \gets MS_s[id]$ - \If{$s_s = \emptyset$} - \Call{Error}{'No $s$ for machine $id$'} + \If{$d \land s_s = \emptyset$} + \State \Call{Error}{'Missing $s$ for machine $id$'} \ElsIf{$id = id_{self}$ and $s_s \neq s_t$} - \State \Call{Error}{'Invalid last $s$ for this machine'} + \State \Call{Error}{'Invalid last $s$ for this machine'} \ElsIf{$id \neq id_{self}$ and $s_{s_{last}} < s_{t_{last}}$} \State \Call{Error}{'Invalid last $s$ for machine $id$'} \Else @@ -427,22 +413,25 @@ $MinCRSeqN(CR_s)= s$ \textit{such that} $\tuple{s, id} \in CR_s \end{algorithmic} \begin{algorithmic}[1] -\Procedure{CheckSlotsRange}{$|SL_s|,s_{s_{min}},s_{s_{max}}$} +\Function{ValidSlotsRange}{$|SL_s|,s_{s_{min}},s_{s_{max}}$} \State $sz_{SL} \gets s_{s_{max}} - s_{s_{min}} + 1$ \If{$sz_{SL} \neq |SL_s|$} - \State \Call{Error}{'Sequence numbers range does not match slots set'} -\EndIf -\State $s_{min} \gets MinLastSeqN(MS)$ -\State $s_{max} \gets MaxLastSeqN(MS)$ -\If{$s_{s_{min}} \leq s_{min}$} - \State \Call{Error}{'Server sent old slot'} + \State \Call{Error}{'Sequence numbers range does not match actual set'} \EndIf -\If{$s_{s_{max}} > s_{max}$} - \State \Call{Error}{'Server sent out-of-range slot'} +\State $s_{s_{last}} \gets MaxSMSeqN(SM)$ +\If{$s_{s_{min}} \leq s_{s_{last}}$} + \State \Call{Error}{'Server sent old slots'} \EndIf -\State $s_{self} \gets MS_s[id_{self}]$ -\State $sz_{expected} \gets s_{max} - s_{self} + 1$ -\If{$sz_{SL} \neq sz_{expected}$} +\State \Return{$s_{s_{min}} > s_{s_{last}} + 1$} +\EndFunction +\end{algorithmic} + +\begin{algorithmic}[1] +\Procedure{CheckSlotsRange}{$|SL_s|$} +\State $s_{s_{max}} \gets MaxLastSeqN(MS)$ +\State $s_{self} \gets MS[id_{self}]$ +\State $sz_{expected} \gets s_{s_{max}} - s_{self} + 1$ +\If{$|SL_s| \neq sz_{expected}$} \State \Call{Error}{'Actual number of slots does not match expected'} \EndIf \EndProcedure @@ -460,7 +449,7 @@ $MinCRSeqN(CR_s)= s$ \textit{such that} $\tuple{s, id} \in CR_s \begin{algorithmic}[1] \Function{UpdateDT}{$DT_s,DE_s,LV_s,s_s$} -\State $DE_{s_{kv}} \gets \{de_s | de_s \in DE_s, de_s = kv\}$ +\State $DE_{s_{kv}} \gets \{de_s | de_s \in DE_s, type(de_s) = "kv"\}$ \ForAll{$de_s \in DE_s$} \State $kv_s \gets GetKV(de_s)$ \State $LV_s \gets \Call{UpdateKVLivEnt}{LV_s,kv_s,s_s}$ @@ -482,6 +471,7 @@ $MinCRSeqN(CR_s)= s$ \textit{such that} $\tuple{s, id} \in CR_s \State $MS_g \gets \emptyset$ \State $\tuple{s_{g_{min}},sv_{g_{min}}} \gets MinSlot(SL_g)$ \State $\tuple{s_{g_{max}},sv_{g_{max}}} \gets MaxSlot(SL_g)$ +\State $d \gets \Call{ValidSlotsRange}{|SL_g|,s_{g_{min}},s_{g_{max}}}$ \For{$s_g \gets s_{g_{min}}$ \textbf{to} $s_{g_{max}}$}\Comment{Process slots in $SL_g$ in order} \State $\tuple{s_g,sv_g} \gets Slot(SL_g,s_g)$ @@ -494,11 +484,10 @@ $MinCRSeqN(CR_s)= s$ \textit{such that} $\tuple{s, id} \in CR_s \EndIf \State $DE_g \gets GetDatEnt(Dat_g)$ \State $hmac_{p_{stored}} \gets GetPrevHmac(Dat_g)$ - \If{$\neg \Call{ValidPrevHmac}{s_g,DE_g,hmac_{p_g},hmac_{p_{stored}}}$} + \If {$ \neg(s_g = 0 \land hmac_{p_g} = 0) \land hmac_{p_{stored}} \neq hmac_{p_g}$} \State \Call{Error}{'Invalid previous HMAC value'} \EndIf - \State $hmac_{c_g} \gets GetCurrHmac(Dat_g)$ - \If{$\neg \Call{ValidHmac}{DE_g,SK,hmac_{c_g}}$} + \If{$\Call{Hmac}{DE_g,SK} \neq GetCurrHmac(Dat_g)$ } \State \Call{Error}{'Invalid current HMAC value'} \EndIf \State $hmac_{p_g} \gets Hmac(DE_g,SK)$\Comment{Update $hmac_{p_g}$ for next check} @@ -534,8 +523,8 @@ $MinCRSeqN(CR_s)= s$ \textit{such that} $\tuple{s, id} \in CR_s \Else \State \Call{Error}{'Actual $SL$ size on server exceeds $max_g$'} \EndIf -\State $\Call{CheckSlotsRange}{SL_g,s_{g_{min}},s_{g_{max}}}$ -\State $\Call{CheckLastSeqN}{MS_g,MS}$ +\State $\Call{CheckLastSeqN}{MS_g,MS,d}$ +\State $\Call{CheckSlotsRange}{|SL_g|}$ \State $\Call{UpdateSSLivEnt}{SS_{live},MS}$ \State $\Call{UpdateCRLivEnt}{CR_{live},MS}$ \State $\Call{UpdateSM}{SM,CR_{live}}$ @@ -551,7 +540,7 @@ $MinCRSeqN(CR_s)= s$ \textit{such that} $\tuple{s, id} \in CR_s \end{algorithmic} \begin{algorithmic}[1] -\Function{GetValFromKey}{$k_g$} +\Function{Get}{$k_g$} \Comment{Interface function to get a value} \State $\tuple{k_s,v_s} \gets \tuple{k,v}$ \textit{such that} $\tuple{k,v} \in DT \land k = k_g$ \State \Return{$v_s$} @@ -597,8 +586,8 @@ $\tuple{ck,\tuple{k, v}} \in KV_s \wedge \forall \tuple{ck_s,\tuple{k_s, v_s}} \in KV_s, k = k_s$ \\ \begin{algorithmic}[1] -\Function{PutKVPair}{$KV_s,\tuple{k_s,v_s}$} -\State $\tuple{ck_s,\tuple{k_s,v_t}} \gets GetKVPair(KV,k_s)$ +\Function{Put}{$KV_s,\tuple{k_s,v_s}$} \Comment{Interface function to update a key-value pair} +\State $\tuple{ck_s,\tuple{k_s,v_t}} \gets GetKVPair(KV_s,k_s)$ \If{$\tuple{ck_s,\tuple{k_s,v_t}} = \emptyset$} \State $KV_s \gets KV_s \cup \{\tuple{ck_p, \tuple{k_s,v_s}}\}$ \State $ck_p \gets ck_p + 1$ @@ -876,9 +865,9 @@ and $\mathsf{Dat_t}$ are exactly the same. \end{defn} \begin{defn}[Parent] -A parent of a message $\mathsf{t}$ is the message $\mathsf{\mathscr{P}_t}$, +A parent of a message $\mathsf{t}$ is the message $\mathsf{p_t}$, unique by the correctness of HMACs in $\mathsf{Dat_t}$, such that -$\mathsf{hmac_p(t) = hmac_c(\mathscr{P}_t)}$. +$\mathsf{hmac_p(t) = hmac_c(p_t)}$. \end{defn} \begin{defn}[Chain] @@ -915,25 +904,26 @@ $\mathsf{\{p \in P | s_p \le n\}}$ is a partial sequence of $\mathsf{T}$. Transitive closure set at sequence number $\mathsf{s_n}$ is a set $\mathsf{\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 $\mathsf{t}$ with sequence number $\mathsf{s_t < s_n}$. -%TODO: Check with Thomas whether this is $\mathsf{s_t > s_n}$ or it should be -%$\mathsf{s_t < s_n}$ +received the same message $\mathsf{t}$ with sequence number $\mathsf{s_t > s_n}$. \end{defn} \subsubsection{Lemmas and Proofs} -\begin{prop} +\begin{prop} +\label{prop:parentmessage} Every client $\mathsf{J}$ who sends a message $\mathsf{t}$ -has $\mathsf{\mathscr{P}_t}$ as its latest stored message, and -$\mathsf{s_t = s_{\mathscr{P}_t} + 1}$. +has parent $\mathsf{p_t}$ as its latest stored message, and +$\mathsf{s_t = s_{p_t} + 1}$. \end{prop} \begin{proof} True by definition, because $J$ sets -$\mathsf{hmac_p(t) = hmac_c(\mathscr{P}_t)}$ and -$\mathsf{s_t = }$ $\mathsf{s_{\mathscr{P}_t + 1}}$ when a message +$\mathsf{hmac_p(t) = hmac_c(p_t)}$ and +$\mathsf{s_t = }$ $\mathsf{s_{p_t + 1}}$ when a message is sent. \end{proof} -\begin{prop} If a rejected message entry is added to the set $\mathsf{CR}$ +\begin{prop} +\label{prop:rejectedmessage} +If a rejected message entry is added to the set $\mathsf{CR}$ at sequence number $\mathsf{s}$, the message will remain in $\mathsf{CR}$ until every client has seen it. \end{prop} @@ -948,7 +938,7 @@ $\mathsf{s - 1}$, this client will have seen the message at $\mathsf{s_{cr}}$. \begin{figure}[h] \centering \xymatrix{ & & L \\ -\dots \ar[r] & q \ar[dr]_{J} \ar[r]^{K} & l_1 \ar[r] & l_2 \ar[r] & \dots \ar[r] & p \ar[r] & \dots \ar[r] & l_n = u \\ +\dots \ar[r] & q \ar[dr]_{J} \ar[r]^{K} & l_1 \ar[r] & l_2 \ar[r] & \dots \ar[r] & m \ar[r] & \dots \ar[r] & l_n = u \\ & & r_1 \ar[r] & r_2 \ar[r] & \dots \ar[r] & r_m = t \\ & & R \save "2,3"."2,8"*+\frm{^\}} @@ -956,136 +946,146 @@ $\mathsf{s - 1}$, this client will have seen the message at $\mathsf{s_{cr}}$. \restore \restore } -\caption{By Lemma 1, receiving $t$ after $u$ is impossible.} +\caption{By \textbf{Lemma \ref{lem:twomessages}}, receiving both $t$ and $u$ here is impossible.} \end{figure} -\begin{lem} Two messages are received without errors by a client $\mathsf{C}$; +\begin{lem} +\label{lem:twomessages} +Two messages are received without errors by a client $\mathsf{C}$; call them $\mathsf{t}$ and $\mathsf{u}$ such that $\mathsf{s_t \le s_u}$. Then $\mathsf{t}$ is in the path of $\mathsf{u}$. \end{lem} \begin{proof} +Assume that there are some pairs of messages $\mathsf{(t,u)}$ that violate this lemma. +Take a specific $\mathsf{(t,u)}$ such that $\mathsf{s_u}$ is minimized, and +$\mathsf{s_t}$ is maximized for this choice of $\mathsf{s_u}$. We will show that $\mathsf{C}$ +cannot receive both $\mathsf{t}$ and $\mathsf{u}$ without throwing an error. + Clearly $\mathsf{C}$ will throw an error if $\mathsf{s_t = s_u}$. So $\mathsf{s_t < s_u}$. Additionally, if $\mathsf{C}$ receives $\mathsf{u}$ before $\mathsf{t}$, this will cause it to throw an error, so $\mathsf{t}$ is received -before $\mathsf{u}$. - -Assume that $\mathsf{t}$ is not in the path of $\mathsf{u}$. Take $\mathsf{u}$ -to be the packet of smallest sequence number for which this occurs, and -$\mathsf{t}$ be the packet with greatest sequence number for this $\mathsf{u}$. -We will prove that an error occurs upon receipt of $\mathsf{u}$. +before $\mathsf{u}$. We will prove that an error occurs upon receipt of $\mathsf{u}$. Let $\mathsf{r_1}$ be the earliest member of the path of $\mathsf{t}$ that is not in the path of $\mathsf{u}$, and $\mathsf{q}$ be its parent. Message $\mathsf{q}$, the last common ancestor of $\mathsf{t}$ and $\mathsf{u}$, must exist, since all clients and the server were initialized with the same state. Let $\mathsf{l_1}$ be the successor of $\mathsf{q}$ that is in the path of $\mathsf{u}$; -we know $\mathsf{l_1 \neq r_1}$. Let $\mathsf{R = (r_1, r_2, \dots, r_m = t)}$ be +we know $\mathsf{l_1 \neq r_1}$. Let $\mathsf{R = (r_1, r_2, \dots, r_{|R|} = t)}$ be the distinct portion of the path of $\mathsf{t}$, and similarly let $\mathsf{L}$ -be the distinct portion of the path of $\mathsf{l_n = u}$. +be the distinct portion of the path of $\mathsf{l_{|L|} = u}$. Let $\mathsf{J}$ be the client who sent $\mathsf{r_1}$; that is, such that $\mathsf{{id_{self}}_J = GetMacID(r_1)}$, and $\mathsf{K}$ be the client who -sent $\mathsf{l_1}$. - -We know the following three facts: +sent $\mathsf{l_1}$. Because no client can send two messages with the same sequence number, and +$\mathsf{s_{r_1} = s_{l_1} = s_q + 1}$, $\mathsf{J \neq K}$. -\begin{enumerate} +We also know the following facts: -\item Because no client can send two messages with the same sequence number, and -$\mathsf{s_{r_1} = s_{l_1} = s_q + 1}$, $\mathsf{J \neq K}$. +\begin{prop} +\label{prop:bothmessages} +No client sends both a message in $\mathsf{(r_2,...,t)}$ and a message in $\mathsf{(l_2,...,u)}$. +\end{prop} -\item To send a message $\mathsf{p}$ that is the parent of some other +\begin{proof} +To send a message $\mathsf{p}$ that is the parent of some other message, one must have received the parent of $\mathsf{p}$. Since $\mathsf{u}$ is the message with smallest sequence number received by any -client that violates this lemma, no client receives both a message in $\mathsf{r}$ -and a message in $\mathsf{l}$; therefore, no client sends both a message in -$\mathsf{(r_2,...,t)}$ and a message in $\mathsf{(l_2,...,u)}$. +client that violates Lemma \ref{lem:twomessages}, no client receives both a message +in $\mathsf{r}$ and a message in $\mathsf{l}$. +\end{proof} -\item Since $\mathsf{u}$ is the message with the greatest- and least- sequence -number that violates this lemma, $\mathsf{C}$ does not receive any message with -sequence number strictly between $\mathsf{s_t}$ and $\mathsf{s_u}$. Because the -$\mathsf{s_{last}}$ that $\mathsf{C}$ stores increases at every message receipt -event, $\mathsf{C}$ also does not receive any message after $\mathsf{t}$ and before -$\mathsf{u}$ in real time. +\begin{prop} +\label{prop:seqnumb} +$\mathsf{C}$ does not receive any message with a +sequence number strictly between $\mathsf{s_t}$ and $\mathsf{s_u}$. +\end{prop} + +\begin{proof} If there were such a message with sequence number smaller than +$\mathsf{s_u}$, it would contradict the assumption that $\mathsf{u}$ is the +message with the least sequence number that violates Lemma \ref{lem:twomessages}. +\end{proof} -\end{enumerate} There are two cases: \begin{itemize} -\item Case 1: $\mathsf{J}$ did not send a message in $\mathsf{L}$. Then -%$\mathsf{v_J(t) > v_J(q) = v_J(u)}$. -$\mathsf{s_{t_J} > s_{q_J} = s_{u_J}}$. +\item Case 1: $\mathsf{J}$ did not send a message in $\mathsf{L}$. Then, where $\mathsf{s_{t_J}}$ +is the greatest sequence number of the messages that client $\mathsf{J}$ sent in +the path of message $\mathsf{t}$, $\mathsf{s_{t_J} > s_{q_J} = s_{u_J}}$. \begin{itemize} \item Case 1.1: $\mathsf{C}$ never updates its slot sequence list $\mathsf{SS}$ between receiving $\mathsf{t}$ and receiving $\mathsf{u}$; this can only happen if $\mathsf{s_t = s_u - 1}$. Since $\mathsf{t}$ is not the parent of $\mathsf{u}$, -$\mathsf{hmac_p(u) \neq hmac_c(t)}$, causing $\mathsf{C}$ to error. +$\mathsf{hmac_p(u) \neq hmac_c(t)}$, causing $\mathsf{C}$ to throw an error. \item Case 1.2: Case 1.1 does not occur; therefore, $\mathsf{C}$ must update its slot sequence list $\mathsf{SS}$ at some point between receiving $\mathsf{t}$ and $\mathsf{u}$. The latest sequence number of $\mathsf{J}$ decreases during this time, which means it must decrease when some message is received, which means $\mathsf{C}$ -throws an error in the $\mathsf{CheckLastSeqN}$ subroutine. +throws an error in the $\mathsf{CheckLastSeqN()}$ subroutine. \end{itemize} \item Case 2: $\mathsf{J}$ sent at least one message in $\mathsf{L}$. Call the -first one $\mathsf{p}$. We know that $\mathsf{s_p > s_{r_1}}$, since -$\mathsf{J \neq K}$ and $\mathsf{p \neq l_1}$. Message $\mathsf{r_1}$ must be sent -either before or after $\mathsf{p}$. +first one $\mathsf{m}$. We know that $\mathsf{s_m > s_{r_1}}$, since +$\mathsf{J \neq K}$ and $\mathsf{m \neq l_1}$. Message $\mathsf{r_1}$ must be sent +either before or after $\mathsf{m}$. \begin{itemize} -\item Case 2.1: Client $\mathsf{J}$ sends $\mathsf{p}$, and then $\mathsf{r_1}$. -Before sending $\mathsf{p}$, the greatest sequence number of a message that +\item Case 2.1: Client $\mathsf{J}$ sends $\mathsf{m}$, and then $\mathsf{r_1}$. +Before sending $\mathsf{m}$, the greatest sequence number of a message that $\mathsf{J}$ has received, $\mathsf{{s_{last}}_J}$, must be equal to -$\mathsf{s_p - 1 \ge s_{r_1}}$. Since $\mathsf{{s_{last}}_J}$ never decreases, +$\mathsf{s_m - 1 \ge s_{r_1}}$. Since $\mathsf{{s_{last}}_J}$ never decreases, client $\mathsf{J}$ cannot then send a message with sequence number $\mathsf{s_{r_1}}$, a contradiction. -\item Case 2.2: Client $\mathsf{J}$ sends $\mathsf{r_1}$, and then $\mathsf{p}$. -Let $\mathsf{X = (r_1, \dots )}$ be the list of messages $\mathsf{J}$ sends -starting before $\mathsf{r_1}$ and ending before $p$. +\item Case 2.2: Client $\mathsf{J}$ sends $\mathsf{r_1}$, and then $\mathsf{m}$. +Let $\mathsf{X = (r_1 = x_1, \dots , x_n)}$ be the list of messages $\mathsf{J}$ sends +starting before $\mathsf{r_1}$ and ending before $m$; clearly these all have sequence +number $\mathsf{s_p = s_q + 1}$. \begin{itemize} -\item Case 2.2.1: Some message in $\mathsf{X}$ was accepted. Let $\mathsf{s_{w_J}}$ -be the greatest sequence number of the messages that client $\mathsf{J}$ sent in -the path of message $\mathsf{w}$. In this case, before sending $\mathsf{p}$, +\item Case 2.2.1: Some message in $\mathsf{X}$ was accepted. Before sending $\mathsf{m}$, $\mathsf{J}$'s value in $\mathsf{MS_J}$ for its own latest sequence number would be strictly greater than $\mathsf{s_{q_J}}$. If there is a sequence of messages with contiguous sequence numbers that $\mathsf{J}$ receives between $\mathsf{r_1}$ and -$\mathsf{p}$, $\mathsf{J}$ throws an error for a similar reason as Case 1.1. Otherwise, -when preparing to send $\mathsf{p}$, $\mathsf{J}$ would have received an update of its +$\mathsf{m}$, $\mathsf{J}$ throws an error for a similar reason as Case 1.1. Otherwise, +when preparing to send $\mathsf{m}$, $\mathsf{J}$ would have received an update of its own latest sequence number as at most $\mathsf{s_{q_J}}$. $J$ throws an error before sending $\mathsf{p}$, because its own latest sequence number decreases. -\item Case 2.2.2: All messages in $\mathsf{X}$ were rejected, making $\mathsf{p}$ -the first message of $\mathsf{J}$ that is accepted after $\mathsf{r_1}$. Note that -$\mathsf{u}$ is the message with least sequence number that violates this lemma, and -therefore the first one that $\mathsf{C}$ receives after $\mathsf{t}$. Therefore, +\item Case 2.2.2: All messages in $\mathsf{X}$ were rejected, making $\mathsf{m}$ +the first message of $\mathsf{J}$ that is accepted after $\mathsf{r_1}$. + +We will show that $\mathsf{C}$ sees $\mathsf{r_1}$. Assume not. Then $\mathsf{(r_2, ..., u)}$ +must have at least $\mathsf{{max_g}_C} \geq 2$ messages for $\mathsf{r_1}$ to fall off the +end of the queue. Consider the sender of $\mathsf{r_3}$ and call it $\mathsf{H}$. +$\mathsf{H \neq J}$ by Proposition \ref{prop:bothmessages} and the existence of $\mathsf{m}$. +Since $\mathsf{H \neq J}$, then by Proposition \ref{prop:bothmessages} it could not also +have sent a message in $\mathsf{(l_2,..., u)}$. Therefore, $\mathsf{s_{u_H} < s_q + 2 = s_{t_H}}$, +so upon receipt of $\mathsf{u}$, $\mathsf{C}$ will throw an error by the decrease in a +last sequence number similar to Case 1, a contradiction. + +Now that we know that $\mathsf{C}$ sees $\mathsf{r_1}$, note that C receives $\mathsf{u}$ +immediately after $\mathsf{t}$ by Proposition \ref{prop:seqnumb}. Therefore, $\mathsf{C}$ could not have seen a message after $\mathsf{t}$ with sequence number less -than $\mathsf{s_p}$. In the $\mathsf{PutDataEntries}$ subroutine, $\mathsf{J}$ adds every -%TODO: Check with Thomas about this part -%rejected message to $\mathsf{CR(p)}$; so for every $\mathsf{s}$, $\mathsf{1 \leq s < |X|}$, -%the $\mathsf{s}$-th element of $\mathsf{X}$ will be recorded in the rejected message list -%$\mathsf{CR}$ of all further elements of $\mathsf{X}$; and every element of -%$\mathsf{X}$ will be recorded in $\mathsf{CR_C(p)}$. Since every rejected message in -%$\mathsf{CR(p)}$ will be in $\mathsf{CR_C(u)}$, ${r_1}$ will be recorded in -%$\mathsf{CR_C(p)}$. When $\mathsf{C}$ receives $\mathsf{u}$, $\mathsf{C}$ will throw -%an error from the match $\mathsf{\tuple{s_q+1, id_J}}$ in $\mathsf{CR_C(p)}$. +than $\mathsf{s_m}$. In the $\mathsf{PutDataEntries()}$ subroutine, $\mathsf{J}$ adds every $\mathsf{cr}$ entry that contains sequence number $\mathsf{s}$ and machine ID -$\mathsf{id}$ of the messsages that win in the collisions before $\mathsf{p}$ into +$\mathsf{id}$ of the messsages that win in the collisions before $\mathsf{m}$ into $\mathsf{CR}$; $\mathsf{CR}$ keeps the collection of live $\mathsf{cr}$ entries, namely -those which not all clients have seen. Hence, for every $\mathsf{s}$, $\mathsf{1 \leq s < |X|}$, -the collision winner that has collided with $\mathsf{s}$-th element of $\mathsf{X}$ -will be recorded appropriately. Since all the $\mathsf{cr}$ entries that record -the results of the collisions before $\mathsf{p}$ will also be seen when $\mathsf{u}$ -is received, ${l_1}$ will be recorded in a $\mathsf{cr}$ entry as the winner in the -collision against ${r_1}$. When $\mathsf{C}$ receives $\mathsf{u}$, if $\mathsf{C}$ -has seen the $\mathsf{cr}$ entry that records the collision, it will already throw +those which not all clients have seen. Hence, for every $\mathsf{i}$, $\mathsf{1 \leq i < |X|}$, +the collision winner that has collided with $\mathsf{x_i}$ will be recorded appropriately. Since all the $\mathsf{cr}$ entries that record the results of the collisions before $\mathsf{p}$ will also be seen when $\mathsf{u}$ +is received, and $\mathsf{C}$ sees $\mathsf{r_1}$, ${l_1}$ will be recorded in a $\mathsf{cr}$ entry as the winner in the +collision against ${r_1}$. + +When $\mathsf{C}$ receives $\mathsf{u}$, if $\mathsf{C}$ +has seen the $\mathsf{cr}$ entry that records the collision at index $\mathsf{s_q + 1}$, it will throw an error from the mismatch of $\mathsf{\tuple{s_q+1, id_J}}$ with $\mathsf{\tuple{s_q+1, id_K}}$ in the corresponding $\mathsf{cr}$ entry. -\item Case 2.2.2.1: + \end{itemize} \end{itemize} \end{itemize} \end{proof} -\begin{lem} If there are two packets $\mathsf{t}$ and $\mathsf{u}$, with +\begin{lem} +\label{lem:pathmessages} +If there are two messages $\mathsf{t}$ and $\mathsf{u}$, with $\mathsf{s_t \leq s_u}$, such that $\mathsf{t}$ is in the path of $\mathsf{u}$, then for any message $\mathsf{p}$ with $\mathsf{s_p \leq s_t}$, iff $\mathsf{p}$ is in the path of $\mathsf{t}$, it is in the path of $\mathsf{u}$. @@ -1124,11 +1124,11 @@ in that slot in $\mathsf{T}$. Let $\mathsf{C_1}$ be some client in the transitiv set, with partial sequence $\mathsf{P_{C_1}}$, and let $\mathsf{u}$ be some message with $\mathsf{s_u > s_n}$ that $\mathsf{C_1}$ shares with another client. Then let $\mathsf{T}$ be the portion of the path of $\mathsf{u}$ ending at sequence number $\mathsf{s_n}$ and -$\mathsf{t}$ be the message at that sequence number. Clearly, by Lemma 1, $\mathsf{P_{C_1}}$ -is consistent with $\mathsf{T}$. We will show that, for every other client $\mathsf{D}$ -with partial sequence $\mathsf{P_D}$, $\mathsf{P_D}$ has some message whose path includes -$\mathsf{t}$. Because $\mathsf{D}$ is in the transitive closure, there is a sequence of -clients $\mathsf{\mathscr{C} = (C_1, C_2, ..., D)}$ from $\mathsf{C_1}$ to $\mathsf{D}$, +$\mathsf{t}$ be the message at that sequence number. Clearly, by Lemma \ref{lem:twomessages}, +$\mathsf{P_{C_1}}$ is consistent with $\mathsf{T}$. We will show that, for every other client +$\mathsf{D}$ with partial sequence $\mathsf{P_D}$, $\mathsf{P_D}$ has some message whose path +includes $\mathsf{t}$. Because $\mathsf{D}$ is in the transitive closure, there is a sequence +of clients $\mathsf{\mathscr{C} = (C_1, C_2, ..., D)}$ from $\mathsf{C_1}$ to $\mathsf{D}$, where each shares an edge with the next. We prove by induction that $\mathsf{P_D}$ has a message whose path includes $\mathsf{t}$. \begin{itemize} @@ -1137,14 +1137,15 @@ We prove by induction that $\mathsf{P_D}$ has a message whose path includes $\ma \item Inductive step: Each client in $\mathsf{\mathscr{C}}$ has a partial sequence with a message that includes $\mathsf{t}$ if the previous client does. Suppose $\mathsf{P_{C_k}}$ has a message $\mathsf{w}$ with a path that includes $\mathsf{t}$, and shares message $\mathsf{x}$ -with $\mathsf{P_{C_{k+1}}}$ such that $\mathsf{s_x > s_n}$. By Lemma 1, $\mathsf{w}$ or -$\mathsf{x}$, whichever has the least sequence number, is in the path of the other, and therefore -by Lemma 2, $\mathsf{t}$ is in the path of $\mathsf{x}$. +with $\mathsf{P_{C_{k+1}}}$ such that $\mathsf{s_x > s_n}$. By Lemma \ref{lem:twomessages}, +$\mathsf{w}$ or $\mathsf{x}$, whichever has the least sequence number, is in the path of the other, +and therefore by Lemma \ref{lem:pathmessages}, $\mathsf{t}$ is in the path of $\mathsf{x}$. \item Let $\mathsf{z}$ be the message of $\mathsf{D}$ whose path includes $\mathsf{t}$. -By Lemma 1, every message in $\mathsf{P_D}$ with sequence number smaller than $\mathsf{s_w}$ -is in the path of $\mathsf{z}$. Since $\mathsf{t}$ is in the path of $\mathsf{z}$, every -message in $\mathsf{P_D}$ with smaller sequence number than $\mathsf{s_t = s_n}$ is in $\mathsf{T}$. +By Lemma \ref{lem:twomessages}, every message in $\mathsf{P_D}$ with sequence number smaller +than $\mathsf{s_w}$ is in the path of $\mathsf{z}$. Since $\mathsf{t}$ is in the path of +$\mathsf{z}$, every message in $\mathsf{P_D}$ with smaller sequence number than +$\mathsf{s_t = s_n}$ is in $\mathsf{T}$. Therefore, $\mathsf{P_D}$ is consistent with $\mathsf{T}$. \end{itemize}