\usepackage{graphicx}\r
\usepackage{mathrsfs}\r
\usepackage{algpseudocode}% http://ctan.org/pkg/algorithmicx\r
+\usepackage[all]{xy}\r
\newtheorem{theorem}{Theorem}\r
\newtheorem{prop}{Proposition}\r
\newtheorem{lem}{Lemma}\r
(a) check its HMAC, and\r
(b) check that the previous entry HMAC field matches the previous\r
entry.\r
-\item Check that the last message version for our machine matches our\r
-last message sent.\r
+\item Check that the last-message entry for our machine matches the stored HMAC of our last message sent.\r
\item For all other machines, check that the latest sequence number is\r
at least as large (never goes backwards).\r
\item That the queue has a current queue state entry.\r
\r
\subsection{Resizing Queue}\r
Client can make a request to resize the queue. This is done as a write that combines:\r
- (a) a slot with the message, and\r
- (b) a request to the server\r
+ (a) a slot with the message, and (b) a request to the server. The queue can only be expanded, never contracted; attempting to decrease the size of the queue will cause future clients to throw an error.\r
\r
\subsection{Server Algorithm}\r
-$s \in SN$ is a sequence number set\\\r
+$s \in SN$ is a sequence number\\\r
$sv \in SV$ is a slot's value\\\r
$slot_s = \tuple{s, sv} \in SL \subseteq SN \times SV$ \\ \\\r
\textbf{State} \\\r
\in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s \geq s_s$ \\\r
$MinSlot(SL_s)= \tuple{s, sv} \mid \tuple{s, sv} \r
\in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s \leq s_s$ \\\r
-$SeqN(\tuple{s, sv})=s$ \\\r
-$SlotVal(\tuple{s, sv})=sv$ \\\r
+$SeqN(slot_s = \tuple{s, sv})=s$ \\\r
+$SlotVal(slot_s = \tuple{s, sv})=sv$ \\\r
\r
\begin{algorithmic}[1]\r
\Function{GetSlot}{$s_g$}\r
\r
\begin{algorithmic}[1]\r
\Function{PutSlot}{$s_p,sv_p,max'$}\r
-\If{$(max' \neq \emptyset)$}\Comment{Resize}\r
+\If{$(max' \neq \emptyset)$} \Comment{Resize}\r
\State $max \gets max'$\r
\EndIf\r
\State $\tuple{s_n,sv_n} \gets MaxSlot(SL)$\Comment{Last sv}\r
-\State $s_n \gets SeqN(\tuple{s_n,sv_n})$\r
+%\State $s_n \gets SeqN(\tuple{s_n,sv_n})$\r
\If{$(s_p = s_n + 1)$}\r
\If{$n = max$}\r
\State $\tuple{s_m,sv_m} \gets MinSlot(SL)$\Comment{First sv}\r
$de$ is a data entry \\\r
$k$ is key of entry \\\r
$v$ is value of entry \\\r
-$kv$ is a key-value entry $\tuple{k,v}$, $kv \in D$ \\\r
+$kv$ is a key-value entry $\tuple{k,v}$, $kv \in DE$ \\\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 (contains $max$ size of queue), $qs \in D$ \\\r
+id + last s of a machine, $ss \in DE$ \\\r
+$qs$ is a queue state entry (contains $max$ size of queue), $qs \in DE$ \\\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
-$DE = \{de \mid de \in D\}$ \\ \\\r
-$s \in SN$ is a sequence number set\\\r
+s + id of a machine that wins a collision, $cr \in DE$ \\\r
+$DE$ is a set of all data entries, possibly of different types, in a single message \\\r
+$s \in SN$ is a sequence number \\\r
$id$ is a machine ID\\\r
$hmac_p$ is the HMAC value of the previous slot \\\r
$hmac_c$ is the HMAC value of the current slot \\\r
$Dat_s = \tuple{s,id,hmac_p,DE,hmac_c}$ \\\r
-$sv_s = \tuple{s, E(Dat_s)} = \r
+$slot_s = \tuple{s, E(Dat_s)} = \r
\tuple{s, E(\tuple{s,id,hmac_p,DE,hmac_c})}$ \\ \\\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{$d$ = delta between the last $s$ recorded and the first $s$ received} \\\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{m = number of slots stored on client (initially $m = 0$)} \\\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
+\textit{MS = associative array of $\tuple{id, s_{last}}$ of all clients on client \r
(initially empty)} \\\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$ = set of $\tuple{s, id}$ of all slots in a previous read\r
+\textit{$SM$ = associative array of $\tuple{s, id}$ of all slots in previous reads\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 \geq s_s$ \\\r
$MinSlot(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 \leq s_s$ \\\r
+ \in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s \leq s_s$ \\\r
$Slot(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
+ \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
+$CreateEntLV(kv_s,s_s)=\tuple{kv_s,s_s}$ \\\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
$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
-$GetKV(de_s$ \textit{such that} $de_s \in D \land de_s = kv)=\tuple{k_s,v_s}$ \\\r
-$GetSS(de_s$ \textit{such that} $de_s \in D \land de_s = ss)=\tuple{id,s_{last}}$ \\\r
-$GetQS(de_s$ \textit{such that} $de_s \in D \land de_s = qs)=qs_s$ \\\r
-$GetCR(de_s$ \textit{such that} $de_s \in D \land de_s = cr)=\tuple{s_s,id_s}$ \\\r
-$GetLastSeqN(MS_s,id_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}}\r
-\in MS_s \wedge \forall \tuple{id_s, s_{s_{last}}} \in MS_s, id = id_s$ \\\r
-$GetMachineId(SM_s,s_s)= id$ \textit{such that} $\tuple{s, id}\r
-\in SM_s \wedge \forall \tuple{s_s, id_s} \in SM_s, s = s_s$ \\\r
-$GetS(\tuple{s, id})=s$ \\\r
-$GetId(\tuple{s, id})=id$ \\\r
-$GetKey(\tuple{k, v})=k$ \\\r
-$GetVal(\tuple{k, v})=v$ \\\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,kv_s)= s$ \textit{such that} $\tuple{kv, s} \in LV_s \r
+ \wedge \forall \tuple{kv_s, s_s} \in LV_s, kv_s = kv$ \\\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} = cr_s$ \\\r
+$GetKey(kv = \tuple{k, v})=k$ \\\r
+$GetVal(kv = \tuple{k, v})=v$ \\\r
+$GetId(ss = \tuple{id, s_{last}})=id$ \\\r
+$GetSLast(ss = \tuple{id, s_{last}})=s_{last}$ \\\r
+$GetS(cr = \tuple{s, id})=s$ \\\r
+$GetId(cr = \tuple{s, id})=id$ \\\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
+ \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
+ \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
+ \wedge \forall \tuple{id_s, s_{s_{last}}} \in MS_s, s_{last} \leq s_{s_{last}}$ \\\r
+$MinCRSeqN(CR_s)= s$ \textit{such that} $\tuple{s, id} \in CR_s \r
+ \wedge \forall \tuple{s_s, id_s} \in CR_s, s \leq s_s$ \\\r
+$MaxSMSeqN(SM_s)= s$ \textit{such that} $\tuple{s, id} \in SM_s \r
+ \wedge \forall \tuple{s_s, id_s} \in SM_s, s \geq s_s$ \\\r
\r
\begin{algorithmic}[1]\r
-\Procedure{ReportError}{$msg$}\r
+\Procedure{Error}{$msg$}\r
\State $Print(msg)$\r
\State $Halt()$\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
-\State \Return {$hmac_{stored} = hmac_{computed}$}\r
+\Function{GetQueSta}{$DE_s$}\r
+\State $de_{qs} \gets ss$ \textit{such that} $ss \in DE_s, \r
+ de_s \in D \land type(de_s) = "qs"$\r
+\If{$de_{qs} \neq \emptyset$}\r
+ \State $qs_{ret} \gets GetQS(de_{qs})$\r
+\Else\r
+ \State $qs_{ret} \gets \emptyset$\r
+\EndIf\r
+\State \Return{$qs_{ret}$}\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 \Return $true$\r
-\Else\r
- \State \Return {$hmac_{p_{sto}} = hmac_{p_s}$}\r
-\EndIf\r
+\Function{GetSlotSeq}{$DE_s$}\r
+\State $DE_{ss} \gets \{de | de \in DE_s \land type(de) = "ss"\}$\r
+\State \Return{$DE_{ss}$}\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
+\begin{algorithmic}[1]\r
+\Function{GetColRes}{$DE_s$}\r
+\State $DE_{cr} \gets \{de | de \in DE_s \land type(de) = "cr"\}$\r
+\State \Return{$DE_{cr}$}\r
+\EndFunction\r
+\end{algorithmic}\r
\r
\begin{algorithmic}[1]\r
-\Function{GetQueSta}{$Dat_s$}\r
-\State $DE_s \gets GetDatEnt(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
- \State $qs_{ret} \gets GetQS(de_{qs})$\r
+\Function{UpdateLastSeqN}{$id_s,s_s,MS_s$}\r
+\State $s_t \gets MS_s[id_s]$\r
+\If{$s_t = \emptyset$}\r
+ \State $MS_s[id_s] = s_s$ \Comment{First occurrence}\r
\Else\r
- \State $qs_{ret} \gets \emptyset$\r
+ \State $MS_S[id_s] \gets max(s_t, s_s)$\r
\EndIf\r
-\State \Return{$qs_{ret}$}\r
+\State \Return{$MS_s$}\r
\EndFunction\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
+\Function{UpdateKVLivEnt}{$LV_s,kv_s,s_s$}\r
+\State $s_t \gets GetLivEntLastS(LV_s,kv_s)$\r
+\If{$s_t = \emptyset$}\r
+ \State $LV_s \gets LV_s \cup \{\tuple{kv_s,s_s}\}$\Comment{First occurrence}\r
\Else\r
- \State $\tuple{id_{ret},s_{last_{ret}}} \gets \emptyset$\r
+ \If{$s_s > s_t$}\Comment{Update entry with a later s}\r
+ \State $LV_s \gets (LV_s - \{\tuple{kv_s,s_t}\}) \cup \r
+ \{\tuple{kv_s,s_s}\}$\r
+ \EndIf\r
\EndIf\r
-\State \Return{$\tuple{id_{ret},s_{last_{ret}}}$}\r
+\State \Return{$LV_s$}\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
+\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 \Return{$\{\tuple{s_{ret},id_{ret}},\tuple{s_{r_{ret}},id_{r_{ret}}}\}$}\r
+\State \Return{$SS_{s_{live}}$}\r
\EndFunction\r
\end{algorithmic}\r
\r
\begin{algorithmic}[1]\r
-\Function{UpdateLastSeqN}{$id_s,s_s,MS_s$}\r
-\State $s_t \gets GetLastSeqN(MS_s,id_s)$\r
-\If{$s_t = \emptyset$}\r
- \State $MS_s \gets MS_s \cup \{\tuple{id_s,s_s}\}$\Comment{First occurrence}\r
-\Else\r
- \If{$s_s > s_t$}\Comment{Update entry with a later s}\r
- \State $MS_s \gets (MS_s - \{\tuple{id_s,s_t}\}) \cup \r
- \{\tuple{id_s,s_s}\}$\r
- \EndIf\r
+\Function{AddCRLivEnt}{$CR_{s_{live}},cr_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 \Return{$MS_s$}\r
+\State \Return{$CR_{s_{live}}$}\r
\EndFunction\r
\end{algorithmic}\r
\r
\begin{algorithmic}[1]\r
-\Procedure{CheckLastSeqN}{$MS_s,MS_t$}\Comment{Check $MS_t$ based on $MS_s$}\r
-\ForAll{$\tuple{id_t,s_{t_{last}}} \in MS_t$}\r
- \State $s_{s_{last}} \gets GetLastSeqN(MS_s,id_t)$\r
- \If{$s_{s_{last}} \neq \emptyset$}\r
- \If{$id_t = id_{self}$}\r
- \If{$s_{s_{last}} \neq s_{t_{last}}$}\r
- \State \Call{ReportError}{'Invalid last $s$ for this machine'}\r
- \EndIf\r
- \Else\r
- \If{$s_{s_{last}} \geq s_{t_{last}}$}\r
- \State $MS_s \gets (MS_s - \{\tuple{id_t,s_{t_{last}}}\}) \cup \r
- \{\tuple{id_t,s_{s_{last}}}\}$\r
- \Else\r
- \State \Call{ReportError}{'Invalid last $s$ for machine $id_t$'}\r
- \EndIf\r
- \EndIf\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 $s_{s_{last}} \gets GetSLast(ss_s)$\r
+ \If{$s_{s_{min}} > s_{s_{last}}$}\Comment{Remove if dead}\r
+ \State $SS_{s_{live}} \gets SS_{s_{live}} - \{ss_s\}$ \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 $s_s \gets GetS(cr_s)$\r
+ \If{$s_{s_{min}} > s_s$}\Comment{Remove if dead}\r
+ \State $CR_{s_{live}} \gets CR_{s_{live}} - \{cr_s\}$ \r
+ \EndIf\r
+\EndFor\r
+\State \Return{$CR_{s_{live}}$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Function{UpdateSM}{$SM_s,CR_s$}\Comment{Remove if dead}\r
+\State $s_{cr_{min}} \gets MinCRSeqN(CR_s)$\r
+ \State $SM_s \gets SM_s - \{\tuple{s_s,id_s} \mid \tuple{s_s,id_s}\r
+ \in SM_s \wedge s_s < s_{cr_{min}}\}$\r
+\State \Return{$CR_{s_{live}}$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Procedure{CheckLastSeqN}{$MS_s,MS_t,d$}\r
+\For {$\tuple{id, s_t}$ in $MS_t$}\Comment{Check $MS_t$ based on the newer $MS_s$}\r
+ \State $s_s \gets MS_s[id]$\r
+ \If{$d \land s_s = \emptyset$}\r
+ \State \Call{Error}{'Missing $s$ for machine $id$'}\r
+ \ElsIf{$id = id_{self}$ and $s_s \neq s_t$}\r
+ \State \Call{Error}{'Invalid last $s$ for this machine'}\r
+ \ElsIf{$id \neq id_{self}$ and $s_{s_{last}} < s_{t_{last}}$}\r
+ \State \Call{Error}{'Invalid last $s$ for machine $id$'}\r
+ \Else\r
+ \State $MS_t[id] \gets s_s$\r
\EndIf\r
\EndFor\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
+\Procedure{CheckCollision}{$MS_s,SM_s,cr_s$}\r
+\If{$cr_s \neq \emptyset$}\r
+ \State $s_s \gets GetS(cr_s)$\r
+ \State $id_s \gets GetId(cr_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
+ \State $id_t \gets SM_s[s_s]$\r
+ \If{$id_s \neq id_t$}\r
+ \State \Call{Error}{'Invalid $id$ for this slot update'}\r
+ \EndIf\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
-\State $id_t \gets GetId(\tuple{s_t,id_t})$\r
-\State $id_s \gets GetMachineId(SM_s,s_t)$\r
-\If{$id_s \neq id_t$}\r
- \State \Call{ReportError}{'Invalid $id_s$ for this slot update'}\r
+\Function{ValidSlotsRange}{$|SL_s|,s_{s_{min}},s_{s_{max}}$}\r
+\State $sz_{SL} \gets s_{s_{max}} - s_{s_{min}} + 1$\r
+\If{$sz_{SL} \neq |SL_s|$}\r
+ \State \Call{Error}{'Sequence numbers range does not match actual set'}\r
+\EndIf\r
+\State $s_{s_{last}} \gets MaxSMSeqN(SM)$\r
+\If{$s_{s_{min}} \leq s_{s_{last}}$}\r
+ \State \Call{Error}{'Server sent old slots'}\r
+\EndIf\r
+\State \Return{$s_{s_{min}} > s_{s_{last}} + 1$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Procedure{CheckSlotsRange}{$|SL_s|$}\r
+\State $s_{s_{max}} \gets MaxLastSeqN(MS)$\r
+\State $s_{self} \gets MS[id_{self}]$\r
+\State $sz_{expected} \gets s_{s_{max}} - s_{self} + 1$\r
+\If{$|SL_s| \neq sz_{expected}$}\r
+ \State \Call{Error}{'Actual number of slots does not match expected'}\r
\EndIf\r
\EndProcedure\r
\end{algorithmic}\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
+\State $DE_{s_{kv}} \gets \{de_s | de_s \in DE_s, type(de_s) = "kv"\}$\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 $\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
- \Else\r
- \State $DT_s \gets (DT_s - \{\tuple{k_s,v_t}\}) \cup \r
+ \State $kv_s \gets GetKV(de_s)$\r
+ \State $LV_s \gets \Call{UpdateKVLivEnt}{LV_s,kv_s,s_s}$\r
+ \State $k_s \gets GetKey(kv_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
+ \Else\r
+ \State $DT_s \gets (DT_s - \{\tuple{k_s,v_t}\}) \cup \r
\{\tuple{k_s,v_s}\}$\r
- \EndIf\r
- \EndIf\r
+ \EndIf\r
\EndFor\r
\State \Return{$DT_s$}\r
\EndFunction\r
\begin{algorithmic}[1]\r
\Procedure{ProcessSL}{$SL_g$}\r
\State $MS_g \gets \emptyset$\r
-\State $SM_{curr} \gets \emptyset$\r
-\State $\tuple{s_{g_{max}},sv_{g_{max}}} \gets MaxSlot(SL_g)$\r
-\State $s_{g_{max}} \gets SeqN(\tuple{s_{g_{max}},sv_{g_{max}}})$\r
\State $\tuple{s_{g_{min}},sv_{g_{min}}} \gets MinSlot(SL_g)$\r
-\State $s_{g_{min}} \gets SeqN(\tuple{s_{g_{min}},sv_{g_{min}}})$\r
+\State $\tuple{s_{g_{max}},sv_{g_{max}}} \gets MaxSlot(SL_g)$\r
+\State $d \gets \Call{ValidSlotsRange}{|SL_g|,s_{g_{min}},s_{g_{max}}}$\r
\For{$s_g \gets s_{g_{min}}$ \textbf{to} $s_{g_{max}}$}\Comment{Process slots \r
in $SL_g$ in order}\r
\State $\tuple{s_g,sv_g} \gets Slot(SL_g,s_g)$\r
- \State $SM_{curr} \gets SM_{curr} \cup \{\tuple{s_g,sv_g}\}$\r
- \State $s_g \gets SeqN(\tuple{s_g,sv_g})$\r
- \State $sv_g \gets SlotVal(\tuple{s_g,sv_g})$\r
\State $Dat_g \gets Decrypt(SK,sv_g)$\r
+ \State $id_g \gets GetMacId(Dat_g)$\r
+ \State $SM \gets SM \cup \{\tuple{s_g,id_g}\}$\r
\State $s_{g_{in}} \gets GetSeqN(Dat_g)$\r
\If{$s_g \neq s_{g_{in}}$}\r
- \State \Call{ReportError}{'Invalid sequence number'}\r
+ \State \Call{Error}{'Invalid sequence number'}\r
\EndIf\r
\State $DE_g \gets GetDatEnt(Dat_g)$\r
\State $hmac_{p_{stored}} \gets GetPrevHmac(Dat_g)$\r
- \If{$\neg \Call{ValidPrevHmac}{DE_g,hmac_{p_g},hmac_{p_{stored}}}$}\r
- \State \Call{ReportError}{'Invalid previous HMAC value'}\r
+ \If {$ \neg(s_g = 0 \land hmac_{p_g} = 0) \land hmac_{p_{stored}} \neq hmac_{p_g}$}\r
+ \State \Call{Error}{'Invalid previous HMAC value'}\r
\EndIf\r
- \State $hmac_{c_g} \gets GetCurrHmac(Dat_g)$\r
- \If{$\neg \Call{ValidHmac}{DE_g,SK,hmac_{c_g}}$}\r
- \State \Call{ReportError}{'Invalid current HMAC value'}\r
+ \If{$\Call{Hmac}{DE_g,SK} \neq GetCurrHmac(Dat_g)$ }\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 $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
+ \If{$DE_{g_{cr}} \neq \emptyset$}\r
+ \ForAll{$de_{g_{cr}} \in DE_{g_{cr}}$}\r
+ \State $cr_g \gets GetCR(de_{g_{cr}})$\r
+ \State $\Call{CheckCollision}{MS,SM,cr_g}$\r
+ \State $CR_{live} \gets \Call{AddCRLivEnt}{CR_{live},cr_g}$\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 $\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
\State $m \gets m + |SL_g|$\r
\Else\r
- \State \Call{ReportError}{'Actual queue size exceeds $max_g$'}\r
+ \State \Call{Error}{'Actual $SL$ size on server exceeds $max_g$'}\r
\EndIf\r
-\State $\Call{CheckLastSeqN}{MS_g,MS}$\r
+\State $\Call{CheckLastSeqN}{MS_g,MS,d}$\r
+\State $\Call{CheckSlotsRange}{|SL_g|}$\r
+\State $\Call{UpdateSSLivEnt}{SS_{live},MS}$\r
+\State $\Call{UpdateCRLivEnt}{CR_{live},MS}$\r
+\State $\Call{UpdateSM}{SM,CR_{live}}$\r
\EndProcedure\r
\end{algorithmic}\r
\r
\end{algorithmic}\r
\r
\begin{algorithmic}[1]\r
-\Function{GetValFromKey}{$k_g$}\r
+\Function{Get}{$k_g$} \Comment{Interface function to get a value}\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 \Return{$v_s$}\r
\end{algorithmic}\r
\r
\subsubsection{Writing Slots}\r
-\textbf{Data Entry} \\\r
-$k$ is key of entry \\\r
-$v$ is value of entry \\\r
-$kv$ is a key-value entry $\tuple{k,v}$\\\r
-$D = \{kv,ss,qs,cr\}$ \\\r
-$DE = \{de \mid de \in D\}$ \\\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
\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{$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
$\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{$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
\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
$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
\r
\begin{algorithmic}[1]\r
-\Function{PutKVPair}{$KV_s,\tuple{k_s,v_s}$}\r
-\State $\tuple{ck_s,\tuple{k_s,v_t}} \gets GetKV(KV_s,k_s)$\r
+\Function{Put}{$KV_s,\tuple{k_s,v_s}$} \Comment{Interface function to update a key-value pair}\r
+\State $\tuple{ck_s,\tuple{k_s,v_t}} \gets GetKVPair(KV_s,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 $ck_p \gets ck_p + 1$\r
\end{algorithmic}\r
\r
\begin{algorithmic}[1]\r
-\Function{CheckResize}{$MS_s,th_s,max'_t,m'_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
+\begin{algorithmic}[1]\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{CheckSLFull}{$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
+\Function{HandleCollision}{$SL_s,s_s$}\r
+\If{$SL_s = \emptyset$}\r
+ \State \Call{Error}{'No slots received from server'}\r
\EndIf\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 $cr_s \gets CreateCR(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}{$need_s,sl_{s_{last}},max'_s$}\r
-\If{$need_s$}\r
- \State $s_s \gets GetLastS(sl_{s_{last}})$\r
- \State $sv_s \gets GetSV(sl_{s_{last}})$\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
+\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
+\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
+ \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
+ \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$}\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
+ \State $live \gets false$\r
+ \EndIf\r
+\Else\r
+ \State \Call{Error}{'Unrecognized $de$ type'}\r
\EndIf\r
-\State \Return{$cr_s$}\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 is $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{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{GetDEPairs}{$KV_s,max'_s,need_s,sl_s$}\r
+\Function{GetKVPairs}{$DE_s,KV_s,cp_s$}\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
+\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_{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
+\State \Return{$\tuple{DE_{ret}}$}\r
\EndFunction\r
\end{algorithmic}\r
\r
\begin{algorithmic}[1]\r
-\Procedure{PutDataEntries}{$th_p,m'_p$}\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 $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 $cr_p \gets \Call{HandleCollision}{\tuple{stat_p,SL_p}}$\r
-\State $cr_{p_{last}} \gets \Call{ReinsertLastSlot}{need_p,sl_{last},max'_p}$\r
-\EndProcedure\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
+ \State $cp_s \gets cp_s - |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
+ \State $cp_s \gets 0$\r
+\EndIf\r
+\State \Return{$\tuple{DE_{ret},cp_s}$}\r
+\EndFunction\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{Definitions for Formal Guarantees}\r
-\r
-\begin{enumerate}\r
-\item Equality: Two messages $t$ and $u$ are equal if their sequence numbers, senders, and contents are exactly the same.\r
-\item Message: A message $t$, is the tuple $t = (i(t), s(t), contents(t))$ containing the sequence number, machine ID of the sender, and contents of $t$ respectively.\r
-\item Parent: A parent of a message $t$ is the message $A(t)$, unique by the correctness of HMACs, such that $HMAC_C(t) = HMAC_P(A(t))$.\r
-\item Chain: A chain of messages with length $n \ge 1$ is a message sequence $(t_i, t_{i+1}, ..., t_{i+n-1})$ such that for every index $i < k \le i+n-1$, $t_k$ has sequence number $k$ and is the parent of $t_{k-1}$. Note that no two entries in a chain can have the same sequence number.\r
-\item Partial message sequence: A partial message sequence is a sequence of messages, no two with the same sequence number, that can be divided into disjoint chains.\r
-\item Total message sequence: A total message sequence $T$ with length $n$ is a chain of messages that starts at $i = 1$. The path of a message $t$ is the total message sequence whose last message is $t$.\r
-\item Consistency: A partial message sequence $P$ is consistent with a total message sequence $T$ of length $n$ if for every message $p \in P$ with $i(p) < n$, $T_{i(p)} = p$. This implies that $\{p \in P | i(p) \le n\}$ is a subsequence of T.\r
-\item Transitive closure set at index $i$: A set $\mathscr{S}$ of clients comprising a connected component of an undirected graph, where two clients are connected by an edge if they both received the same message $t$ with index $i(t) > i$.\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
+ \State $cp_s \gets cp_s - |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
+ \State $cp_s \gets 0$\r
+\EndIf\r
+\State \Return{$\tuple{DE_{ret},cp_s}$}\r
+\EndFunction\r
+\end{algorithmic}\r
\r
-\end{enumerate}\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$}\Comment{Add a qs entry}\r
+ \State $\tuple{DE_p,cp_p} \gets \Call{AddQueSta}{DE_p,max'_p,cp_p}$\r
+ \State $reinsert_{qs} \gets false$\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
+\State $MS \gets \Call{UpdateLastSeqN}{id_{self},s_p,MS}$\r
+\If{$|DE_p| = cp$}\Comment{Update set counters}\r
+ \State $ck_g \gets ck_g + cp_p$\Comment{Middle of set}\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 $need_p \gets \Call{CheckSLFull}{MS,max_g}$\r
+\If{$need_p$}\Comment{SL on server is full}\r
+ \State $\Call{CheckLastSlot}{sl_{last}}$\Comment{Salvage entries from expunged 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
-\subsection{Formal Guarantee}\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{Formal Guarantees}\r
+\subsubsection{Definitions}\r
+\r
+\begin{defn}[Message]\r
+A message $\mathsf{t}$, is the tuple \r
+\begin{center}\r
+$\mathsf{t = \tuple{s, E(Dat_s)}}$ \\\r
+$\mathsf{Dat_t = \tuple{s,id,hmac_p, DE,hmac_c}}$\r
+\end{center}\r
+containing $\mathsf{s}$ as sequence number and $\mathsf{Dat_t}$ as its \r
+encrypted contents. $\mathsf{Dat_t}$ consists of $\mathsf{s}$, \r
+$\mathsf{id}$ as machine ID of the sender, $\mathsf{hmac_p}$ as HMAC \r
+from a previous message, $\mathsf{DE}$ as set of data entries, and \r
+$\mathsf{hmac_c}$ as HMAC from message $\mathsf{t}$ respectively.\r
+\end{defn}\r
+\r
+\begin{defn}[Equality]\r
+Two messages $\mathsf{t}$ and $\mathsf{u}$ are equal if their $\mathsf{s}$, \r
+and $\mathsf{Dat_t}$ are exactly the same.\r
+\end{defn}\r
+\r
+\begin{defn}[Parent]\r
+A parent of a message $\mathsf{t}$ is the message $\mathsf{p_t}$, \r
+unique by the correctness of HMACs in $\mathsf{Dat_t}$, such that \r
+$\mathsf{hmac_p(t) = hmac_c(p_t)}$.\r
+\end{defn}\r
+\r
+\begin{defn}[Chain]\r
+A chain of messages with length $\mathsf{n \ge 1}$ is a message sequence \r
+$\mathsf{R = (r_s, r_{s+1}, ..., r_{s+n-1})}$ such that for every sequence \r
+number $\mathsf{s < k \le s+n-1}$, $\mathsf{r_k}$ has sequence number \r
+$\mathsf{k}$ and is the parent of $\mathsf{r_{k-1}}$.\r
+\end{defn}\r
+\r
+\begin{defn}[Partial sequence]\r
+A partial sequence $\mathsf{P}$ is a sequence of messages, no two \r
+with the same sequence number, that can be divided into disjoint chains.\r
+\end{defn}\r
+\r
+\begin{defn}[Total sequence]\r
+A total sequence $\mathsf{T =}$ $\mathsf{(t_1, t_2, ..., t_n)}$ with \r
+length $\mathsf{n}$ is a chain of messages that starts at $\mathsf{s = 1}$.\r
+\end{defn}\r
+\r
+\begin{defn}[Path]\r
+The path of a message $\mathsf{t}$ is the chain that starts at $\mathsf{s = 1}$ \r
+and whose last message is $\mathsf{t}$. The uniqueness of a path follows \r
+from the uniqueness of a parent.\r
+\end{defn}\r
+\r
+\begin{defn}[Consistency]\r
+A partial sequence $\mathsf{P}$ is consistent with a total sequence \r
+$\mathsf{T}$ of length $\mathsf{n}$ if for every message $\mathsf{p \in P}$ \r
+with $\mathsf{s_p \leq n}$, $\mathsf{t_{s_p} = p}$. This implies that \r
+$\mathsf{\{p \in P | s_p \le n\}}$ is a partial sequence of $\mathsf{T}$.\r
+\end{defn}\r
+\r
+\begin{defn}[Transitive closure]\r
+Transitive closure set at sequence number $\mathsf{s_n}$ is a set \r
+$\mathsf{\mathscr{S}}$ of clients comprising a connected component of an \r
+undirected graph, where two clients are connected by an edge if they both \r
+received the same message $\mathsf{t}$ with sequence number $\mathsf{s_t > s_n}$.\r
+\end{defn}\r
+\r
+\subsubsection{Lemmas and Proofs}\r
+\r
+\begin{prop} \r
+Every client $\mathsf{J}$ who sends a message $\mathsf{t}$ \r
+has parent $\mathsf{p_t}$ as its latest stored message, and \r
+$\mathsf{s_t = s_{p_t} + 1}$. \r
+\end{prop}\r
+\begin{proof} True by definition, because $J$ sets \r
+$\mathsf{hmac_p(t) = hmac_c(p_t)}$ and \r
+$\mathsf{s_t = }$ $\mathsf{s_{p_t + 1}}$ when a message \r
+is sent. \r
+\end{proof}\r
\r
-\begin{prop} Every client $J$ who sends a message $t$ has $A(t)$ as its latest stored message, and $i(t) = i(A(t)) + 1$. \end{prop}\r
-\begin{proof} True by definition, because $J$ sets $HMAC_P(t) = HMAC_C(A(t))$ and $i(t) = i(A(t)) + 1$ when a message is sent. \end{proof}\r
+\begin{prop} If a rejected message entry is added to the set $\mathsf{CR}$ \r
+at sequence number $\mathsf{s}$, the message will remain in $\mathsf{CR}$ \r
+until every client has seen it. \r
+\end{prop}\r
+\begin{proof} Every $\mathsf{CR}$ entry $\mathsf{cr}$ remains in the queue until it \r
+reaches the tail, and is refreshed by the next sender $\mathsf{J}$ at that time if \r
+$\mathsf{min(MS) > s_{cr}}$; that is, until every client has sent a message with \r
+sequence number greater than $\mathsf{s_{cr}}$. Because every client who sends a \r
+message with sequence number $\mathsf{s}$ has the state of the set $\mathsf{SL}$ at \r
+$\mathsf{s - 1}$, this client will have seen the message at $\mathsf{s_{cr}}$. \r
+\end{proof}\r
\r
-\begin{prop} If a rejected message entry is added to the RML at index $i$, the message will remain in the RML until every client has seen it. \end{prop}\r
-\begin{proof} Every RML entry $e$ remains in the queue until it reaches the tail, and is refreshed by the next sender $J$ at that time if $min(MS) > i(e)$; that is, until every client has sent a message with sequence number greater than $i(e)$. Because every client who sends a message with index $i$ has the state of the queue at $i - 1$, this client will have seen the message at $i(e)$. \end{proof}\r
+\begin{figure}[h]\r
+ \centering\r
+ \xymatrix{ & & L \\\r
+\dots \ar[r] & q \ar[dr]_{J} \ar[r]^{K} & l_1 \ar[r] & l_2 \ar[r] & \dots \ar[r] & m \ar[r] & \dots \ar[r] & l_n = u \\\r
+& & r_1 \ar[r] & r_2 \ar[r] & \dots \ar[r] & r_m = t \\\r
+& & R\r
+\save "2,3"."2,8"*+\frm{^\}}\r
+\save "3,3"."3,6"*+\frm{_\}}\r
+\restore\r
+\restore\r
+}\r
+\caption{By Lemma 1, receiving both $t$ and $u$ here is impossible.}\r
+\end{figure}\r
+\r
+\begin{lem} Two messages are received without errors by a client $\mathsf{C}$; \r
+call them $\mathsf{t}$ and $\mathsf{u}$ such that $\mathsf{s_t \le s_u}$. \r
+Then $\mathsf{t}$ is in the path of $\mathsf{u}$. \r
+\end{lem}\r
+\begin{proof}\r
+Assume that there are some pairs of messages $\mathsf{(t,u)}$ that violate this lemma. \r
+Take a specific $\mathsf{(t,u)}$ such that $\mathsf{s_u}$ is minimized, and \r
+$\mathsf{s_t}$ is maximized for this choice of $\mathsf{s_u}$. We will show that $\mathsf{C}$\r
+cannot receive both $\mathsf{t}$ and $\mathsf{u}$ without throwing an error.\r
+\r
+Clearly $\mathsf{C}$ will throw an error if $\mathsf{s_t = s_u}$. So \r
+$\mathsf{s_t < s_u}$. Additionally, if $\mathsf{C}$ receives $\mathsf{u}$ before \r
+$\mathsf{t}$, this will cause it to throw an error, so $\mathsf{t}$ is received \r
+before $\mathsf{u}$. We will prove that an error occurs upon receipt of $\mathsf{u}$.\r
+\r
+Let $\mathsf{r_1}$ be the earliest member of the path of $\mathsf{t}$ that is \r
+not in the path of $\mathsf{u}$, and $\mathsf{q}$ be its parent. Message \r
+$\mathsf{q}$, the last common ancestor of $\mathsf{t}$ and $\mathsf{u}$, must exist, \r
+since all clients and the server were initialized with the same state. Let \r
+$\mathsf{l_1}$ be the successor of $\mathsf{q}$ that is in the path of $\mathsf{u}$; \r
+we know $\mathsf{l_1 \neq r_1}$. Let $\mathsf{R = (r_1, r_2, \dots, r_{|R|} = t)}$ be \r
+the distinct portion of the path of $\mathsf{t}$, and similarly let $\mathsf{L}$ \r
+be the distinct portion of the path of $\mathsf{l_{|L|} = u}$.\r
+\r
+Let $\mathsf{J}$ be the client who sent $\mathsf{r_1}$; that is, such that \r
+$\mathsf{{id_{self}}_J = GetMacID(r_1)}$, and $\mathsf{K}$ be the client who \r
+sent $\mathsf{l_1}$. Because no client can send two messages with the same sequence number, and \r
+$\mathsf{s_{r_1} = s_{l_1} = s_q + 1}$, $\mathsf{J \neq K}$.\r
+\r
+We also know the following facts: \r
+\r
+\begin{prop} No client sends both a message in \r
+$\mathsf{(r_2,...,t)}$ and a message in $\mathsf{(l_2,...,u)}$. \r
+\end{prop}\r
\r
-\begin{lem} If two packets $t$ and $u$, with $i(t) \le i(u)$, are received without errors by a client $C$, then $t$ is in the path of $u$. \end{lem}\r
\begin{proof}\r
-Assume that $t$ is not in the path of $u$. Take $u$ to be the packet of smallest index for which this occurs, and $t$ be the packet with largest index for this $u$. We will prove that an error occurs upon receipt of $u$.\r
+To send a message $\mathsf{p}$ that is the parent of some other \r
+message, one must have received the parent of $\mathsf{p}$. Since \r
+$\mathsf{u}$ is the message with smallest sequence number received by any \r
+client that violates Lemma 1, no client receives both a message in $\mathsf{r}$ \r
+and a message in $\mathsf{l}$. \r
+\end{proof}\r
\r
-Let $R_1$ be the earliest member of the path of $t$ that is not in the path of $u$, and $q$ be its parent. $q$, the last common ancestor of $t$ and $u$, must exist, since all clients and the server were initialized with the same state. Let $S_1$ be the successor of $q$ that is in the path of $u$; we know $S_1 \neq R_1$. Let $R = (R_1, R_2, \dots, R_m = t)$ be the distinct portion of the path of $t$, and similarly let $S$ be the distinct portion of the path of $S_n = u$.\r
+\begin{prop} $\mathsf{C}$ does not receive any message with a\r
+sequence number strictly between $\mathsf{s_t}$ and $\mathsf{s_u}$. \r
+\end{prop}\r
\r
-Let $J = s(R_1)$, and $K = s(S_1)$. Because no client can send two messages with the same index, and $i(R_1) = i(S_1) = i(q) + 1$, we know that $J \neq K$.\r
+\begin{proof} If there were such a message with sequence number smaller than \r
+$\mathsf{s_u}$, it would contradict the assumption that $\mathsf{u}$ is the \r
+message with the least sequence number that violates Lemma 1. \r
+\end{proof}\r
\r
There are two cases:\r
-\r
\begin{itemize}\r
-\item Case 1: $J$ did not send a message in $S$. Then $v_J(t) > v_J(q) = v_J(u)$. $C$ will throw an error, because the latest index of $J$ changes in the opposite direction of the sequence number: $v_J(u) < v_J(t)$ but $i(u) > i(t)$.\r
-\item Case 2: $J$ sent at least one message in $S$. Call the first one $p$. We know that $i(p) > i(S_1)$, since $J \neq K$. $R_1$ must be sent either before or after $p$.\r
+\item Case 1: $\mathsf{J}$ did not send a message in $\mathsf{L}$. Then, where $\mathsf{s_{t_J}}$ \r
+is the greatest sequence number of the messages that client $\mathsf{J}$ sent in \r
+the path of message $\mathsf{t}$, $\mathsf{s_{t_J} > s_{q_J} = s_{u_J}}$.\r
+\begin{itemize}\r
+\item Case 1.1: $\mathsf{C}$ never updates its slot sequence list $\mathsf{SS}$ \r
+between receiving $\mathsf{t}$ and receiving $\mathsf{u}$; this can only happen if \r
+$\mathsf{s_t = s_u - 1}$. Since $\mathsf{t}$ is not the parent of $\mathsf{u}$, \r
+$\mathsf{hmac_p(u) \neq hmac_c(t)}$, causing $\mathsf{C}$ to error.\r
+\item Case 1.2: Case 1.1 does not occur; therefore, $\mathsf{C}$ must update \r
+its slot sequence list $\mathsf{SS}$ at some point between receiving $\mathsf{t}$ \r
+and $\mathsf{u}$. \r
+The latest sequence number of $\mathsf{J}$ decreases during this time, which \r
+means it must decrease when some message is received, which means $\mathsf{C}$ \r
+throws an error in the $\mathsf{CheckLastSeqN}$ subroutine.\r
+\end{itemize}\r
+\r
+\item Case 2: $\mathsf{J}$ sent at least one message in $\mathsf{L}$. Call the \r
+first one $\mathsf{m}$. We know that $\mathsf{s_m > s_{r_1}}$, since \r
+$\mathsf{J \neq K}$ and $\mathsf{m \neq l_1}$. Message $\mathsf{r_1}$ must be sent \r
+either before or after $\mathsf{m}$.\r
\begin{itemize}\r
-\item Case 2.1: Client $J$ sends $p$, and then $R_1$. When $p$ was sent, whether it was accepted or rejected, $i(J, p) \geq i(p)$. Since $i(p) > i(S_1)$, $i(J, p) > q$. So $i(q) < i(J, p)$, which would cause $J$ to fail to send $R_1$, a contradiction.\r
-\item Case 2.2: Client $J$ sends $R_1$, and then $p$. Let $X = (R_1, \dots )$ be the list of messages $J$ sends starting before $R_1$ and ending before $p$.\r
+\item Case 2.1: Client $\mathsf{J}$ sends $\mathsf{m}$, and then $\mathsf{r_1}$. \r
+Before sending $\mathsf{m}$, the greatest sequence number of a message that \r
+$\mathsf{J}$ has received, $\mathsf{{s_{last}}_J}$, must be equal to \r
+$\mathsf{s_m - 1 \ge s_{r_1}}$. Since $\mathsf{{s_{last}}_J}$ never decreases, \r
+client $\mathsf{J}$ cannot then send a message with sequence number \r
+$\mathsf{s_{r_1}}$, a contradiction.\r
+\item Case 2.2: Client $\mathsf{J}$ sends $\mathsf{r_1}$, and then $\mathsf{m}$. \r
+Let $\mathsf{X = (r_1 = x_1, \dots , x_n)}$ be the list of messages $\mathsf{J}$ sends \r
+starting before $\mathsf{r_1}$ and ending before $m$; clearly these all have sequence number $\mathsf{s_p = s_q + 1}$.\r
\begin{itemize}\r
-\item Case 2.2.1: Some message in $X$ was accepted. In this case, before sending $p$, $J$'s value for its own latest index would be strictly greater than $v_J(q)$. ($J$ could not have sent a message with index less than $i(q)$ after receiving $q$). When preparing to send $p$, $J$ would have received its own latest index as at most $v_J(q)$. $J$ throws an error before sending $p$, because its own latest index decreases.\r
-\item Case 2.2.2: All messages in $X$ were rejected. Client $J$ will always add the latest rejected message to the rejected-message list in the next update; so for every $i$, $1 \leq i < |X|$, the $i$th element of $X$ will be recorded in the RML of all further elements of $X$; and every element of $X$ will be recorded in $RML(p)$. Since every rejected message in $RML(p)$ will be in $RML(C, u)$, and $u$ is the first message that $C$ sees which does not have $t$ in its path, $R_1$ will be recorded in $RML(C, p)$. When $C$ receives $u$, $C$ will throw an error from the match $(J, iq+1)$ in $RML(C, p)$.\r
+\item Case 2.2.1: Some message in $\mathsf{X}$ was accepted. Before sending $\mathsf{m}$, \r
+$\mathsf{J}$'s value in $\mathsf{MS_J}$ for its own latest sequence number would \r
+be strictly greater than $\mathsf{s_{q_J}}$. If there is a sequence of messages with \r
+contiguous sequence numbers that $\mathsf{J}$ receives between $\mathsf{r_1}$ and \r
+$\mathsf{m}$, $\mathsf{J}$ throws an error for a similar reason as Case 1.1. Otherwise, \r
+when preparing to send $\mathsf{m}$, $\mathsf{J}$ would have received an update of its \r
+own latest sequence number as at most $\mathsf{s_{q_J}}$. $J$ throws an error before \r
+sending $\mathsf{p}$, because its own latest sequence number decreases.\r
+\item Case 2.2.2: All messages in $\mathsf{X}$ were rejected, making $\mathsf{m}$ \r
+the first message of $\mathsf{J}$ that is accepted after $\mathsf{r_1}$.\r
+\r
+We will show that $\mathsf{C}$ sees $\mathsf{r_1}$. Assume not. Then $\mathsf{(r_2, ..., u)}$ must have at least $\mathsf{{max_g}_C} >= 2$ messages for $\mathsf{r_1}$ to fall off the end of the queue. Consider the sender of $\mathsf{r_3}$ and call it $\mathsf{H}$. $\mathsf{H \neq J}$ by Proposition 3 and the existence of $\mathsf{m}$. Since $\mathsf{H \neq J}$, then by Proposition 3 it could not also have sent a message in $\mathsf{(l_2,..., u}$. Therefore, $\mathsf{s_{u_H} < s_q + 2 = s_{t_H}}$, so upon receipt of $\mathsf{u}$, $\mathsf{C}$ will throw an error by the decrease in a last sequence number similar to Case 1, a contradiction.\r
+\r
+Now that we know that $\mathsf{C}$ sees $\mathsf{r_1}$, note that C receives $\mathsf{u}$ immediately after $\mathsf{t}$ by Proposition 4. Therefore, \r
+$\mathsf{C}$ could not have seen a message after $\mathsf{t}$ with sequence number less \r
+than $\mathsf{s_m}$. In the $\mathsf{PutDataEntries}$ subroutine, $\mathsf{J}$ adds every \r
+$\mathsf{cr}$ entry that contains sequence number $\mathsf{s}$ and machine ID \r
+$\mathsf{id}$ of the messsages that win in the collisions before $\mathsf{m}$ into \r
+$\mathsf{CR}$; $\mathsf{CR}$ keeps the collection of live $\mathsf{cr}$ entries, namely\r
+those which not all clients have seen. Hence, for every $\mathsf{i}$, $\mathsf{1 \leq i < |X|}$, \r
+the collision winner that has collided with $\mathsf{x_i}$ will be recorded appropriately. Since all the $\mathsf{cr}$ entries that record the results of the collisions before $\mathsf{p}$ will also be seen when $\mathsf{u}$ \r
+is received, and $\mathsf{C}$ sees $\mathsf{r_1}$, ${l_1}$ will be recorded in a $\mathsf{cr}$ entry as the winner in the \r
+collision against ${r_1}$.\r
+\r
+When $\mathsf{C}$ receives $\mathsf{u}$, if $\mathsf{C}$ \r
+has seen the $\mathsf{cr}$ entry that records the collision at index $\mathsf{s_q + 1}$, it will throw \r
+an error from the mismatch of $\mathsf{\tuple{s_q+1, id_J}}$ with \r
+$\mathsf{\tuple{s_q+1, id_K}}$ in the corresponding $\mathsf{cr}$ entry.\r
+\r
\end{itemize}\r
\end{itemize}\r
+\r
+\end{itemize}\r
+\end{proof}\r
+\r
+\begin{lem} If there are two packets $\mathsf{t}$ and $\mathsf{u}$, with \r
+$\mathsf{s_t \leq s_u}$, such that $\mathsf{t}$ is in the path of $\mathsf{u}$, \r
+then for any message $\mathsf{p}$ with $\mathsf{s_p \leq s_t}$, iff $\mathsf{p}$ is in \r
+the path of $\mathsf{t}$, it is in the path of $\mathsf{u}$. \r
+\end{lem}\r
+\r
+\begin{proof}\r
+If $\mathsf{s_t = s_u}$ or $\mathsf{s_p = s_t}$, then we are done, because the two \r
+relevant messages are the same. If they are different messages, then:\r
+\begin{itemize}\r
+\item Reverse direction: The definition of $\mathsf{t}$ being in the path of \r
+$\mathsf{u}$ is the existence of a message sequence $\mathsf{(\dots, t, \dots, u)}$ \r
+such that each message except $\mathsf{u}$ is the parent of the succeeding message. \r
+The path of $\mathsf{u}$ must contain some message with sequence number $\mathsf{s_p}$; \r
+because $\mathsf{p}$ is in the path of $\mathsf{u}$, this message is $\mathsf{p}$ \r
+itself. The path of $\mathsf{t}$ is then the prefix of this path ending at $\mathsf{t}$, \r
+which clearly contains $\mathsf{p}$.\r
+\r
+\item Forward direction: The path of $\mathsf{t}$ is a substring of the path of \r
+$\mathsf{u}$, so if the path of $\mathsf{t}$ contains $\mathsf{p}$, so does the path \r
+of $\mathsf{u}$.\r
\end{itemize}\r
\end{proof}\r
\r
\begin{theorem}\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
+Suppose that there is a transitive closure set $\mathsf{\mathscr{S}}$ of clients, \r
+at sequence number $\mathsf{s_n}$. Then there is some total sequence $\mathsf{T}$ of \r
+length $\mathsf{n}$ such that every client $\mathsf{C}$ in $\mathsf{\mathscr{S}}$ \r
+sees a partial sequence $\mathsf{P_C}$ consistent with $\mathsf{T}$. \r
+\end{theorem}\r
\r
\begin{proof}\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) > i$ that $C_1$ shares with another client. Then let $T$ be the portion of the path of $u$ ending at index $i$ and $t$ be the message at that index. Clearly, by Lemma 1, $P_{C_1}$ is consistent with $T$, and furthermore. 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 edges from $C_1$ to $D$. Call this $\mathscr{C} = (C_1, C_2, ..., D)$. I will prove by induction that $D$ has a message whose path includes $t$.\r
\r
-For the base case, $P_{C_1}$ includes $u$, whose path includes $t$. For the inductive step, suppose $P_{C_k}$ has an message $w$ with a path that includes $t$, and shares message $x$ with $P_{C_{k+1}}$ such that $i(x) > i$. If $i(w) = i(x)$, then $w = x$. If $i(w) < i(x)$, then, by Lemma 1, $w$ is in the path of $x$. If $i(w) > i(x)$, $x$ is in the path of $w$; note again that its index is greater than $i$. In any case, $t$ is in the path of $u_k+1$.\r
+The definition of consistency of $\mathsf{P_C}$ with $\mathsf{T}$ is that every message \r
+$\mathsf{p \in P_C}$ with sequence number $\mathsf{s_p \le s_n}$ is equal to the message \r
+in that slot in $\mathsf{T}$. Let $\mathsf{C_1}$ be some client in the transitive closure \r
+set, with partial sequence $\mathsf{P_{C_1}}$, and let $\mathsf{u}$ be some message with \r
+$\mathsf{s_u > s_n}$ that $\mathsf{C_1}$ shares with another client. Then let $\mathsf{T}$ \r
+be the portion of the path of $\mathsf{u}$ ending at sequence number $\mathsf{s_n}$ and \r
+$\mathsf{t}$ be the message at that sequence number. Clearly, by Lemma 1, $\mathsf{P_{C_1}}$ \r
+is consistent with $\mathsf{T}$. We will show that, for every other client $\mathsf{D}$ \r
+with partial sequence $\mathsf{P_D}$, $\mathsf{P_D}$ has some message whose path includes \r
+$\mathsf{t}$. Because $\mathsf{D}$ is in the transitive closure, there is a sequence of \r
+clients $\mathsf{\mathscr{C} = (C_1, C_2, ..., D)}$ from $\mathsf{C_1}$ to $\mathsf{D}$, \r
+where each shares an edge with the next.\r
+We prove by induction that $\mathsf{P_D}$ has a message whose path includes $\mathsf{t}$.\r
+\begin{itemize}\r
+\item Base case: $\mathsf{P_{C_1}}$ includes $\mathsf{u}$, whose path includes $\mathsf{t}$.\r
+\r
+\item Inductive step: Each client in $\mathsf{\mathscr{C}}$ has a partial sequence with a message \r
+that includes $\mathsf{t}$ if the previous client does. Suppose $\mathsf{P_{C_k}}$ has \r
+a message $\mathsf{w}$ with a path that includes $\mathsf{t}$, and shares message $\mathsf{x}$ \r
+with $\mathsf{P_{C_{k+1}}}$ such that $\mathsf{s_x > s_n}$. By Lemma 1, $\mathsf{w}$ or \r
+$\mathsf{x}$, whichever has the least sequence number, is in the path of the other, and therefore \r
+by Lemma 2, $\mathsf{t}$ is in the path of $\mathsf{x}$.\r
+\r
+\item Let $\mathsf{z}$ be the message of $\mathsf{D}$ whose path includes $\mathsf{t}$. \r
+By Lemma 1, every message in $\mathsf{P_D}$ with sequence number smaller than $\mathsf{s_w}$ \r
+is in the path of $\mathsf{z}$. Since $\mathsf{t}$ is in the path of $\mathsf{z}$, every \r
+message in $\mathsf{P_D}$ with smaller sequence number than $\mathsf{s_t = s_n}$ is in $\mathsf{T}$. \r
+Therefore, $\mathsf{P_D}$ is consistent with $\mathsf{T}$.\r
\r
-Let $w$ 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 $w$. Since $t$ is in the path of $w$, every message in $P_D$ with smaller index than $i(t)$ is in $T$. Therefore, $P_D$ is consistent with $T$.\r
+\end{itemize}\r
\end{proof}\r
\r
\subsection{Future Work}\r
\r
Idea is to separate subspace of entries... Shared with other cloud...\r
\end{document}\r
-\r
projects / iotcloud.git / blobdiff