From: tkwa Date: Thu, 18 Aug 2016 00:12:39 +0000 (-0700) Subject: Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/iotcloud X-Git-Url: http://plrg.eecs.uci.edu/git/?p=iotcloud.git;a=commitdiff_plain;h=f498aec54ac8672e6b7c5d813f6487b4a57ed5a6;hp=-c Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/iotcloud --- f498aec54ac8672e6b7c5d813f6487b4a57ed5a6 diff --combined doc/iotcloud.tex index e08d6e1,de40d0e..4d0c9f4 --- a/doc/iotcloud.tex +++ b/doc/iotcloud.tex @@@ -587,7 -587,7 +587,7 @@@ $\tuple{ck,\tuple{k, v}} \in KV_s \wedg \begin{algorithmic}[1] \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,k_s)$ +\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$ @@@ -909,7 -909,8 +909,8 @@@ received the same message $\mathsf{t}$ \subsubsection{Lemmas and Proofs} - \begin{prop} + \begin{prop} + \label{prop:parentmessage} Every client $\mathsf{J}$ who sends a message $\mathsf{t}$ has parent $\mathsf{p_t}$ as its latest stored message, and $\mathsf{s_t = s_{p_t} + 1}$. @@@ -920,7 -921,9 +921,9 @@@ $\mathsf{s_t = }$ $\mathsf{s_{p_t + 1}} 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} @@@ -943,18 -946,19 +946,20 @@@ $\mathsf{s - 1}$, this client will hav \restore \restore } - \caption{By Lemma 1, receiving both $t$ and $u$ here 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 otherwise. Then there are some pairs $\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}$. +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 @@@ -977,25 -981,28 +982,28 @@@ $\mathsf{s_{r_1} = s_{l_1} = s_q + 1}$ We also know the following facts: - \begin{prop} No client sends both a message in - $\mathsf{(r_2,...,t)}$ and a message in $\mathsf{(l_2,...,u)}$. + \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} \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 Lemma 1, no client receives both a message in $\mathsf{r}$ - and a message in $\mathsf{l}$. + client that violates Lemma \ref{lem:twomessages}, no client receives both a message + in $\mathsf{r}$ and a message in $\mathsf{l}$. \end{proof} - \begin{prop} $\mathsf{C}$ does not receive any message with a + \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 1. + message with the least sequence number that violates Lemma \ref{lem:twomessages}. \end{proof} There are two cases: @@@ -1007,13 -1014,13 +1015,13 @@@ the path of message $\mathsf{t}$, $\mat \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 @@@ -1029,7 -1036,8 +1037,8 @@@ client $\mathsf{J}$ cannot then send a $\mathsf{s_{r_1}}$, a contradiction. \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}$. + 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. Before sending $\mathsf{m}$, $\mathsf{J}$'s value in $\mathsf{MS_J}$ for its own latest sequence number would @@@ -1042,11 -1050,19 +1051,19 @@@ sending $\mathsf{p}$, because its own l \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, + 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_m}$. In the $\mathsf{PutDataEntries}$ subroutine, $\mathsf{J}$ adds every + 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{m}$ into $\mathsf{CR}$; $\mathsf{CR}$ keeps the collection of live $\mathsf{cr}$ entries, namely @@@ -1066,7 -1082,9 +1083,9 @@@ $\mathsf{\tuple{s_q+1, id_K}}$ in the c \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}$. @@@ -1105,11 -1123,11 +1124,11 @@@ in that slot in $\mathsf{T}$. Let $\mat 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} @@@ -1118,14 -1136,15 +1137,15 @@@ \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}