Client read slots algorithm - Cleaning up, adding error function, making sure that...

diff --git a/doc/iotcloud.tex b/doc/iotcloud.tex
index eb6fca108e8d8819a20d66a56bb33a7d06359803..67204d1e3bbd320882c74ade3ecc997cd390b54d 100644 (file)
--- a/doc/iotcloud.tex
+++ b/doc/iotcloud.tex
@@ -76,7 +76,7 @@ or user-level data) is dead if there is a newer slot from the same machine.
 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
@@ -202,16 +202,18 @@ $sv_s = \tuple{s, E(Dat_s)} =
 \textit{$MS_c$ = 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{m = number of slots on client (initially $m = 0 and 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
 \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
 $Decrypt(SK_s,sv_s)=Dat_s=\tuple{s,id,hmac_p,DE,hmac_c}$ \\\r
@@ -223,73 +225,63 @@ $GetMacId(Dat_s = \tuple{s,id,hmac_p,DE,hmac_c})=id$ \\
 $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
+$GetQS(de_s$ \textit{such that} $de_s \in D \land de_s = qs)=qs$ \\\r
+$GetSS(de_s$ \textit{such that} $de_s \in D \land de_s = ss)=ss$ \\\r
+$GetKV(de_s$ \textit{such that} $de_s \in D \land de_s = kv)=kv=\tuple{k,v}$ \\\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, \r
 id = id_s$ \\\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
 \r
 \begin{algorithmic}[1]\r
-\Function{CreateSK}{$uid,pw$}\r
-\State $SK = ComputeHash(uid + pw)$\r
-\State \Return{$SK$}\r
-\EndFunction\r
-\end{algorithmic}\r
-\r
-\begin{algorithmic}[1]\r
-\Function{Hmac}{$Dat_s,SK_s$}\r
-\State \Return{$ComputeHmac(Dat_s,SK_s)$}\r
-\EndFunction\r
+\Procedure{ReportError}{$msg$}\r
+\State $Print(msg)$\r
+\State $Halt()$\r
+\EndProcedure\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
+\State $hmac_{computed} \gets Hmac(Dat_s,SK_s)$\r
 \If{$hmac_{stored} = hmac_{computed}$}\r
-       \State \Return{$true$}\r
+       \State $valid \gets true$\r
 \Else\r
-       \State \Return{$false$}\r
+       \State $valid \gets false$\r
 \EndIf\r
+\State \Return{$valid$}\r
 \EndFunction\r
 \end{algorithmic}\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
+       \State $valid \gets true$\r
 \Else\r
-       \State \Return{$false$}\r
+       \State $hmac_{stored} \gets GetPrevHmac(Dat_s)$\r
+       \If{$hmac_{stored} = hmac_{p_s}$}\r
+               \State $valid \gets true$\r
+       \Else\r
+               \State $valid \gets false$\r
+       \EndIf\r
 \EndIf\r
+\State \Return{$valid$}\r
 \EndFunction\r
 \end{algorithmic}\r
 \r
 \begin{algorithmic}[1]\r
 \Function{GetQueSta}{$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 $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 $qs_{ret} \gets \emptyset$\r
+\EndIf\r
 \State \Return{$qs_{ret}$}\r
 \EndFunction\r
 \end{algorithmic}\r
@@ -297,13 +289,13 @@ $GetKeyVal(DT_s,k_s)= \tuple{k, v} \mid \tuple{k, v}
 \begin{algorithmic}[1]\r
 \Function{GetSlotSeq}{$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 = 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 $de_{ss} \gets de_s$ \textit{such that} $de_s \in DE_s, \r
+       de_s \in D \land de_s = ss$\r
+\If{$\tuple{id_{ret},s_{last_{ret}}} \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
@@ -324,36 +316,33 @@ $GetKeyVal(DT_s,k_s)= \tuple{k, v} \mid \tuple{k, v}
 \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
-\EndFunction\r
+\EndProcedure\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
+\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 $k_s \gets GetKey(\tuple{k_s,v_s})$\r
                \State $\tuple{k_s,v_t} \gets GetKeyVal(DT_s,k_s)$\r
                \If{$\tuple{k_s,v_t} = \emptyset$}\r
@@ -372,47 +361,55 @@ $GetKeyVal(DT_s,k_s)= \tuple{k, v} \mid \tuple{k, v}
 \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
+\State $\tuple{s_{c_{max}},sv_{c_{max}}} \gets MaxSlot(SL_c)$\r
+\State $s_{c_{max}} \gets SeqN(\tuple{s_{c_{max}},sv_{c_{max}}})$\r
+\State $\tuple{s_{c_{min}},sv_{c_{min}}} \gets MinSlot(SL_c)$\r
+\State $s_{c_{min}} \gets SeqN(\tuple{s_{c_{max}},sv_{c_{max}}})$\r
+%\For{$\{\tuple{s_c,sv_c} \mid \tuple{s_c,sv_c} \in SL_c\}$}\r
+\For{$s_c \gets s_{c_{min}}$ \textbf{to} $s_{c_{max}}$}\r
+       \State $\tuple{s_c,sv_c} \gets Slot(SL_c,s_c)$\r
+    \State $s_c \gets SeqN(\tuple{s_c,sv_c})$\r
+       \State $sv_c \gets SlotVal(\tuple{s_c,sv_c})$\r
+       \State $Dat_c \gets Decrypt(SK,sv_c)$\r
+       \State $s_{c_{in}} \gets GetSeqN(Dat_c)$\r
+    \If{$s_c \neq s_{c_{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
+       \If{$\neg \Call{ValidPrevHmac}{Dat_c,hmac_p}$}\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
+       \If{$\neg \Call{ValidHmac}{Dat_c,SK}$}\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 $hmac_p \gets Hmac(Dat_c,SK)$\Comment{Update $hmac_p$ for next slot check}\r
+       \State $qs_c \gets \Call{GetQueSta}{Dat_c}$\Comment{Handle qs}\r
+       \If{$qs_c \neq \emptyset \land qs_c > max_c$}\r
                \State $max_c \gets qs_c$\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_c \gets GetMacId(Dat_c)$\Comment{Handle last s}\r
+       \State $MS_c \gets \Call{UpdateLastSeqN}{id_c,s_c,MS_c}$\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_c}$\Comment{Handle ss}\r
+       \If{$\tuple{id_d,s_{d_{last}}} \neq \emptyset$}\r
+       \State $MS_c \gets \Call{UpdateLastSeqN}{id_d,s_{d_{last}},MS_c}$\r
+       \EndIf\r
+       \State $DT \gets \Call{UpdateDT}{DT,Dat_c}$\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
 \Else\r
-       \State $error \gets$ 'Actual queue size exceeds $max_c$'\r
+       \State \Call{ReportError}{'Actual queue size exceeds $max_c$'}\r
 \EndIf\r
-       \State $error \gets \Call{CheckLastSeqN}{MS_c,MS}$\r
+       \State $\Call{CheckLastSeqN}{MS_c,MS}$\r
 \State \Return{$DT$}\r
 \EndFunction\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 $\tuple{k_s,v_s} \gets \tuple{k,v}$ \textit{such that} $\tuple{k,v} \r
+       \in DT \land k = k_g$\r
 \State $v_s \gets GetVal(\tuple{k_s,v_s})$\r
 \State \Return{$v_s$}\r
 \EndFunction\r