Formal Document edits

diff --git a/version2/doc/iotcloud_formal/iotcloud.tex b/version2/doc/iotcloud_formal/iotcloud.tex
index ad3e4bf4b676cc86ad6b68b8891daad809daf901..679c218fe228d7200b070acc53ad7085a085954b 100644 (file)
--- a/version2/doc/iotcloud_formal/iotcloud.tex
+++ b/version2/doc/iotcloud_formal/iotcloud.tex
@@ -29,8 +29,6 @@
 \r
 \r
 \r
-\r
-\r
 \section{\textbf{Server}}\r
 The server maintains a collection of slots such that each slot contains some data.\r
 The operations on the slot are as follows:\r
@@ -140,7 +138,7 @@ $abort_s = \tuple{tid_s,mid_s,vc_s}$\\
 $sequence_s = \tuple{rid_s, ssn_s}$\\\r
 $delete_s = \tuple{ssn_d}$\\\r
 $resize_s = \tuple{x | x \in \mathbb{N}}$\\\r
-$newkey_s = \tuple{k_s, vc_s, ssn_s$ or $-1, mid_s}$\\\r
+$newkey_s = \tuple{k_s, vc_s, ssn_s$ or $NULL, mid_s}$\\\r
 \r
 $payload_s = \{x_1, x_2,..., x_k | \forall k, x_k \in \{$transaction, commit, abort, resize, newkey, sequence, delete$\}\}$\\\r
 $rd_s = \tuple{mid_s, vc_s, hmac_s, payload_s}$ \\\r
@@ -168,7 +166,7 @@ The following helper functions are needed:\\
 \end{varwidth}% \r
 }\r
 \r
-\r
+%Error Message\r
 \begin{algorithmic}[1]\r
 \Procedure{Error}{$msg$}\r
 \State $Print(msg)$\r
@@ -177,6 +175,19 @@ The following helper functions are needed:\\
 \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
@@ -345,7 +356,7 @@ The following helper functions are needed:\\
     \State $ANK \gets \emptyset$    \Comment{Set of all Payload Items that are new keys}\r
     \State $\tuple{k_s, vc_s, ssn_s, mid_s}\gets newkey_s$\\\r
     \r
-    \If{$ssn_s = -1$}                    \Comment{Make sure ssn is the correct one}\r
+    \If{$ssn_s = NULL$}                    \Comment{Make sure ssn is the correct one}\r
         \State $ssn_s \gets ssn_r$\r
     \EndIf\\\r
     \r
@@ -549,17 +560,56 @@ The following helper functions are needed:\\
 \end{varwidth}% \r
 }\r
 \r
-\textbf{Evaluate Guard Condition:}\\\r
-\textbf{Get Latest Data Structure From Server:}\\\r
-\textbf{Check Data Structure for Malicious Activity:}\\\r
+%Get Arbitrator\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Get Arbitrator:}\r
+\begin{algorithmic}[1]\r
+\Function{GetArbitrator}{$key$}\r
+    \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\\\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 $newkey) \land$ \Call{IsLive}{$payload, ssn$}}\r
+            \State $\tuple{k', vc', ssn', mid'} \gets payload$\r
+            \r
+            \If{$k' = key$}\r
+                \State \Return{$mid'$}\r
+            \EndIf\r
+        \EndIf\r
+    \EndFor\\\r
+    \State \Call{Error}{No arbitrator for key: $key$}\r
+\EndFunction\r
+\end{algorithmic}\r
 \r
+\begin{algorithmic}[1]\r
+\Function{GetArbitrator}{$guard$}\r
+    \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\r
+    \State $\tuple{kvSet, condition} \gets guard$\\\r
+    \r
+    \ForAll{record in R}\r
+        \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}\r
+    \EndFor\\\r
+    \r
+    \ForAll{$\tuple{key, value}$ in $kvSet$}\r
+        \ForAll{$\tuple{ssn, payload}$ in $API$}\r
+            \If{($payload$ is a $newkey) \land$ \Call{IsLive}{$payload, ssn$}}\r
+                \State $\tuple{k', vc', ssn', mid'} \gets payload$\r
+                \If{$k' = key$}\r
+                    \State \Return{$mid'$}\r
+                \EndIf\r
+            \EndIf\r
+        \EndFor\r
+    \EndFor\\\r
+    \State \Call{Error}{No arbitrator for key: $key$}\r
+\EndFunction\r
+\end{algorithmic}\r
 \r
-\textbf{Get Arbitrator for key}:\\\r
-\textbf{Get Transaction Arbitrator}:\\\r
-\textbf{Transaction Live}:\\\r
-\textbf{Commit Live}:\\\r
-\textbf{Key Value Live}:\\\r
-\textbf{Get Vector Clock}:\\\r
+\end{varwidth}% \r
+}\r
 \r
 %Insert Payload\r
 \noindent\fbox{%\r
@@ -571,10 +621,10 @@ The following helper functions are needed:\\
     \State $numOfRecords \gets |R|+1$\r
     \State $targetSize \gets $ \Call{GetDataStrucSize}{ }\r
     \State $numToDelete \gets numOfRecords - targetSize$\r
-    \State $rp \gets NULL$\\\r
+    \State $rp \gets NULL$\r
     \State $hmac \gets NULL$\r
     \State $vc \gets NULL$\r
-    \State $record \gets NULL$\r
+    \State $record \gets NULL$\\\r
 \r
     \If{\Call{GetSize}{$payload_s$} $> MaxPayloadSize$}\r
         \State \Call{Error}{Payload too large}\r
@@ -591,9 +641,9 @@ The following helper functions are needed:\\
         \EndIf\r
     \EndIf\\\r
     \r
-    \r
     \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 $record \gets \tuple{mid,vc,hmac,payload}$\r
     \State $record \gets $\Call{Encrypt}{$record$}\r
@@ -603,34 +653,79 @@ The following helper functions are needed:\\
 \end{varwidth}% \r
 }\r
 \r
+\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
-%-Deletes\r
-%-Resize\r
-%-Puts\r
+%    - Need to Change New Key ssn in transaction\r
 %-Gets\r
-%-New Key\r
 %-Arbitration\r
+%   - Insert Commit\r
 %-Check Data Structure\r
 \r
+\r
+\r
+\subsection{\textbf{Create new key}}\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Create new key:}\r
+\begin{algorithmic}[1]\r
+\Function{CreateNewKey}{$keyName, mid$}\r
+    \State $vc \gets $ \Call{GenerateVectorClock}{ }\r
+    \State $newKeyPayload \gets \tuple{keyName, vc, NULL, mid}$\r
+    \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\\\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 $newkey) \land$ \Call{IsLive}{$payload, ssn$}}\r
+            \State $\tuple{k', vc', ssn', mid'} \gets payload$\r
+            \r
+            \If{$k' = key$}\r
+                \State \Return{False}\r
+            \EndIf\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \State \Call{InsertPayload}{$newKeyPayload$}\r
+    \State \Return{True}\r
+\EndFunction\r
+\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
+\r
 \subsection{\textbf{Put Transaction}}\r
 This operation puts a transaction into the data structure if this transaction fits inside a payload.\r
-If by adding this transaction the data structure size exceeds the proposed max data structure size then deletes take place.  If no deletes can take place (too much live data) then the data structure is resized.\r
+If by adding this transaction the data structure size exceeds the proposed max data structure size then deletes take place.  If no deletes can take place (too much live data) then the data structure is resized.\\\r
 \r
-\r
-%Create Resize Data Structure Payload Item\r
+%\r
 \noindent\fbox{%\r
 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 \textbf{Put Transaction:}\r
 \begin{algorithmic}[1]\r
 \Function{PutTransaction}{$kVUpdates, guard$}\r
-    \State $mid \gets -1$\\\r
-    \State $dsSize \gets $\r
-    \r
+    \State $mid \gets NULL$\r
+    \State $vc \gets $ \Call{GenerateVectorClock}{ }\r
+    \State $transPayload \gets NULL$\\\r
+\r
+    \State \Call{GetLatestDataStruct}{ } \Comment{Update local version of data struct}\\\r
+\r
     \ForAll{$kv$ in $kVUpdates$}\r
         \State $\tuple{k', v'} \gets kv$\r
         \r
-        \If{$mid = -1$}\r
+        \If{$mid = NULL$}\r
             \State $mid \gets$ \Call{GetArbitrator}{$k'$}\r
         \ElsIf{$mid \neq $ \Call{GetArbitrator}{$k'$}}\r
             \State \Call{Error}{Multiple Arbitrators}\r
@@ -639,17 +734,20 @@ If by adding this transaction the data structure size exceeds the proposed max d
     \r
     \If{\Call{GetArbitrator}{$guard$} $\neq mid$}\r
         \State \Call{Error}{Multiple Arbitrators}\r
-    \EndIf\r
-    \r
-    \r
+    \EndIf\\\r
     \r
+    \State $transPayload \gets \tuple{mid, vc, kVUpdates, guard}$\r
+    \State \Call{InsertPayload}{$transPayload$}\r
 \EndFunction\r
 \end{algorithmic}\r
 \end{varwidth}% \r
 }\r
 \r
 \subsection{\textbf{Get key-value pair}}\r
-\subsection{\textbf{Create new key}}\r
+\r
+\r
+\r
+\r
 \r
 \r
 \end{document}\r