$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{$id_{self}$ = machine Id of this client} \\\r
\textit{$max_g$ = maximum number of slots (initially $max_g > 0$)} \\\r
\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{$LV$ = live set of $kv$ entries on client, contains \r
+ $\tuple{kv,s}$ entries} \\\r
+\textit{$SS_{live}$ = live set of $ss$ entries on client} \\\r
+\textit{$CR_{live}$ = live set of $cr$ entries on client} \\\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$ = associative array of $\tuple{s, id}$ of all slots in a previous read\r
(initially empty)} \\ \\\r
-\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
$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
+$GetLiveSS(SS_{live},ss_s)= ss$ \textit{such that} $ss \in SS_{live} \r
+\wedge \forall ss_s \in SS_{live}, ss = ss_s$ \\\r
+$GetLiveCR(CR_{live},cr_s)= cr$ \textit{such that} $cr \in CR_{live} \r
+\wedge \forall cr_s \in CR_{live}, cr = cr_s$ \\\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
+$GetKV($key-value data entry$)=\tuple{k_s,v_s} = kv_s$ \\\r
+$GetSS($slot-sequence data entry$)=\tuple{id_s,s_{s_{last}}} = ss_s$ \\\r
$GetQS($queue-state data entry$)=qs_s$ \\\r
-$GetCR($collision-resolution data entry$)=\tuple{s_s,id_s}$ \\\r
+$GetCR($collision-resolution data entry$)=\tuple{s_s,id_s} = cr_s$ \\\r
$GetS(\tuple{s, id})=s$ \\\r
$GetId(\tuple{s, id})=id$ \\\r
$GetKey(\tuple{k, v})=k$ \\\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
+\Function{AddSSLivEnt}{$SS_{s_{live}},de_s$}\r
+\State $ss_s \gets GetSS(de_s)$\r
+\State $ss_t \gets GetLiveSS(SS_{s_{live}},ss_s)$\r
+\If{$ss_t = \emptyset$}\r
+ \State $SS_{s_{live}} \gets SS_{s_{live}} \cup \{ss_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
+\State \Return{$SS_{s_{live}}$}\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
+\Function{AddCRLivEnt}{$CR_{s_{live}},de_s$}\r
+\State $cr_s \gets GetCR(de_s)$\r
+\State $cr_t \gets GetLiveCR(CR_{s_{live}},cr_s)$\r
+\If{$cr_t = \emptyset$}\r
+ \State $CR_{s_{live}} \gets CR_{s_{live}} \cup \{cr_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
+\State \Return{$CR_{s_{live}}$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Function{UpdateSSLivEnt}{$SS_{s_{live}},MS_s$}\r
+\State $s_{s_{min}} \gets MinLastSeqN(MS_s)$\r
+\ForAll{$ss_s \in SS_{s_{live}}$}\r
+ \State $\tuple{id_s,s_{s_{last}}} \gets GetSS(ss_s)$\r
+ \If{$s_{s_{min}} > s_{s_{last}}$}\Comment{Remove if dead}\r
+ \State $SS_{s_{live}} \gets SS_{s_{live}} - \{\tuple{id_s,s_{s_{last}}}\}$ \r
+ \EndIf\r
+\EndFor\r
+\State \Return{$SS_{s_{live}}$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Function{UpdateCRLivEnt}{$CR_{s_{live}},MS_s$}\r
+\State $s_{s_{min}} \gets MinLastSeqN(MS_s)$\r
+\ForAll{$cr_s \in CR_{s_{live}}$}\r
+ \State $\tuple{s_s,id_s} \gets GetCR(cr_s)$\r
+ \If{$s_{s_{min}} > s_s$}\Comment{Remove if dead}\r
+ \State $SS_{s_{live}} \gets SS_{s_{live}} - \{\tuple{s_s,id_s}\}$ \r
+ \EndIf\r
+\EndFor\r
+\State \Return{$CR_{s_{live}}$}\r
\EndFunction\r
\end{algorithmic}\r
\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
+ \State $SS_{live} \gets \Call{AddSSLivEnt}{SS_{live},de_{g_{ss}}}$\r
\EndFor\r
\EndIf\r
\State $DE_{g_{cr}} \gets \Call{GetColRes}{DE_g}$\Comment{Handle cr}\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
+ \State $CR_{live} \gets \Call{AddCRLivEnt}{SS_{live},de_{g_{cr}}}$\r
\EndFor\r
\EndIf\r
\State $sl_{last} \gets \Call{StoreLastSlot}{MS,sl_{last},s_g,sv_g,id_g}$\r
\State \Call{Error}{'Actual queue size exceeds $max_g$'}\r
\EndIf\r
\State $\Call{CheckLastSeqN}{MS_g,MS}$\r
+\State $\Call{UpdateSSLivEnt}{SS_{live},MS}$\r
+\State $\Call{UpdateCRLivEnt}{CR_{live},MS}$\r
\EndProcedure\r
\end{algorithmic}\r
\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{$cs_p$ = counter of $ss \in SS$ for putting pairs (initially 0)} \\\r
+\textit{$cs_g$ = counter of $ss \in SS$ for getting pairs (initially 0)} \\\r
+\textit{$cc_p$ = counter of $cr \in CR$ for putting pairs (initially 0)} \\\r
+\textit{$cc_g$ = counter of $cr \in CR$ for getting pairs (initially 0)} \\\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{$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{$SS$ = set of $\tuple{cs, \tuple{id,s_{last}}}$ of ss entries on client} \\\r
+\textit{$CR$ = set of $\tuple{cc, \tuple{s_{col},id_{col}}}$ of cr entries on client} \\\r
\textit{$SL_p$ = set of returned slots on client} \\\r
-\textit{SK = Secret Key} \\\r
-\textit{$CR$ = set of $cr$ entries on client} \\ \\\r
-\textit{$SS$ = set of $ss$ entries on client} \\ \\\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
+$CreateSS(id_s,s_{s_{last}})=\tuple{id_s,s_{s_{last}}} = ss_s$ \\\r
+$CreateQS(max'_s)=qs_s$ \\\r
+$CreateCR(s_s,id_s)=\tuple{s_s,id_s} = cr_s$ \\\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
$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}{$KV_s,\tuple{k_s,v_s}$}\r
\end{algorithmic}\r
\r
\begin{algorithmic}[1]\r
-\Function{HandleCollision}{$SL_s$}\r
+\Function{HandleCollision}{$SL_s,s_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 $cr_s \gets CreateCR(s_{col},id_{col})$\r
\State $\Call{ProcessSL}{SL_s}$\r
\State \Return{$cr_s$}\r
\EndFunction\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
+ \ElsIf{$de_s = ss$}\r
+ \State $\tuple{id_s,s_{s_{last}}} \gets GetSS(de_s)$\r
+ \State $SS \gets \Call{PutSSPair}{SS,\tuple{id_s,s_{s_{last}}}}$\r
+ \ElsIf{$de_s = cr$}\r
+ \State $\tuple{s_s,id_s} \gets GetCR(de_s)$\r
+ \State $CR \gets \Call{PutCRPair}{CR,\tuple{s_s,id_s}}$\r
+ \ElsIf{$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
\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
+\If{$de_s = kv$}\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 = ss$}\r
+ \State $ss_s \gets GetSS(de_s)$\r
+ \State $ss_l \gets GetLiveSS(SS_{live},ss_s)$\r
+ \If{$ss_l = \emptyset$}\r
+ \State $live \gets false$\r
+ \EndIf\r
+\ElsIf{$de_s = cr$}\r
+ \State $cr_s \gets GetCR(de_s)$\r
+ \State $cr_l \gets GetLiveCR(CR_{live},cr_s)$\r
+ \If{$cr_l = \emptyset$}\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
\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{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
+\Function{PutSSPair}{$SS_s,\tuple{id_s,s_{s_{last}}}$}\Comment{Insert a set of $ss$ entries}\r
+\State $SS_s \gets SS_s \cup \{\tuple{cs_p, \tuple{id_s,s_{s_{last}}}}\}$\r
+\State $cs_p \gets cs_p + 1$\r
+\State \Return{$SS_s$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Function{PutCRPair}{$CR_s,\tuple{s_s,id_s}$}\Comment{Insert a set of $cr$ entries}\r
+\State $CR_s \gets CR_s \cup \{\tuple{cc_p, \tuple{s_s,id_s}}\}$\r
+\State $cc_p \gets cc_p + 1$\r
+\State \Return{$CR_s$}\r
\EndFunction\r
\end{algorithmic}\r
\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{AddColRes}{$DE_s,CR_s,cp_s$}\Comment{Insert a $cr$}\r
+\Function{GetKVPairs}{$DE_s,KV_s,cp_s$}\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
+\If{$|KV_s| \leq cp_s$}\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_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
+\EndIf\r
+\State \Return{$\tuple{DE_{ret}}$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Function{GetSSPairs}{$DE_s,SS_s,cp_s$}\r
+\State $DE_{ret} \gets \emptyset$\r
+\If{$|SS_s| \leq cp_s$}\Comment{$SS$ set can span multiple slots}\r
+ \State $DE_{ret} \gets DE_s \cup\r
+ \{\tuple{id_s,s_{s_{last}}} \mid \tuple{cs_s,\tuple{id_s,s_{s_{last}}}} \in SS_s\}$\r
+\Else\r
+ \State $DE_{ret} \gets DE_s \cup\r
+ \{\tuple{id_s,s_{s_{last}}} \mid \tuple{cs_s,\tuple{id_s,s_{s_{last}}}} \in SS_s,\r
+ cs_g \leq cs_s < cs_g + cp_s\}$\r
+\EndIf\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{GetKVPairs}{$DE_s,KV_s,cp_s$}\r
+\Function{GetCRPairs}{$DE_s,CR_s,cp_s$}\r
\State $DE_{ret} \gets \emptyset$\r
-\If{$|KV_s| \leq cp$}\Comment{$KV$ set can span multiple slots}\r
+\If{$|CR_s| \leq cp_s$}\Comment{$CR$ 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
+ \{\tuple{s_s,id_s} \mid \tuple{cc_s,\tuple{s_s,id_s}} \in CR_s\}$\r
\Else\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
+ \{\tuple{s_s,id_s} \mid \tuple{cc_s,\tuple{s_s,id_s}} \in CR_s,\r
+ cc_g \leq cc_s < cc_g + cp_s\}$\r
\EndIf\r
-\State \Return{$DE_{ret}$}\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
\Procedure{PutDataEntries}{$th_p,m'_p$}\r
-\State $success \gets false$\r
+\State $success_p \gets false$\r
\State $CR_p \gets \emptyset$\r
-\While{$\neg success$}\r
+\While{$\neg success_p$}\r
\State $DE_p \gets \emptyset$\r
\State $s_p \gets MaxLastSeqN(MS)$\r
\State $cp_p \gets cp$\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
+ \If{$SS \neq \emptyset$}\Comment{Add $ss$ entries}\r
+ \State $\tuple{DE_p,cp_p} \gets \Call{GetSSPairs}{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
+ \State $\tuple{DE_p,cp_p} \gets \Call{GetCRPairs}{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 $\tuple{DE_p,cp_p} \gets \Call{GetKVPairs}{DE_p,KV,cp_p}$\Comment{Add $kv$ entries}\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 $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 $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
+ \State $\tuple{success_p,SL_p} \gets \Call{PutSlot}{s_p,sv_p,max'_p}$\r
+ \If{$\neg success_p$}\r
+ \State $cr_p \gets \Call{HandleCollision}{SL_p,s_p}$\r
+ \State $\tuple{s_{p_{col}},id_{p_{col}}} \gets GetCR(cr_p)$\r
+ \State $CR \gets \Call{PutCRPair}{CR,\tuple{s_{p_{col}},id_{p_{col}}}}$\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
+\If{$|DE_p| = cp$}\Comment{Middle of set}\r
+ \State $ck_g \gets ck_g + cp_s$\r
+ \State $cs_g \gets cs_g + |SS|$\r
+ \State $cc_g \gets cc_g + |CR|$\r
+\Else\Comment{End of set}\r
+ \State $ck_g \gets 0$\r
+ \State $cs_g \gets 0$\r
+ \State $cc_g \gets 0$\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 $\Call{CheckLastSlot}{sl_{last}}$\Comment{Get ready to expunge first slot}\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
+ \State $\tuple{id_p,s_{p_{last}}} \gets GetSS(ss_p)$\r
+ \State $SS \gets \Call{PutSSPair}{SS,\tuple{id_p,s_{p_{last}}}}$\Comment{Add ss}\r
\EndIf\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
+%\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
+%\note{General comments... Work on structuring things to improve readability... This include names of functions/variables, how things are partitioned into functions, adding useful comments,...}\r
\r
-\note{Also Missing liveness state definition in algorithm...}\r
+%\note{Also Missing liveness state definition in algorithm...}\r
\r
\r
\subsection{Definitions for Formal Guarantees}\r
projects / iotcloud.git / commitdiff