Adding collision resolution entry - preserved by checking against last sequence numbe...

diff --git a/doc/iotcloud.tex b/doc/iotcloud.tex
index 24afdf162a341db9c235e316c7f58c8bf1da28a2..db89d2b2c2e02e7a34285d043ebf64a0d8b9f3aa 100644 (file)
--- a/doc/iotcloud.tex
+++ b/doc/iotcloud.tex
@@ -56,7 +56,7 @@ e.g. 50 and 70, the client knows that when it sees 50, it should expect
 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
@@ -185,7 +185,9 @@ $kv$ is a key-value entry $\tuple{k,v}$, $kv \in D$ \\
 $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
+$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
@@ -201,6 +203,8 @@ $sv_s = \tuple{s, E(Dat_s)} =
 (initially empty)} \\\r
 \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{$SM$ = set of $\tuple{s, id}$ of all slots in a previous read\r
+(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 and m \leq n$)} \\\r
 \textit{$hmac_p$ = the HMAC value of the previous slot ($hmac_p = \emptyset$ \r
@@ -217,20 +221,21 @@ $Slot(SL_s,s_s)= \tuple{s, sv}$ \textit{such that} $\tuple{s, sv}
 $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
-$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$ \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
+$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, \r
-id = id_s$ \\\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}$ \textit{such that} $\tuple{k, v} \r
@@ -291,7 +296,7 @@ $GetKeyVal(DT_s,k_s)= \tuple{k, v}$ \textit{such that} $\tuple{k, v}
 \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{$\tuple{id_{ret},s_{last_{ret}}} \neq \emptyset$}\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
@@ -300,6 +305,21 @@ $GetKeyVal(DT_s,k_s)= \tuple{k, v}$ \textit{such that} $\tuple{k, v}
 \EndFunction\r
 \end{algorithmic}\r
 \r
+\begin{algorithmic}[1]\r
+\Function{GetColRes}{$Dat_s$}\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 \Return{$\tuple{s_{ret},id_{ret}}$}\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
@@ -337,6 +357,17 @@ $GetKeyVal(DT_s,k_s)= \tuple{k, v}$ \textit{such that} $\tuple{k, v}
 \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{UpdateDT}{$DT_s,Dat_s$}\r
 \State $DE_s \gets GetDatEnt(Dat_s)$\r
@@ -361,13 +392,15 @@ $GetKeyVal(DT_s,k_s)= \tuple{k, v}$ \textit{such that} $\tuple{k, v}
 \Function{GetKVPairs}{$s$}\r
 \State $SL_c \gets \Call{GetSlot}{s}$\r
 \State $MS_c \gets \emptyset$\r
+\State $SM_{curr} \gets \emptyset$\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_{min}},sv_{c_{min}}})$\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
+\For{$s_c \gets s_{c_{min}}$ \textbf{to} $s_{c_{max}}$}\Comment{Process slots \r
+       in $SL_c$ in order}\r
        \State $\tuple{s_c,sv_c} \gets Slot(SL_c,s_c)$\r
+       \State $SM_{curr} \gets SM_{curr} \cup \{\tuple{s_c,sv_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
@@ -394,14 +427,25 @@ $GetKeyVal(DT_s,k_s)= \tuple{k, v}$ \textit{such that} $\tuple{k, v}
        \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 $\tuple{s_e,id_e} \gets \r
+       \Call{GetColRes}{Dat_c}$\Comment{Handle cr}\r
+       \If{$\tuple{s_e,id_e} \neq \emptyset$}\r
+               \State $s_e \gets GetS(\tuple{s_e,id_e})$\r
+               \State $id_e \gets GetId(\tuple{s_e,id_e})$\r
+               \State $s_{c_{last}} \gets GetLastSeqN(MS,id_e)$\r
+               \If{$s_{c_{last}} < s_e$}\r
+                       \State $\Call{CheckColRes}{SM,\tuple{s_e,id_e}}$\r
+               \EndIf\r
+    \EndIf\r
        \State $DT \gets \Call{UpdateDT}{DT,Dat_c}$\r
 \EndFor\r
+\State $SM \gets SM_{curr}$\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 \Call{ReportError}{'Actual queue size exceeds $max_c$'}\r
 \EndIf\r
-       \State $\Call{CheckLastSeqN}{MS_c,MS}$\r
+\State $\Call{CheckLastSeqN}{MS_c,MS}$\r
 \State \Return{$DT$}\r
 \EndFunction\r
 \end{algorithmic}\r