Formal Edits
[iotcloud.git] / version2 / doc / iotcloud_formal / iotcloud.tex
index b13d0302ef5200f77a26ab6e77c1fa99a3005a65..17c03f059234639d42d45b6bb19b368ec4c067af 100644 (file)
@@ -187,11 +187,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,15 +312,192 @@ The following helper functions are needed:\\
 \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
+%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
-\textbf{Evaluate Guard Condition:}\\\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
+    \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
-\textbf{Get Latest Data Structure From Server:}\\\r
-\textbf{Delete Records:}\\\r
-\textbf{Check Data Structure for Malicious Activity:}\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
+%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$}\r
+    \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 \Call{ResizeDataStruc}{ }\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
+\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
+\textbf{Get Transaction Arbitrator}:\\\r
+\textbf{Transaction Live}:\\\r
+\textbf{Commit Live}:\\\r
+\textbf{New Key Live}:\\\\r
+\textbf{Key Value Live}:\\\\r
+\r
+%-Rescues\r
+%    - Need to Change Transaction sizes\r
+%-Deletes\r
+%-Resize\r
+%-Puts\r
+%-Gets\r
+%-New Key\r
+%-Arbitration\r
+%-Check Data Structure\r
 \r
 \subsection{\textbf{Put Transaction}}\r
 \r
@@ -334,4 +506,5 @@ The following helper functions are needed:\\
 \subsection{\textbf{Get key-value pair}}\r
 \subsection{\textbf{Create new key}}\r
 \r
+\r
 \end{document}\r