Adding rollback/mismatch detection when updating last sequence number
authorrtrimana <rtrimana@uci.edu>
Mon, 22 Aug 2016 23:12:14 +0000 (16:12 -0700)
committerrtrimana <rtrimana@uci.edu>
Mon, 22 Aug 2016 23:12:14 +0000 (16:12 -0700)
doc/iotcloud.tex

index 1016f55..9d10557 100644 (file)
@@ -310,6 +310,15 @@ $MaxSMSeqN(SM_s)= s$ \textit{such that} $\tuple{s, id} \in SM_s
 \If{$s_t = \emptyset$}\r
        \State $MS_s[id_s] = s_s$  \Comment{First occurrence}\r
 \Else\r
+       \If{$id_s = id_{self}$}\r
+               \If{$s_t \neq s_s$}\Comment{Check for mismatch on $s$}\r
+                       \State \Call{Error}{'Mismatch on $s$ for $id_{self}$'}\r
+               \EndIf\r
+       \Else\r
+               \If{$s_t > s_s$}\Comment{Check for rollback on $s$}\r
+                       \State \Call{Error}{'Rollback on $s$ for $id_s$'}\r
+               \EndIf\r
+       \EndIf\r
        \State $MS_S[id_s] \gets max(s_t, s_s)$\r
 \EndIf\r
 \State \Return{$MS_s$}\r