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