\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
$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
$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
\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
$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
\EndProcedure\r
\end{algorithmic}\r
\r
+\note{Don't include ``such that'' in the argument of a function...}\r
+\r
\begin{algorithmic}[1]\r
\Function{ValidHmac}{$DE_s,SK_s,hmac_{stored}$}\r
\State $hmac_{computed} \gets Hmac(DE_s,SK_s)$\r
-\If{$hmac_{stored} = hmac_{computed}$}\r
- \State $valid \gets true$\r
-\Else\r
- \State $valid \gets false$\r
-\EndIf\r
-\State \Return{$valid$}\r
+\State \Return {$hmac_{stored} = hmac_{computed}$}\r
\EndFunction\r
\end{algorithmic}\r
\r
\begin{algorithmic}[1]\r
\Function{ValidPrevHmac}{$DE_s,hmac_{p_s},hmac_{p_{sto}}$}\r
\If{$hmac_{p_s} = \emptyset$}\Comment{First slot - no previous HMAC}\r
- \State $valid \gets true$\r
+ \State \Return $true$\r
\Else\r
- \If{$hmac_{p_{sto}} = hmac_{p_s}$}\r
- \State $valid \gets true$\r
- \Else\r
- \State $valid \gets false$\r
- \EndIf\r
+ \State \Return {$hmac_{p_{sto}} = hmac_{p_s}$}\r
\EndIf\r
-\State \Return{$valid$}\r
\EndFunction\r
\end{algorithmic}\r
\r
+\note{So if a slot has a null previous hmac, everything is fine? What if it isn't the first slot?}\r
+\r
\begin{algorithmic}[1]\r
\Function{GetQueSta}{$Dat_s$}\r
\State $DE_s \gets GetDatEnt(DE_s)$\r
\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
\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
\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
\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
\ForAll{$de_s \in DE_s$}\r
\If{$de_s$ \textit{such that} $de_s \in D \land de_s = kv$}\r
\State $\tuple{k_s,v_s} \gets GetKV(de_s)$\r
- \State $k_s \gets GetKey(\tuple{k_s,v_s})$\r
\State $\tuple{k_s,v_t} \gets GetKeyVal(DT_s,k_s)$\r
\If{$\tuple{k_s,v_t} = \emptyset$}\r
\State $DT_s \gets DT_s \cup \{\tuple{k_s,v_s}\}$\r
\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
\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
\Function{GetValFromKey}{$k_g$}\r
\State $\tuple{k_s,v_s} \gets \tuple{k,v}$ \textit{such that} $\tuple{k,v} \r
\in DT \land k = k_g$\r
-\State $v_s \gets GetVal(\tuple{k_s,v_s})$\r
\State \Return{$v_s$}\r
\EndFunction\r
\end{algorithmic}\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
-\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
-\State $k_s \gets GetKey(\tuple{k_s,v_s})$\r
-\State $\tuple{ck_s,\tuple{k_s,v_t}} \gets GetKV(KV_s,k_s)$\r
+\Function{PutKVPair}{$\tuple{k_s,v_s}$}\r
+\State $\tuple{ck_s,\tuple{k_s,v_t}} \gets GetKV(KV,k_s)$\r
\If{$\tuple{ck_s,\tuple{k_s,v_t}} = \emptyset$}\r
- \State $KV_s \gets KV_s \cup \{\tuple{ck_p, \tuple{k_s,v_s}}\}$\r
+ \State $KV \gets KV \cup \{\tuple{ck_p, \tuple{k_s,v_s}}\}$\r
\State $ck_p \gets ck_p + 1$\r
\Else\r
- \State $KV_s \gets (KV_s - \{\tuple{ck_s, \tuple{k_s,v_t}}\}) \cup \r
+ \State $KV \gets (KV - \{\tuple{ck_s, \tuple{k_s,v_t}}\}) \cup \r
\{\tuple{ck_s, \tuple{k_s,v_s}}\}$\r
\EndIf\r
\State \Return{$KV_s$}\r
\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
+\State \Return {$n_{dead} = 0$}\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}{$MS_s,SK_s,sl_{s_{last}},max'_s,hmac_{p_s}$}\r
+\State $s_s \gets MaxLastSeqN(MS_s)$\r
+\State $sv_s \gets GetSV(sl_{s_{last}})$\r
+\State $Dat_s \gets Decrypt(SK,sv_s)$\r
+\State $DE_s \gets GetDatEnt(Dat_s)$\r
+\State $hmac_{c_s} \gets Hmac(DE_s,SK_s)$\r
+\State $Dat_s \gets CreateDat(s_s,id_{self},hmac_{p_s},DE_p,hmac_{c_s})$\r
+\State $hmac_{p_s} \gets hmac_{c_s}$\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
+\State \Return{$\tuple{cr_s,hmac_{p_p}}$}\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 if $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
-\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
\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
+\State $cr_p \gets \Call{HandleCollision}{\tuple{stat_p,SL_p}}$\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
-\State $\Call{ProcessSL}{SL_p}$\r
-\State \Return{$ST$}\r
-\EndFunction\r
+\EndProcedure\r
\end{algorithmic}\r
\r
+\note{Lots of problems with PutDataEntries: (1) What happens if lose network connectivity after adding the key value pair, but before reinserting the last slot? You probably need to create space first and then insert your data entry... (2) What if reinsertlastslot kicks something else important out? What if the server rejects our update because it is out of date? At the very least, any putdataentries function w/o a loop is wrong!}\r
+\r
+\note{General comments... Work on structuring things to improve\r
+ readability... This include names of functions/variables, how\r
+ things are partitioned into functions, adding useful comments,...}\r
+\r
+\r
\subsection{Formal Guarantees}\r
\r
\textit{To be completed ...}\r
projects / iotcloud.git / blobdiff