-\subsection{Formal Guarantees}\r
-\r
-\textit{To be completed ...}\r
-\r
-\begin{defn}[System Execution]\r
-Let \\\r
-\begin{center}\r
-$Q = \{slot_{sn_1}, slot_{sn_2}, \dots, Slot_{sn_n}\}$, \\\r
-$SN = \{sn_1, sn_2, \dots, sn_n\}$ \\\r
-\end{center}\r
-denote a queue $Q$ of $n$ slots, with each slot entry being denoted by a\r
-valid sequence number $sn_i \in SN$. $Q$ represents a total order of all \r
-slot updates from all corresponding machines.\r
-%\textit{Formalize a system execution as a sequence of slot updates...\r
-%There is a total order of all slot updates.}\r
-\end{defn}\r
-\r
-\begin{defn}[Transitive Closure]\r
-A transitive closure $\tau : \tau = \epsilon_{update(slot_i)} R $\r
-$\epsilon_{receive(slot_i)}$ is a relation from slot update event\r
-$\epsilon$ to a slot receive event $\epsilon$ for $slot_i$.\r
-%Define transitive closure relation for slot updates... There is an\r
-%edge from a slot update to a slot receive event if the receive event\r
-%reads from the update event.\r
-\end{defn}\r
-\r
-\begin{defn}[Suborder]\r
-Let \\\r
-\begin{center}\r
-$q = \{slot_{i}, slot_{i+1}, \dots, slot_{j}\}, \r
-sn_1 \leq i \leq j \leq sn_n \Longrightarrow q \subseteq Q$\r
-\end{center}\r
-denote a suborder of the total order. Set q is a sequence of contiguous\r
-slot updates that is a subset of a total order of all slot updates in Q.\r
-%Define suborder of total order. It is a sequence of contiguous slots\r
-%updates (as observed by a given device).\r
-\end{defn}\r
-\r
-\begin{defn}[Prefix of a suborder]\r
-Given a suborder \\ \r
-\begin{center}\r
-$q' = \{slot_{i}, slot_{i+1}, \dots, slot_{j}, \dots\}, \r
-sn_1 \leq i \leq j \leq sn_n \Longrightarrow \r
-q' \subseteq Q$\r
-\end{center}\r
-with $slot_{j}$ as a slot update in $q'$, the prefix of $q'$ is a sequence \r
-of all slot updates $\{slot_{i}, slot_{i+1}, \dots, slot_{j-1}\} \cup\r
-slot_{j}$.\r
-%Given a sub order $o=u_{i},u_{i+1},...,u_j, u_{j+i},..., u', ...$ and\r
-%a slot update $u'$ in $o$, the prefix of $o$ is a sequence of all\r
-%updates that occur before $u'$ and $u'$.\r
-\end{defn}\r
-\r
-\begin{defn}[Consistency between a suborder and a total order]\r
-A suborder $q'$ is consistent with a total order $T$ of $Q$, if all\r
-updates in $q'$ appear in $T$ and they appear in the same order, as \r
-the following:\r
-\begin{center}\r
-$q' = \{slot_{i}, slot_{i+1}, \dots, slot_{j}\},$\r
-$T = \{slot_{sn_1}, \dots, slot_{i}, slot_{i+1}, \dots, slot_{j}, \dots,\r
-slot_{sn_n}\},$ \\ $sn_1 \leq i \leq j \leq sn_n \Longrightarrow\r
-q' \subseteq T$\r
-\end{center}\r
-%A suborder $o$ is consistent with a total order $t$, if all updates in $o$ %appear in $t$ and they appear in the same order.\r
-\end{defn}\r
-\r
-\begin{defn}[Consistency between suborders]\r
-Two suborders U and V are consistent if there exist a total order T \r
-such that both U and V are suborders of T.\r
-\begin{center}\r
-$U = \{slot_{i}, slot_{i+1}, \dots, slot_{j}\},$ \\\r
-$V = \{slot_{k}, slot_{k+1}, \dots, slot_{l}\},$ \\\r
-$sn_1 \leq i \leq j \leq k \leq l \leq sn_n,$ \\\r
-$U \subset T \land V \subset T$ \\\r
-$T = \{slot_{sn_1}, \dots, slot_{i}, slot_{i+1}, \dots, slot_{j}, $\\\r
-$\dots, slot_{k}, slot_{k+1}, \dots, slot_{l}, \dots, slot_{sn_n}\}$\r
-\end{center}\r
-%Define notion of consistency between suborders... Two suborders U,V\r
-%are consistent if there exist a total order T such that both U and V\r
-%are suborders of T.\r
-\end{defn}\r
-\r
-\begin{defn}[Error-free execution]\r
-An error-free execution, for which the client does not flag any errors\r
-is defined by the following criteria:\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{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
+\begin{algorithmic}[1]\r
+\Function{AddQueSta}{$DE_s,max'_s,cp_s$}\Comment{Insert a $qs$}\r
+\State $DE_{ret} \gets \emptyset$\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_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{GetCRPairs}{$DE_s,CR_s,cp_s$}\r
+\State $DE_{ret} \gets \emptyset$\r
+\If{$|CR_s| \leq cp_s$}\Comment{$CR$ set can span multiple slots}\r
+ \State $DE_{ret} \gets DE_s \cup\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{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 $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_p \gets false$\r
+\State $CR_p \gets \emptyset$\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 $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{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{GetCRPairs}{DE_p,CR,cp_p}$\r
+ \EndIf\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{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{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 $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 $\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
+\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
+\r
+\r
+\subsection{Definitions for Formal Guarantees}\r
+\r