\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
\EndProcedure\r
\end{algorithmic}\r
\r
+\note{Don't include ``such that'' in the argument of a function...}\r
+\r
\begin{algorithmic}[1]\r
\Function{ValidHmac}{$DE_s,SK_s,hmac_{stored}$}\r
\State $hmac_{computed} \gets Hmac(DE_s,SK_s)$\r
-\If{$hmac_{stored} = hmac_{computed}$}\r
- \State $valid \gets true$\r
-\Else\r
- \State $valid \gets false$\r
-\EndIf\r
-\State \Return{$valid$}\r
+\State \Return {$hmac_{stored} = hmac_{computed}$}\r
\EndFunction\r
\end{algorithmic}\r
\r
\begin{algorithmic}[1]\r
\Function{ValidPrevHmac}{$DE_s,hmac_{p_s},hmac_{p_{sto}}$}\r
\If{$hmac_{p_s} = \emptyset$}\Comment{First slot - no previous HMAC}\r
- \State $valid \gets true$\r
+ \State \Return $true$\r
\Else\r
- \If{$hmac_{p_{sto}} = hmac_{p_s}$}\r
- \State $valid \gets true$\r
- \Else\r
- \State $valid \gets false$\r
- \EndIf\r
+ \State \Return {$hmac_{p_{sto}} = hmac_{p_s}$}\r
\EndIf\r
-\State \Return{$valid$}\r
\EndFunction\r
\end{algorithmic}\r
\r
+\note{So if a slot has a null previous hmac, everything is fine? What if it isn't the first slot?}\r
+\r
\begin{algorithmic}[1]\r
\Function{GetQueSta}{$Dat_s$}\r
\State $DE_s \gets GetDatEnt(DE_s)$\r
\ForAll{$de_s \in DE_s$}\r
\If{$de_s$ \textit{such that} $de_s \in D \land de_s = kv$}\r
\State $\tuple{k_s,v_s} \gets GetKV(de_s)$\r
- \State $k_s \gets GetKey(\tuple{k_s,v_s})$\r
\State $\tuple{k_s,v_t} \gets GetKeyVal(DT_s,k_s)$\r
\If{$\tuple{k_s,v_t} = \emptyset$}\r
\State $DT_s \gets DT_s \cup \{\tuple{k_s,v_s}\}$\r
\Function{GetValFromKey}{$k_g$}\r
\State $\tuple{k_s,v_s} \gets \tuple{k,v}$ \textit{such that} $\tuple{k,v} \r
\in DT \land k = k_g$\r
-\State $v_s \gets GetVal(\tuple{k_s,v_s})$\r
\State \Return{$v_s$}\r
\EndFunction\r
\end{algorithmic}\r
\r
\begin{algorithmic}[1]\r
\Function{PutKVPair}{$KV_s,\tuple{k_s,v_s}$}\r
-\State $k_s \gets GetKey(\tuple{k_s,v_s})$\r
\State $\tuple{ck_s,\tuple{k_s,v_t}} \gets GetKV(KV_s,k_s)$\r
\If{$\tuple{ck_s,\tuple{k_s,v_t}} = \emptyset$}\r
\State $KV_s \gets KV_s \cup \{\tuple{ck_p, \tuple{k_s,v_s}}\}$\r
\State $s_{last_{max}} \gets MaxLastSeqN(MS_s)$\r
\State $n_{live} \gets s_{last_{max}} - s_{last_{min}}$\Comment{Number of live slots}\r
\State $n_{dead} \gets max'_t - n_{live}$\r
-\If{$n_{dead} = 0$}\r
- \State $need \gets true$\r
-\Else\r
- \State $need \gets false$\r
-\EndIf\r
-\State \Return{$need$}\r
+\State \Return {$n_{dead} = 0$}\r
\EndFunction\r
\end{algorithmic}\r
\r
\State \Return{$cr_s$}\r
\EndFunction\r
\end{algorithmic}\r
+\note{Shouldn't this function do something pretty sophisticated about seeing what data we actually need to keep from the last slot and not just insert the entire thing?}\r
+\r
+\note{Probably best to just not call this function is $need_s$ is false and not pass in such parameters. It makes it harder to read.}\r
+\r
\r
\begin{algorithmic}[1]\r
\Function{GetDEPairs}{$KV_s,max'_s,need_s,sl_s$}\r
\EndProcedure\r
\end{algorithmic}\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
+\note{Lots of problems with PutDataEntries: (1) What happens if lose network connectivity after adding the key value pair, but before reinserting the last slot? You probably need to create space first and then insert your data entry... (2) What if reinsertlastslot kicks something else important out? What if the server rejects our update because it is out of date? At the very least, any putdataentries function w/o a loop is wrong!}\r
+\r
+\note{General comments... Work on structuring things to improve\r
+ readability... This include names of functions/variables, how\r
+ things are partitioned into functions, adding useful comments,...}\r
+\r
+\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
projects / iotcloud.git / blobdiff