at most 50 slots in the queue and after it sees 70, it should expect \r
50 slots before that queue state entry slot 50 and at most 70 slots. \r
The queue state entry slot 70 is counted as slot number 51 in the queue.}\r
-\item Collision resolution entry: Machine id + message identifier of\r
+\item Collision resolution entry: message identifier + machine id of a\r
collision winner\r
\newline {The purpose of this is to keep keep track of the winner of \r
all the collisions until all clients have seen the particular entry.}\r
entry 50 is dead and 70 is live. However, not until the number of slots reaches \r
70 that queue state entry 50 will be expunged from the queue.}\r
\r
-\item Collision resolution entry is dead if there this entry has been seen\r
+\item Collision resolution entry is dead if this entry has been seen\r
by all clients after a collision happens.\r
\end{enumerate}\r
\r
\subsection{Server Algorithm}\r
$s \in SN$ is a sequence number set\\\r
$sv \in SV$ is a slot's value\\\r
-$slot_s = \tuple{s, sv} \in SL \subseteq SN \times SV$ \\\r
-\r
+$slot_s = \tuple{s, sv} \in SL \subseteq SN \times SV$ \\ \\\r
\textbf{State} \\\r
\textit{SL = set of live slots on server} \\\r
\textit{max = maximum number of slots (input only for resize message)} \\\r
\end{algorithmic}\r
\r
\subsection{Client Algorithm}\r
+\subsubsection{Reading Slots}\r
\textbf{Data Entry} \\\r
$de$ is a data entry \\\r
$k$ is key of entry \\\r
$kv$ is a key-value entry $\tuple{k,v}$, $kv \in D$ \\\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, $qs \in D$ \\\r
-$D = \{kv,ss,qs\}$ \\\r
+$qs$ is a queue state entry (contains $max$ size of queue), $qs \in D$ \\\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
$id$ is a machine ID\\\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
-\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{$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{$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
(initially empty)} \\\r
-\textit{$MS_c$ = set MS to save all $\tuple{id, s_{last}}$ pairs while\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{$max_c$ = maximum number of slots (initially $max_c > 0$)} \\\r
-\textit{m = number of slots on client (initially $m = 0 \mid m \leq n$)} \\\r
-\textit{$hmac_p$ = the HMAC value of the previous slot ($hmac_p = \emptyset$ \r
-for the first slot)} \\\r
-\textit{$id_{self}$ = machine Id of this client} \\\r
-\textit{SK = Secret Key} \\ \\\r
+\textit{SK = Secret Key} \\\r
+\textit{$SM$ = set of $\tuple{s, id}$ of all slots in a previous read\r
+(initially empty)} \\ \\\r
\textbf{Helper Functions} \\\r
-$MaxSlot(SL_s)= \tuple{s, sv} \mid \tuple{s, sv}\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
-$MinSlot(SL_s)= \tuple{s, sv} \mid \tuple{s, sv} \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
+$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
$SeqN(\tuple{s, sv})=s$ \\\r
$SlotVal(\tuple{s, sv})=sv$ \\\r
+$CreateLastSL(s,sv,id)=\tuple{s,sv,id}=sl_{last}$ \\\r
$Decrypt(SK_s,sv_s)=Dat_s=\tuple{s,id,hmac_p,DE,hmac_c}$ \\\r
-$ComputeHash(bit_s)$ is a hash function that generates hash value on $bit_s$ \\\r
-$ComputeHmac(bit_s,SK_s)$ is a HMAC function that generates HMAC value on $bit_s$ \r
-based on key $SK_s$\\\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
-$GetQS(de_s \mid de_s \in D \land de_s = qs)=qs$ \\\r
-$GetSS(de_s \mid de_s \in D \land de_s = ss)=ss$ \\\r
-$GetKV(de_s \mid de_s \in D \land de_s = kv)=kv=\tuple{k,v}$ \\\r
-$GetLastSeqN(MS_s,id_s)= s_{last} \mid \tuple{id, s_{last}}\r
-\in MS_s \wedge \forall \tuple{id_s, s_{s_{last}}} \in MS_s, \r
-id = id_s$ \\\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
-$GetKeyVal(DT_s,k_s)= \tuple{k, v} \mid \tuple{k, v} \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
+$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
+$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
\r
\begin{algorithmic}[1]\r
-\Function{CreateSK}{$uid,pw$}\r
-\State $SK = ComputeHash(uid + pw)$\r
-\State \Return{$SK$}\r
-\EndFunction\r
+\Procedure{ReportError}{$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{Hmac}{$Dat_s,SK_s$}\r
-\State \Return{$ComputeHmac(Dat_s,SK_s)$}\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
\EndFunction\r
\end{algorithmic}\r
\r
\begin{algorithmic}[1]\r
-\Function{ValidHmac}{$Dat_s,SK_s$}\r
-\State $hmac_{stored} \gets GetCurrHmac(Dat_s)$\r
-\State $hmac_{computed} \gets \Call{Hmac}{Dat_s,SK_s}$\r
-\If{$hmac_{stored} = hmac_{computed}$}\r
- \State \Return{$true$}\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{$false$}\r
+ \State \Return {$hmac_{p_{sto}} = hmac_{p_s}$}\r
\EndIf\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
+\r
\begin{algorithmic}[1]\r
-\Function{ValidPrevHmac}{$Dat_s,hmac_{p_s}$}\r
-\If{$hmac_{p_s} = \emptyset$}\Comment{First slot - no previous HMAC}\r
- \State \Return{$true$}\r
-\EndIf\r
-\State $hmac_{stored} \gets GetPrevHmac(Dat_s)$\r
-\If{$hmac_{stored} = hmac_{p_s}$}\r
- \State \Return{$true$}\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
\Else\r
- \State \Return{$false$}\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{GetQueSta}{$Dat_s$}\r
+\Function{GetSlotSeq}{$Dat_s$}\r
\State $DE_s \gets GetDatEnt(Dat_s)$\r
-%\State $qs_{ret} \gets max_s$\r
-%\ForAll{$de_i \in DE_s$}\r
-% \If{$de_i \mid de_i \in D \land de_i = qs$}\r
-% \State $qs_i \gets GetQS(de_i)$\r
-% \If{$qs_i > qs_{ret}$}\r
-% \State $qs_{ret} \gets qs_i$\r
-% \EndIf\r
-% \EndIf\r
-%\EndFor\r
-\State $de_{qs} \gets de_s \mid de_s \in DE_s, de_s \in D \land de_s = qs$\r
-\State $qs_{ret} \gets GetQS(de_{qs})$\r
-%\If{$qs_{ret} > max_s$}\r
-%\State $qs_{ret} \gets qs_i$\r
-%\EndIf\r
-\State \Return{$qs_{ret}$}\r
+\State $de_{ss} \gets de_s$ \textit{such that} $de_s \in DE_s, \r
+ de_s \in D \land de_s = ss$\r
+\If{$de_{ss} \neq \emptyset$}\r
+ \State $\tuple{id_{ret},s_{last_{ret}}} \gets GetSS(de_{ss})$\r
+\Else\r
+ \State $\tuple{id_{ret},s_{last_{ret}}} \gets \emptyset$\r
+\EndIf\r
+\State \Return{$\tuple{id_{ret},s_{last_{ret}}}$}\r
\EndFunction\r
\end{algorithmic}\r
\r
\begin{algorithmic}[1]\r
-\Function{GetSlotSeq}{$Dat_s$}\r
+\Function{GetColRes}{$Dat_s$}\Comment{At most 2 $cr$ entries in a slot}\r
\State $DE_s \gets GetDatEnt(Dat_s)$\r
-%\ForAll{$de_i \in DE_s$}\r
- %\If{$de_i \mid de_i \in D \land de_i = ss$}\r
- %\State $\tuple{id_{ret},s_{last_{ret}}} \gets GetSS(de_i)$\r
- %\EndIf\r
-%\EndFor\r
-\State $de_{ss} \gets de_s \mid de_s \in DE_s, de_s \in D \land de_s = ss$\r
-\State $\tuple{id_{ret},s_{last_{ret}}} \gets GetSS(de_{ss})$\r
-\State \Return{$\tuple{id_{ret},s_{last_{ret}}}$}\r
+\State $de_{cr} \gets de_s$ \textit{such that} $de_s \in DE_s, \r
+ de_s \in D \land de_s = cr$\r
+\If{$de_{cr} \neq \emptyset$}\r
+ \State $\tuple{s_{ret},id_{ret}} \gets GetCR(de_{cr})$\r
+\Else\r
+ \State $\tuple{s_{ret},id_{ret}} \r
+ \gets \emptyset$\r
+\EndIf\r
+\State $de_{r_{cr}} \gets de_s$ \textit{such that} $de_s \in DE_s, \r
+ de_s \in D \land de_s = cr \land de_s \neq de_{cr}$\r
+\If{$de_{r_{cr}} \neq \emptyset$}\r
+ \State $\tuple{s_{r_{ret}},id_{r_{ret}}} \gets GetCR(de_{r_{cr}})$\r
+\Else\r
+ \State $\tuple{s_{r_{ret}},id_{r_{ret}}} \r
+ \gets \emptyset$\r
+\EndIf\r
+\State \Return{$\{\tuple{s_{ret},id_{ret}},\tuple{s_{r_{ret}},id_{r_{ret}}}\}$}\r
\EndFunction\r
\end{algorithmic}\r
\r
\end{algorithmic}\r
\r
\begin{algorithmic}[1]\r
-\Function{CheckLastSeqN}{$MS_s,MS_t$}\Comment{Check $MS_t$ based on $MS_s$}\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 $error \gets$ 'Invalid last $s$ for this machine'\r
- \State \Return{error}\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 $error \gets$ 'Invalid last $s$ for machine $id_t$'\r
- \State \Return{error}\r
+ \State \Call{ReportError}{'Invalid last $s$ for machine $id_t$'}\r
\EndIf\r
\EndIf\r
\EndIf\r
\EndFor\r
-\State \Return{$\emptyset$}\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
+ \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
+ \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
+\EndIf\r
+\EndProcedure\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Function{StoreLastSlot}{$MS_s,sl_l,s_s,sv_s,id_s$}\r
+\State $s_{min} \gets MinLastSeqN(MS_s)$\r
+\If{$s_{min} \neq \emptyset \land s_{min} = s_s$}\Comment{$MS$ initially empty}\r
+ \State $sl_l \gets CreateLastSL(s_s,sv_s,id_s)$\r
+\EndIf\r
+\State \Return{$sl_l$}\r
\EndFunction\r
\end{algorithmic}\r
\r
\begin{algorithmic}[1]\r
\Function{UpdateDT}{$DT_s,Dat_s$}\r
\State $DE_s \gets GetDatEnt(Dat_s)$\r
-\ForAll{$de_i \in DE_s$}\r
- \If{$de_i \mid de_i \in D \land de_i = kv$}\r
- \State $\tuple{k_s,v_s} \gets GetKV(de_i)$\r
- \State $k_s \gets GetKey(\tuple{k_s,v_s})$\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
\end{algorithmic}\r
\r
\begin{algorithmic}[1]\r
-\Function{GetKVPairs}{$s$}\r
-\State $SL_c \gets \Call{GetSlot}{s}$\r
-\State $MS_c \gets \emptyset$\r
-\ForAll{$\tuple{s_i,sv_i} \in SL_c$}\r
- \State $s_i \gets SeqN(\tuple{s_i,sv_i})$\r
- \State $sv_i \gets SlotVal(\tuple{s,sv_i})$\r
- \State $Dat_i \gets Decrypt(SK,sv_i)$\r
- \State $s_s \gets GetSeqN(Dat_s)$\r
- \If{$s_i \neq s_s$}\r
- \State $error \gets$ 'Invalid sequence number'\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
+\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 $s_{g_{in}} \gets GetSeqN(Dat_g)$\r
+ \If{$s_g \neq s_{g_{in}}$}\r
+ \State \Call{ReportError}{'Invalid sequence number'}\r
\EndIf\r
- \If{$\Call{ValidPrevHmac}{Dat_i,hmac_p} = false$}\r
- \State $error \gets$ 'Invalid previous HMAC value'\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
\EndIf\r
- \If{$\Call{ValidHmac}{Dat_i,SK} = false$}\r
- \State $error \gets$ 'Invalid current HMAC value'\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
\EndIf\r
- \State $hmac_p \gets \Call{Hmac}{Dat_i,SK}$\Comment{Update $hmac_p$ for next slot check}\r
- %\State $max_c \gets \Call{GetQueSta}{Dat_i,max_c}$\Comment{Handle qs}\r
- \State $qs_c \gets \Call{GetQueSta}{Dat_i}$\Comment{Handle qs}\r
- \If{$qs_c > max_c$}\r
- \State $max_c \gets qs_c$\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
+ \If{$qs_g \neq \emptyset \land qs_g > max_g$}\r
+ \State $max_g \gets qs_g$\r
\EndIf\r
%Check for last s in Dat\r
- \State $id_i \gets GetMacId(Dat_i)$\Comment{Handle last s}\r
- \State $MS_c \gets \Call{UpdateLastSeqN}{id_i,s_i,MS_c}$\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_j,s_{j_{last}}} \gets \Call{GetSlotSeq}{Dat_i}$\Comment{Handle ss}\r
- \State $MS_c \gets \Call{UpdateLastSeqN}{id_j,s_{j_{last}},MS_c}$\r
- \State $DT \gets \Call{UpdateDT}{DT,Dat_i}$\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
+ \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
\EndFor\r
-\If{$m + |SL_c| \leq max_c$}\Comment{Check actual size against $max_c$}\r
- \State $m \gets m + |SL_c|$\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 $error \gets$ 'Actual queue size exceeds $max_c$'\r
+ \State \Call{ReportError}{'Actual queue size exceeds $max_g$'}\r
\EndIf\r
- \State $error \gets \Call{CheckLastSeqN}{MS_c,MS}$\r
-\State \Return{$DT$}\r
-\EndFunction\r
+\State $\Call{CheckLastSeqN}{MS_g,MS}$\r
+\EndProcedure\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Procedure{GetKVPairs}{}\r
+\State $s_g \gets GetLastSeqN(MS,id_{self}) + 1$\r
+\State $SL_c \gets \Call{GetSlot}{s_g}$\r
+\State $\Call{ProcessSL}{SL_c}$\Comment{Process slots and update DT}\r
+\EndProcedure\r
\end{algorithmic}\r
\r
\begin{algorithmic}[1]\r
\Function{GetValFromKey}{$k_g$}\r
-\State $\tuple{k_s,v_s} \gets \tuple{k,v} \mid \tuple{k,v} \in DT \land k = k_g$\r
-\State $v_s \gets GetVal(\tuple{k_s,v_s})$\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
\EndFunction\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{$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{$id_{self}$ = machine Id of this client} \\\r
+\textit{$sl_{last}$ = info of last slot in queue = \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{$KV$ = set of $\tuple{ck, \tuple{k,v}}$ of kv 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
+$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
+$\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
+\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
+\Else\r
+ \State $KV_s \gets (KV_s - \{\tuple{ck_s, \tuple{k_s,v_t}}\}) \cup \r
+ \{\tuple{ck_s, \tuple{k_s,v_s}}\}$\r
+\EndIf\r
+\State \Return{$KV_s$}\r
+\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
+\If{$n_{dead} \leq th_s$}\r
+ \State $max'_s \gets max'_t + m'_s$\r
+\Else\r
+ \State $max'_s \gets \emptyset$\r
+\EndIf\r
+\State \Return{$max'_s$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Function{CheckNeedSS}{$MS_s,max'_t$}\Comment{Check if $ss$ is needed}\r
+\State $s_{last_{min}} \gets MinLastSeqN(MS_s)$\r
+\State $s_{last_{max}} \gets MaxLastSeqN(MS_s)$\r
+\State $n_{live} \gets s_{last_{max}} - s_{last_{min}}$\Comment{Number of live slots}\r
+\State $n_{dead} \gets max'_t - n_{live}$\r
+\State \Return {$n_{dead} = 0$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Function{HandleCollision}{$\tuple{stat_s,SL_s}$}\r
+\State $stat_s \gets GetStatus(\tuple{stat_s,SL_s})$\r
+\State $SL_s \gets GetSL(\tuple{stat_s,SL_s})$\r
+\If{$\neg stat_s$}\Comment{Handle collision}\r
+ \State $\tuple{s_{col},sv_{col}} \gets GetColSeqN(SL_s,s_s)$\r
+ \State $s_{col} \gets SeqN(\tuple{s_{col},sv_{col}})$\r
+ \State $sv_{col} \gets SlotVal(\tuple{s_{col},sv_{col}})$\r
+ \State $Dat_{col} \gets Decrypt(SK,sv_{col})$\r
+ \State $id_{col} \gets GetMacId(Dat_{col})$\r
+ \State $\tuple{s_{col},id_{col}} \gets CreateCR(s_{col},id_{col})$\r
+ \State $cr_s \gets \tuple{s_{col},id_{col}}$\r
+\Else\r
+ \State $cr_s \gets \emptyset$\r
+\EndIf\r
+\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
+\EndIf\r
+\State \Return{$cr_s$}\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
+\r
+\r
+\begin{algorithmic}[1]\r
+\Function{GetDEPairs}{$KV_s,max'_s,need_s,sl_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
+ \{\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
+ \{\tuple{k_s,v_s} \mid \tuple{ck_s,\tuple{k_s,v_s}} \in KV_s,\r
+ ck_g \leq ck_s < ck_g + cp_s\}$\r
+ \If{$|DE_{ret}| = cp$}\r
+ \State $ck_g \gets ck_g + cp_s$\Comment{Middle of KV set}\r
+ \Else\r
+ \State $ck_g \gets 0$\Comment{End of KV set}\r
+ \EndIf\r
+\EndIf\r
+\State \Return{$DE_{ret}$}\r
+\EndFunction\r
+\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
+\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{Formal Guarantees}\r
\r
\textit{To be completed ...}\r
projects / iotcloud.git / blobdiff