Adding liveness and more states - half baked, need to recheck the states, especially...

diff --git a/doc/iotcloud.tex b/doc/iotcloud.tex
index 5276310492b90a4eaefb44ca1c8ff39266888c79..a795fa88804a7930b7bc04e28625590bacd3aae0 100644 (file)
--- a/doc/iotcloud.tex
+++ b/doc/iotcloud.tex
@@ -209,6 +209,8 @@ $sv_s = \tuple{s, E(Dat_s)} =
 \textit{DT = set of $\tuple{k,v}$ on client} \\\r
 \textit{MS = associative array of $\tuple{id, s_{last}}$ of all clients on client \r
 (initially empty)} \\\r
+\textit{$LV$ = live set of $de$ entries on client, contains \r
+       $\tuple{de,s}$ entries} \\\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
@@ -231,6 +233,8 @@ $GetMacId(Dat_s = \tuple{s,id,hmac_p,DE,hmac_c})=id$ \\
 $GetPrevHmac(Dat_s = \tuple{s,id,hmac_p,DE,hmac_c})=hmac_p$ \\\r
 $GetCurrHmac(Dat_s = \tuple{s,id,hmac_p,DE,hmac_c})=hmac_c$ \\\r
 $GetDatEnt(Dat_s = \tuple{s,id,hmac_p,DE,hmac_c})=DE$ \\\r
+$GetLivEntLastS(LV_s,de_s)= s$ \textit{such that} $\tuple{de, s} \in LV_s \r
+\wedge \forall \tuple{de_s, s_s} \in LV_s, de_s = de$ \\\r
 $GetKV($key-value data entry$)=\tuple{k_s,v_s}$ \\\r
 $GetSS($slot-sequence data entry$)=\tuple{id,s_{last}}$ \\\r
 $GetQS($queue-state data entry$)=qs_s$ \\\r
@@ -271,8 +275,7 @@ $MinLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s
 \end{algorithmic}\r
 \r
 \begin{algorithmic}[1]\r
-\Function{GetQueSta}{$Dat_s$}\r
-\State $DE_s \gets GetDatEnt(DE_s)$\r
+\Function{GetQueSta}{$DE_s$}\r
 \State $de_{qs} \gets de_s$ \textit{such that} $de_s \in DE_s, \r
        de_s \in D \land de_s = qs$\r
 \If{$de_{qs} \neq \emptyset$}\r
@@ -285,40 +288,16 @@ $MinLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s
 \end{algorithmic}\r
 \r
 \begin{algorithmic}[1]\r
-\Function{GetSlotSeq}{$Dat_s$}\r
-\State $DE_s \gets GetDatEnt(Dat_s)$\r
-\State $de_{ss} \gets de_s$ \textit{such that} $de_s \in DE_s, \r
-       de_s \in D \land de_s = ss$\r
-\If{$de_{ss} \neq \emptyset$}\r
-       \State $\tuple{id_{ret},s_{last_{ret}}} \gets GetSS(de_{ss})$\r
-\Else\r
-       \State $\tuple{id_{ret},s_{last_{ret}}} \gets \emptyset$\r
-\EndIf\r
-\State \Return{$\tuple{id_{ret},s_{last_{ret}}}$}\r
+\Function{GetSlotSeq}{$DE_s$}\r
+\State $DE_{ss} \gets \{de_s | de_s \in DE_s, de_s \in D \land de_s = ss\}$\r
+\State \Return{$DE_{ss}$}\r
 \EndFunction\r
 \end{algorithmic}\r
 \r
 \begin{algorithmic}[1]\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
-\If{$de_{cr} \neq \emptyset$}\r
-       \State $\tuple{s_{ret},id_{ret}} \gets GetCR(de_{cr})$\r
-\Else\r
-       \State $\tuple{s_{ret},id_{ret}} \r
-       \gets \emptyset$\r
-\EndIf\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
-\State \Return{$\{\tuple{s_{ret},id_{ret}}\}$}\r
+\Function{GetColRes}{$DE_s$}\r
+\State $DE_{cr} \gets \{de_s | de_s \in DE_s, de_s \in D \land de_s = cr\}$\r
+\State \Return{$DE_{cr}$}\r
 \EndFunction\r
 \end{algorithmic}\r
 \r
@@ -334,6 +313,51 @@ $MinLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s
 \EndFunction\r
 \end{algorithmic}\r
 \r
+\begin{algorithmic}[1]\r
+\Function{UpdateKVLivEnt}{$LV_s,de_s,s_s$}\r
+\State $s_t \gets GetLivEntLastS(LV_s,de_s)$\r
+\If{$s_t = \emptyset$}\r
+       \State $LV_s \gets LV_s \cup \{\tuple{de_s,s_s}\}$\Comment{First occurrence}\r
+\Else\r
+       \If{$s_s > s_t$}\Comment{Update entry with a later s}\r
+               \State $LV_s \gets (LV_s - \{\tuple{de_s,s_t}\}) \cup \r
+               \{\tuple{de_s,s_s}\}$\r
+       \EndIf\r
+\EndIf\r
+\State \Return{$LV_s$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Function{UpdateSSLivEnt}{$LV_s,MS_s,de_s$}\r
+\State $s_t \gets GetLivEntLastS(LV_s,de_s)$\r
+\If{$s_t = \emptyset$}\r
+       \State $LV_s \gets LV_s \cup \{\tuple{de_s,s_s}\}$\Comment{First occurrence}\r
+\EndIf\r
+\State $\tuple{id_s,s_{s_{last}}} \gets GetSS(de_s)$\r
+\State $s_t \gets MS_s[id_s]$\r
+\If{$s_t > s_{s_{last}}$}\Comment{Remove if dead}\r
+       \State $LV_s \gets LV_s - \{\tuple{de_s,s_{s_{last}}}\}$        \r
+\EndIf\r
+\State \Return{$LV_s$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Function{UpdateCRLivEnt}{$LV_s,MS_s,de_s$}\r
+\State $s_t \gets GetLivEntLastS(LV_s,de_s)$\r
+\If{$s_t = \emptyset$}\r
+       \State $LV_s \gets LV_s \cup \{\tuple{de_s,s_s}\}$\Comment{First occurrence}\r
+\EndIf\r
+\State $\tuple{s_s,id_s} \gets GetCR(de_s)$\r
+\State $s_t \gets MinLastSeqN(MS_s)$\r
+\If{$s_t > s_s$}\Comment{Remove if dead}\r
+       \State $LV_s \gets LV_s - \{\tuple{de_s,s_s}\}$ \r
+\EndIf\r
+\State \Return{$LV_s$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
 \begin{algorithmic}[1]\r
 \Procedure{CheckLastSeqN}{$MS_s,MS_t$}\Comment{Check $MS_t$ based on the newer $MS_s$}\r
 \For {$\tuple{id, s_t}$ in $MS_t$}\r
@@ -384,9 +408,9 @@ $MinLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s
 \end{algorithmic}\r
 \r
 \begin{algorithmic}[1]\r
-\Function{UpdateDT}{$DT_s,Dat_s$}\r
-\State $DE_s \gets GetDatEnt(Dat_s)$\r
+\Function{UpdateDT}{$DT_s,DE_s,LV_s,s_s$}\r
 \ForAll{$de_s \in DE_s$}\r
+       \State $LV_s \gets \Call{UpdateKVLivEnt}{LV_s,de_s,s_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 $\tuple{k_s,v_t} \gets GetKeyVal(DT_s,k_s)$\r
@@ -427,7 +451,7 @@ $MinLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s
                \State \Call{Error}{'Invalid current HMAC value'}\r
        \EndIf\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
+       \State $qs_g \gets \Call{GetQueSta}{DE_g}$\Comment{Handle qs}\r
        \If{$qs_g \neq \emptyset \land qs_g > max_g$}\r
                \State $max_g \gets qs_g$\r
        \EndIf\r
@@ -435,17 +459,24 @@ $MinLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s
        \State $id_g \gets GetMacId(Dat_g)$\Comment{Handle last s}\r
        \State $MS_g \gets \Call{UpdateLastSeqN}{id_g,s_g,MS_g}$\r
     %Check for last s in DE in Dat\r
-    \State $\tuple{id_d,s_{d_{last}}} \gets \Call{GetSlotSeq}{Dat_g}$\Comment{Handle ss}\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
+       \State $DE_{g_{ss}} \gets \Call{GetSlotSeq}{DE_g}$\Comment{Handle ss}\r
+       \If{$DE_{g_{ss}} \neq \emptyset$}\r
+               \ForAll{$de_{g_{ss}} \in DE_{g_{ss}}$}\r
+                       \State $\tuple{id_d,s_{d_{last}}} \gets GetSS(de_{g_{ss}})$\r
+                       \State $MS_g \gets \Call{UpdateLastSeqN}{id_d,s_{d_{last}},MS_g}$\r
+                       \State $LV \gets \Call{UpdateSSLivEnt}{LV,MS,de_{g_{ss}}}$\r
+               \EndFor\r
+       \EndIf\r
+       \State $DE_{g_{cr}} \gets \Call{GetColRes}{DE_g}$\Comment{Handle cr}\r
+       \If{$DE_{g_{cr}} \neq \emptyset$}\r
+               \ForAll{$de_{g_{cr}} \in DE_{g_{cr}}$}\r
+                       \State $\tuple{s_e,id_e} \gets GetCR(de_{g_{cr}})$\r
+                       \State $\Call{CheckCollision}{MS,SM,\tuple{s_e,id_e}}$\r
+                       \State $LV \gets \Call{UpdateCRLivEnt}{LV,MS,de_{g_{cr}}}$\r
+               \EndFor\r
        \EndIf\r
-       %\State $\{\tuple{s_e,id_e},\tuple{s_f,id_f}\} \gets \r
-    %  \Call{GetColRes}{Dat_g}$\Comment{Handle cr}\r
-       \State $\{\tuple{s_e,id_e}\} \gets \Call{GetColRes}{Dat_g}$\Comment{Handle cr}\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
+       \State $DT \gets \Call{UpdateDT}{DT,DE_g,LV,s_g}$\r
 \EndFor\r
 \State $SM \gets SM_{curr}$\r
 \If{$m + |SL_g| \leq max_g$}\Comment{Check actual size against $max_g$}\r
@@ -499,9 +530,18 @@ collision in reinserting the last slot (sent in the following slot)} \\
        $\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{$reinsert_{qs}$ = boolean to decide $qs$($max_g$) reinsertion} \\\r
 \textit{$KV$ = set of $\tuple{ck, \tuple{k,v}}$ of kv entries on client} \\\r
+%\textit{$LV_{kv}$ = live set of $kv$ entries on client, contains a few \r
+%      $\tuple{kv,s_{last}}$ entries} \\\r
+%\textit{$LV_{ss}$ = live set of $ss$ entries on client, contains a few \r
+%      $\tuple{ss,s_{last}}$ entries} \\\r
+%\textit{$LV_{cr}$ = live set of $cr$ entries on client, contains a few \r
+%      $\tuple{cr,s_{last}}$ entries} \\\r
 \textit{$SL_p$ = set of returned slots on client} \\\r
-\textit{SK = Secret Key} \\ \\\r
+\textit{SK = Secret Key} \\\r
+\textit{$CR$ = set of $cr$ entries on client} \\ \\\r
+\textit{$SS$ = set of $ss$ entries on client} \\ \\\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
@@ -515,18 +555,24 @@ $GetSV(sl = \tuple{s,sv,id})=sv$ \\
 $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
-$GetKV(KV_s,k_s)= \tuple{ck,\tuple{k, v}}$ \textit{such that} \r
+$GetKVPair(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
+%$GetKVLastSeqN(LV_{kv},kv_s)= s_{last}$ \textit{such that} $\tuple{kv, s_{last}} \in LV_{kv} \r
+%\wedge \forall \tuple{kv_s, s_{s_{last}}} \in LV_{kv}, s_{last} \geq s_{s_{last}}$ \\\r
+%$GetSSLastSeqN(LV_{ss},ss_s)= s_{last}$ \textit{such that} $\tuple{ss, s_{last}} \in LV_{ss} \r
+%\wedge \forall \tuple{ss_s, s_{s_{last}}} \in LV_{ss}, s_{last} \geq s_{s_{last}}$ \\\r
+%$GetCRLastSeqN(LV_{cr},cr_s)= s_{last}$ \textit{such that} $\tuple{cr, s_{last}} \in LV_{cr} \r
+%\wedge \forall \tuple{cr_s, s_{s_{last}}} \in LV_{cr}, s_{last} \geq s_{s_{last}}$ \\\r
 \r
 \begin{algorithmic}[1]\r
-\Function{PutKVPair}{$\tuple{k_s,v_s}$}\r
-\State $\tuple{ck_s,\tuple{k_s,v_t}} \gets GetKV(KV,k_s)$\r
+\Function{PutKVPair}{$KV_s,\tuple{k_s,v_s}$}\r
+\State $\tuple{ck_s,\tuple{k_s,v_t}} \gets GetKVPair(KV,k_s)$\r
 \If{$\tuple{ck_s,\tuple{k_s,v_t}} = \emptyset$}\r
-       \State $KV \gets KV \cup \{\tuple{ck_p, \tuple{k_s,v_s}}\}$\r
+       \State $KV_s \gets KV_s \cup \{\tuple{ck_p, \tuple{k_s,v_s}}\}$\r
        \State $ck_p \gets ck_p + 1$\r
 \Else\r
-       \State $KV \gets (KV - \{\tuple{ck_s, \tuple{k_s,v_t}}\}) \cup \r
+       \State $KV_s \gets (KV_s - \{\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
@@ -534,13 +580,13 @@ $\tuple{ck,\tuple{k, v}} \in KV_s \wedge
 \end{algorithmic}\r
 \r
 \begin{algorithmic}[1]\r
-\Function{CheckResize}{$MS_s,th_s,max'_t,m'_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
+\State $n_{live} \gets s_{last_{max}} - s_{last_{min}} + 1$\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
+       \State $max'_s \gets max_t + m'_s$\r
 \Else\r
        \State $max'_s \gets \emptyset$\r
 \EndIf\r
@@ -549,11 +595,11 @@ $\tuple{ck,\tuple{k, v}} \in KV_s \wedge
 \end{algorithmic}\r
 \r
 \begin{algorithmic}[1]\r
-\Function{CheckNeedSS}{$MS_s,max'_t$}\Comment{Check if $ss$ is needed}\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 $n_{dead} \gets max_t - n_{live}$\r
 \State \Return {$n_{dead} = 0$}\r
 \EndFunction\r
 \end{algorithmic}\r
@@ -571,29 +617,67 @@ $\tuple{ck,\tuple{k, v}} \in KV_s \wedge
 \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
+\Procedure{CheckLastSlot}{$sl_{s_{last}}$}\r
+\State $s_s \gets GetLastS(sl_{s_{last}})$\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
+\ForAll{$de_s \in DE_s$}\r
+       \State $live \gets \Call{CheckLiveness}{s_s,de_s}$\r
+       \If{$live$}\r
+               \If{$de_s = kv$}\r
+                       \State $\tuple{k_s,v_s} \gets GetKV(de_s)$\r
+                       \State $KV \gets \Call{PutKVPair}{KV,\tuple{k_s,v_s}}$\r
+               \EndIf\r
+               \If{$de_s = ss$}\r
+                       \State $ss_s \gets GetSS(de_s)$\r
+                       \State $SS \gets SS \cup ss_s$\r
+               \EndIf\r
+               \If{$de_s = qs$}\r
+                       \State $reinsert_{qs} \gets true$\r
+               \EndIf\r
+               \If{$de_s = cr$}\r
+                       \State $cr_s \gets GetCR(de_s)$\r
+                       \State $CR \gets CR \cup cr_s$\r
+               \EndIf\r
+       \EndIf\r
+\EndFor\r
+\EndProcedure\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Function{CheckLiveness}{$s_s,de_s$}\r
+\State $live \gets true$\r
+\If{$de_s = kv \lor de_s = ss \lor de_s = cr$}\r
+       \State $s_l \gets GetLivEntLastS(LV,de_s)$\r
+       \If{$s_l = \emptyset \lor s_s < s_l$}\r
+               \State $live \gets false$\r
+       \EndIf\r
+\ElsIf{$de_s = qs$}\r
+       \State $qs_s \gets GetQS(de_s)$\r
+       \If{$qs_s \neq max_g$}\r
+               \State $live \gets false$\r
+       \EndIf\r
+\Else\r
+       \State \Call{Error}{'Unrecognized $de$ type'}\r
+\EndIf\r
+\State \Return{$live$}\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
 \begin{algorithmic}[1]\r
-\Function{AddSlotSeq}{$DE_s,sl_s,cp_s$}\Comment{Insert a $ss$}\r
-\State $DE_{ret} \gets \emptyset$\r
+\Function{CreateSlotSeq}{$sl_s$}\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{ss_s}$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Function{AddSlotSeq}{$DE_s,SS_s,cp_s$}\Comment{Insert a $ss$}\r
+\State $DE_{ret} \gets DE_s \cup SS_s$\r
+\State $cp_s \gets cp_s - |SS_s|$\r
 \State \Return{$\tuple{DE_{ret},cp_s}$}\r
 \EndFunction\r
 \end{algorithmic}\r
@@ -609,10 +693,10 @@ $\tuple{ck,\tuple{k, v}} \in KV_s \wedge
 \end{algorithmic}\r
 \r
 \begin{algorithmic}[1]\r
-\Function{AddCollRes}{$DE_s,cr_p,cp_s$}\Comment{Insert a $cr$}\r
+\Function{AddColRes}{$DE_s,CR_s,cp_s$}\Comment{Insert a $cr$}\r
 \State $DE_{ret} \gets \emptyset$\r
-\State $DE_{ret} \gets DE_s \cup cr_p$\r
-\State $cp_s \gets cp_s - 1$\r
+\State $DE_{ret} \gets DE_s \cup CR_s$\r
+\State $cp_s \gets cp_s - |CR_s|$\r
 \State \Return{$\tuple{DE_{ret},cp_s}$}\r
 \EndFunction\r
 \end{algorithmic}\r
@@ -635,18 +719,31 @@ $\tuple{ck,\tuple{k, v}} \in KV_s \wedge
 \begin{algorithmic}[1]\r
 \Procedure{PutDataEntries}{$th_p,m'_p$}\r
 \State $success \gets false$\r
+\State $CR_p \gets \emptyset$\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
+       \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
+               \State $\tuple{DE_p,cp_p} \gets \Call{AddQueSta}{DE_p,max'_p,cp_p}$\Comment{Add qs}\r
+       \Else\Comment{Check if there is $qs$ reinsertion}\r
+               \If{$reinsert_{qs}$}\r
+                       \State $\tuple{DE_p,cp_p} \gets \Call{AddQueSta}{DE_p,max_g,cp_p}$\r
+                       \State $reinsert_{qs} \gets false$\r
+               \EndIf\r
+       \EndIf\r
+       \If{$SS \neq \emptyset$}\Comment{Reinsert $ss$ entries}\r
+               %\State $\tuple{DE_p,cp_p} \gets \Call{ReinsertSS}{DE_p,SS,cp_p}$\r
+               \State $\tuple{DE_p,cp_p} \gets \Call{AddSlotSeq}{DE_p,SS,cp_p}$\r
        \EndIf\r
-       \State $need_p \gets \Call{CheckNeedSS}{MS,max'_g}$\r
-       \If{$need_p$}\r
-               \State $\tuple{DE_p,cp_p} \gets \Call{AddSlotSequence}{DE_p,sl_{last},cp_p}$\Comment{Add ss}\r
+       \If{$CR \neq \emptyset$}\Comment{Add $cr$ entries}\r
+               \State $\tuple{DE_p,cp_p} \gets \Call{AddColRes}{DE_p,CR,cp_p}$\r
        \EndIf\r
+       %\State $need_p \gets \Call{CheckNeedSS}{MS,max_g}$\r
+       %\If{$need_p$}\r
+       %       \State $\tuple{DE_p,cp_p} \gets \Call{AddSlotSeq}{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
@@ -656,11 +753,8 @@ $\tuple{ck,\tuple{k, v}} \in KV_s \wedge
        \State $success \gets stat_p$\r
        \If{$\neg success$}\r
                \State $cr_p \gets \Call{HandleCollision}{SL_p}$\r
+               \State $CR_p \gets CR_p \cup cr_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
@@ -668,6 +762,14 @@ $\tuple{ck,\tuple{k, v}} \in KV_s \wedge
        \State $ck_g \gets 0$\Comment{End of KV set}\r
 \EndIf\r
 \State $MS \gets \Call{UpdateLastSeqN}{id_{self},s_p,MS}$\r
+\State $SS \gets \emptyset$\r
+\State $CR \gets CR_p$\r
+\State $need_p \gets \Call{CheckNeedSS}{MS,max_g}$\r
+\If{$need_p$}\r
+       \State $ss_p \gets \Call{CreateSlotSeq}{sl_{last}}$\r
+       \State $SS \gets SS \cup ss_p$\Comment{Add ss}\r
+       \State $\Call{CheckLastSlot}{sl_{last}}$\Comment{SL on server is full}\r
+\EndIf\r
 \EndProcedure\r
 \end{algorithmic}\r
 \r