From: rtrimana <rtrimana@uci.edu>
Date: Wed, 3 Aug 2016 00:04:43 +0000 (-0700)
Subject: Dividing data entry formation into smaller functions, fixing loop for PutDataEntries... 
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=8fad98f5ce9687a1d535a4dfc0da98f44c45f1a6;p=iotcloud.git

Dividing data entry formation into smaller functions, fixing loop for PutDataEntries function
---

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