author tkwa Sat, 23 Jul 2016 01:10:08 +0000 (18:10 -0700) committer tkwa Sat, 23 Jul 2016 01:10:08 +0000 (18:10 -0700)
 doc/iotcloud.tex patch | blob | history

@@ -2,8 +2,13 @@
\newcommand{\tuple}[1]{\ensuremath \langle #1 \rangle}\r
\usepackage{color}\r
\usepackage{amsthm}\r
+\usepackage{amsmath}\r
+\usepackage{graphicx}\r
+\usepackage{mathrsfs}\r
\usepackage{algpseudocode}% http://ctan.org/pkg/algorithmicx\r
\newtheorem{theorem}{Theorem}\r
+\newtheorem{prop}{Proposition}\r
+\newtheorem{lem}{Lemma}\r
\newtheorem{defn}{Definition}\r
\newcommand{\note}[1]{{\color{red} \bf [[#1]]}}\r
\newcommand{\push}[1][1]{\hskip\dimexpr #1\algorithmicindent\relax}\r
@@ -675,118 +680,61 @@ $\tuple{ck,\tuple{k, v}} \in KV_s \wedge things are partitioned into functions, adding useful comments,...}\r \r \r -\subsection{Formal Guarantees}\r -\r -\textit{To be completed ...}\r -\r -\begin{defn}[System Execution]\r -Let \\\r -\begin{center}\r -$Q = \{slot_{sn_1}, slot_{sn_2}, \dots, Slot_{sn_n}\}$, \\\r -$SN = \{sn_1, sn_2, \dots, sn_n\}$\\\r -\end{center}\r -denote a queue$Q$of$n$slots, with each slot entry being denoted by a\r -valid sequence number$sn_i \in SN$.$Q$represents a total order of all \r -slot updates from all corresponding machines.\r -%\textit{Formalize a system execution as a sequence of slot updates...\r -%There is a total order of all slot updates.}\r -\end{defn}\r -\r -\begin{defn}[Transitive Closure]\r -A transitive closure$\tau : \tau = \epsilon_{update(slot_i)} R $\r -$\epsilon_{receive(slot_i)}$is a relation from slot update event\r -$\epsilon$to a slot receive event$\epsilon$for$slot_i$.\r -%Define transitive closure relation for slot updates... There is an\r -%edge from a slot update to a slot receive event if the receive event\r -%reads from the update event.\r -\end{defn}\r -\r -\begin{defn}[Suborder]\r -Let \\\r -\begin{center}\r -$q = \{slot_{i}, slot_{i+1}, \dots, slot_{j}\}, \r
-sn_1 \leq i \leq j \leq sn_n \Longrightarrow q \subseteq Q$\r -\end{center}\r -denote a suborder of the total order. Set q is a sequence of contiguous\r -slot updates that is a subset of a total order of all slot updates in Q.\r -%Define suborder of total order. It is a sequence of contiguous slots\r -%updates (as observed by a given device).\r -\end{defn}\r -\r -\begin{defn}[Prefix of a suborder]\r -Given a suborder \\ \r -\begin{center}\r -$q' = \{slot_{i}, slot_{i+1}, \dots, slot_{j}, \dots\}, \r
-sn_1 \leq i \leq j \leq sn_n \Longrightarrow \r
-q' \subseteq Q$\r -\end{center}\r -with$slot_{j}$as a slot update in$q'$, the prefix of$q'$is a sequence \r -of all slot updates$\{slot_{i}, slot_{i+1}, \dots, slot_{j-1}\} \cup\r
-slot_{j}$.\r -%Given a sub order$o=u_{i},u_{i+1},...,u_j, u_{j+i},..., u', ...$and\r -%a slot update$u'$in$o$, the prefix of$o$is a sequence of all\r -%updates that occur before$u'$and$u'$.\r -\end{defn}\r -\r -\begin{defn}[Consistency between a suborder and a total order]\r -A suborder$q'$is consistent with a total order$T$of$Q$, if all\r -updates in$q'$appear in$T$and they appear in the same order, as \r -the following:\r -\begin{center}\r -$q' = \{slot_{i}, slot_{i+1}, \dots, slot_{j}\},$\r -$T = \{slot_{sn_1}, \dots, slot_{i}, slot_{i+1}, \dots, slot_{j}, \dots,\r
-slot_{sn_n}\},$\\$sn_1 \leq i \leq j \leq sn_n \Longrightarrow\r
-q' \subseteq T$\r -\end{center}\r -%A suborder$o$is consistent with a total order$t$, if all updates in$o$%appear in$t$and they appear in the same order.\r -\end{defn}\r -\r -\begin{defn}[Consistency between suborders]\r -Two suborders U and V are consistent if there exist a total order T \r -such that both U and V are suborders of T.\r -\begin{center}\r -$U = \{slot_{i}, slot_{i+1}, \dots, slot_{j}\},$\\\r -$V = \{slot_{k}, slot_{k+1}, \dots, slot_{l}\},$\\\r -$sn_1 \leq i \leq j \leq k \leq l \leq sn_n,$\\\r -$U \subset T \land V \subset T$\\\r -$T = \{slot_{sn_1}, \dots, slot_{i}, slot_{i+1}, \dots, slot_{j}, $\\\r -$\dots, slot_{k}, slot_{k+1}, \dots, slot_{l}, \dots, slot_{sn_n}\}$\r -\end{center}\r -%Define notion of consistency between suborders... Two suborders U,V\r -%are consistent if there exist a total order T such that both U and V\r -%are suborders of T.\r -\end{defn}\r -\r -\begin{defn}[Error-free execution]\r -An error-free execution, for which the client does not flag any errors\r -is defined by the following criteria:\r +\subsection{Definitions for Formal Guarantees}\r +\r \begin{enumerate}\r -\item Item 1\r -\item Item 2\r +\item Equality: Two messages$t$and$u$are equal if their sequence numbers, senders, and contents are exactly the same.\r +\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 +\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 +\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.\r +\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 +\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 +\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 +\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$.\r +\r \end{enumerate}\r -%not flag any errors...\r -%Define error-free execution --- execution for which the client does\r -%not flag any errors...\r -\end{defn}\r -\r -\begin{theorem} Error-free execution of algorithm ensures that the suborder\r -for node n is consistent with the prefix suborder for all other nodes\r -that are in the transitive closure.\r -\end{theorem}\r +\r +\subsection{Formal Guarantee}\r +\r +\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 +\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 +\r +\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 +\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 +\r +\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$. \end{lem}\r \begin{proof}\r -\textit{TODO}\r +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 +\r +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 +\r +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 +\r +There are two cases:\r +\r +\begin{itemize}\r +\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)$.\r +\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 +\begin{itemize}\r +\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.\r +\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 +\begin{itemize}\r +\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 +\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)$.\r +\end{itemize}\r +\end{itemize}\r +\end{itemize}\r \end{proof}\r \r -\begin{defn}[State of Data Structure]\r -Define in terms of playing all updates sequentially onto local data\r -structure.\r -\end{defn}\r -\r \begin{theorem}\r -Algorithm gives consistent view of data structure.\r -\end{theorem}\r +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 +\r \begin{proof}\r -\textit{TODO}\r +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. 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 +\r +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 +\r +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
\end{proof}\r
\r
\subsection{Future Work}\r