Formal Document edits
[iotcloud.git] / version2 / doc / iotcloud_formal / iotcloud.tex
index b13d0302ef5200f77a26ab6e77c1fa99a3005a65..679c218fe228d7200b070acc53ad7085a085954b 100644 (file)
@@ -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
@@ -154,6 +152,42 @@ $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
+%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
@@ -187,11 +221,6 @@ The following helper functions are needed:\\
 \end{varwidth}% \r
 }\r
 \r
-\r
-\textbf{Get Transaction Arbitrator}:\\\r
-\textbf{Transaction Live}:\\\r
-\textbf{Commit Live}:\\\r
-\r
 %Sequence Live\r
 \noindent\fbox{%\r
 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
@@ -317,21 +346,408 @@ 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 = NULL$}                    \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
+\textbf{Is Live:}:\r
+\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
+    \r
+    \ElsIf{$item_s$ is a $commit$}\r
+        \State \Return{\Call{CommitLive}{$item_s, ssn_s$}}\r
+    \r
+    \ElsIf{$item_s$ is a $abort$}\r
+        \State \Return{\Call{AbortLive}{$item_s$}}\r
+            \r
+    \ElsIf{$item_s$ is a $delete$}\r
+        \State \Return{\Call{DeleteLive}{$item_s, ssn_s$}}\r
+        \r
+    \ElsIf{$item_s$ is a $commit$}\r
+        \State \Return{\Call{ResizeLive}{$item_s, ssn_s$}}\r
+        \r
+    \ElsIf{$item_s$ is a $sequence$}\r
+        \State \Return{\Call{SequenceLive}{$item_s, ssn_s$}}\r
+        \r
+    \ElsIf{$item_s$ is a $newkey$}\r
+        \State \Return{\Call{NewKeyLive}{$item_s, ssn_s$}}\r
+        \r
+    \ElsIf{$item_s$ is a $keyvalue$}\r
+        \State \Return{\Call{KeyValueLive}{$item_s, ssn_s$}}\r
+    \EndIf\\\r
+    \r
+    \State \Return{False}  \Comment{Will never get here}\r
+\EndFunction\r
+\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
 \r
-\textbf{Evaluate Guard Condition:}\\\r
+%Record has live payload data\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Record has live payload data:}:\r
+\begin{algorithmic}[1]\r
+\Function{HasLivePayload}{$record_s, ssn_s$}\r
+    \State $\tuple{mid_s, vc_s, hmac_s, payload_s} \gets record_s$\r
+    \ForAll{$item$ in $payload_s$}\r
+        \If{\Call{IsLive}{$item, ssn_s$}}\r
+            \State \Return{True}\r
+        \EndIf\r
+    \EndFor\r
+    \State \Return{False}\r
+\EndFunction\r
+\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
 \r
+% Get Data Structure Size\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Get Data Structure Size:}\r
+\begin{algorithmic}[1]\r
+\Function{GetDataStrucSize}{ }\r
+    \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\r
+    \State $AR \gets \emptyset$    \Comment{Set of all Payload Items that are resize}\r
 \r
-\textbf{Get Latest Data Structure From Server:}\\\r
-\textbf{Delete Records:}\\\r
-\textbf{Check Data Structure for Malicious Activity:}\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 $resize) \land$ \Call{IsLive}{$payload, ssn$}}\r
+            \State $\tuple{size'} \gets payload$\r
+            \State \Return{$size'$}\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \State \Return{$0$}  \Comment{Get Here only if data structure has no entries}\r
+\EndFunction\r
+\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
 \r
+%Rescue Payload Items\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Rescue Payload Items}:\r
+\begin{algorithmic}[1]\r
+\Function{RescuePayloadItems}{$payload_s$}\r
+    \State $PIList =$ empty list of $\tuple{ssn, payload}$\r
+    \State $SpaceRemaining = MaxPayloadSize - $ \Call{GetSize}{$payload_s$}\r
+    \r
+    \If{$SpaceRemaining = 0$}\r
+        \Return{$payload_s$}\r
+    \EndIf\\\r
+    \r
+    \ForAll{record in R}\r
+        \State $PIList \gets PIList \cup$ \Call{GetPayloadItemsWithSSN}{$record$}\r
+    \EndFor\\\r
+    \r
+    \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
+        \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
+        \EndIf\r
+    \EndFor\\\r
+    \State \Return{$payload_s$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
 \r
-\subsection{\textbf{Put Transaction}}\r
+%Pad Payload\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Pad Payload}:\r
+\begin{algorithmic}[1]\r
+\Function{PadPayload}{$payload_s$}    \State $SpaceRemaining =  MaxPayloadSize - $ \Call{GetSize}{$payload_s$}\r
+    \r
+    \If{$SpaceRemaining = 0$}\r
+        \State \Return{$payload_s$}\r
+    \EndIf\\\r
+    \State \Return{$payload_s \gets payload_s \cup$ \Call{GenerateFiller}{$SpaceRemaining$}}\r
+\EndFunction\r
+\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
+\r
+%Delete Records\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Delete Records (Deletes n records)}:\r
+\begin{algorithmic}[1]\r
+\Function{Delete}{$num\_of\_records$}\r
+    \State $RS \gets$ List of all Records sorted by ssn and has form $\tuple{ssn_s, record_s}$\r
+    \State $n \gets 0$\\\r
+        \r
+    \ForAll{$\tuple{ssn_s, record_s}$ in $RS$}\r
+        \If{\Call{HasLivePayload}{$record_s, ssn_s$}}\r
+            \State \Return{False}\r
+        \Else\r
+            \State \Call{DeleteSlotServer}{$ssn_s$}\r
+            \State $n \gets n + 1$\r
+        \EndIf\\\r
+        \r
+        \If{$n = num\_of\_records$}\r
+            \State \textbf{break}\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \State \Return{True}\r
+    \r
+\EndFunction\r
+\end{algorithmic}\r
+\end{varwidth}% \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
+%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
+\end{varwidth}% \r
+}\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
+    \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
+    \State \Call{PutSlotServer}{$record$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\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
+%    - Need to Change New Key ssn in transaction\r
+%-Gets\r
+%-Arbitration\r
+%   - Insert Commit\r
+%-Check Data Structure\r
 \r
 \r
 \r
-\subsection{\textbf{Get key-value pair}}\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
+\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 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 = NULL$}\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
+    \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
+\r
+\r
+\r
+\r
+\r
 \r
 \end{document}\r