From: tkwa Date: Fri, 12 Aug 2016 23:59:34 +0000 (-0700) Subject: Restructured proof; should be complete now X-Git-Url: http://plrg.eecs.uci.edu/git/?p=iotcloud.git;a=commitdiff_plain;h=694aaf2c6313b2c120f72e4c6b71eede56879695 Restructured proof; should be complete now --- diff --git a/doc/iotcloud.tex b/doc/iotcloud.tex index b96f391..52ec3f0 100644 --- a/doc/iotcloud.tex +++ b/doc/iotcloud.tex @@ -883,9 +883,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] @@ -922,9 +922,7 @@ $\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} @@ -955,7 +953,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{^\}} @@ -963,7 +961,7 @@ $\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 Lemma 1, receiving both $t$ and $u$ here is impossible.} \end{figure} \begin{lem} Two messages are received without errors by a client $\mathsf{C}$; @@ -986,41 +984,37 @@ 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 three 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} 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 1, 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} $\mathsf{C}$ does not receive any message with +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 least sequence number that violates Lemma 1. \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 @@ -1035,57 +1029,49 @@ 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} >= 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 3 and the existence of $\mathsf{m}$. Since $\mathsf{H \neq J}$, then by Proposition 3 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 4. 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}