\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
\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
\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
\State $SL \gets SL - SD$\r
\EndFunction\r
\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
\r
\r
\r
\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
projects / iotcloud.git / commitdiff