Completing client algorithm (first complete version); adjusting putting and getting...
authorrtrimana <rtrimana@uci.edu>
Tue, 19 Jul 2016 18:40:34 +0000 (11:40 -0700)
committerrtrimana <rtrimana@uci.edu>
Tue, 19 Jul 2016 18:40:34 +0000 (11:40 -0700)
doc/iotcloud.tex

index 08c71c6..49f0b2a 100644 (file)
@@ -133,8 +133,7 @@ Client can make a request to resize the queue. This is done as a write that comb
 \subsection{Server Algorithm}\r
 $s \in SN$ is a sequence number set\\\r
 $sv \in SV$ is a slot's value\\\r
-$slot_s = \tuple{s, sv} \in SL \subseteq SN \times SV$ \\\r
-\r
+$slot_s = \tuple{s, sv} \in SL \subseteq SN \times SV$ \\ \\\r
 \textbf{State} \\\r
 \textit{SL = set of live slots on server} \\\r
 \textit{max = maximum number of slots (input only for resize message)} \\\r
@@ -185,7 +184,7 @@ $v$ is value of entry \\
 $kv$ is a key-value entry $\tuple{k,v}$, $kv \in D$ \\\r
 $ss$ is a slot sequence entry $\tuple{id,s_{last}}$, \r
 id + last s of a machine, $ss \in D$ \\\r
-$qs$ is a queue state entry, $qs \in D$ \\\r
+$qs$ is a queue state entry (contains $max$ size of queue), $qs \in D$ \\\r
 $cr$ is a collision resolution entry $\tuple{s_{col},id_{col}}$, \r
 s + id of a machine that wins a collision, $cr \in D$ \\\r
 $D = \{kv,ss,qs,cr\}$ \\\r
@@ -197,21 +196,22 @@ $hmac_c$ is the HMAC value of the current slot \\
 $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
-\r
 \textbf{States} \\\r
+\textit{$hmac_{p_g}$ = the HMAC value of the previous slot \r
+($hmac_{p_g} = \emptyset$ for the first slot)} \\\r
+\textit{$id_{self}$ = machine Id of this client} \\\r
+\textit{$max_g$ = maximum number of slots (initially $max_g > 0$)} \\\r
+\textit{m = number of slots on client (initially $m = 0$ and $m \leq n$)} \\\r
+\textit{$sl_{last}$ = info of last slot in queue = \r
+       $\tuple{s_{last},sv_{last},id_{last}}$ (initially $\emptyset$)} \\\r
 \textit{DT = set of $\tuple{k,v}$ on client} \\\r
 \textit{MS = set of $\tuple{id, s_{last}}$ of all clients on client \r
 (initially empty)} \\\r
 \textit{$MS_g$ = set MS to save all $\tuple{id, s_{last}}$ pairs while\r
 traversing DT after a request to server (initially empty)} \\\r
+\textit{SK = Secret Key} \\\r
 \textit{$SM$ = set of $\tuple{s, id}$ of all slots in a previous read\r
-(initially empty)} \\\r
-\textit{$max_g$ = maximum number of slots (initially $max_c > 0$)} \\\r
-\textit{m = number of slots on client (initially $m = 0 and m \leq n$)} \\\r
-\textit{$hmac_{p_g}$ = the HMAC value of the previous slot \r
-($hmac_{p_g} = \emptyset$ for the first slot)} \\\r
-\textit{$id_{self}$ = machine Id of this client} \\\r
-\textit{SK = Secret Key} \\ \\\r
+(initially empty)} \\ \\\r
 \textbf{Helper Functions} \\\r
 $MaxSlot(SL_s)= \tuple{s, sv}$ \textit{such that} $\tuple{s, sv}\r
 \in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s \geq s_s$ \\\r
@@ -221,6 +221,7 @@ $Slot(SL_s,s_s)= \tuple{s, sv}$ \textit{such that} $\tuple{s, sv}
 \in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s = s_s$ \\\r
 $SeqN(\tuple{s, sv})=s$ \\\r
 $SlotVal(\tuple{s, sv})=sv$ \\\r
+$CreateLastSL(s,sv,id)=\tuple{s,sv,id}=sl_{last}$ \\\r
 $Decrypt(SK_s,sv_s)=Dat_s=\tuple{s,id,hmac_p,DE,hmac_c}$ \\\r
 $GetSeqN(Dat_s = \tuple{s,id,hmac_p,DE,hmac_c})=s$ \\\r
 $GetMacId(Dat_s = \tuple{s,id,hmac_p,DE,hmac_c})=id$ \\\r
@@ -241,6 +242,10 @@ $GetKey(\tuple{k, v})=k$ \\
 $GetVal(\tuple{k, v})=v$ \\\r
 $GetKeyVal(DT_s,k_s)= \tuple{k, v}$ \textit{such that} $\tuple{k, v} \r
 \in DT_s \wedge \forall \tuple{k_s, v_s} \in DT_s, k = k_s$ \\\r
+$MaxLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s \r
+\wedge \forall \tuple{id_s, s_{s_{last}}} \in MS_s, s_{last} \geq s_{s_{last}}$ \\\r
+$MinLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s \r
+\wedge \forall \tuple{id_s, s_{s_{last}}} \in MS_s, s_{last} \leq s_{s_{last}}$ \\\r
 \r
 \begin{algorithmic}[1]\r
 \Procedure{ReportError}{$msg$}\r
@@ -305,7 +310,7 @@ $GetKeyVal(DT_s,k_s)= \tuple{k, v}$ \textit{such that} $\tuple{k, v}
 \end{algorithmic}\r
 \r
 \begin{algorithmic}[1]\r
-\Function{GetColRes}{$Dat_s$}\r
+\Function{GetColRes}{$Dat_s$}\Comment{At most 2 $cr$ entries in a slot}\r
 \State $DE_s \gets GetDatEnt(Dat_s)$\r
 \State $de_{cr} \gets de_s$ \textit{such that} $de_s \in DE_s, \r
        de_s \in D \land de_s = cr$\r
@@ -315,7 +320,15 @@ $GetKeyVal(DT_s,k_s)= \tuple{k, v}$ \textit{such that} $\tuple{k, v}
        \State $\tuple{s_{ret},id_{ret}} \r
        \gets \emptyset$\r
 \EndIf\r
-\State \Return{$\tuple{s_{ret},id_{ret}}$}\r
+\State $de_{r_{cr}} \gets de_s$ \textit{such that} $de_s \in DE_s, \r
+       de_s \in D \land de_s = cr \land de_s \neq de_{cr}$\r
+\If{$de_{r_{cr}} \neq \emptyset$}\r
+       \State $\tuple{s_{r_{ret}},id_{r_{ret}}} \gets GetCR(de_{r_{cr}})$\r
+\Else\r
+       \State $\tuple{s_{r_{ret}},id_{r_{ret}}} \r
+       \gets \emptyset$\r
+\EndIf\r
+\State \Return{$\{\tuple{s_{ret},id_{ret}},\tuple{s_{r_{ret}},id_{r_{ret}}}\}$}\r
 \EndFunction\r
 \end{algorithmic}\r
 \r
@@ -356,6 +369,19 @@ $GetKeyVal(DT_s,k_s)= \tuple{k, v}$ \textit{such that} $\tuple{k, v}
 \EndProcedure\r
 \end{algorithmic}\r
 \r
+\begin{algorithmic}[1]\r
+\Procedure{CheckCollision}{$MS_s,SM_s,\tuple{s_s,id_s}$}\r
+\If{$\tuple{s_s,id_s} \neq \emptyset$}\r
+       \State $s_s \gets GetS(\tuple{s_s,id_s})$\r
+       \State $id_s \gets GetId(\tuple{s_s,id_s})$\r
+       \State $s_{s_{last}} \gets GetLastSeqN(MS_s,id_s)$\r
+       \If{$s_{s_{last}} < s_s$}\r
+               \State $\Call{CheckColRes}{SM_s,\tuple{s_s,id_s}}$\r
+       \EndIf\r
+\EndIf\r
+\EndProcedure\r
+\end{algorithmic}\r
+\r
 \begin{algorithmic}[1]\r
 \Procedure{CheckColRes}{$SM_s,\tuple{s_t,id_t}$}\Comment{Check $id_s$ in $SM_s$}\r
 \State $s_t \gets GetS(\tuple{s_t,id_t})$\r
@@ -367,6 +393,16 @@ $GetKeyVal(DT_s,k_s)= \tuple{k, v}$ \textit{such that} $\tuple{k, v}
 \EndProcedure\r
 \end{algorithmic}\r
 \r
+\begin{algorithmic}[1]\r
+\Function{StoreLastSlot}{$MS_s,sl_l,s_s,sv_s,id_s$}\r
+\State $s_{min} \gets MinLastSeqN(MS_s)$\r
+\If{$s_{min} \neq \emptyset \land s_{min} = s_s$}\Comment{$MS$ initially empty}\r
+       \State $sl_l \gets CreateLastSL(s_s,sv_s,id_s)$\r
+\EndIf\r
+\State \Return{$sl_l$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
 \begin{algorithmic}[1]\r
 \Function{UpdateDT}{$DT_s,Dat_s$}\r
 \State $DE_s \gets GetDatEnt(Dat_s)$\r
@@ -415,7 +451,7 @@ $GetKeyVal(DT_s,k_s)= \tuple{k, v}$ \textit{such that} $\tuple{k, v}
        \If{$\neg \Call{ValidHmac}{DE_g,SK,hmac_{c_g}}$}\r
                \State \Call{ReportError}{'Invalid current HMAC value'}\r
        \EndIf\r
-       \State $hmac_{p_g} \gets Hmac(Dat_g,SK)$\Comment{Update $hmac_{p_g}$ for next check}\r
+       \State $hmac_{p_g} \gets Hmac(DE_g,SK)$\Comment{Update $hmac_{p_g}$ for next check}\r
        \State $qs_g \gets \Call{GetQueSta}{Dat_g}$\Comment{Handle qs}\r
        \If{$qs_g \neq \emptyset \land qs_g > max_g$}\r
                \State $max_g \gets qs_g$\r
@@ -428,16 +464,11 @@ $GetKeyVal(DT_s,k_s)= \tuple{k, v}$ \textit{such that} $\tuple{k, v}
        \If{$\tuple{id_d,s_{d_{last}}} \neq \emptyset$}\r
        \State $MS_g \gets \Call{UpdateLastSeqN}{id_d,s_{d_{last}},MS_g}$\r
        \EndIf\r
-       \State $\tuple{s_e,id_e} \gets \r
+       \State $\{\tuple{s_e,id_e},\tuple{s_f,id_f}\} \gets \r
        \Call{GetColRes}{Dat_g}$\Comment{Handle cr}\r
-       \If{$\tuple{s_e,id_e} \neq \emptyset$}\r
-               \State $s_e \gets GetS(\tuple{s_e,id_e})$\r
-               \State $id_e \gets GetId(\tuple{s_e,id_e})$\r
-               \State $s_{c_{last}} \gets GetLastSeqN(MS,id_e)$\r
-               \If{$s_{c_{last}} < s_e$}\r
-                       \State $\Call{CheckColRes}{SM,\tuple{s_e,id_e}}$\r
-               \EndIf\r
-    \EndIf\r
+       \State $\Call{CheckCollision}{MS,SM,\tuple{s_e,id_e}}$\Comment{From normal slot}\r
+       \State $\Call{CheckCollision}{MS,SM,\tuple{s_f,id_f}}$\Comment{From reinsertion}\r
+       \State $sl_{last} \gets \Call{StoreLastSlot}{MS,sl_{last},s_g,sv_g,id_g}$\r
        \State $DT \gets \Call{UpdateDT}{DT,Dat_g}$\r
 \EndFor\r
 \State $SM \gets SM_{curr}$\r
@@ -477,35 +508,41 @@ $DE = \{de \mid de \in D\}$ \\
 $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
-\r
 \textbf{States} \\\r
 \textit{$cp$ = 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
+collision in reinserting the last slot (sent in the following slot)} \\\r
 \textit{$ck_p$ = counter of $kv \in KV$ for putting pairs (initially 0)} \\\r
 \textit{$ck_g$ = counter of $kv \in KV$ for getting pairs (initially 0)} \\\r
-\textit{$id_{self}$ = machine Id of this client} \\\r
 \textit{$hmac_{c_p}$ = the HMAC value of the current slot} \\\r
 \textit{$hmac_{p_p}$ = the HMAC value of the previous slot \r
 ($hmac_{p_p} = \emptyset$ for the first slot)} \\\r
+\textit{$id_{self}$ = machine Id of this client} \\\r
+\textit{$sl_{last}$ = info of last slot in queue = \r
+       $\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{$ST$ = set of $DE$ objects on client} \\\r
 \textit{$SL_p$ = set of returned slots on client} \\\r
-\textit{SK = Secret Key} \\\r
-\r
+\textit{SK = Secret Key} \\ \\\r
 \textbf{Helper Functions} \\\r
 $CreateDat(s,id,hmac_p,DE,hmac_c)=Dat_s=\tuple{s,id,hmac_p,DE,hmac_c}$ \\\r
+$CreateCR(s,id)=\tuple{s,id}$ \\\r
+$CreateQS(max')=qs$ \\\r
+$CreateSS(id,s_{last})=\tuple{id,s_{last}}$ \\\r
 $Encrypt(Dat_s,SK_s)=sv_s$ \\\r
 $GetStatus(\tuple{status,SL})=status$ \\\r
 $GetSL(\tuple{status,SL})=SL$ \\\r
+$GetLastS(sl = \tuple{s,sv,id})=s$ \\\r
+$GetSV(sl = \tuple{s,sv,id})=sv$ \\\r
+$GetID(sl = \tuple{s,sv,id})=id$ \\\r
 $GetColSeqN(SL_s,s_s)= \tuple{s, sv}$ \textit{such that} $\tuple{s, sv}\r
 \in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s = s_s$ \\\r
-$CreateCR(s,id)=\tuple{s,id}$ \\\r
 $GetKV(KV_s,k_s)= \tuple{ck,\tuple{k, v}}$ \textit{such that} \r
 $\tuple{ck,\tuple{k, v}} \in KV_s \wedge\r
 \forall \tuple{ck_s,\tuple{k_s, v_s}} \in KV_s, k = k_s$ \\\r
-$MaxLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s \r
-\wedge \forall \tuple{id_s, s_{s_{last}}} \in MS_s, s_{last} \geq s_{s_{last}}$ \\\r
 \r
 \begin{algorithmic}[1]\r
 \Function{PutKVPair}{$KV_s,\tuple{k_s,v_s}$}\r
@@ -523,14 +560,92 @@ $MaxLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s
 \end{algorithmic}\r
 \r
 \begin{algorithmic}[1]\r
-\Function{GetDEPairs}{$KV_s$}\r
+\Function{CheckResize}{$MS_s,th_s,max'_t,m'_s$}\r
+\State $s_{last_{min}} \gets MinLastSeqN(MS_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} \leq th_s$}\r
+       \State $max'_s \gets max'_t + m'_s$\r
+\Else\r
+       \State $max'_s \gets \emptyset$\r
+\EndIf\r
+\State \Return{$max'_s$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Function{CheckNeedSS}{$MS_s,max'_t$}\Comment{Check if $ss$ is needed}\r
+\State $s_{last_{min}} \gets MinLastSeqN(MS_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
+\EndFunction\r
+\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
+\State $\Call{ProcessSL}{SL_s}$\r
+\State \Return{$cr_s$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Function{ReinsertLastSlot}{$need_s,sl_{s_{last}},max'_s$}\r
+\If{$need_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
+\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
-\If{$cr_p \neq \emptyset$}\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{$|KV_s| \leq cp$}\Comment{KV set can extend multiple slots based on $cp$}\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
        \{\tuple{k_s,v_s} \mid \tuple{ck_s,\tuple{k_s,v_s}} \in KV_s\}$\r
 \Else\r
@@ -548,30 +663,19 @@ $MaxLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s
 \end{algorithmic}\r
 \r
 \begin{algorithmic}[1]\r
-\Function{PutDataEntries}{$max'_p$}\r
+\Procedure{PutDataEntries}{$th_p,m'_p$}\r
 \State $s_p \gets MaxLastSeqN(MS)$\r
-\State $DE_p \gets GetDEPairs(KV)$\r
+\State $max'_p \gets \Call{CheckResize}{MS,th_p,max'_g,m'_p}$\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
 \State $hmac_{c_p} \gets Hmac(DE_p,SK)$\r
-\State $Dat_p \gets CreateSlot(s_p,id_{self},hmac_{p_p},DE_p,hmac_{c_p})$\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
 \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 $stat_p \gets GetStatus(\tuple{stat_p,SL_p})$\r
-\State $SL_p \gets GetSL(\tuple{stat_p,SL_p})$\r
-\If{$\neg stat_p$}\Comment{Handle collision}\r
-       \State $\tuple{s_{col},sv_{col}} \gets GetColSeqN(SL_p,s_p)$\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_p \gets \tuple{s_{col},id_{col}}$\r
-\Else\r
-       \State $cr_p \gets \emptyset$\r
-\EndIf\r
-\State $\Call{ProcessSL}{SL_p}$\r
-\State \Return{$ST$}\r
-\EndFunction\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
+\EndProcedure\r
 \end{algorithmic}\r
 \r
 \subsection{Formal Guarantees}\r