Formal Edits
authorAli Younis <ayounis@uci.edu>
Thu, 13 Oct 2016 22:44:11 +0000 (15:44 -0700)
committerAli Younis <ayounis@uci.edu>
Thu, 13 Oct 2016 22:44:11 +0000 (15:44 -0700)
version2/doc/iotcloud_formal/iotcloud.tex

index 6615895..b13d030 100644 (file)
@@ -5,14 +5,18 @@
 \usepackage{amsmath}\r
 \usepackage{graphicx}\r
 \usepackage{mathrsfs}\r
+\usepackage{amssymb}\r
 \usepackage{algpseudocode}% http://ctan.org/pkg/algorithmicx\r
 \usepackage[all]{xy}\r
+\usepackage{varwidth}\r
+\r
 \newtheorem{theorem}{Theorem}\r
 \newtheorem{prop}{Proposition}\r
 \newtheorem{lem}{Lemma}\r
 \newtheorem{defn}{Definition}\r
 \newcommand{\note}[1]{{\color{red} \bf [[#1]]}}\r
 \newcommand{\push}[1][1]{\hskip\dimexpr #1\algorithmicindent\relax}\r
+\newcommand*\xor{\mathbin{\oplus}}\r
 \begin{document}\r
 \r
 \r
@@ -52,6 +56,9 @@ $n = 0$
 \subsection{\textbf{Put Slot}}\r
 Put slot is an operation that inserts data into a new slot at the server.\\\r
 \r
+%Put Function\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 \textbf{Put Function:}\r
 \begin{algorithmic}[1]\r
 \Function{PutSlotServer}{$sv_p$}\r
@@ -60,21 +67,30 @@ Put slot is an operation that inserts data into a new slot at the server.\\
     \State $SL \gets SL \cup \{\tuple{s_p,sv_p}\}$\r
 \EndFunction\r
 \end{algorithmic}\r
-\r
+\end{varwidth}% \r
+}\r
 \r
 \subsection{\textbf{Get Slot}}\r
 Get slot is an operation that returns all server slots that are greater than some server sequence number.\\\r
 \r
+% Get Function\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 \textbf{Get Function:}\r
 \begin{algorithmic}[1]\r
 \Function{GetSlotServer}{$s_g$}\r
     \State \Return{$\{\tuple{s, sv} \in SL \mid s \geq s_g\}$}\r
 \EndFunction\r
 \end{algorithmic}\r
+\end{varwidth}% \r
+}\r
 \r
 \subsection{\textbf{Delete Slot}}\r
 Delete slot is an operation that deletes all live slots that have server sequence numbers that are equal to or less than some server sequence number.\\\r
 \r
+%Delete Function\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 \textbf{Delete Function:}\r
 \begin{algorithmic}[1]\r
 \Function{DeleteSlotServer}{$s_d$}\r
@@ -82,6 +98,8 @@ Delete slot is an operation that deletes all live slots that have server sequenc
     \State $SL \gets SL - SD$\r
 \EndFunction\r
 \end{algorithmic}\r
+\end{varwidth}% \r
+}\r
 \r
 \r
 \r
@@ -100,22 +118,210 @@ The data structure exposes the following functions:
 \end{itemize}\r
 \r
 \subsection{\textbf{Client Notation Conventions}}\r
+\r
+$K$ is the set of all keys.\\\r
+$MID$ is the set of the machine IDs of the devices that are in the system.\r
+$K_{mid}$ is a set of all keys that have device mid as the arbitrator\\\r
+$ssn_s$ is the server sequence number of a record $s$\\\r
 $mid_s \in MID$ is the machine ID for the device that created $record_s$.\\\r
 $hmac_s$ is the HMAC of $record_s$\\\r
 $c_{mid}$ is the latest read clock for a device with machine ID $mid$\\\r
 $vc_s = \{c_{mid} | mid \in MID\}$\\\r
-\r
-\r
-$payload_s = \{x_1, x_2,..., x_k | \forall k, x_k \in \{$transaction, commit, abort, resize, new-key, sequence, delete$\}\}$\\\r
-$record_s = \tuple{mid_s, vc_s, hmac_s, payload_s}$ \\\r
+$rid_s = \tuple{mid_s, c_{mid_s}}$\r
+$k$ is a key entry\\\r
+$v$ is a value entry\\\r
+$kv_n$ is a key-value entry $\tuple{k_n,v_n} , k \in K$\\\r
+\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
+$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
+$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
+\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
+$record_s = \tuple{ssn_s,rd_s}$\\\r
 \r
 \subsection{\textbf{Client State}}\r
 \textit{s = largest server sequence number pulled from the server by a device} \\\r
-\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
+%Get Payload Items from Record with SSN\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Get Payload Items from Record with SSN}:\r
+\begin{algorithmic}[1]\r
+\Function{GetPayloadItemsWithSSN}{$record_s$}\r
+    \State $PISSN \gets \emptyset$ \Comment{Set of Payload Items with ssn}\r
+    \State $\tuple{ssn_s, rd_s} \gets record_s$\r
+    \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
+    \EndFor\\\r
+    \r
+    \State \Return {$PISSN$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
+\r
+%Get rid For Record\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Get rid For 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
+    \State \Return {$\tuple{mid_s, c_{mid_s}}$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\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
+\textbf{Sequence Live}:\r
+\begin{algorithmic}[1]\r
+\Function{SequenceLive}{$sequence_s, ssn_{s1}$}\r
+    \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\r
+    \State $AS \gets \emptyset$    \Comment{Set of all Payload Items that are sequences}\r
+    \State $StillHasRecord \gets False$\r
+    \State $\tuple{rid_s, ssn_{s2}} \gets sequence_s$\\\r
+    \r
+    \ForAll{$record$ in $R$}\r
+        \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}\r
+        \If{$rid_s = $\Call{GetRid}{$record$}}\r
+            \State $StillHasRecord \gets True$\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \If{$\lnot StillHasRecord$}  \Comment{The Record does not exists anymore}\r
+        \State \Return{False}\r
+    \EndIf\\\r
+    \r
+    \ForAll{$\tuple{ssn, payload}$ in $API$}\r
+        \If{$payload$ is a $sequence$}\r
+            \State $AS \gets AS \cup \{\tuple{ssn, payload}\}$   \Comment{Extract all sequence payloads}\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \ForAll{$\tuple{ssn_1', \tuple{rid', ssn_2'}}$ in $AS$}\r
+        \If{$(rid'=rid_s) \land (ssn_1' > ssn_{s_1})$}\r
+            \State \Return{False}\r
+        \EndIf\r
+    \EndFor \\\r
+    \State \Return{True}\r
+\EndFunction\r
+\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
+\r
+% Delete Live\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Delete Live}:\r
+\begin{algorithmic}[1]\r
+\Function{DeleteLive}{$delete_s, ssn_s$}\r
+    \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\r
+    \State $AD \gets \emptyset$    \Comment{Set of all Payload Items that are deletes}\r
+    \State $\tuple{ssn_d} \gets delete_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 $delete$}\r
+            \State $AD \gets AD \cup \{\tuple{ssn, payload}\}$   \Comment{Extract all delete payloads}\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \ForAll{delete in AD}\r
+        \State $\tuple{{ssn_s}', \tuple{{ssn_d}'}} \gets delete$\r
+        \If{${ssn_d}' > ssn_d$}    \Comment{More recently deleted record}\r
+            \State \Return{False}\r
+        \ElsIf{$({ssn_d}'= ssn_d) \land ({ssn_s}' > ssn_s)$} \Comment{More recent delete of same record}\r
+            \State \Return{False}\r
+        \EndIf\r
+    \EndFor \\\r
+    \State \Return{True}\r
+\EndFunction\r
+\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
+\r
+%Abort Live\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Abort Live}:\r
+\begin{algorithmic}[1]\r
+\Function{AbortLive}{$abort_s$}\r
+    \State $\tuple{tid_s,mid_s,vc_s} \gets abort_s$\\\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
+        \EndIf\r
+    \EndFor\\\r
+    \State \Return{False}\r
+\EndFunction\r
+\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
+\r
+%Resize Live\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Resize Live}:\r
+\begin{algorithmic}[1]\r
+\Function{ResizeLive}{$resize_s, ssn_s$}\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
+    \State $\tuple{size} \gets resize_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 $resize$}\r
+            \State $AR \gets AR \cup \{\tuple{ssn, payload}\}$   \Comment{Extract all resize payloads}\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \ForAll{$\tuple{ssn', \tuple{size'}}$ in $AR$}\r
+        \If{$size' > size$}\r
+            \State \Return{False}\r
+        \ElsIf{$(size'=size) \land (ssn' > 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
+\r
+\r
+\textbf{Evaluate Guard Condition:}\\\r
+\r
+\r
 \textbf{Get Latest Data Structure From Server:}\\\r
 \textbf{Delete Records:}\\\r
 \textbf{Check Data Structure for Malicious Activity:}\r