\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
$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
\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
\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
\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
\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
\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
\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
$\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
$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
\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
\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
\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
+\Function{HandleCollision}{$SL_s$}\r
+\State $\tuple{s_{col},sv_{col}} \gets GetColSeqN(SL_s,s_s)$\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
\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
+\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
-\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
+\begin{algorithmic}[1]\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 \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
\r
\begin{algorithmic}[1]\r
-\Function{GetDEPairs}{$KV_s,max'_s,need_s,sl_s$}\r
+\Function{AddQueSta}{$DE_s,max'_s,cp_s$}\Comment{Insert a $qs$}\r
\State $DE_{ret} \gets \emptyset$\r
-\State $cp_s \gets cp$\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{$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
+\State $qs_s \gets max'_s$\r
+\State $DE_{ret} \gets DE_s \cup qs_s$\r
+\State $cp_s \gets cp_s - 1$\r
+\State \Return{$\tuple{DE_{ret},cp_s}$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\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_s$\r
+\State $cp_s \gets cp_s - |CR_s|$\r
+\State \Return{$\tuple{DE_{ret},cp_s}$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Function{GetKVPairs}{$DE_s,KV_s,cp_s$}\r
+\State $DE_{ret} \gets \emptyset$\r
+\If{$|KV_s| \leq cp$}\Comment{$KV$ set can span multiple slots}\r
+ \State $DE_{ret} \gets DE_s \cup\r
\{\tuple{k_s,v_s} \mid \tuple{ck_s,\tuple{k_s,v_s}} \in KV_s\}$\r
\Else\r
- \State $DE_{ret} \gets DE_{ret} \cup\r
+ \State $DE_{ret} \gets DE_s \cup\r
\{\tuple{k_s,v_s} \mid \tuple{ck_s,\tuple{k_s,v_s}} \in KV_s,\r
ck_g \leq ck_s < ck_g + cp_s\}$\r
- \If{$|DE_{ret}| = cp$}\r
- \State $ck_g \gets ck_g + cp_s$\Comment{Middle of KV set}\r
- \Else\r
- \State $ck_g \gets 0$\Comment{End of KV set}\r
- \EndIf\r
\EndIf\r
\State \Return{$DE_{ret}$}\r
\EndFunction\r
\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 $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 $cp_p \gets cp$\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{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
+ \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
\State $hmac_{p_p} \gets hmac_{c_p}$\r
\State $\tuple{stat_p,SL_p} \gets \Call{PutSlot}{s_p,sv_p,max'_p}$\r
\State $success \gets stat_p$\r
\If{$\neg success$}\r
- \State $cr_p \gets \Call{HandleCollision}{\tuple{stat_p,SL_p}}$\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
+\Else\r
+ \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
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}\r
\r
\begin{proof}\r
+\r
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) > n$ that $C_1$ shares with another client. Then let $T$ be the portion of the path of $u$ ending at index $n$ 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 clients $\mathscr{C} = (C_1, C_2, ..., D)$ from $C_1$ to $D$, where each shares an edge with the next.\r
\r
We prove by induction that $P_D$ has a message whose path includes $t$.\r
\item Inductive step: Each client in $\mathscr{C}$ has a partial message sequence with a message that includes $t$ if the previous client does. 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) > n$. By Lemma 1, $w$ or $x$, whichever has the least sequence number, is in the path of the other, and therefore by Lemma 2, $t$ is in the path of $x$.\r
\r
\item Let $z$ be 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 $z$. Since $t$ is in the path of $z$, every message in $P_D$ with smaller index than $i(t)$ is in $T$. Therefore, $P_D$ is consistent with $T$.\r
+\r
\end{itemize}\r
\end{proof}\r
\r