From: tkwa Date: Tue, 2 Aug 2016 23:48:24 +0000 (-0700) Subject: Minor changes to proof X-Git-Url: http://plrg.eecs.uci.edu/git/?p=iotcloud.git;a=commitdiff_plain;h=f40df7bf3734c9d10f9e102193a7818f526aeca0 Minor changes to proof --- diff --git a/doc/iotcloud.tex b/doc/iotcloud.tex index bf11fb0..6688131 100644 --- a/doc/iotcloud.tex +++ b/doc/iotcloud.tex @@ -679,9 +679,10 @@ $\tuple{ck,\tuple{k, v}} \in KV_s \wedge \item Equality: Two messages $t$ and $u$ are equal if their sequence numbers, senders, and contents are exactly the same. \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. \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))$. -\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, where 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}$. +\item Chain: A chain of messages with length $n \ge 1$ is a message sequence $R = (R_i, R_{i+1}, ..., R_{i+n-1})$ such that for every index $i < k \le i+n-1$, $R_k$ has sequence number $k$ and is the parent of $R_{k-1}$. +\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. \item Total message sequence: A total message sequence $T$ with length $n$ is a chain of messages that starts at $i = 1$. -\item Path: The path of a message $t$ is the total message sequence whose last message is $t$. +\item Path: The path of a message $t$ is the chain that starts at $i = 1$ and whose last message is $t$. The uniqueness of a path follows from the uniqueness of a parent. \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. \item Transitive closure set at index $n$: 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) > n$. @@ -709,11 +710,11 @@ $\tuple{ck,\tuple{k, v}} \in KV_s \wedge \caption{By Lemma 1, receiving $u$ after $t$ is impossible.} \end{figure} -\begin{lem} Two packets are received without errors by a client $C$; call them $t$ and $u$ such that $i(t) \le i(u)$. Then $t$ is in the path of $u$. \end{lem} +\begin{lem} Two messages are received without errors by a client $C$; call them $t$ and $u$ such that $i(t) \le i(u)$. Then $t$ is in the path of $u$. \end{lem} \begin{proof} Clearly $C$ will throw an error if $i(t) = i(u)$. So $i(t) < i(u)$. Additionally, if $C$ receives $u$ before $t$, this will cause it to throw an error, so $t$ is received before $u$. -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$. +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 greatest index for this $u$. We will prove that an error occurs upon receipt of $u$. 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$. @@ -733,23 +734,39 @@ There are two cases: \item Case 2.1: Client $J$ sends $p$, and then $R_1$. Before sending $p$, the greatest sequence number of a message that $J$ has received, ${s_{last}}_j$, must be equal to $i(p) - 1 \ge i(R_1)$. Since ${s_{last}}_j$ never decreases, Client $J$ cannot then send a message with sequence number $i(R_1)$, a contradiction. \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$. \begin{itemize} -\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. -\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)$. +\item Case 2.2.1: Some message in $X$ was accepted. Let $v_J(w)$ be the greatest sequence number of the messages that client $J$ sent in the path of message $w$. In this case, before sending $p$, $J$'s value $SM_J[J]$ for its own latest index would be strictly greater than $v_J(q)$. If there is a sequence of messages with contiguous sequence numbers that $J$ receives between $R_1$ and $p$, J throws an error for a similar reason as Case 1.1. Otherwise, when preparing to send $p$, $J$ would have received an update of its own latest index as at most $v_J(q)$. $J$ throws an error before sending $p$, because its own latest index decreases. +\item Case 2.2.2: All messages in $X$ were rejected, making $p$ the first message of $J$ that is accepted after $R_1$. Note that $u$ is the message with least sequence number that violates this lemma, and therefore the first one that $C$ receives after $t$. Therefore, $C$ could not have seen a message after $t$ with index less than $i(p)$. In the $PutDataEntries$ subroutine, $J$ adds every rejected message to the ; 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 $CR_C(p)$. Since every rejected message in $CR(p)$ will be in $CR_C(u)$, $R_1$ will be recorded in $CR_C(p)$. When $C$ receives $u$, $C$ will throw an error from the match $(J, i(q)+1)$ in $CR_C(p)$. +\item Case 2.2.2.1: \end{itemize} \end{itemize} \end{itemize} \end{proof} +\begin{lem} If there are two packets $t$ and $u$, with $i(t) <= i(u)$, such that $t$ is in the path of $u$, then for any message $p$ with $i(p) <= i(t)$, iff $p$ is in the path of $t$, it is in the path of $u$. \end{lem} + +\begin{proof} +If $i(t) = i(u)$ or $i(p) = i(t)$, then we are done, because the two relevant messages are the same. + +Reverse direction: The definition of $t$ being in the path of $u$ is the existence of a message sequence $(..., t, ..., u)$ such that each message except $u$ is the parent of the succeeding message. The path of $u$ must contain some message with index $i(p)$; because $p$ is in the path of $u$, this message is $p$ itself. The path of $t$ is then the prefix of this path ending at $t$, which clearly contains $p$. + +Forward direction: The path of $t$ is a substring of the path of $u$, so if the path of $t$ contains $p$, so does the path of $u$. +\end{proof} + \begin{theorem} 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} \begin{proof} -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$. 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$. +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) > n$ that $C_1$ shares with another client. Then let $T$ be the portion of the path of $u$ ending at index $n$ and $t$ be the message at that index. Clearly, by Lemma 1, $P_{C_1}$ is consistent with $T$. 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 clients $\mathscr{C} = (C_1, C_2, ..., D)$ from $C_1$ to $D$, where each shares an edge with the next. + +We prove by induction that $P_D$ has a message whose path includes $t$. +\begin{itemize} +\item Base case: $P_{C_1}$ includes $u$, whose path includes $t$. -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$. +\item Inductive step: Each client in $\mathscr{C}$ has a partial message sequence with a message that includes $t$ if the previous client does. Suppose $P_{C_k}$ has a message $w$ with a path that includes $t$, and shares message $x$ with $P_{C_{k+1}}$ such that $i(x) > n$. By Lemma 1, $w$ or $x$, whichever has the least sequence number, is in the path of the other, and therefore by Lemma 2, $t$ is in the path of $x$. -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$. +\item Let $z$ be 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 $z$. Since $t$ is in the path of $z$, every message in $P_D$ with smaller index than $i(t)$ is in $T$. Therefore, $P_D$ is consistent with $T$. +\end{itemize} \end{proof} \subsection{Future Work}