From: tkwa Date: Tue, 2 Aug 2016 00:07:58 +0000 (-0700) Subject: More fixes to Lemma 1 of the proof and misc. subroutines X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=21d1d65712c836839d97d0f34bbe182a4e87815d;p=iotcloud.git More fixes to Lemma 1 of the proof and misc. subroutines --- diff --git a/doc/iotcloud.tex b/doc/iotcloud.tex index 250ddcf..ab9cf85 100644 --- a/doc/iotcloud.tex +++ b/doc/iotcloud.tex @@ -135,7 +135,7 @@ Client can make a request to resize the queue. This is done as a write that comb (a) a slot with the message, and (b) a request to the server. The queue can only be expanded, never contracted; attempting to decrease the size of the queue will cause future clients to throw an error. \subsection{Server Algorithm} -$s \in SN$ is a sequence number set\\ +$s \in SN$ is a sequence number\\ $sv \in SV$ is a slot's value\\ $slot_s = \tuple{s, sv} \in SL \subseteq SN \times SV$ \\ \\ \textbf{State} \\ @@ -192,7 +192,7 @@ $qs$ is a queue state entry (contains $max$ size of queue), $qs \in DE$ \\ $cr$ is a collision resolution entry $\tuple{s_{col},id_{col}}$, s + id of a machine that wins a collision, $cr \in DE$ \\ $DE$ is a set of all data entries, possibly of different types, in a single message \\ -$s \in SN$ is a sequence number set \\ +$s \in SN$ is a sequence number \\ $id$ is a machine ID\\ $hmac_p$ is the HMAC value of the previous slot \\ $hmac_c$ is the HMAC value of the current slot \\ @@ -408,9 +408,7 @@ $MinLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s \State $MS_g \gets \emptyset$ \State $SM_{curr} \gets \emptyset$ \State $\tuple{s_{g_{max}},sv_{g_{max}}} \gets MaxSlot(SL_g)$ -\State $s_{g_{max}} \gets SeqN(\tuple{s_{g_{max}},sv_{g_{max}}})$ \State $\tuple{s_{g_{min}},sv_{g_{min}}} \gets MinSlot(SL_g)$ -\State $s_{g_{min}} \gets SeqN(\tuple{s_{g_{min}},sv_{g_{min}}})$ \For{$s_g \gets s_{g_{min}}$ \textbf{to} $s_{g_{max}}$}\Comment{Process slots in $SL_g$ in order} \State $\tuple{s_g,sv_g} \gets Slot(SL_g,s_g)$ @@ -480,13 +478,12 @@ $MinLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s $k$ is key of entry \\ $v$ is value of entry \\ $kv$ is a key-value entry $\tuple{k,v}$\\ -$D = \{kv,ss,qs,cr\}$ \\ -$DE = \{de \mid de \in D\}$ \\ +$DE$ is a set of data entries, possibly of different types \\ $Dat_s = \tuple{s,id,hmac_p,DE,hmac_c}$ \\ $sv_s = \tuple{s, E(Dat_s)} = \tuple{s, E(\tuple{s,id,hmac_p,DE,hmac_c})}$ \\ \\ \textbf{States} \\ -\textit{$cp$ = data entry $DE$ maximum size/capacity} \\ +\textit{$capacity$ = data entry $DE$ maximum size/capacity} \\ \textit{$cr_p$ = saved cr entry $\tuple{s,id}$ on client if there is a collision (sent in the following slot)} \\ \textit{$cr_{p_{last}}$ = saved cr entry $\tuple{s,id}$ on client if there is a @@ -501,7 +498,7 @@ collision in reinserting the last slot (sent in the following slot)} \\ $\tuple{s_{last},sv_{last},id_{last}}$ (initially $\emptyset$)} \\ \textit{$th_p$ = threshold number of dead slots for a resize to happen} \\ \textit{$m'_p$ = offset added to $max$ for resize} \\ -\textit{$KV$ = set of $\tuple{ck, \tuple{k,v}}$ of kv entries on client} \\ +\textit{$KV$ = associative array of $\tuple{ck, \tuple{k,v}}$ kv entries on client} \\ \textit{$SL_p$ = set of returned slots on client} \\ \textit{SK = Secret Key} \\ \\ \textbf{Helper Functions} \\ @@ -581,54 +578,50 @@ $\tuple{ck,\tuple{k, v}} \in KV_s \wedge \end{algorithmic} \begin{algorithmic}[1] -\Function{ReinsertLastSlot}{$need_s,sl_{s_{last}},max'_s$} -\If{$need_s$} +\Function{ReinsertLastSlot}{$sl_{s_{last}},max'_s$} \State $s_s \gets GetLastS(sl_{s_{last}})$ \State $sv_s \gets GetSV(sl_{s_{last}})$ \State $\tuple{stat_s,SL_s} \gets \Call{PutSlot}{s_s,sv_s,max'_s}$ \State $cr_s \gets \Call{HandleCollision}{\tuple{stat_s,SL_s}}$ -\EndIf \State \Return{$cr_s$} \EndFunction \end{algorithmic} \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?} -\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.} - \begin{algorithmic}[1] \Function{GetDEPairs}{$KV_s,max'_s,need_s,sl_s$} \State $DE_{ret} \gets \emptyset$ -\State $cp_s \gets cp$ +\State $capacity_s \gets capacity$ \If{$cr_p \neq \emptyset$}\Comment{Check and insert a $cr$} \State $DE_{ret} \gets DE_{ret} \cup cr_p$ - \State $cp_s \gets cp_s - 1$ + \State $capacity_s \gets capacity_s - 1$ \EndIf \If{$cr_{p_{last}} \neq \emptyset$}\Comment{Check and insert a $cr$} \State $DE_{ret} \gets DE_{ret} \cup cr_{p_{last}}$ - \State $cp_s \gets cp_s - 1$ + \State $capacity_s \gets capacity_s - 1$ \EndIf \If{$max'_s \neq \emptyset$}\Comment{Check and insert a $qs$} \State $qs_s \gets max'_s$ \State $DE_{ret} \gets DE_{ret} \cup qs_s$ - \State $cp_s \gets cp_s - 1$ + \State $capacity_s \gets capacity_s - 1$ \EndIf \If{$need_s$}\Comment{Check and insert a $ss$} \State $id_s \gets GetID(sl_s)$ \State $s_{s_{last}} \gets GetLastS(sl_s)$ \State $ss_s \gets CreateSS(id_s,s_{s_{last}})$ \State $DE_{ret} \gets DE_{ret} \cup ss_s$ - \State $cp_s \gets cp_s - 1$ + \State $capacity_s \gets capacity_s - 1$ \EndIf -\If{$|KV_s| \leq cp$}\Comment{$KV$ set can extend multiple slots} +\If{$|KV_s| \leq capacity$}\Comment{$KV$ set can extend multiple slots} \State $DE_{ret} \gets DE_{ret} \cup \{\tuple{k_s,v_s} \mid \tuple{ck_s,\tuple{k_s,v_s}} \in KV_s\}$ \Else \State $DE_{ret} \gets DE_{ret} \cup \{\tuple{k_s,v_s} \mid \tuple{ck_s,\tuple{k_s,v_s}} \in KV_s, - ck_g \leq ck_s < ck_g + cp_s\}$ - \If{$|DE_{ret}| = cp$} - \State $ck_g \gets ck_g + cp_s$\Comment{Middle of KV set} + ck_g \leq ck_s < ck_g + capacity_s\}$ + \If{$|DE_{ret}| = capacity$} + \State $ck_g \gets ck_g + capacity_s$\Comment{Middle of KV set} \Else \State $ck_g \gets 0$\Comment{End of KV set} \EndIf @@ -649,7 +642,9 @@ $\tuple{ck,\tuple{k, v}} \in KV_s \wedge \State $sv_p \gets Encrypt(Dat_p,SK)$ \State $\tuple{stat_p,SL_p} \gets \Call{PutSlot}{s_p,sv_p,max'_p}$ \State $cr_p \gets \Call{HandleCollision}{\tuple{stat_p,SL_p}}$ -\State $cr_{p_{last}} \gets \Call{ReinsertLastSlot}{need_p,sl_{last},max'_p}$ +\If{$need_p$} + \State $cr_{p_{last}} \gets \Call{ReinsertLastSlot}{sl_{last},max'_p}$ +\EndIf \EndProcedure \end{algorithmic} @@ -682,20 +677,18 @@ $\tuple{ck,\tuple{k, v}} \in KV_s \wedge \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} \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} -\begin{lem} - -\end{lem} - \begin{figure}[h] \centering \xymatrix{ \dots \ar[r] & q \ar[dr]_{J} \ar[r]^{K} & S_1 \ar[r] & S_2 \ar[rr] & & \dots \ar[r] & S_n = u \\ & & R_1 \ar[r] & R_2 \ar[r] & \dots \ar[r] & R_m = t} -\caption{By Lemma 2, receiving $t$ before $u$ is impossible.} +\caption{By Lemma 1, receiving $u$ after $t$ is impossible.} \end{figure} -\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} +\begin{lem} Two packets are received without errors by a client $C$; we can 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$. 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$. @@ -707,9 +700,8 @@ There are two cases: \begin{itemize} \item Case 1: $J$ did not send a message in $S$. Then $v_J(t) > v_J(q) = v_J(u)$. \begin{itemize} -\item Case 1.1: $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)$. - - +\item Case 1.2: $C$ receives a sequence of messages between $t$ and $u$ with contiguous sequence numbers. In particular, there is some packet $p$ such that $i(p) = i(u) + 1$. If $p$ is the parent of $u$, messages $t$ and $p$ are a violation of this lemma such that $p$ has a smaller sequence number than $u$; but this contradicts our assumption that $u$ had the smallest sequence number. If $t$ is not the parent of $u$, $HMAC_p(u) \neq HMAC_c(t)$, causing $C$ to error. +\item Case 1.2: Case 1.1 does not occur; therefore, $C$ must update its slot sequence list at some point between receiving $t$ and $u$. The latest index of $J$ decreases overall during this time, which means it must decrease when some message is received, which means C throws an error in the $CheckLastSeqN$ subroutine. \end{itemize} @@ -737,7 +729,7 @@ There are two cases: 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$, 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$. +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$. 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$.