Updates

diff --git a/version2/doc/iotcloud_formal/iotcloud.tex b/version2/doc/iotcloud_formal/iotcloud.tex
index 17c03f059234639d42d45b6bb19b368ec4c067af..ad3e4bf4b676cc86ad6b68b8891daad809daf901 100644 (file)
--- a/version2/doc/iotcloud_formal/iotcloud.tex
+++ b/version2/doc/iotcloud_formal/iotcloud.tex
@@ -154,6 +154,29 @@ $record_s = \tuple{ssn_s,rd_s}$\\
 \subsection{Helper Functions}\r
 The following helper functions are needed:\\\r
 \r
+\r
+%Throw Error\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Throw Error:}\r
+\begin{algorithmic}[1]\r
+\Function{Error}{$msg$}\r
+    \State $Print(msg)$\r
+    \State $Halt()$\r
+\EndFunction\r
+\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
+\r
+\r
+\begin{algorithmic}[1]\r
+\Procedure{Error}{$msg$}\r
+\State $Print(msg)$\r
+\State $Halt()$\r
+\EndProcedure\r
+\end{algorithmic}\r
+\r
+\r
 %Get Payload Items from Record with SSN\r
 \noindent\fbox{%\r
 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
@@ -312,6 +335,43 @@ The following helper functions are needed:\\
 \end{varwidth}% \r
 }\r
 \r
+%New Key Live\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{New Key Live:}\r
+\begin{algorithmic}[1]\r
+\Function{NewKeyLive}{$newkey_s, ssn_r$}\r
+    \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\r
+    \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
+        \State $ssn_s \gets ssn_r$\r
+    \EndIf\\\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$}\r
+            \State $ANK \gets ANK \cup \{\tuple{ssn', payload'}\}$   \Comment{Extract all new key payloads}\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \ForAll{$\tuple{ssn', \tuple{k_s', vc_s', ssn_s', mid_s'}}$ in $ANK$}\r
+        \If{$vc_s' < vc_s$}\r
+            \State \Return{False}\r
+        \ElsIf{$\lnot (vc_s' < vc_s) \land (ssn_s' < ssn_s)$}\r
+            \State \Return{False}\r
+        \EndIf\r
+    \EndFor \\\r
+    \State \Return{True}\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
@@ -434,8 +494,7 @@ The following helper functions are needed:\\
 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 \textbf{Pad Payload}:\r
 \begin{algorithmic}[1]\r
-\Function{PadPayload}{$payload_s$}\r
-    \State $SpaceRemaining = MaxPayloadSize - $ \Call{GetSize}{$payload_s$}\r
+\Function{PadPayload}{$payload_s$}    \State $SpaceRemaining =  MaxPayloadSize - $ \Call{GetSize}{$payload_s$}\r
     \r
     \If{$SpaceRemaining = 0$}\r
         \State \Return{$payload_s$}\r
@@ -457,7 +516,6 @@ The following helper functions are needed:\\
         \r
     \ForAll{$\tuple{ssn_s, record_s}$ in $RS$}\r
         \If{\Call{HasLivePayload}{$record_s, ssn_s$}}\r
-            \State \Call{ResizeDataStruc}{ }\r
             \State \Return{False}\r
         \Else\r
             \State \Call{DeleteSlotServer}{$ssn_s$}\r
@@ -476,18 +534,74 @@ The following helper functions are needed:\\
 \end{varwidth}% \r
 }\r
 \r
-\r
-\r
+%Create Resize Data Structure Payload Item\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Create Resize Data Structure Payload Item:}\r
+\begin{algorithmic}[1]\r
+\Function{MakeResizePayload}{ }\r
+    \State $rp \gets$ Empty $resize$ payload\r
+    \State $cs \gets$ \Call{GetDataStrucSize}{ }\r
+    \State $rp \gets \tuple{cs * 2}$\r
+    \State \Return{$rp$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\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
-\textbf{Resize Data Structure:}\\\r
+\r
+\r
+\textbf{Get Arbitrator for key}:\\\r
 \textbf{Get Transaction Arbitrator}:\\\r
 \textbf{Transaction Live}:\\\r
 \textbf{Commit Live}:\\\r
-\textbf{New Key Live}:\\\\r
-\textbf{Key Value Live}:\\\\r
+\textbf{Key Value Live}:\\\r
+\textbf{Get Vector Clock}:\\\r
+\r
+%Insert Payload\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Insert Payload:}\r
+\begin{algorithmic}[1]\r
+\Function{InsertPayload}{$payload_s$}\r
+    \r
+    \State $numOfRecords \gets |R|+1$\r
+    \State $targetSize \gets $ \Call{GetDataStrucSize}{ }\r
+    \State $numToDelete \gets numOfRecords - targetSize$\r
+    \State $rp \gets NULL$\\\r
+    \State $hmac \gets NULL$\r
+    \State $vc \gets NULL$\r
+    \State $record \gets NULL$\r
+\r
+    \If{\Call{GetSize}{$payload_s$} $> MaxPayloadSize$}\r
+        \State \Call{Error}{Payload too large}\r
+    \EndIf\\\r
+    \r
+    \If{$numToDelete > 0$}\r
+        \If{$\lnot$\Call{Delete}{$numToDelete$}}\r
+            \State $rp \gets$\Call{MakeResizePayload}{ }\r
+            \If{\Call{GetSize}{$payload_s \cup rp$} $> MaxPayloadSize$}\r
+                \State \Call{InsertPayload}{$rp$}\r
+            \Else\r
+                \State $payload_s \gets payload_s \cup rp$\r
+            \EndIf\r
+        \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 $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
+    \State \Call{PutSlotServer}{$record$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
 \r
 %-Rescues\r
 %    - Need to Change Transaction sizes\r
@@ -500,8 +614,39 @@ The following helper functions are needed:\\
 %-Check Data Structure\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
 \r
 \r
+%Create Resize Data Structure Payload Item\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
+    \ForAll{$kv$ in $kVUpdates$}\r
+        \State $\tuple{k', v'} \gets kv$\r
+        \r
+        \If{$mid = -1$}\r
+            \State $mid \gets$ \Call{GetArbitrator}{$k'$}\r
+        \ElsIf{$mid \neq $ \Call{GetArbitrator}{$k'$}}\r
+            \State \Call{Error}{Multiple Arbitrators}\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \If{\Call{GetArbitrator}{$guard$} $\neq mid$}\r
+        \State \Call{Error}{Multiple Arbitrators}\r
+    \EndIf\r
+    \r
+    \r
+    \r
+\EndFunction\r
+\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
 \r
 \subsection{\textbf{Get key-value pair}}\r
 \subsection{\textbf{Create new key}}\r