More fixes to Lemma 1 of the proof and misc. subroutines
authortkwa <kwathomas0@gmail.com>
Tue, 2 Aug 2016 00:07:58 +0000 (17:07 -0700)
committertkwa <kwathomas0@gmail.com>
Tue, 2 Aug 2016 00:07:58 +0000 (17:07 -0700)
doc/iotcloud.tex

index 250ddcf..ab9cf85 100644 (file)
@@ -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.\r
 \r
 \subsection{Server Algorithm}\r
-$s \in SN$ is a sequence number set\\\r
+$s \in SN$ is a sequence number\\\r
 $sv \in SV$ is a slot's value\\\r
 $slot_s = \tuple{s, sv} \in SL \subseteq SN \times SV$ \\ \\\r
 \textbf{State} \\\r
@@ -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}}$, \r
 s + id of a machine that wins a collision, $cr \in DE$ \\\r
 $DE$ is a set of all data entries, possibly of different types, in a single message \\\r
-$s \in SN$ is a sequence number set \\\r
+$s \in SN$ is a sequence number \\\r
 $id$ is a machine ID\\\r
 $hmac_p$ is the HMAC value of the previous slot \\\r
 $hmac_c$ is the HMAC value of the current slot \\\r
@@ -408,9 +408,7 @@ $MinLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s
 \State $MS_g \gets \emptyset$\r
 \State $SM_{curr} \gets \emptyset$\r
 \State $\tuple{s_{g_{max}},sv_{g_{max}}} \gets MaxSlot(SL_g)$\r
-\State $s_{g_{max}} \gets SeqN(\tuple{s_{g_{max}},sv_{g_{max}}})$\r
 \State $\tuple{s_{g_{min}},sv_{g_{min}}} \gets MinSlot(SL_g)$\r
-\State $s_{g_{min}} \gets SeqN(\tuple{s_{g_{min}},sv_{g_{min}}})$\r
 \For{$s_g \gets s_{g_{min}}$ \textbf{to} $s_{g_{max}}$}\Comment{Process slots \r
        in $SL_g$ in order}\r
        \State $\tuple{s_g,sv_g} \gets Slot(SL_g,s_g)$\r
@@ -480,13 +478,12 @@ $MinLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s
 $k$ is key of entry \\\r
 $v$ is value of entry \\\r
 $kv$ is a key-value entry $\tuple{k,v}$\\\r
-$D = \{kv,ss,qs,cr\}$ \\\r
-$DE = \{de \mid de \in D\}$ \\\r
+$DE$ is a set of data entries, possibly of different types \\\r
 $Dat_s = \tuple{s,id,hmac_p,DE,hmac_c}$ \\\r
 $sv_s = \tuple{s, E(Dat_s)} = \r
 \tuple{s, E(\tuple{s,id,hmac_p,DE,hmac_c})}$ \\ \\\r
 \textbf{States} \\\r
-\textit{$cp$ = data entry $DE$ maximum size/capacity} \\\r
+\textit{$capacity$ = data entry $DE$ maximum size/capacity} \\\r
 \textit{$cr_p$ = saved cr entry $\tuple{s,id}$ on client if there is a collision\r
 (sent in the following slot)} \\\r
 \textit{$cr_{p_{last}}$ = saved cr entry $\tuple{s,id}$ on client if there is a \r
@@ -501,7 +498,7 @@ collision in reinserting the last slot (sent in the following slot)} \\
        $\tuple{s_{last},sv_{last},id_{last}}$ (initially $\emptyset$)} \\\r
 \textit{$th_p$ = threshold number of dead slots for a resize to happen} \\\r
 \textit{$m'_p$ = offset added to $max$ for resize} \\\r
-\textit{$KV$ = set of $\tuple{ck, \tuple{k,v}}$ of kv entries on client} \\\r
+\textit{$KV$ = associative array of $\tuple{ck, \tuple{k,v}}$ kv entries on client} \\\r
 \textit{$SL_p$ = set of returned slots on client} \\\r
 \textit{SK = Secret Key} \\ \\\r
 \textbf{Helper Functions} \\\r
@@ -581,54 +578,50 @@ $\tuple{ck,\tuple{k, v}} \in KV_s \wedge
 \end{algorithmic}\r
 \r
 \begin{algorithmic}[1]\r
-\Function{ReinsertLastSlot}{$need_s,sl_{s_{last}},max'_s$}\r
-\If{$need_s$}\r
+\Function{ReinsertLastSlot}{$sl_{s_{last}},max'_s$}\r
        \State $s_s \gets GetLastS(sl_{s_{last}})$\r
        \State $sv_s \gets GetSV(sl_{s_{last}})$\r
        \State $\tuple{stat_s,SL_s} \gets \Call{PutSlot}{s_s,sv_s,max'_s}$\r
        \State $cr_s \gets \Call{HandleCollision}{\tuple{stat_s,SL_s}}$\r
-\EndIf\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
 \State $DE_{ret} \gets \emptyset$\r
-\State $cp_s \gets cp$\r
+\State $capacity_s \gets capacity$\r
 \If{$cr_p \neq \emptyset$}\Comment{Check and insert a $cr$}\r
        \State $DE_{ret} \gets DE_{ret} \cup cr_p$\r
-       \State $cp_s \gets cp_s - 1$\r
+       \State $capacity_s \gets capacity_s - 1$\r
 \EndIf\r
 \If{$cr_{p_{last}} \neq \emptyset$}\Comment{Check and insert a $cr$}\r
        \State $DE_{ret} \gets DE_{ret} \cup cr_{p_{last}}$\r
-       \State $cp_s \gets cp_s - 1$\r
+       \State $capacity_s \gets capacity_s - 1$\r
 \EndIf\r
 \If{$max'_s \neq \emptyset$}\Comment{Check and insert a $qs$}\r
        \State $qs_s \gets max'_s$\r
        \State $DE_{ret} \gets DE_{ret} \cup qs_s$\r
-       \State $cp_s \gets cp_s - 1$\r
+       \State $capacity_s \gets capacity_s - 1$\r
 \EndIf\r
 \If{$need_s$}\Comment{Check and insert a $ss$}\r
        \State $id_s \gets GetID(sl_s)$\r
        \State $s_{s_{last}} \gets GetLastS(sl_s)$\r
        \State $ss_s \gets CreateSS(id_s,s_{s_{last}})$\r
        \State $DE_{ret} \gets DE_{ret} \cup ss_s$\r
-       \State $cp_s \gets cp_s - 1$\r
+       \State $capacity_s \gets capacity_s - 1$\r
 \EndIf\r
-\If{$|KV_s| \leq cp$}\Comment{$KV$ set can extend multiple slots}\r
+\If{$|KV_s| \leq capacity$}\Comment{$KV$ set can extend multiple slots}\r
        \State $DE_{ret} \gets DE_{ret} \cup\r
        \{\tuple{k_s,v_s} \mid \tuple{ck_s,\tuple{k_s,v_s}} \in KV_s\}$\r
 \Else\r
        \State $DE_{ret} \gets DE_{ret} \cup\r
        \{\tuple{k_s,v_s} \mid \tuple{ck_s,\tuple{k_s,v_s}} \in KV_s,\r
-               ck_g \leq ck_s < ck_g + cp_s\}$\r
-       \If{$|DE_{ret}| = cp$}\r
-               \State $ck_g \gets ck_g + cp_s$\Comment{Middle of KV set}\r
+               ck_g \leq ck_s < ck_g + capacity_s\}$\r
+       \If{$|DE_{ret}| = capacity$}\r
+               \State $ck_g \gets ck_g + capacity_s$\Comment{Middle of KV set}\r
        \Else\r
                \State $ck_g \gets 0$\Comment{End of KV set}\r
        \EndIf\r
@@ -649,7 +642,9 @@ $\tuple{ck,\tuple{k, v}} \in KV_s \wedge
 \State $sv_p \gets Encrypt(Dat_p,SK)$\r
 \State $\tuple{stat_p,SL_p} \gets \Call{PutSlot}{s_p,sv_p,max'_p}$\r
 \State $cr_p \gets \Call{HandleCollision}{\tuple{stat_p,SL_p}}$\r
-\State $cr_{p_{last}} \gets \Call{ReinsertLastSlot}{need_p,sl_{last},max'_p}$\r
+\If{$need_p$}\r
+       \State $cr_{p_{last}} \gets \Call{ReinsertLastSlot}{sl_{last},max'_p}$\r
+\EndIf\r
 \EndProcedure\r
 \end{algorithmic}\r
 \r
@@ -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}\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} \r
-\r
-\end{lem}\r
-\r
 \begin{figure}[h]\r
   \centering\r
       \xymatrix{\r
 \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
 & & R_1 \ar[r] & R_2 \ar[r] & \dots \ar[r] & R_m = t}\r
-\caption{By Lemma 2, receiving $t$ before $u$ is impossible.}\r
+\caption{By Lemma 1, receiving $u$ after $t$ is impossible.}\r
 \end{figure}\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{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}\r
 \begin{proof}\r
+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$.\r
+\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
@@ -707,9 +700,8 @@ There are two cases:
 \begin{itemize}\r
 \item Case 1: $J$ did not send a message in $S$. Then $v_J(t) > v_J(q) = v_J(u)$.\r
 \begin{itemize}\r
-\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)$.\r
-\r
-\r
+\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.\r
+\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.\r
 \r
 \end{itemize}\r
 \r
@@ -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}\r
 \r
 \begin{proof}\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
+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$.\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