Dividing data entry formation into smaller functions, fixing loop for PutDataEntries...
authorrtrimana <rtrimana@uci.edu>
Wed, 3 Aug 2016 00:04:43 +0000 (17:04 -0700)
committerrtrimana <rtrimana@uci.edu>
Wed, 3 Aug 2016 00:04:43 +0000 (17:04 -0700)
doc/iotcloud.tex

index bf11fb0..5276310 100644 (file)
@@ -559,20 +559,12 @@ $\tuple{ck,\tuple{k, v}} \in KV_s \wedge
 \end{algorithmic}\r
 \r
 \begin{algorithmic}[1]\r
-\Function{HandleCollision}{$\tuple{stat_s,SL_s}$}\r
-\State $stat_s \gets GetStatus(\tuple{stat_s,SL_s})$\r
-\State $SL_s \gets GetSL(\tuple{stat_s,SL_s})$\r
-\If{$\neg stat_s$}\Comment{Handle collision}\r
-       \State $\tuple{s_{col},sv_{col}} \gets GetColSeqN(SL_s,s_s)$\r
-       \State $s_{col} \gets SeqN(\tuple{s_{col},sv_{col}})$\r
-       \State $sv_{col} \gets SlotVal(\tuple{s_{col},sv_{col}})$\r
-       \State $Dat_{col} \gets Decrypt(SK,sv_{col})$\r
-       \State $id_{col} \gets GetMacId(Dat_{col})$\r
-       \State $\tuple{s_{col},id_{col}} \gets CreateCR(s_{col},id_{col})$\r
-       \State $cr_s \gets \tuple{s_{col},id_{col}}$\r
-\Else\r
-       \State $cr_s \gets \emptyset$\r
-\EndIf\r
+\Function{HandleCollision}{$SL_s$}\r
+\State $\tuple{s_{col},sv_{col}} \gets GetColSeqN(SL_s,s_s)$\r
+\State $Dat_{col} \gets Decrypt(SK,sv_{col})$\r
+\State $id_{col} \gets GetMacId(Dat_{col})$\r
+\State $\tuple{s_{col},id_{col}} \gets CreateCR(s_{col},id_{col})$\r
+\State $cr_s \gets \tuple{s_{col},id_{col}}$\r
 \State $\Call{ProcessSL}{SL_s}$\r
 \State \Return{$cr_s$}\r
 \EndFunction\r
@@ -594,45 +586,47 @@ $\tuple{ck,\tuple{k, v}} \in KV_s \wedge
 \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 if $need_s$ is false and not pass in such parameters.  It makes it harder to read.}\r
+\begin{algorithmic}[1]\r
+\Function{AddSlotSeq}{$DE_s,sl_s,cp_s$}\Comment{Insert a $ss$}\r
+\State $DE_{ret} \gets \emptyset$\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_s \cup ss_s$\r
+\State $cp_s \gets cp_s - 1$\r
+\State \Return{$\tuple{DE_{ret},cp_s}$}\r
+\EndFunction\r
+\end{algorithmic}\r
 \r
+\begin{algorithmic}[1]\r
+\Function{AddQueSta}{$DE_s,max'_s,cp_s$}\Comment{Insert a $qs$}\r
+\State $DE_{ret} \gets \emptyset$\r
+\State $qs_s \gets max'_s$\r
+\State $DE_{ret} \gets DE_s \cup qs_s$\r
+\State $cp_s \gets cp_s - 1$\r
+\State \Return{$\tuple{DE_{ret},cp_s}$}\r
+\EndFunction\r
+\end{algorithmic}\r
 \r
 \begin{algorithmic}[1]\r
-\Function{GetDEPairs}{$KV_s,max'_s,need_s,sl_s$}\r
+\Function{AddCollRes}{$DE_s,cr_p,cp_s$}\Comment{Insert a $cr$}\r
 \State $DE_{ret} \gets \emptyset$\r
-\State $cp_s \gets cp$\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
-\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
-%\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
-\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
-%\EndIf\r
-\If{$|KV_s| \leq cp$}\Comment{$KV$ set can extend multiple slots}\r
-       \State $DE_{ret} \gets DE_{ret} \cup\r
+\State $DE_{ret} \gets DE_s \cup cr_p$\r
+\State $cp_s \gets cp_s - 1$\r
+\State \Return{$\tuple{DE_{ret},cp_s}$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Function{GetKVPairs}{$DE_s,KV_s,cp_s$}\r
+\State $DE_{ret} \gets \emptyset$\r
+\If{$|KV_s| \leq cp$}\Comment{$KV$ set can span multiple slots}\r
+       \State $DE_{ret} \gets DE_s \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
+       \State $DE_{ret} \gets DE_s \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
-       \Else\r
-               \State $ck_g \gets 0$\Comment{End of KV set}\r
-       \EndIf\r
 \EndIf\r
 \State \Return{$DE_{ret}$}\r
 \EndFunction\r
@@ -642,10 +636,18 @@ $\tuple{ck,\tuple{k, v}} \in KV_s \wedge
 \Procedure{PutDataEntries}{$th_p,m'_p$}\r
 \State $success \gets false$\r
 \While{$\neg success$}\r
+       \State $DE_p \gets \emptyset$\r
        \State $s_p \gets MaxLastSeqN(MS)$\r
+       \State $cp_p \gets cp$\r
        \State $max'_p \gets \Call{CheckResize}{MS,th_p,max'_g,m'_p}$\r
+       \If{$max'_p \neq \emptyset$}\r
+               \State $\tuple{DE_p,cp_p} \gets \Call{AddQueueState}{DE_p,max'_p,cp_p}$\Comment{Add qs}\r
+       \EndIf\r
        \State $need_p \gets \Call{CheckNeedSS}{MS,max'_g}$\r
-       \State $DE_p \gets \Call{GetDEPairs}{KV,max'_p,need_p,sl_{last}}$\r
+       \If{$need_p$}\r
+               \State $\tuple{DE_p,cp_p} \gets \Call{AddSlotSequence}{DE_p,sl_{last},cp_p}$\Comment{Add ss}\r
+       \EndIf\r
+       \State $DE_p \gets \Call{GetKVPairs}{DE_p,KV,cp_p}$\Comment{Add kv pairs}\r
        \State $hmac_{c_p} \gets Hmac(DE_p,SK)$\r
        \State $Dat_p \gets CreateDat(s_p,id_{self},hmac_{p_p},DE_p,hmac_{c_p})$\r
        \State $hmac_{p_p} \gets hmac_{c_p}$\r
@@ -653,13 +655,18 @@ $\tuple{ck,\tuple{k, v}} \in KV_s \wedge
        \State $\tuple{stat_p,SL_p} \gets \Call{PutSlot}{s_p,sv_p,max'_p}$\r
        \State $success \gets stat_p$\r
        \If{$\neg success$}\r
-               \State $cr_p \gets \Call{HandleCollision}{\tuple{stat_p,SL_p}}$\r
+               \State $cr_p \gets \Call{HandleCollision}{SL_p}$\r
        \EndIf\r
        %\If{$need_p$}\r
        %       \State $\tuple{cr_{p_{last}},hmac_{p_p}} \gets \r
        %       \Call{ReinsertLastSlot}{MS,SK,sl_{last},max'_p,hmac_{p_p}}$\r
        %\EndIf\r
 \EndWhile\r
+\If{$|DE_p| = cp$}\Comment{Check and advance $ck_g$}\r
+       \State $ck_g \gets ck_g + cp_s$\Comment{Middle of KV set}\r
+\Else\r
+       \State $ck_g \gets 0$\Comment{End of KV set}\r
+\EndIf\r
 \State $MS \gets \Call{UpdateLastSeqN}{id_{self},s_p,MS}$\r
 \EndProcedure\r
 \end{algorithmic}\r
@@ -745,11 +752,14 @@ 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$. 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)$. \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
+We subsequently prove by induction that $D$ has a message whose path includes $t$.\r
+\begin{itemize}\r
+\item For the base case, $P_{C_1}$ includes $u$, whose path includes $t$. \r
+\item For the inductive step, 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) > 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
+\item 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{itemize}\r
 \end{proof}\r
 \r
 \subsection{Future Work}\r