Edits
[iotcloud.git] / version2 / doc / iotcloud_formal / iotcloud.tex
index 679c218fe228d7200b070acc53ad7085a085954b..8f1559282d592b68082f3bbe197a9092cc55c68f 100644 (file)
@@ -102,10 +102,6 @@ Delete slot is an operation that deletes all live slots that have server sequenc
 \r
 \r
 \r
-\r
-\r
-\r
-\r
 \section{\textbf{Client}}\r
 The data structure acts as a key store where key-value pairs can be read and set.\r
 The data structure exposes the following functions:\r
@@ -115,6 +111,43 @@ The data structure exposes the following functions:
     \item Create new key\r
 \end{itemize}\r
 \r
+\r
+\subsubsection{\textbf{Types of Payloads}}\r
+The different types of record payloads are:\r
+\begin{itemize}\r
+    \item Transactions\r
+        \begin{itemize}\r
+            \item Used to make updates to key value pairs.\r
+        \end{itemize}\r
+    \item Commit notifications\r
+        \begin{itemize}\r
+            \item Contains the commit of a single transaction, the whole transaction.\r
+            \item There is 1 commit per transaction.\r
+            \item Generated by the arbitrator for the set of key-value gets and sets in the transaction.\r
+        \end{itemize}\r
+    \item Abort notifications\r
+        \begin{itemize}\r
+            \item Causes a transaction to be aborted, key-values not used in updates.\r
+        \end{itemize}\r
+    \item Data structure re-size notifications\r
+        \begin{itemize}\r
+            \item Contains new size of data structure (number of record allowed in the data structure or something like that).\r
+        \end{itemize}\r
+    \item Server sequence number confirmations.\r
+        \begin{itemize}\r
+            \item Created by any device if that device finds a record with a server sequence number that does not have a server sequence number conformation yet.\r
+        \end{itemize}\r
+    \item Delete notifications\r
+        \begin{itemize}\r
+            \item Generated when a device deletes a record.\r
+            \item records the record that was last deleted\r
+        \end{itemize}\r
+    \item New Key notification\r
+        \begin{itemize}\r
+            \item Generated when a device generates a new (never used) key-value pair.\r
+        \end{itemize}\r
+\end{itemize}\r
+\r
 \subsection{\textbf{Client Notation Conventions}}\r
 \r
 $K$ is the set of all keys.\\\r
@@ -132,7 +165,7 @@ $kv_n$ is a key-value entry $\tuple{k_n,v_n} , k \in K$\\
 \r
 $tid_s = \tuple{mid_s,c_{mid_s}}$\\\r
 $guard_s = \tuple{\{kv_1, kv_2, ... ,kv_n | \exists mid \in MID, \forall n, kv_n[k] \in K_{mid}\},$ boolean condition using $ \{kv_1, kv_2, ... ,kv_n\}} $\\\r
-$transaction_s = \{mid_s,vc_{s_t} ,\{kv_1, kv_2,...kv_n | \exists mid \in MID, mid = guard_s[mid], \forall n, kv_n[k] \in K_{mid}\},guard_s\}$\\\r
+$transaction_s = \tuple{mid_s,vc_{s_t} ,\{kv_1, kv_2,...kv_n | \exists mid \in MID, mid = guard_s[mid], \forall n, kv_n[k] \in K_{mid}\},guard_s}$\\\r
 $commit_s = \tuple{tid_s,vc_s}$\\\r
 $abort_s = \tuple{tid_s,mid_s,vc_s}$\\\r
 $sequence_s = \tuple{rid_s, ssn_s}$\\\r
@@ -147,16 +180,14 @@ $record_s = \tuple{ssn_s,rd_s}$\\
 \subsection{\textbf{Client State}}\r
 \textit{s = largest server sequence number pulled from the server by a device} \\\r
 \textit{R = set of records pulled from the server so far with their server sequence numbers} \\\r
-\textit{RL = set of records that contain live data} \\\r
 \r
 \subsection{Helper Functions}\r
 The following helper functions are needed:\\\r
 \r
-\r
-%Throw Error\r
+% Error\r
 \noindent\fbox{%\r
 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
-\textbf{Throw Error:}\r
+\textbf{ Error:}\r
 \begin{algorithmic}[1]\r
 \Function{Error}{$msg$}\r
     \State $Print(msg)$\r
@@ -166,28 +197,6 @@ The following helper functions are needed:\\
 \end{varwidth}% \r
 }\r
 \r
-%Error Message\r
-\begin{algorithmic}[1]\r
-\Procedure{Error}{$msg$}\r
-\State $Print(msg)$\r
-\State $Halt()$\r
-\EndProcedure\r
-\end{algorithmic}\r
-\r
-\r
-%Get Latest Data Structure From Server\r
-\noindent\fbox{%\r
-\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
-\textbf{Get  Latest Data Structure From Server}:\r
-\begin{algorithmic}[1]\r
-\Function{GetLatestDataStruct}{}\r
-    \State $largestSsn \gets $ Largest $ssn$ of all $ssn$ in $R$\r
-    \State $R \gets R \cup $ \Call{GetSlotServer}{$largestSsn + 1$}\r
-\EndFunction\r
-\end{algorithmic}\r
-\end{varwidth}% \r
-}\r
-\r
 %Get Payload Items from Record with SSN\r
 \noindent\fbox{%\r
 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
@@ -199,7 +208,7 @@ The following helper functions are needed:\\
     \State $\tuple{mid_s, vc_s, hmac_s, payload_s} \gets rd_s$\\\r
     \r
     \ForAll{$payloadItems$ in $payload_s$}\r
-        \State $PISSN \gets PISSN \cup \tuple{payloadItem, ssn_s}$\r
+        \State $PISSN \gets PISSN \cup \{\tuple{payloadItem, ssn_s}\}$\r
     \EndFor\\\r
     \r
     \State \Return {$PISSN$}\r
@@ -208,10 +217,10 @@ The following helper functions are needed:\\
 \end{varwidth}% \r
 }\r
 \r
-%Get rid For Record\r
+%Get rid of record\r
 \noindent\fbox{%\r
 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
-\textbf{Get rid For Record}:\r
+\textbf{Get rid of record:}\r
 \begin{algorithmic}[1]\r
 \Function{GetRid}{$record_s$}\r
     \State $\tuple{ssn_s, \tuple{mid_s, \{c_{mid_1}, c_{mid_2}, ... , c_{mid_k}\}, hmac_s, payload_s}} \gets record_s$\r
@@ -221,6 +230,82 @@ The following helper functions are needed:\\
 \end{varwidth}% \r
 }\r
 \r
+%Get tid of transaction\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Get tid of transaction:}\r
+\begin{algorithmic}[1]\r
+\Function{GetTid}{$transaction_s$}\r
+    \State $\tuple{ssn_s,\{c_{mid_1}, c_{mid_2}, ... , c_{mid_k}\}, \{kv_1, kv_2,...kv_n\}, guard_s} \gets record_s$\r
+    \State \Return {$\tuple{mid_s, c_{mid_s}}$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
+\r
+%Key Value Live\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Key Value Live:}\r
+\begin{algorithmic}[1]\r
+\Function{KeyValueLive}{$keyName_s, transaction_s$}\r
+    \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\r
+    \State $AT \gets \emptyset$    \Comment{Set of all Payload Items that are transactions}\r
+    \State $AC \gets \emptyset$    \Comment{Set of all Payload Items that are commits}\r
+    \State $AA \gets \emptyset$    \Comment{Set of all Payload Items that are aborts}\r
+    \State $commitTrans = NULL$\r
+    \State $tid \gets $ \Call{GetTid}{$transaction_s$}\\\r
+\r
+    \ForAll{$record$ in $R$}\r
+        \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}\r
+    \EndFor\\\r
+    \r
+    \ForAll{$\tuple{ssn, payload}$ in $API$}\r
+        \If{$payload$ is a $transaction$}\r
+            \State $AT \gets AT \cup \{payload\}$\r
+        \ElsIf{$payload$ is a $commit$}\r
+            \State $AC \gets AC \cup \{payload\}$\r
+        \ElsIf{$payload$ is a $abort$}\r
+            \State $AA \gets AA \cup \{payload\}$\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \ForAll{$\tuple{tid',mid',vc'}$ in $AA$} \Comment{Has an abort}\r
+        \If{$tid' = tid$}\r
+            \State \Return{False}\r
+        \EndIf\r
+    \EndFor\\\r
+\r
+    \ForAll{$\tuple{tid',vc'}$ in $AC$} \Comment{Has a commit}\r
+        \If{$tid' = tid$}\r
+            \State $commitTrans \gets \tuple{tid',vc'}$\r
+            \State Break\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \If{$commitTrans = NULL$}   \r
+        \State \Return{True} \Comment{If transaction not yet committed then alive}\r
+    \EndIf\\\r
+    \r
+    \State $\tuple{tid_c, vc_c} \gets commitTrans$\r
+    \ForAll{$trans$ in $AT$}\r
+        \State $\{mid_t,vc_t ,\{\tuple{k_1, v_1}, \tuple{k_2, v_2},..., \tuple{k_k, v_k}\},guard_t\} \gets trans$\r
+        \If{$(trans \neq transaction_s) \land (keyName_s = k_n)$}\r
+            \ForAll{$\tuple{tid_c',vc_c'}$ in $AC$}\r
+                \If{$(tid_c = $ \Call{GetTid}{$trans$} $) \land (vc_c' > vc_c)$}\r
+                    \State \Return{False}\r
+                \EndIf\r
+            \EndFor\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \State \Return{True}\r
+    \r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
 %Sequence Live\r
 \noindent\fbox{%\r
 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
@@ -300,14 +385,32 @@ The following helper functions are needed:\\
 \textbf{Abort Live}:\r
 \begin{algorithmic}[1]\r
 \Function{AbortLive}{$abort_s$}\r
+    \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\r
+    \State $tid \gets NULL$\r
     \State $\tuple{tid_s,mid_s,vc_s} \gets abort_s$\\\r
+\r
+    \ForAll{$record$ in $R$}\r
+        \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}\r
+    \EndFor\\\r
+    \r
+    \ForAll{$\tuple{ssn, payload}$ in $API$} \Comment{Transaction still in data structure}\r
+        \If{$payload$ is a $transaction$}\r
+            \State $tid \gets $\Call{GetTid}{$payload$}\r
+            \If{$tid = tid_s$}\r
+                \State Return{True}\r
+            \EndIf\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \r
+    \r
     \ForAll{record in R}\r
         \State $\tuple{ssn_s',\tuple{mid_s', vc_s', hmac_s', payload_s'}} \gets record$\r
         \If{$(mid_s'=mid_s) \land (vc_s' > vc_s)$}\r
-            \State \Return{True}\r
+            \State \Return{False}\r
         \EndIf\r
     \EndFor\\\r
-    \State \Return{False}\r
+    \State \Return{True}\r
 \EndFunction\r
 \end{algorithmic}\r
 \end{varwidth}% \r
@@ -383,6 +486,91 @@ The following helper functions are needed:\\
 \end{varwidth}% \r
 }\r
 \r
+%Transaction Live\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Transaction Live:}\r
+\begin{algorithmic}[1]\r
+\Function{TransactionLive}{$transaction_s$}\r
+    \State $AA \gets \emptyset$    \Comment{Set of all Payload Items that are aborts}\r
+    \State $AC \gets \emptyset$    \Comment{Set of all Payload Items that are commits}\r
+    \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\r
+    \State $tid \gets $ \Call{GetTid}{$transaction_s$}\r
+    \State $foundCommit \gets False$\\\r
+    \r
+    \ForAll{$record$ in $R$}\r
+        \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}\r
+    \EndFor\\\r
+    \r
+    \ForAll{$\tuple{ssn, payload}$ in $API$}\r
+        \If{$payload$ is a $abort$}\r
+            \State $AA \gets AA \cup \{payload\}$\r
+        \ElsIf{$payload$ is a $commit$}\r
+            \State $AC \gets AC \cup \{payload\}$\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \ForAll{$\tuple{tid',mid',vc'}$ in $AA$} \Comment{There is an abort}\r
+        \If{$tid' = tid$}\r
+            \State \Return{False}\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \ForAll{$\tuple{tid',vc'}$ in $AC$} \Comment{There is no commit}\r
+        \If{$tid' = tid$}\r
+            \State $foundCommit \gets True$\r
+            \State Break\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \If{$\lnot foundCommit$}\r
+        \State \Return{True}\r
+    \EndIf\\\r
+    \r
+    \State $\tuple{mid',vc' ,kvSet',guard'} \gets transaction_s$ \Comment{All Keys are dead}\r
+    \ForAll{$\tuple{k',v'}$ in $kvSet'$}\r
+        \If{\Call{KeyValueLive}{$k', transaction_s$}}\r
+            \State \Return{True}\r
+        \EndIf\r
+    \EndFor\r
+\r
+    \State \Return{False}\r
+\r
+\EndFunction\r
+\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
+\r
+%Commit Live\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Commit Live:}\r
+\begin{algorithmic}[1]\r
+\Function{CommitLive}{$commit_s, ssn_s$}\r
+    \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\r
+    \State $AT \gets \emptyset$    \Comment{Set of all Payload Items that are transaction}\r
+    \State $tid' \gets NULL$ \r
+    \State $\tuple{tid, vc} \gets commit_s$ \\ \r
+\r
+    \ForAll{$record$ in $R$}\r
+        \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}\r
+    \EndFor\\\r
+    \r
+    \ForAll{$\tuple{ssn, payload}$ in $API$}\r
+        \If{$payload$ is a $transaction$}\r
+            \State $tid' \gets$ \Call{GetTid}{$payload$}\r
+            \If{$tid' = tid$}\r
+                \State \Return{True}\r
+            \EndIf\r
+        \EndIf\r
+    \EndFor\\\r
+\r
+    \State \Return{False}\r
+\EndFunction\r
+\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
+\r
 %Is Live\r
 \noindent\fbox{%\r
 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
@@ -390,7 +578,7 @@ The following helper functions are needed:\\
 \begin{algorithmic}[1]\r
 \Function{IsLive}{$item_s, ssn_S$}\r
     \If{$item_s$ is a $tansaction$}\r
-        \State \Return{\Call{TransactionLive}{$item_s, ssn_s$}}\r
+        \State \Return{\Call{TransactionLive}{$item_s$}}\r
     \r
     \ElsIf{$item_s$ is a $commit$}\r
         \State \Return{\Call{CommitLive}{$item_s, ssn_s$}}\r
@@ -464,6 +652,41 @@ The following helper functions are needed:\\
 \end{varwidth}% \r
 }\r
 \r
+%Rescue New Key\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Rescue New Key:}\r
+\begin{algorithmic}[1]\r
+\Function{RescueNewKey}{$newKeyPayload, ssn$}\r
+    \State $\tuple{k', vc', ssn', mid'} \gets newKeyPayload$\r
+    \State \Return{$\tuple{k', vc', ssn, mid'}$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
+\r
+%Rescue Transaction\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Rescue New Key:}\r
+\begin{algorithmic}[1]\r
+\Function{RescueTransaction}{$transPayload, ssn$}\r
+    \State $KVRescue \gets \emptyset$\r
+    \State $\tuple{mid',vc', KVSet,guard_s} \gets transPayload$\\\r
+    \r
+    \ForAll{$\tuple{k,v}$ in $KVSet$}\r
+        \If{\Call{KeyValueLive}{$k, transPayload$}}\r
+            \State $KVRescue \gets KVRescue \cup \{\tuple{k,v}\}$\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \State \Return{$\tuple{mid',vc', KVRescue,guard_s}$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
+\r
+\r
 %Rescue Payload Items\r
 \noindent\fbox{%\r
 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
@@ -484,14 +707,20 @@ The following helper functions are needed:\\
     \State Sort $PIList$ by $ssn$ from lowest to highest\\\r
     \r
     \ForAll{$\tuple{ssn', payload'}$ in $PIList$}\r
-        \If{\Call{IsLive}{$payload', ssn'$} $\land$ \Call{getRandomBoolean}{ } }\r
+        \If{\Call{IsLive}{$payload', ssn'$} $\land$ \Call{getRandomBoolean}{ } }\\\r
+            \r
+            \If{$payload'$ is a $newkey$}\r
+                \State $payload' \gets $ \Call{RescueNewKey}{$payload'$}\r
+            \ElsIf{$payload'$ is a $transaction$}\r
+                \State $payload' \gets $ \Call{RescueTransaction}{$payload'$}\r
+            \EndIf\\\r
         \r
             \If{\Call{GetSize}{$payload'$} $ > SpaceRemaining$} \Comment{No more space for resuces in payload}\r
                 \State \Return{$payload_s$}\r
             \EndIf\r
             \r
             \State $SpaceRemaining \gets SpaceRemaining -$ \Call{GetSize}{$payload'$}\r
-            \State $payload_s \gets payload_s \cup payload'$\r
+            \State $payload_s \gets payload_s \cup \{payload'\}$\r
         \EndIf\r
     \EndFor\\\r
     \State \Return{$payload_s$}\r
@@ -554,7 +783,7 @@ The following helper functions are needed:\\
     \State $rp \gets$ Empty $resize$ payload\r
     \State $cs \gets$ \Call{GetDataStrucSize}{ }\r
     \State $rp \gets \tuple{cs * 2}$\r
-    \State \Return{$rp$}\r
+    \State \Return{$\{rp\}$}\r
 \EndFunction\r
 \end{algorithmic}\r
 \end{varwidth}% \r
@@ -644,7 +873,8 @@ The following helper functions are needed:\\
     \State $payload_s \gets$ \Call{RescuePayloadItems}{$payload_s$}\r
     \State $payload_s \gets$ \Call{PadPayload}{$payload_s$}\r
     \State $vc \gets $ \Call{GenerateVectorClock}{ }\r
-    \State $hmac \gets$ \Call{GetHmac}{$mid, vc, payload_s$}\r
+    \State \Call{IncrementVectorClock}{ }\r
+    \State $hmac \gets$ \Call{GenerateHmac}{$mid, vc, payload_s$}\r
     \State $record \gets \tuple{mid,vc,hmac,payload}$\r
     \State $record \gets $\Call{Encrypt}{$record$}\r
     \State \Call{PutSlotServer}{$record$}\r
@@ -653,27 +883,174 @@ The following helper functions are needed:\\
 \end{varwidth}% \r
 }\r
 \r
+%Check Data Structure for Malicious Activity\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Check Data Structure for Malicious Activity:}\r
+\begin{algorithmic}[1]\r
+\Function{CheckDataStructForValidity}{ }\r
+    \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\r
+    \State $ASeq \gets \emptyset$   \Comment{Set of all Payload Items that are sequences}\r
+    \State $MID \gets \emptyset$   \Comment{Set of all machine IDs}\r
+    \State $midClocks \gets \emptyset$ \Comment{Set of all clocks for the same machine IDs}\r
+    \State $oldestDeletedSsn \gets NULL$\r
+    \State $didFindSsn \gets False$\r
+    \State $didFindClock \gets False$\r
+    \State $hmac \gets NULL$\\\r
+    \r
+    \State Sort $R$ by $ssn$ from smallest $ssn$ to largest $ssn$\\\r
+    \r
+    \ForAll{record in R}\r
+        \State $\tuple{ssn',\tuple{mid', vc', hmac', payload'}} \gets record$\r
+        \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}\r
+        \State $MID \gets MID \cup \{mid'\}$\r
+    \EndFor\\\r
 \r
+    \ForAll{$record$ in $R$} \Comment{Check HMACs are all valid}\r
+        \State $\tuple{ssn',\tuple{mid', vc', hmac', payload'}} \gets record$\r
+        \State $hmac \gets $ \Call{GenerateHmac}{$mid', vc', payload'$}\r
+        \If{$hmac \neq hmac'$}\r
+            \State \Call{Error}{HMAC mismatch}\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \ForAll{$record_1$ in $R$} \Comment{Check no SSN duplicates}\r
+        \State $\tuple{ssn_1,rData_1} \gets record_1$\r
+        \ForAll{$record_2$ in $R$}\r
+            \If{$record_2 \neq record_1$}\r
+               \State $\tuple{ssn_2,rData_2} \gets record_2$\r
+               \If{$ssn_2 = ssn_1$}\r
+                    \State \Call{Error}{Duplicate SSN for different records}\r
+               \EndIf\r
+            \EndIf\r
+        \EndFor\r
+    \EndFor\\\r
+    \r
+    \r
+    \ForAll{$record_1$ in $R[0:-1]$} \Comment{Check for missing SSN}\r
+        \State $\tuple{ssn_1,rData_1} \gets record_1$\r
+        \State $didFindSsn \gets False$\r
+        \ForAll{$record_2$ in $R[1:]$}\r
+            \State $\tuple{ssn_2,rData_2} \gets record_2$\r
+            \If{$ssn_2 = (ssn_1 + 1)$}\r
+                \    State $didFindSsn \gets True$\r
+                \State Break\r
+            \EndIf\r
+        \EndFor\r
+        \r
+        \If{$\lnot didFindSsn$}\r
+            \State \Call{Error}{Missing SSN in SSN sequence.}\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+     \ForAll{$\tuple{ssn, payload}$ in $API$}\r
+        \If{($payload$ is a $delete) \land$ \Call{IsLive}{$payload, ssn$}}\r
+            \State $\tuple{ssn'} \gets payload$\r
+            \State $oldestDeleteSsn \gets ssn'$\r
+        \ElsIf{($payload$ is a $sequence) \land$ \Call{IsLive}{$payload, ssn$}}\r
+            \State $ASeq \gets ASeq \cup \{payload\}$\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \r
+    \ForAll{$record$ in $R$} \Comment{Check SSN's are all valid}\r
+        \State $\tuple{ssn, rData} \gets record$\r
+        \ForAll{$\tuple{rid', ssn'}$ in $ASeq$}\r
+            \If{$(rid' =$ \Call{GetRid}{$record$}$) \land ssn' \neq ssn$}\r
+                \State \Call{Error}{SSN mismatch}\r
+            \EndIf\r
+        \EndFor\r
+    \EndFor\\\r
+    \r
+    \r
+    \State $\tuple{ssn, payload} \gets R[0]$ \Comment{Get first record in the sorted R}\r
+    \If{$ssn > (oldestDeleteSsn + 1) $}\r
+        \State \Call{Error}{Missing records}\r
+   \EndIf\\\r
+    \r
+    \r
+    \ForAll{$mid$ in $MID$}\r
+        \State $midClocks \gets \emptyset$\r
+        \r
+        \ForAll{record in R}\r
+            \State $\tuple{ssn',\tuple{mid', vc', hmac', payload'}} \gets record$\r
+            \If{$mid' = mid$}\r
+                \State $\tuple{c_{mid_1}, c_{mid_2},...,c_{mid_k}} \gets vc'$\r
+                \State $midClocks \gets midClocks \cup \{c_{mid_n}|mid_n=mid\}$\r
+            \EndIf\r
+        \EndFor\\\r
+        \r
+        \State Sort $midClocks$ from smallest clock to largest clock\\\r
+        \r
+        \ForAll{$c_1$ in $midClocks[0:-1]$} \Comment{Check for missing SSN}\r
+            \State $didFindSsn \gets False$\r
+            \ForAll{$c_2$ in $midClocks[1:]$}\r
+                \If{$c_2 = (c_1 + 1)$}\r
+                    \State $didFindC\r
+ock\gets True$\r
+                    \State Break\r
+                \EndIf\r
+            \EndFor\r
+        \EndFor\r
+        \r
+        \If{$\lnot didFindClock$}\r
+            \State \Call{Error}{Missing clock in clock sequence for: $mid$.}\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \State \Comment{If got here then data structure is valid}\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
 \r
+%Get Latest Data Structure From Server\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Get  Latest Data Structure From Server}:\r
+\begin{algorithmic}[1]\r
+\Function{GetLatestDataStruct}{}\r
+    \State $largestSsn \gets $ Largest $ssn$ of all $ssn$ in $R$\r
+    \State $R \gets R \cup $ \Call{GetSlotServer}{$largestSsn + 1$}\r
+    \State \Call{CheckDataStructForValidity}{ }\r
+\EndFunction\r
+\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
 \r
-\r
-\textbf{Check Data Structure for Malicious Activity:}\\\r
-\textbf{Transaction Live}:\\\r
-\textbf{Commit Live}:\\\r
-\textbf{Key Value Live}:\\\r
-\r
-\r
-%-Rescues\r
-%    - Need to Change Transaction sizes\r
-%    - Need to Change New Key ssn in transaction\r
-%-Gets\r
-%-Arbitration\r
-%   - Insert Commit\r
-%-Check Data Structure\r
-\r
-\r
+%Update Key Value Set\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Update Key Value Set:}\r
+\begin{algorithmic}[1]\r
+\Function{UpdateKVSet}{$currentKV, kvSet$}\r
+    \State $newKVSet \gets kvSet$\r
+    \State $foundKey \gets False$\\\r
+    \r
+    \ForAll{$\tuple{k,v}$ in $currentKV$}\r
+        \State $foundKey \gets False$\\\r
+        \r
+        \ForAll{$\tuple{k',v'}$ in $kvSet$}\r
+            \If{$k = k'$}\r
+                \State $foundKey \gets True$\r
+                \State Break\r
+            \EndIf\r
+        \EndFor\\\r
+        \r
+        \If{$\lnot foundKey$}\r
+            \State $newKVSet \gets newKVSet \cup \{\tuple{k,v}\}$\r
+        \EndIf\r
+    \EndFor\r
+    \r
+    \State \Return{$newKVSet$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
 \r
 \subsection{\textbf{Create new key}}\r
+This operation creates a key and assigns an arbitrator to arbitrate on that new key.  In the case where more than one clients concurrently try to create the same new key, the client that inserted the newkey payload with the lowest ssn will be the client to generate the key, all other clients generation attempts would be invalid.\r
+\r
 \noindent\fbox{%\r
 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 \textbf{Create new key:}\r
@@ -744,10 +1121,192 @@ If by adding this transaction the data structure size exceeds the proposed max d
 }\r
 \r
 \subsection{\textbf{Get key-value pair}}\r
+This operation gets the latest key value pair from the data structure.  This is done by starting at the last known committed key value pairs then extrapolating into the future of uncommitted transactions till the transaction with the largest ssn is reached.  Everytime a new transaction is evaluated, it is evaluated against the current best guess of key value pairs based on the transactions up to the transaction being evaluated (by ssn).  This allows each client to "guess" what the latest value for a specified key will be even when the arbitrator has not stepped in yet to arbitrate.\r
 \r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Get  Latest Data Structure From Server}:\r
+\begin{algorithmic}[1]\r
+\Function{GetValueForKey}{$keyName$}\r
+    \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\r
+    \State $AT \gets \emptyset$    \Comment{Set of all Payload Items that are transactions}\r
+    \State $AC \gets \emptyset$    \Comment{Set of all Payload Items that are commits}\r
+    \State $AA \gets \emptyset$    \Comment{Set of all Payload Items that are aborts}\r
+    \State $kSet \gets \emptyset$ \Comment{Set of all key names in the system}\r
+    \State $tid \gets NULL$\r
+    \State $currentKV \gets \emptyset$\\\r
+    \r
+    \State \Call{GetLatestDataStruct}{ } \Comment{Update local version of data struct}\\\r
+    \r
+    \ForAll{$record$ in $R$}\r
+        \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}\r
+    \EndFor\\\r
+    \r
+    \ForAll{$\tuple{ssn, payload}$ in $API$}\r
+        \If{$payload$ is a $transaction$}\r
+            \State $AT \gets AT \cup \{\tuple{ssn,payload}\}$\r
+        \ElsIf{$payload$ is a $commit$}\r
+            \State $AC \gets AC \cup \{payload\}$\r
+        \ElsIf{$payload$ is a $abort$}\r
+            \State $AA \gets AA \cup \{payload\}$\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \State Sort $AT$ by ssn from oldest to newest\\\r
+    \r
+    \ForAll{$trans$ in $AT$} \Comment{Get the latest committed keys}\r
+        \State $\tuple{mid,vc ,kvSet,guard} \gets trans$\\\r
+    \r
+        \ForAll{$\tuple{k,v}$ in $kvSet$} \Comment{Get all key names in the system}\r
+            \State $kSet \gets kSet \cup \{k\}$\r
+        \EndFor\\\r
 \r
+        \If{$\lnot $\Call{TransactionLive}{$trans$}} \Comment{Only keep live transactions}\r
+            \State $AT \gets AT - \{trans\}$\r
+            \State Continue\r
+        \EndIf\\\r
+    \r
+        \State $tid \gets $ \Call{GetTid}{$trans$}\r
+        \ForAll{$com$ in $AC$}\r
+            \State $\tuple{tid', vc'} \gets com$\r
+            \If{$tid' = tid$}\r
+                \ForAll{$\tuple{k,v}$ in $kvSet$}\r
+                    \If{\Call{KeyValueLive}{$k,trans$}}\r
+                        \State $currentKV \gets currentKV \cup \{\tuple{k,v}\}$\r
+                    \EndIf\r
+                \EndFor\\\r
+                \r
+                \State $AT \gets AT - \{trans\}$ \Comment{No need for committed transactions}\r
+                \State Break\r
+            \EndIf\r
+        \EndFor\r
+    \EndFor\\\r
+    \r
+    \ForAll{$trans$ in $AT$} \Comment{Uncommitted ones only in order from lowest ssn to highest ssn}\r
+        \State $\tuple{mid,vc ,kvSet,guard} \gets trans$\r
+        \If{\Call{EvaluateGuard}{$guard, currentKV$}} \Comment{Check if will abort}\r
+            \State $currentKV \gets $\Call{UpdateKVSet}{$currentKV, kvSet$}\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \r
+    \ForAll{$\tuple{k,v}$ in $currentKV$} \Comment{Return the latest guessed value}\r
+        \If{$k = keyName$}\r
+            \State \Return{$v$}\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \State \Return{$NULL$} \Comment{Key was not present}\r
+    \r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
 \r
+\subsection{\textbf{Arbitrate On Transaction}}\r
 \r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Get  Latest Data Structure From Server}:\r
+\begin{algorithmic}[1]\r
+\Function{Arbitrate }{ }\r
+    \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\r
+    \State $AT \gets \emptyset$    \Comment{Set of all Payload Items that are transactions}\r
+    \State $AC \gets \emptyset$    \Comment{Set of all Payload Items that are commits}\r
+    \State $AA \gets \emptyset$    \Comment{Set of all Payload Items that are aborts}\r
+    \State $kSet \gets \emptyset$ \Comment{Set of all key names in the system}\r
+    \State $tid \gets NULL$\r
+    \State $currentKV \gets \emptyset$\r
+    \State $newPayload \gets NULL$\r
+    \State $midClient \gets mid$ of this client\\\r
+    \r
+    \State \Call{GetLatestDataStruct}{ } \Comment{Update local version of data struct}\\\r
+    \r
+    \ForAll{$record$ in $R$}\r
+        \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}\r
+    \EndFor\\\r
+    \r
+    \ForAll{$\tuple{ssn, payload}$ in $API$}\r
+        \If{$payload$ is a $transaction$}\r
+            \State $AT \gets AT \cup \{\tuple{ssn,payload}\}$\r
+        \ElsIf{$payload$ is a $commit$}\r
+            \State $AC \gets AC \cup \{payload\}$\r
+        \ElsIf{$payload$ is a $abort$}\r
+            \State $AA \gets AA \cup \{payload\}$\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \State Sort $AT$ by ssn from oldest to newest\\\r
+    \r
+    \ForAll{$trans$ in $AT$} \Comment{Get the latest committed keys}\r
+        \State $\tuple{mid,vc ,kvSet,guard} \gets trans$\\\r
+    \r
+        \ForAll{$\tuple{k,v}$ in $kvSet$} \Comment{Get all key names in the system}\r
+            \State $kSet \gets kSet \cup \{k\}$\r
+        \EndFor\\\r
+\r
+        \If{$\lnot $\Call{TransactionLive}{$trans$}} \Comment{Only keep live transactions}\r
+            \State $AT \gets AT - \{trans\}$\r
+            \State Continue\r
+        \EndIf\\\r
+    \r
+        \State $tid \gets $ \Call{GetTid}{$trans$}\r
+        \ForAll{$com$ in $AC$}\r
+            \State $\tuple{tid', vc'} \gets com$\r
+            \If{$tid' = tid$}\r
+                \ForAll{$\tuple{k,v}$ in $kvSet$}\r
+                    \If{\Call{KeyValueLive}{$k,trans$}}\r
+                        \State $currentKV \gets currentKV \cup \{\tuple{k,v}\}$\r
+                    \EndIf\r
+                \EndFor\\\r
+                \r
+                \State $AT \gets AT - \{trans\}$ \Comment{No need for committed transactions}\r
+                \State Break\r
+            \EndIf\r
+        \EndFor\r
+    \EndFor\\\r
+    \r
+    \ForAll{$trans$ in $AT$} \Comment{Uncommitted ones only in order from lowest ssn to highest ssn}\r
+        \State $\tuple{mid,vc ,kvSet,guard} \gets trans$\r
+        \r
+        \If{\Call{GetArbitrator}{$guard$} $\neq midClient$}\r
+            \State Continue\r
+        \EndIf\r
+        \r
+        \If{\Call{EvaluateGuard}{$guard, currentKV$}} \Comment{Check if will abort}\r
+            \State $currentKV \gets $\Call{UpdateKVSet}{$currentKV, kvSet$}\r
+            \State $newPayload \gets \tuple{$\Call{GetTid}{$trans$}$, $\Call{GenerateVectorClock}{ } $}$ \Comment{Make new commit payload}\r
+        \Else\r
+            \State $newPayload \gets \tuple{$\Call{GetTid}{$trans$}$, mid, $\Call{GenerateVectorClock}{ } $}$ \Comment{Make new abort payload}\r
+        \EndIf\\\r
+        \r
+        \State \Call{InsertPayload}{$newPayload$}\r
+    \EndFor\\\r
+    \r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+\r
+\r
+\section{\textbf{System Guarantees}}\r
+\begin{itemize}\r
+    \item Server cannot view data inside records\r
+    \item Server cannot forge or modify or create any records\r
+    \item Server cannot withhold any records\r
+    \item Server cannot reorder records that could not have been ordered differently due to network latency\r
+    \item Server cannot delete records unless told to do so.\r
+    \item There will always be an obvious key-value pair that is the latest key value pair.\r
+    \item The data structure is bounded in size such that $m$ is the minimum size of the data structure,  $n$ is the number of devices in the system and $s$ is the current size of the data structure: $m \leq s \leq (m+n-1)$\r
+    \item Data structure can only grow when there are too may key-value pairs (and aborts) than what fit in the current data structure size within reason.\r
+    \item No currently valid data can be lost by the system and go undetected.\r
+    \item Devices can operate offline and re-sync with the system and get a consistent view of the system\r
+    \item If the server tries to hold a device on an older version of the data structure, that device can eventually rejoin the main data structure without problems.\r
+    \item Devices that have a transaction aborted will be able to be notified about the abort indefinitely (no time frame when notification must be accepted).\r
+    \item Server cannot hold a device on an old version of the data structure and then move them to a newer version of the data structure without being detected (The server sequence numbers would reveal conflicts or gaps or both).\r
+\r
+\end{itemize}\r
 \r
 \r
 \end{document}\r