From: Ali Younis Date: Wed, 21 Dec 2016 23:38:07 +0000 (-0800) Subject: Deleted Redundent Files X-Git-Url: http://plrg.eecs.uci.edu/git/?p=iotcloud.git;a=commitdiff_plain;h=9ce98cd22cdf689d65fface4d31741f74ca54121 Deleted Redundent Files --- diff --git a/version2/doc/iotcloud_formal/iotcloud.tex b/version2/doc/iotcloud_formal/iotcloud.tex deleted file mode 100644 index 8f15592..0000000 --- a/version2/doc/iotcloud_formal/iotcloud.tex +++ /dev/null @@ -1,1312 +0,0 @@ -\documentclass[11pt]{article} -\newcommand{\tuple}[1]{\ensuremath \langle #1 \rangle} -\usepackage{color} -\usepackage{amsthm} -\usepackage{amsmath} -\usepackage{graphicx} -\usepackage{mathrsfs} -\usepackage{amssymb} -\usepackage{algpseudocode}% http://ctan.org/pkg/algorithmicx -\usepackage[all]{xy} -\usepackage{varwidth} - -\newtheorem{theorem}{Theorem} -\newtheorem{prop}{Proposition} -\newtheorem{lem}{Lemma} -\newtheorem{defn}{Definition} -\newcommand{\note}[1]{{\color{red} \bf [[#1]]}} -\newcommand{\push}[1][1]{\hskip\dimexpr #1\algorithmicindent\relax} -\newcommand*\xor{\mathbin{\oplus}} -\begin{document} - - -\setlength\parindent{0pt} % Removes all indentation from paragraphs - comment this line for an assignment with lots of text - - -\section{\textbf{Introduction}} - - - - - -\section{\textbf{Server}} -The server maintains a collection of slots such that each slot contains some data. -The operations on the slot are as follows: -\begin{itemize} - \item Put slot - \item Get slot - \item Delete Slot -\end{itemize} - -\subsection{\textbf{Server Notation Conventions}} -$s \in SN$ is a server sequence number\\ -$sv \in SV$ is a slot's value\\ -$slot_s = \tuple{s, sv} \in SL \subseteq SN \times SV$ - -\subsection{\textbf{Server State}} -\textit{n = current server sequence number}\\ -\textit{SL = set of live slots on the server}\\ - -\textbf{Initial Server State}\\ -$SL = \emptyset$\\ -$n = 0$ - -\subsection{\textbf{Put Slot}} -Put slot is an operation that inserts data into a new slot at the server.\\ - -%Put Function -\noindent\fbox{% -\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} -\textbf{Put Function:} -\begin{algorithmic}[1] -\Function{PutSlotServer}{$sv_p$} - \State $s_p \gets n$ - \State $n \gets n + 1$ - \State $SL \gets SL \cup \{\tuple{s_p,sv_p}\}$ -\EndFunction -\end{algorithmic} -\end{varwidth}% -} - -\subsection{\textbf{Get Slot}} -Get slot is an operation that returns all server slots that are greater than some server sequence number.\\ - -% Get Function -\noindent\fbox{% -\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} -\textbf{Get Function:} -\begin{algorithmic}[1] -\Function{GetSlotServer}{$s_g$} - \State \Return{$\{\tuple{s, sv} \in SL \mid s \geq s_g\}$} -\EndFunction -\end{algorithmic} -\end{varwidth}% -} - -\subsection{\textbf{Delete Slot}} -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.\\ - -%Delete Function -\noindent\fbox{% -\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} -\textbf{Delete Function:} -\begin{algorithmic}[1] -\Function{DeleteSlotServer}{$s_d$} - \State $SD \gets \{\tuple{s, sv} \in SL \mid s \leq s_g\}$ - \State $SL \gets SL - SD$ -\EndFunction -\end{algorithmic} -\end{varwidth}% -} - - - - -\section{\textbf{Client}} -The data structure acts as a key store where key-value pairs can be read and set. -The data structure exposes the following functions: -\begin{itemize} - \item Put Transaction - \item Get key-value pair - \item Create new key -\end{itemize} - - -\subsubsection{\textbf{Types of Payloads}} -The different types of record payloads are: -\begin{itemize} - \item Transactions - \begin{itemize} - \item Used to make updates to key value pairs. - \end{itemize} - \item Commit notifications - \begin{itemize} - \item Contains the commit of a single transaction, the whole transaction. - \item There is 1 commit per transaction. - \item Generated by the arbitrator for the set of key-value gets and sets in the transaction. - \end{itemize} - \item Abort notifications - \begin{itemize} - \item Causes a transaction to be aborted, key-values not used in updates. - \end{itemize} - \item Data structure re-size notifications - \begin{itemize} - \item Contains new size of data structure (number of record allowed in the data structure or something like that). - \end{itemize} - \item Server sequence number confirmations. - \begin{itemize} - \item Created by any device if that device finds a record with a server sequence number that does not have a server sequence number conformation yet. - \end{itemize} - \item Delete notifications - \begin{itemize} - \item Generated when a device deletes a record. - \item records the record that was last deleted - \end{itemize} - \item New Key notification - \begin{itemize} - \item Generated when a device generates a new (never used) key-value pair. - \end{itemize} -\end{itemize} - -\subsection{\textbf{Client Notation Conventions}} - -$K$ is the set of all keys.\\ -$MID$ is the set of the machine IDs of the devices that are in the system. -$K_{mid}$ is a set of all keys that have device mid as the arbitrator\\ -$ssn_s$ is the server sequence number of a record $s$\\ -$mid_s \in MID$ is the machine ID for the device that created $record_s$.\\ -$hmac_s$ is the HMAC of $record_s$\\ -$c_{mid}$ is the latest read clock for a device with machine ID $mid$\\ -$vc_s = \{c_{mid} | mid \in MID\}$\\ -$rid_s = \tuple{mid_s, c_{mid_s}}$ -$k$ is a key entry\\ -$v$ is a value entry\\ -$kv_n$ is a key-value entry $\tuple{k_n,v_n} , k \in K$\\ - -$tid_s = \tuple{mid_s,c_{mid_s}}$\\ -$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\}} $\\ -$transaction_s = \tuple{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}$\\ -$commit_s = \tuple{tid_s,vc_s}$\\ -$abort_s = \tuple{tid_s,mid_s,vc_s}$\\ -$sequence_s = \tuple{rid_s, ssn_s}$\\ -$delete_s = \tuple{ssn_d}$\\ -$resize_s = \tuple{x | x \in \mathbb{N}}$\\ -$newkey_s = \tuple{k_s, vc_s, ssn_s$ or $NULL, mid_s}$\\ - -$payload_s = \{x_1, x_2,..., x_k | \forall k, x_k \in \{$transaction, commit, abort, resize, newkey, sequence, delete$\}\}$\\ -$rd_s = \tuple{mid_s, vc_s, hmac_s, payload_s}$ \\ -$record_s = \tuple{ssn_s,rd_s}$\\ - -\subsection{\textbf{Client State}} -\textit{s = largest server sequence number pulled from the server by a device} \\ -\textit{R = set of records pulled from the server so far with their server sequence numbers} \\ - -\subsection{Helper Functions} -The following helper functions are needed:\\ - -% Error -\noindent\fbox{% -\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} -\textbf{ Error:} -\begin{algorithmic}[1] -\Function{Error}{$msg$} - \State $Print(msg)$ - \State $Halt()$ -\EndFunction -\end{algorithmic} -\end{varwidth}% -} - -%Get Payload Items from Record with SSN -\noindent\fbox{% -\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} -\textbf{Get Payload Items from Record with SSN}: -\begin{algorithmic}[1] -\Function{GetPayloadItemsWithSSN}{$record_s$} - \State $PISSN \gets \emptyset$ \Comment{Set of Payload Items with ssn} - \State $\tuple{ssn_s, rd_s} \gets record_s$ - \State $\tuple{mid_s, vc_s, hmac_s, payload_s} \gets rd_s$\\ - - \ForAll{$payloadItems$ in $payload_s$} - \State $PISSN \gets PISSN \cup \{\tuple{payloadItem, ssn_s}\}$ - \EndFor\\ - - \State \Return {$PISSN$} -\EndFunction -\end{algorithmic} -\end{varwidth}% -} - -%Get rid of record -\noindent\fbox{% -\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} -\textbf{Get rid of record:} -\begin{algorithmic}[1] -\Function{GetRid}{$record_s$} - \State $\tuple{ssn_s, \tuple{mid_s, \{c_{mid_1}, c_{mid_2}, ... , c_{mid_k}\}, hmac_s, payload_s}} \gets record_s$ - \State \Return {$\tuple{mid_s, c_{mid_s}}$} -\EndFunction -\end{algorithmic} -\end{varwidth}% -} - -%Get tid of transaction -\noindent\fbox{% -\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} -\textbf{Get tid of transaction:} -\begin{algorithmic}[1] -\Function{GetTid}{$transaction_s$} - \State $\tuple{ssn_s,\{c_{mid_1}, c_{mid_2}, ... , c_{mid_k}\}, \{kv_1, kv_2,...kv_n\}, guard_s} \gets record_s$ - \State \Return {$\tuple{mid_s, c_{mid_s}}$} -\EndFunction -\end{algorithmic} -\end{varwidth}% -} - -%Key Value Live -%\noindent\fbox{% -%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} -\textbf{Key Value Live:} -\begin{algorithmic}[1] -\Function{KeyValueLive}{$keyName_s, transaction_s$} - \State $API \gets \emptyset$ \Comment{Set of all Payload Items} - \State $AT \gets \emptyset$ \Comment{Set of all Payload Items that are transactions} - \State $AC \gets \emptyset$ \Comment{Set of all Payload Items that are commits} - \State $AA \gets \emptyset$ \Comment{Set of all Payload Items that are aborts} - \State $commitTrans = NULL$ - \State $tid \gets $ \Call{GetTid}{$transaction_s$}\\ - - \ForAll{$record$ in $R$} - \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record} - \EndFor\\ - - \ForAll{$\tuple{ssn, payload}$ in $API$} - \If{$payload$ is a $transaction$} - \State $AT \gets AT \cup \{payload\}$ - \ElsIf{$payload$ is a $commit$} - \State $AC \gets AC \cup \{payload\}$ - \ElsIf{$payload$ is a $abort$} - \State $AA \gets AA \cup \{payload\}$ - \EndIf - \EndFor\\ - - \ForAll{$\tuple{tid',mid',vc'}$ in $AA$} \Comment{Has an abort} - \If{$tid' = tid$} - \State \Return{False} - \EndIf - \EndFor\\ - - \ForAll{$\tuple{tid',vc'}$ in $AC$} \Comment{Has a commit} - \If{$tid' = tid$} - \State $commitTrans \gets \tuple{tid',vc'}$ - \State Break - \EndIf - \EndFor\\ - - \If{$commitTrans = NULL$} - \State \Return{True} \Comment{If transaction not yet committed then alive} - \EndIf\\ - - \State $\tuple{tid_c, vc_c} \gets commitTrans$ - \ForAll{$trans$ in $AT$} - \State $\{mid_t,vc_t ,\{\tuple{k_1, v_1}, \tuple{k_2, v_2},..., \tuple{k_k, v_k}\},guard_t\} \gets trans$ - \If{$(trans \neq transaction_s) \land (keyName_s = k_n)$} - \ForAll{$\tuple{tid_c',vc_c'}$ in $AC$} - \If{$(tid_c = $ \Call{GetTid}{$trans$} $) \land (vc_c' > vc_c)$} - \State \Return{False} - \EndIf - \EndFor - \EndIf - \EndFor\\ - - \State \Return{True} - -\EndFunction -\end{algorithmic} -%\end{varwidth}% -%} - -%Sequence Live -\noindent\fbox{% -\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} -\textbf{Sequence Live}: -\begin{algorithmic}[1] -\Function{SequenceLive}{$sequence_s, ssn_{s1}$} - \State $API \gets \emptyset$ \Comment{Set of all Payload Items} - \State $AS \gets \emptyset$ \Comment{Set of all Payload Items that are sequences} - \State $StillHasRecord \gets False$ - \State $\tuple{rid_s, ssn_{s2}} \gets sequence_s$\\ - - \ForAll{$record$ in $R$} - \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record} - \If{$rid_s = $\Call{GetRid}{$record$}} - \State $StillHasRecord \gets True$ - \EndIf - \EndFor\\ - - \If{$\lnot StillHasRecord$} \Comment{The Record does not exists anymore} - \State \Return{False} - \EndIf\\ - - \ForAll{$\tuple{ssn, payload}$ in $API$} - \If{$payload$ is a $sequence$} - \State $AS \gets AS \cup \{\tuple{ssn, payload}\}$ \Comment{Extract all sequence payloads} - \EndIf - \EndFor\\ - - \ForAll{$\tuple{ssn_1', \tuple{rid', ssn_2'}}$ in $AS$} - \If{$(rid'=rid_s) \land (ssn_1' > ssn_{s_1})$} - \State \Return{False} - \EndIf - \EndFor \\ - \State \Return{True} -\EndFunction -\end{algorithmic} -\end{varwidth}% -} - -% Delete Live -\noindent\fbox{% -\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} -\textbf{Delete Live}: -\begin{algorithmic}[1] -\Function{DeleteLive}{$delete_s, ssn_s$} - \State $API \gets \emptyset$ \Comment{Set of all Payload Items} - \State $AD \gets \emptyset$ \Comment{Set of all Payload Items that are deletes} - \State $\tuple{ssn_d} \gets delete_s$\\ - - \ForAll{record in R} - \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record} - \EndFor\\ - - \ForAll{$\tuple{ssn, payload}$ in $API$} - \If{$payload$ is a $delete$} - \State $AD \gets AD \cup \{\tuple{ssn, payload}\}$ \Comment{Extract all delete payloads} - \EndIf - \EndFor\\ - - \ForAll{delete in AD} - \State $\tuple{{ssn_s}', \tuple{{ssn_d}'}} \gets delete$ - \If{${ssn_d}' > ssn_d$} \Comment{More recently deleted record} - \State \Return{False} - \ElsIf{$({ssn_d}'= ssn_d) \land ({ssn_s}' > ssn_s)$} \Comment{More recent delete of same record} - \State \Return{False} - \EndIf - \EndFor \\ - \State \Return{True} -\EndFunction -\end{algorithmic} -\end{varwidth}% -} - -%Abort Live -\noindent\fbox{% -\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} -\textbf{Abort Live}: -\begin{algorithmic}[1] -\Function{AbortLive}{$abort_s$} - \State $API \gets \emptyset$ \Comment{Set of all Payload Items} - \State $tid \gets NULL$ - \State $\tuple{tid_s,mid_s,vc_s} \gets abort_s$\\ - - \ForAll{$record$ in $R$} - \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record} - \EndFor\\ - - \ForAll{$\tuple{ssn, payload}$ in $API$} \Comment{Transaction still in data structure} - \If{$payload$ is a $transaction$} - \State $tid \gets $\Call{GetTid}{$payload$} - \If{$tid = tid_s$} - \State Return{True} - \EndIf - \EndIf - \EndFor\\ - - - - \ForAll{record in R} - \State $\tuple{ssn_s',\tuple{mid_s', vc_s', hmac_s', payload_s'}} \gets record$ - \If{$(mid_s'=mid_s) \land (vc_s' > vc_s)$} - \State \Return{False} - \EndIf - \EndFor\\ - \State \Return{True} -\EndFunction -\end{algorithmic} -\end{varwidth}% -} - -%Resize Live -\noindent\fbox{% -\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} -\textbf{Resize Live}: -\begin{algorithmic}[1] -\Function{ResizeLive}{$resize_s, ssn_s$} - \State $API \gets \emptyset$ \Comment{Set of all Payload Items} - \State $AR \gets \emptyset$ \Comment{Set of all Payload Items that are resize} - \State $\tuple{size} \gets resize_s$\\ - - \ForAll{record in R} - \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record} - \EndFor\\ - - \ForAll{$\tuple{ssn, payload}$ in $API$} - \If{$payload$ is a $resize$} - \State $AR \gets AR \cup \{\tuple{ssn, payload}\}$ \Comment{Extract all resize payloads} - \EndIf - \EndFor\\ - - \ForAll{$\tuple{ssn', \tuple{size'}}$ in $AR$} - \If{$size' > size$} - \State \Return{False} - \ElsIf{$(size'=size) \land (ssn' > ssn_s)$} - \State \Return{False} - \EndIf - \EndFor \\ - \State \Return{True} -\EndFunction -\end{algorithmic} -\end{varwidth}% -} - -%New Key Live -\noindent\fbox{% -\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} -\textbf{New Key Live:} -\begin{algorithmic}[1] -\Function{NewKeyLive}{$newkey_s, ssn_r$} - \State $API \gets \emptyset$ \Comment{Set of all Payload Items} - \State $ANK \gets \emptyset$ \Comment{Set of all Payload Items that are new keys} - \State $\tuple{k_s, vc_s, ssn_s, mid_s}\gets newkey_s$\\ - - \If{$ssn_s = NULL$} \Comment{Make sure ssn is the correct one} - \State $ssn_s \gets ssn_r$ - \EndIf\\ - - \ForAll{record in R} - \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record} - \EndFor\\ - - \ForAll{$\tuple{ssn', payload'}$ in $API$} - \If{$payload'$ is a $newkey$} - \State $ANK \gets ANK \cup \{\tuple{ssn', payload'}\}$ \Comment{Extract all new key payloads} - \EndIf - \EndFor\\ - - \ForAll{$\tuple{ssn', \tuple{k_s', vc_s', ssn_s', mid_s'}}$ in $ANK$} - \If{$vc_s' < vc_s$} - \State \Return{False} - \ElsIf{$\lnot (vc_s' < vc_s) \land (ssn_s' < ssn_s)$} - \State \Return{False} - \EndIf - \EndFor \\ - \State \Return{True} -\EndFunction -\end{algorithmic} -\end{varwidth}% -} - -%Transaction Live -\noindent\fbox{% -\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} -\textbf{Transaction Live:} -\begin{algorithmic}[1] -\Function{TransactionLive}{$transaction_s$} - \State $AA \gets \emptyset$ \Comment{Set of all Payload Items that are aborts} - \State $AC \gets \emptyset$ \Comment{Set of all Payload Items that are commits} - \State $API \gets \emptyset$ \Comment{Set of all Payload Items} - \State $tid \gets $ \Call{GetTid}{$transaction_s$} - \State $foundCommit \gets False$\\ - - \ForAll{$record$ in $R$} - \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record} - \EndFor\\ - - \ForAll{$\tuple{ssn, payload}$ in $API$} - \If{$payload$ is a $abort$} - \State $AA \gets AA \cup \{payload\}$ - \ElsIf{$payload$ is a $commit$} - \State $AC \gets AC \cup \{payload\}$ - \EndIf - \EndFor\\ - - \ForAll{$\tuple{tid',mid',vc'}$ in $AA$} \Comment{There is an abort} - \If{$tid' = tid$} - \State \Return{False} - \EndIf - \EndFor\\ - - \ForAll{$\tuple{tid',vc'}$ in $AC$} \Comment{There is no commit} - \If{$tid' = tid$} - \State $foundCommit \gets True$ - \State Break - \EndIf - \EndFor\\ - - \If{$\lnot foundCommit$} - \State \Return{True} - \EndIf\\ - - \State $\tuple{mid',vc' ,kvSet',guard'} \gets transaction_s$ \Comment{All Keys are dead} - \ForAll{$\tuple{k',v'}$ in $kvSet'$} - \If{\Call{KeyValueLive}{$k', transaction_s$}} - \State \Return{True} - \EndIf - \EndFor - - \State \Return{False} - -\EndFunction -\end{algorithmic} -\end{varwidth}% -} - -%Commit Live -\noindent\fbox{% -\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} -\textbf{Commit Live:} -\begin{algorithmic}[1] -\Function{CommitLive}{$commit_s, ssn_s$} - \State $API \gets \emptyset$ \Comment{Set of all Payload Items} - \State $AT \gets \emptyset$ \Comment{Set of all Payload Items that are transaction} - \State $tid' \gets NULL$ - \State $\tuple{tid, vc} \gets commit_s$ \\ - - \ForAll{$record$ in $R$} - \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record} - \EndFor\\ - - \ForAll{$\tuple{ssn, payload}$ in $API$} - \If{$payload$ is a $transaction$} - \State $tid' \gets$ \Call{GetTid}{$payload$} - \If{$tid' = tid$} - \State \Return{True} - \EndIf - \EndIf - \EndFor\\ - - \State \Return{False} -\EndFunction -\end{algorithmic} -\end{varwidth}% -} - -%Is Live -\noindent\fbox{% -\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} -\textbf{Is Live:}: -\begin{algorithmic}[1] -\Function{IsLive}{$item_s, ssn_S$} - \If{$item_s$ is a $tansaction$} - \State \Return{\Call{TransactionLive}{$item_s$}} - - \ElsIf{$item_s$ is a $commit$} - \State \Return{\Call{CommitLive}{$item_s, ssn_s$}} - - \ElsIf{$item_s$ is a $abort$} - \State \Return{\Call{AbortLive}{$item_s$}} - - \ElsIf{$item_s$ is a $delete$} - \State \Return{\Call{DeleteLive}{$item_s, ssn_s$}} - - \ElsIf{$item_s$ is a $commit$} - \State \Return{\Call{ResizeLive}{$item_s, ssn_s$}} - - \ElsIf{$item_s$ is a $sequence$} - \State \Return{\Call{SequenceLive}{$item_s, ssn_s$}} - - \ElsIf{$item_s$ is a $newkey$} - \State \Return{\Call{NewKeyLive}{$item_s, ssn_s$}} - - \ElsIf{$item_s$ is a $keyvalue$} - \State \Return{\Call{KeyValueLive}{$item_s, ssn_s$}} - \EndIf\\ - - \State \Return{False} \Comment{Will never get here} -\EndFunction -\end{algorithmic} -\end{varwidth}% -} - -%Record has live payload data -\noindent\fbox{% -\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} -\textbf{Record has live payload data:}: -\begin{algorithmic}[1] -\Function{HasLivePayload}{$record_s, ssn_s$} - \State $\tuple{mid_s, vc_s, hmac_s, payload_s} \gets record_s$ - \ForAll{$item$ in $payload_s$} - \If{\Call{IsLive}{$item, ssn_s$}} - \State \Return{True} - \EndIf - \EndFor - \State \Return{False} -\EndFunction -\end{algorithmic} -\end{varwidth}% -} - -% Get Data Structure Size -\noindent\fbox{% -\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} -\textbf{Get Data Structure Size:} -\begin{algorithmic}[1] -\Function{GetDataStrucSize}{ } - \State $API \gets \emptyset$ \Comment{Set of all Payload Items} - \State $AR \gets \emptyset$ \Comment{Set of all Payload Items that are resize} - - \ForAll{record in R} - \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record} - \EndFor\\ - - \ForAll{$\tuple{ssn, payload}$ in $API$} - \If{($payload$ is a $resize) \land$ \Call{IsLive}{$payload, ssn$}} - \State $\tuple{size'} \gets payload$ - \State \Return{$size'$} - \EndIf - \EndFor\\ - - \State \Return{$0$} \Comment{Get Here only if data structure has no entries} -\EndFunction -\end{algorithmic} -\end{varwidth}% -} - -%Rescue New Key -\noindent\fbox{% -\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} -\textbf{Rescue New Key:} -\begin{algorithmic}[1] -\Function{RescueNewKey}{$newKeyPayload, ssn$} - \State $\tuple{k', vc', ssn', mid'} \gets newKeyPayload$ - \State \Return{$\tuple{k', vc', ssn, mid'}$} -\EndFunction -\end{algorithmic} -\end{varwidth}% -} - -%Rescue Transaction -\noindent\fbox{% -\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} -\textbf{Rescue New Key:} -\begin{algorithmic}[1] -\Function{RescueTransaction}{$transPayload, ssn$} - \State $KVRescue \gets \emptyset$ - \State $\tuple{mid',vc', KVSet,guard_s} \gets transPayload$\\ - - \ForAll{$\tuple{k,v}$ in $KVSet$} - \If{\Call{KeyValueLive}{$k, transPayload$}} - \State $KVRescue \gets KVRescue \cup \{\tuple{k,v}\}$ - \EndIf - \EndFor\\ - - \State \Return{$\tuple{mid',vc', KVRescue,guard_s}$} -\EndFunction -\end{algorithmic} -\end{varwidth}% -} - - -%Rescue Payload Items -\noindent\fbox{% -\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} -\textbf{Rescue Payload Items}: -\begin{algorithmic}[1] -\Function{RescuePayloadItems}{$payload_s$} - \State $PIList =$ empty list of $\tuple{ssn, payload}$ - \State $SpaceRemaining = MaxPayloadSize - $ \Call{GetSize}{$payload_s$} - - \If{$SpaceRemaining = 0$} - \Return{$payload_s$} - \EndIf\\ - - \ForAll{record in R} - \State $PIList \gets PIList \cup$ \Call{GetPayloadItemsWithSSN}{$record$} - \EndFor\\ - - \State Sort $PIList$ by $ssn$ from lowest to highest\\ - - \ForAll{$\tuple{ssn', payload'}$ in $PIList$} - \If{\Call{IsLive}{$payload', ssn'$} $\land$ \Call{getRandomBoolean}{ } }\\ - - \If{$payload'$ is a $newkey$} - \State $payload' \gets $ \Call{RescueNewKey}{$payload'$} - \ElsIf{$payload'$ is a $transaction$} - \State $payload' \gets $ \Call{RescueTransaction}{$payload'$} - \EndIf\\ - - \If{\Call{GetSize}{$payload'$} $ > SpaceRemaining$} \Comment{No more space for resuces in payload} - \State \Return{$payload_s$} - \EndIf - - \State $SpaceRemaining \gets SpaceRemaining -$ \Call{GetSize}{$payload'$} - \State $payload_s \gets payload_s \cup \{payload'\}$ - \EndIf - \EndFor\\ - \State \Return{$payload_s$} -\EndFunction -\end{algorithmic} -\end{varwidth}% -} - -%Pad Payload -\noindent\fbox{% -\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} -\textbf{Pad Payload}: -\begin{algorithmic}[1] -\Function{PadPayload}{$payload_s$} \State $SpaceRemaining = MaxPayloadSize - $ \Call{GetSize}{$payload_s$} - - \If{$SpaceRemaining = 0$} - \State \Return{$payload_s$} - \EndIf\\ - \State \Return{$payload_s \gets payload_s \cup$ \Call{GenerateFiller}{$SpaceRemaining$}} -\EndFunction -\end{algorithmic} -\end{varwidth}% -} - -%Delete Records -\noindent\fbox{% -\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} -\textbf{Delete Records (Deletes n records)}: -\begin{algorithmic}[1] -\Function{Delete}{$num\_of\_records$} - \State $RS \gets$ List of all Records sorted by ssn and has form $\tuple{ssn_s, record_s}$ - \State $n \gets 0$\\ - - \ForAll{$\tuple{ssn_s, record_s}$ in $RS$} - \If{\Call{HasLivePayload}{$record_s, ssn_s$}} - \State \Return{False} - \Else - \State \Call{DeleteSlotServer}{$ssn_s$} - \State $n \gets n + 1$ - \EndIf\\ - - \If{$n = num\_of\_records$} - \State \textbf{break} - \EndIf - \EndFor\\ - - \State \Return{True} - -\EndFunction -\end{algorithmic} -\end{varwidth}% -} - -%Create Resize Data Structure Payload Item -\noindent\fbox{% -\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} -\textbf{Create Resize Data Structure Payload Item:} -\begin{algorithmic}[1] -\Function{MakeResizePayload}{ } - \State $rp \gets$ Empty $resize$ payload - \State $cs \gets$ \Call{GetDataStrucSize}{ } - \State $rp \gets \tuple{cs * 2}$ - \State \Return{$\{rp\}$} -\EndFunction -\end{algorithmic} -\end{varwidth}% -} - -%Get Arbitrator -\noindent\fbox{% -\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} -\textbf{Get Arbitrator:} -\begin{algorithmic}[1] -\Function{GetArbitrator}{$key$} - \State $API \gets \emptyset$ \Comment{Set of all Payload Items}\\ - - \ForAll{record in R} - \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record} - \EndFor\\ - - \ForAll{$\tuple{ssn, payload}$ in $API$} - \If{($payload$ is a $newkey) \land$ \Call{IsLive}{$payload, ssn$}} - \State $\tuple{k', vc', ssn', mid'} \gets payload$ - - \If{$k' = key$} - \State \Return{$mid'$} - \EndIf - \EndIf - \EndFor\\ - \State \Call{Error}{No arbitrator for key: $key$} -\EndFunction -\end{algorithmic} - -\begin{algorithmic}[1] -\Function{GetArbitrator}{$guard$} - \State $API \gets \emptyset$ \Comment{Set of all Payload Items} - \State $\tuple{kvSet, condition} \gets guard$\\ - - \ForAll{record in R} - \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record} - \EndFor\\ - - \ForAll{$\tuple{key, value}$ in $kvSet$} - \ForAll{$\tuple{ssn, payload}$ in $API$} - \If{($payload$ is a $newkey) \land$ \Call{IsLive}{$payload, ssn$}} - \State $\tuple{k', vc', ssn', mid'} \gets payload$ - \If{$k' = key$} - \State \Return{$mid'$} - \EndIf - \EndIf - \EndFor - \EndFor\\ - \State \Call{Error}{No arbitrator for key: $key$} -\EndFunction -\end{algorithmic} - -\end{varwidth}% -} - -%Insert Payload -\noindent\fbox{% -\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} -\textbf{Insert Payload:} -\begin{algorithmic}[1] -\Function{InsertPayload}{$payload_s$} - - \State $numOfRecords \gets |R|+1$ - \State $targetSize \gets $ \Call{GetDataStrucSize}{ } - \State $numToDelete \gets numOfRecords - targetSize$ - \State $rp \gets NULL$ - \State $hmac \gets NULL$ - \State $vc \gets NULL$ - \State $record \gets NULL$\\ - - \If{\Call{GetSize}{$payload_s$} $> MaxPayloadSize$} - \State \Call{Error}{Payload too large} - \EndIf\\ - - \If{$numToDelete > 0$} - \If{$\lnot$\Call{Delete}{$numToDelete$}} - \State $rp \gets$\Call{MakeResizePayload}{ } - \If{\Call{GetSize}{$payload_s \cup rp$} $> MaxPayloadSize$} - \State \Call{InsertPayload}{$rp$} - \Else - \State $payload_s \gets payload_s \cup rp$ - \EndIf - \EndIf - \EndIf\\ - - \State $payload_s \gets$ \Call{RescuePayloadItems}{$payload_s$} - \State $payload_s \gets$ \Call{PadPayload}{$payload_s$} - \State $vc \gets $ \Call{GenerateVectorClock}{ } - \State \Call{IncrementVectorClock}{ } - \State $hmac \gets$ \Call{GenerateHmac}{$mid, vc, payload_s$} - \State $record \gets \tuple{mid,vc,hmac,payload}$ - \State $record \gets $\Call{Encrypt}{$record$} - \State \Call{PutSlotServer}{$record$} -\EndFunction -\end{algorithmic} -\end{varwidth}% -} - -%Check Data Structure for Malicious Activity -%\noindent\fbox{% -%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} -\textbf{Check Data Structure for Malicious Activity:} -\begin{algorithmic}[1] -\Function{CheckDataStructForValidity}{ } - \State $API \gets \emptyset$ \Comment{Set of all Payload Items} - \State $ASeq \gets \emptyset$ \Comment{Set of all Payload Items that are sequences} - \State $MID \gets \emptyset$ \Comment{Set of all machine IDs} - \State $midClocks \gets \emptyset$ \Comment{Set of all clocks for the same machine IDs} - \State $oldestDeletedSsn \gets NULL$ - \State $didFindSsn \gets False$ - \State $didFindClock \gets False$ - \State $hmac \gets NULL$\\ - - \State Sort $R$ by $ssn$ from smallest $ssn$ to largest $ssn$\\ - - \ForAll{record in R} - \State $\tuple{ssn',\tuple{mid', vc', hmac', payload'}} \gets record$ - \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record} - \State $MID \gets MID \cup \{mid'\}$ - \EndFor\\ - - \ForAll{$record$ in $R$} \Comment{Check HMACs are all valid} - \State $\tuple{ssn',\tuple{mid', vc', hmac', payload'}} \gets record$ - \State $hmac \gets $ \Call{GenerateHmac}{$mid', vc', payload'$} - \If{$hmac \neq hmac'$} - \State \Call{Error}{HMAC mismatch} - \EndIf - \EndFor\\ - - \ForAll{$record_1$ in $R$} \Comment{Check no SSN duplicates} - \State $\tuple{ssn_1,rData_1} \gets record_1$ - \ForAll{$record_2$ in $R$} - \If{$record_2 \neq record_1$} - \State $\tuple{ssn_2,rData_2} \gets record_2$ - \If{$ssn_2 = ssn_1$} - \State \Call{Error}{Duplicate SSN for different records} - \EndIf - \EndIf - \EndFor - \EndFor\\ - - - \ForAll{$record_1$ in $R[0:-1]$} \Comment{Check for missing SSN} - \State $\tuple{ssn_1,rData_1} \gets record_1$ - \State $didFindSsn \gets False$ - \ForAll{$record_2$ in $R[1:]$} - \State $\tuple{ssn_2,rData_2} \gets record_2$ - \If{$ssn_2 = (ssn_1 + 1)$} - \ State $didFindSsn \gets True$ - \State Break - \EndIf - \EndFor - - \If{$\lnot didFindSsn$} - \State \Call{Error}{Missing SSN in SSN sequence.} - \EndIf - \EndFor\\ - - \ForAll{$\tuple{ssn, payload}$ in $API$} - \If{($payload$ is a $delete) \land$ \Call{IsLive}{$payload, ssn$}} - \State $\tuple{ssn'} \gets payload$ - \State $oldestDeleteSsn \gets ssn'$ - \ElsIf{($payload$ is a $sequence) \land$ \Call{IsLive}{$payload, ssn$}} - \State $ASeq \gets ASeq \cup \{payload\}$ - \EndIf - \EndFor\\ - - - \ForAll{$record$ in $R$} \Comment{Check SSN's are all valid} - \State $\tuple{ssn, rData} \gets record$ - \ForAll{$\tuple{rid', ssn'}$ in $ASeq$} - \If{$(rid' =$ \Call{GetRid}{$record$}$) \land ssn' \neq ssn$} - \State \Call{Error}{SSN mismatch} - \EndIf - \EndFor - \EndFor\\ - - - \State $\tuple{ssn, payload} \gets R[0]$ \Comment{Get first record in the sorted R} - \If{$ssn > (oldestDeleteSsn + 1) $} - \State \Call{Error}{Missing records} - \EndIf\\ - - - \ForAll{$mid$ in $MID$} - \State $midClocks \gets \emptyset$ - - \ForAll{record in R} - \State $\tuple{ssn',\tuple{mid', vc', hmac', payload'}} \gets record$ - \If{$mid' = mid$} - \State $\tuple{c_{mid_1}, c_{mid_2},...,c_{mid_k}} \gets vc'$ - \State $midClocks \gets midClocks \cup \{c_{mid_n}|mid_n=mid\}$ - \EndIf - \EndFor\\ - - \State Sort $midClocks$ from smallest clock to largest clock\\ - - \ForAll{$c_1$ in $midClocks[0:-1]$} \Comment{Check for missing SSN} - \State $didFindSsn \gets False$ - \ForAll{$c_2$ in $midClocks[1:]$} - \If{$c_2 = (c_1 + 1)$} - \State $didFindC -ock\gets True$ - \State Break - \EndIf - \EndFor - \EndFor - - \If{$\lnot didFindClock$} - \State \Call{Error}{Missing clock in clock sequence for: $mid$.} - \EndIf - \EndFor\\ - - \State \Comment{If got here then data structure is valid} -\EndFunction -\end{algorithmic} -%\end{varwidth}% -%} - -%Get Latest Data Structure From Server -\noindent\fbox{% -\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} -\textbf{Get Latest Data Structure From Server}: -\begin{algorithmic}[1] -\Function{GetLatestDataStruct}{} - \State $largestSsn \gets $ Largest $ssn$ of all $ssn$ in $R$ - \State $R \gets R \cup $ \Call{GetSlotServer}{$largestSsn + 1$} - \State \Call{CheckDataStructForValidity}{ } -\EndFunction -\end{algorithmic} -\end{varwidth}% -} - -%Update Key Value Set -\noindent\fbox{% -\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} -\textbf{Update Key Value Set:} -\begin{algorithmic}[1] -\Function{UpdateKVSet}{$currentKV, kvSet$} - \State $newKVSet \gets kvSet$ - \State $foundKey \gets False$\\ - - \ForAll{$\tuple{k,v}$ in $currentKV$} - \State $foundKey \gets False$\\ - - \ForAll{$\tuple{k',v'}$ in $kvSet$} - \If{$k = k'$} - \State $foundKey \gets True$ - \State Break - \EndIf - \EndFor\\ - - \If{$\lnot foundKey$} - \State $newKVSet \gets newKVSet \cup \{\tuple{k,v}\}$ - \EndIf - \EndFor - - \State \Return{$newKVSet$} -\EndFunction -\end{algorithmic} -\end{varwidth}% -} - -\subsection{\textbf{Create new key}} -This operation creates a key and assigns an arbitrator to arbitrate on that new key. In the case where more than one clients concurrently try to create the same new key, the client that inserted the newkey payload with the lowest ssn will be the client to generate the key, all other clients generation attempts would be invalid. - -\noindent\fbox{% -\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} -\textbf{Create new key:} -\begin{algorithmic}[1] -\Function{CreateNewKey}{$keyName, mid$} - \State $vc \gets $ \Call{GenerateVectorClock}{ } - \State $newKeyPayload \gets \tuple{keyName, vc, NULL, mid}$ - \State $API \gets \emptyset$ \Comment{Set of all Payload Items}\\ - - \State \Call{GetLatestDataStruct}{ } \Comment{Update local version of data struct}\\ - - \ForAll{record in R} - \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record} - \EndFor\\ - - \ForAll{$\tuple{ssn, payload}$ in $API$} - \If{($payload$ is a $newkey) \land$ \Call{IsLive}{$payload, ssn$}} - \State $\tuple{k', vc', ssn', mid'} \gets payload$ - - \If{$k' = key$} - \State \Return{False} - \EndIf - \EndIf - \EndFor\\ - - \State \Call{InsertPayload}{$newKeyPayload$} - \State \Return{True} -\EndFunction -\end{algorithmic} -\end{varwidth}% -} - -\subsection{\textbf{Put Transaction}} -This operation puts a transaction into the data structure if this transaction fits inside a payload. -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.\\ - -% -\noindent\fbox{% -\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} -\textbf{Put Transaction:} -\begin{algorithmic}[1] -\Function{PutTransaction}{$kVUpdates, guard$} - \State $mid \gets NULL$ - \State $vc \gets $ \Call{GenerateVectorClock}{ } - \State $transPayload \gets NULL$\\ - - \State \Call{GetLatestDataStruct}{ } \Comment{Update local version of data struct}\\ - - \ForAll{$kv$ in $kVUpdates$} - \State $\tuple{k', v'} \gets kv$ - - \If{$mid = NULL$} - \State $mid \gets$ \Call{GetArbitrator}{$k'$} - \ElsIf{$mid \neq $ \Call{GetArbitrator}{$k'$}} - \State \Call{Error}{Multiple Arbitrators} - \EndIf - \EndFor\\ - - \If{\Call{GetArbitrator}{$guard$} $\neq mid$} - \State \Call{Error}{Multiple Arbitrators} - \EndIf\\ - - \State $transPayload \gets \tuple{mid, vc, kVUpdates, guard}$ - \State \Call{InsertPayload}{$transPayload$} -\EndFunction -\end{algorithmic} -\end{varwidth}% -} - -\subsection{\textbf{Get key-value pair}} -This operation gets the latest key value pair from the data structure. This is done by starting at the last known committed key value pairs then extrapolating into the future of uncommitted transactions till the transaction with the largest ssn is reached. Everytime a new transaction is evaluated, it is evaluated against the current best guess of key value pairs based on the transactions up to the transaction being evaluated (by ssn). This allows each client to "guess" what the latest value for a specified key will be even when the arbitrator has not stepped in yet to arbitrate. - -%\noindent\fbox{% -%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} -\textbf{Get Latest Data Structure From Server}: -\begin{algorithmic}[1] -\Function{GetValueForKey}{$keyName$} - \State $API \gets \emptyset$ \Comment{Set of all Payload Items} - \State $AT \gets \emptyset$ \Comment{Set of all Payload Items that are transactions} - \State $AC \gets \emptyset$ \Comment{Set of all Payload Items that are commits} - \State $AA \gets \emptyset$ \Comment{Set of all Payload Items that are aborts} - \State $kSet \gets \emptyset$ \Comment{Set of all key names in the system} - \State $tid \gets NULL$ - \State $currentKV \gets \emptyset$\\ - - \State \Call{GetLatestDataStruct}{ } \Comment{Update local version of data struct}\\ - - \ForAll{$record$ in $R$} - \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record} - \EndFor\\ - - \ForAll{$\tuple{ssn, payload}$ in $API$} - \If{$payload$ is a $transaction$} - \State $AT \gets AT \cup \{\tuple{ssn,payload}\}$ - \ElsIf{$payload$ is a $commit$} - \State $AC \gets AC \cup \{payload\}$ - \ElsIf{$payload$ is a $abort$} - \State $AA \gets AA \cup \{payload\}$ - \EndIf - \EndFor\\ - - \State Sort $AT$ by ssn from oldest to newest\\ - - \ForAll{$trans$ in $AT$} \Comment{Get the latest committed keys} - \State $\tuple{mid,vc ,kvSet,guard} \gets trans$\\ - - \ForAll{$\tuple{k,v}$ in $kvSet$} \Comment{Get all key names in the system} - \State $kSet \gets kSet \cup \{k\}$ - \EndFor\\ - - \If{$\lnot $\Call{TransactionLive}{$trans$}} \Comment{Only keep live transactions} - \State $AT \gets AT - \{trans\}$ - \State Continue - \EndIf\\ - - \State $tid \gets $ \Call{GetTid}{$trans$} - \ForAll{$com$ in $AC$} - \State $\tuple{tid', vc'} \gets com$ - \If{$tid' = tid$} - \ForAll{$\tuple{k,v}$ in $kvSet$} - \If{\Call{KeyValueLive}{$k,trans$}} - \State $currentKV \gets currentKV \cup \{\tuple{k,v}\}$ - \EndIf - \EndFor\\ - - \State $AT \gets AT - \{trans\}$ \Comment{No need for committed transactions} - \State Break - \EndIf - \EndFor - \EndFor\\ - - \ForAll{$trans$ in $AT$} \Comment{Uncommitted ones only in order from lowest ssn to highest ssn} - \State $\tuple{mid,vc ,kvSet,guard} \gets trans$ - \If{\Call{EvaluateGuard}{$guard, currentKV$}} \Comment{Check if will abort} - \State $currentKV \gets $\Call{UpdateKVSet}{$currentKV, kvSet$} - \EndIf - \EndFor\\ - - - \ForAll{$\tuple{k,v}$ in $currentKV$} \Comment{Return the latest guessed value} - \If{$k = keyName$} - \State \Return{$v$} - \EndIf - \EndFor\\ - - \State \Return{$NULL$} \Comment{Key was not present} - -\EndFunction -\end{algorithmic} -%\end{varwidth}% -%} - -\subsection{\textbf{Arbitrate On Transaction}} - -%\noindent\fbox{% -%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} -\textbf{Get Latest Data Structure From Server}: -\begin{algorithmic}[1] -\Function{Arbitrate }{ } - \State $API \gets \emptyset$ \Comment{Set of all Payload Items} - \State $AT \gets \emptyset$ \Comment{Set of all Payload Items that are transactions} - \State $AC \gets \emptyset$ \Comment{Set of all Payload Items that are commits} - \State $AA \gets \emptyset$ \Comment{Set of all Payload Items that are aborts} - \State $kSet \gets \emptyset$ \Comment{Set of all key names in the system} - \State $tid \gets NULL$ - \State $currentKV \gets \emptyset$ - \State $newPayload \gets NULL$ - \State $midClient \gets mid$ of this client\\ - - \State \Call{GetLatestDataStruct}{ } \Comment{Update local version of data struct}\\ - - \ForAll{$record$ in $R$} - \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record} - \EndFor\\ - - \ForAll{$\tuple{ssn, payload}$ in $API$} - \If{$payload$ is a $transaction$} - \State $AT \gets AT \cup \{\tuple{ssn,payload}\}$ - \ElsIf{$payload$ is a $commit$} - \State $AC \gets AC \cup \{payload\}$ - \ElsIf{$payload$ is a $abort$} - \State $AA \gets AA \cup \{payload\}$ - \EndIf - \EndFor\\ - - \State Sort $AT$ by ssn from oldest to newest\\ - - \ForAll{$trans$ in $AT$} \Comment{Get the latest committed keys} - \State $\tuple{mid,vc ,kvSet,guard} \gets trans$\\ - - \ForAll{$\tuple{k,v}$ in $kvSet$} \Comment{Get all key names in the system} - \State $kSet \gets kSet \cup \{k\}$ - \EndFor\\ - - \If{$\lnot $\Call{TransactionLive}{$trans$}} \Comment{Only keep live transactions} - \State $AT \gets AT - \{trans\}$ - \State Continue - \EndIf\\ - - \State $tid \gets $ \Call{GetTid}{$trans$} - \ForAll{$com$ in $AC$} - \State $\tuple{tid', vc'} \gets com$ - \If{$tid' = tid$} - \ForAll{$\tuple{k,v}$ in $kvSet$} - \If{\Call{KeyValueLive}{$k,trans$}} - \State $currentKV \gets currentKV \cup \{\tuple{k,v}\}$ - \EndIf - \EndFor\\ - - \State $AT \gets AT - \{trans\}$ \Comment{No need for committed transactions} - \State Break - \EndIf - \EndFor - \EndFor\\ - - \ForAll{$trans$ in $AT$} \Comment{Uncommitted ones only in order from lowest ssn to highest ssn} - \State $\tuple{mid,vc ,kvSet,guard} \gets trans$ - - \If{\Call{GetArbitrator}{$guard$} $\neq midClient$} - \State Continue - \EndIf - - \If{\Call{EvaluateGuard}{$guard, currentKV$}} \Comment{Check if will abort} - \State $currentKV \gets $\Call{UpdateKVSet}{$currentKV, kvSet$} - \State $newPayload \gets \tuple{$\Call{GetTid}{$trans$}$, $\Call{GenerateVectorClock}{ } $}$ \Comment{Make new commit payload} - \Else - \State $newPayload \gets \tuple{$\Call{GetTid}{$trans$}$, mid, $\Call{GenerateVectorClock}{ } $}$ \Comment{Make new abort payload} - \EndIf\\ - - \State \Call{InsertPayload}{$newPayload$} - \EndFor\\ - -\EndFunction -\end{algorithmic} -%\end{varwidth}% -%} - - - -\section{\textbf{System Guarantees}} -\begin{itemize} - \item Server cannot view data inside records - \item Server cannot forge or modify or create any records - \item Server cannot withhold any records - \item Server cannot reorder records that could not have been ordered differently due to network latency - \item Server cannot delete records unless told to do so. - \item There will always be an obvious key-value pair that is the latest key value pair. - \item The data structure is bounded in size such that $m$ is the minimum size of the data structure, $n$ is the number of devices in the system and $s$ is the current size of the data structure: $m \leq s \leq (m+n-1)$ - \item Data structure can only grow when there are too may key-value pairs (and aborts) than what fit in the current data structure size within reason. - \item No currently valid data can be lost by the system and go undetected. - \item Devices can operate offline and re-sync with the system and get a consistent view of the system - \item If the server tries to hold a device on an older version of the data structure, that device can eventually rejoin the main data structure without problems. - \item Devices that have a transaction aborted will be able to be notified about the abort indefinitely (no time frame when notification must be accepted). - \item Server cannot hold a device on an old version of the data structure and then move them to a newer version of the data structure without being detected (The server sequence numbers would reveal conflicts or gaps or both). - -\end{itemize} - - -\end{document} diff --git a/version2/doc/iotcloud_formal/makefile b/version2/doc/iotcloud_formal/makefile deleted file mode 100644 index cff4a15..0000000 --- a/version2/doc/iotcloud_formal/makefile +++ /dev/null @@ -1,8 +0,0 @@ -LATEX := pdflatex -halt-on-error - -default: - $(LATEX) iotcloud.tex - -clean: - rm -f *.dvi *.log *.aux *.blg *.bbl *~ - rm -f iotcloud.ps iotcloud.pdf diff --git a/version2/doc/iotcloud_informal/iotcloud.out b/version2/doc/iotcloud_informal/iotcloud.out deleted file mode 100644 index 14b3549..0000000 --- a/version2/doc/iotcloud_informal/iotcloud.out +++ /dev/null @@ -1,32 +0,0 @@ -\BOOKMARK [1][-]{section.1}{Introduction}{}% 1 -\BOOKMARK [1][-]{section.2}{Device Approach}{}% 2 -\BOOKMARK [2][-]{subsection.2.1}{Records}{section.2}% 3 -\BOOKMARK [3][-]{subsubsection.2.1.1}{Types of Payloads}{subsection.2.1}% 4 -\BOOKMARK [2][-]{subsection.2.2}{Pulling the data structure}{section.2}% 5 -\BOOKMARK [2][-]{subsection.2.3}{Updates}{section.2}% 6 -\BOOKMARK [2][-]{subsection.2.4}{Deletions}{section.2}% 7 -\BOOKMARK [2][-]{subsection.2.5}{Reading a key-value pair}{section.2}% 8 -\BOOKMARK [2][-]{subsection.2.6}{Rescuing Transactions, Commits, Aborts, Ext}{section.2}% 9 -\BOOKMARK [2][-]{subsection.2.7}{Checking the Data Structure}{section.2}% 10 -\BOOKMARK [2][-]{subsection.2.8}{The Arbitrator}{section.2}% 11 -\BOOKMARK [3][-]{subsubsection.2.8.1}{Commits}{subsection.2.8}% 12 -\BOOKMARK [3][-]{subsubsection.2.8.2}{Aborts}{subsection.2.8}% 13 -\BOOKMARK [2][-]{subsection.2.9}{Setting Up New Keys \(Choosing the Arbitrator\)}{section.2}% 14 -\BOOKMARK [2][-]{subsection.2.10}{Live Status}{section.2}% 15 -\BOOKMARK [1][-]{section.3}{Server Approach}{}% 16 -\BOOKMARK [2][-]{subsection.3.1}{Pull all current slots}{section.3}% 17 -\BOOKMARK [2][-]{subsection.3.2}{Put a new record in a slot}{section.3}% 18 -\BOOKMARK [2][-]{subsection.3.3}{Delete a slot}{section.3}% 19 -\BOOKMARK [1][-]{section.4}{Data Structure Abstraction}{}% 20 -\BOOKMARK [2][-]{subsection.4.1}{Put Operation}{section.4}% 21 -\BOOKMARK [2][-]{subsection.4.2}{Get Operation}{section.4}% 22 -\BOOKMARK [2][-]{subsection.4.3}{Check put status}{section.4}% 23 -\BOOKMARK [2][-]{subsection.4.4}{Create New Key Operation}{section.4}% 24 -\BOOKMARK [1][-]{section.5}{System Guarantees}{}% 25 -\BOOKMARK [1][-]{section.6}{System Correctness}{}% 26 -\BOOKMARK [2][-]{subsection.6.1}{Data Integrity and Authentication}{section.6}% 27 -\BOOKMARK [2][-]{subsection.6.2}{Ordering of Records}{section.6}% 28 -\BOOKMARK [2][-]{subsection.6.3}{Data Structure Functions}{section.6}% 29 -\BOOKMARK [3][-]{subsubsection.6.3.1}{Put}{subsection.6.3}% 30 -\BOOKMARK [3][-]{subsubsection.6.3.2}{Get}{subsection.6.3}% 31 -\BOOKMARK [3][-]{subsubsection.6.3.3}{Create New Key}{subsection.6.3}% 32 diff --git a/version2/doc/iotcloud_informal/iotcloud.tex b/version2/doc/iotcloud_informal/iotcloud.tex deleted file mode 100644 index 01b6449..0000000 --- a/version2/doc/iotcloud_informal/iotcloud.tex +++ /dev/null @@ -1,437 +0,0 @@ -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Short Sectioned Assignment -% LaTeX Template -% Version 1.0 (5/5/12) -% -% This template has been downloaded from: -% http://www.LaTeXTemplates.com -% -% Original author: -% Frits Wenneker (http://www.howtotex.com) -% -% License: -% CC BY-NC-SA 3.0 (http://creativecommons.org/licenses/by-nc-sa/3.0/) -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -%---------------------------------------------------------------------------------------- -% PACKAGES AND OTHER DOCUMENT CONFIGURATIONS -%---------------------------------------------------------------------------------------- - -\documentclass[paper=letter, fontsize=11pt]{scrartcl} % A4 paper and 11pt font size - -\usepackage[T1]{fontenc} % Use 8-bit encoding that has 256 glyphs -\usepackage{fourier} % Use the Adobe Utopia font for the document - comment this line to return to the LaTeX default -\usepackage[english]{babel} % English language/hyphenation -\usepackage{amsmath,amsfonts,amsthm} % Math packages -\usepackage{graphicx} -\usepackage{lipsum} % Used for inserting dummy 'Lorem ipsum' text into the template -\usepackage{hyperref} -\usepackage{amssymb} -\usepackage{listings} -\usepackage[]{algorithm2e} -\usepackage{algpseudocode} -\usepackage{enumerate} -\usepackage[table,xcdraw]{xcolor} -\usepackage{sectsty} % Allows customizing section commands -\usepackage{float} -\usepackage{caption} -\usepackage{gensymb} % to used degree symbol -\usepackage{siunitx} -\usepackage{enumitem} - -\usepackage[sc]{mathpazo} -\allsectionsfont{ \normalfont\scshape} % Make all sections the default font and small caps -\usepackage{fancyhdr} % Custom headers and footers -\pagestyle{fancyplain} % Makes all pages in the document conform to the custom headers and footers -\fancyhead{} % No page header - if you want one, create it in the same way as the footers below -\fancyfoot[L]{} % Empty left footer -\fancyfoot[C]{} % Empty center footer -\fancyfoot[R]{\thepage} % Page numbering for right footer -\renewcommand{\headrulewidth}{0pt} % Remove header underlines -\renewcommand{\footrulewidth}{0pt} % Remove footer underlines -\setlength{\headheight}{13.6pt} % Customize the height of the header - -\numberwithin{equation}{section} % Number equations within sections (i.e. 1.1, 1.2, 2.1, 2.2 instead of 1, 2, 3, 4) -\numberwithin{figure}{section} % Number figures within sections (i.e. 1.1, 1.2, 2.1, 2.2 instead of 1, 2, 3, 4) -\numberwithin{table}{section} % Number tables within sections (i.e. 1.1, 1.2, 2.1, 2.2 instead of 1, 2, 3, 4) - -\setlength\parindent{0pt} % Removes all indentation from paragraphs - comment this line for an assignment with lots of text - -%---------------------------------------------------------------------------------------- -% TITLE SECTION -%---------------------------------------------------------------------------------------- -\newcommand{\horrule}[1]{\rule{\linewidth}{#1}} % Create horizontal rule command with 1 argument of height - -\title{ -\normalfont \normalsize -\textsc{University of California Irvine} \\ % Your university, school and/or department name(s) -\textsc{Prgramming Language Research Group} \\ [25pt] -\horrule{0.5pt} \\[0.4cm] % Thin top horizontal rule -\huge IoTCloud Version 2.0\\ % The assignment title -\horrule{2pt} \\[0.5cm] % Thick bottom horizontal rule -} - -\author{Authors} % Your name - - -\date{\normalsize\today} % Today's date or a custom date - -\begin{document} - -\maketitle % Print the title - - - - -%--------------------------------------------------------------------------------------- -% Custom Stuff -%--------------------------------------------------------------------------------------- -\newcommand{\tab}[1]{\hspace{.2\textwidth}\rlap{#1}} - - - - -\section{\textbf{Introduction}} - -\section{\textbf{Device Approach}} - -\subsection{\textbf{Records}} -Each record has the following information included in it: -\begin{itemize} - \item Machine ID of the device creating the record - \item The vector clock using the largest clock values from each device it knows and its own largest clock value incremented by 1. - \item Data payload - \item HMAC of the record. -\end{itemize} - -Records can be identified by the machine ID and the local machine clock, hereby referred to as the record ID. - -\subsubsection{\textbf{Types of Payloads}} -The different types of record payloads are: -\begin{itemize} - - \item Transactions - \begin{itemize} - \item Contains: - \begin{itemize} - \item Transaction ID - \item key-value pair gets (reads) - \item A guard condition (boolean condition) that can be evaluated on the key-value gets. - \item A set of key-value pairs that are to be updated if the guard condition is met. - \item Can only get and set key-value pairs that are from 1 arbitrator. Getting and/or setting key-value pairs from more than 1 arbitrator causes the transaction to be invalid and dead. - \end{itemize} - \end{itemize} - \item Commit notifications - \begin{itemize} - \item Contains the commit of a single transaction, the whole transaction. - \item There is 1 commit per transaction. - \item Generated by the arbitrator for the set of key-value gets and sets in the transaction. - \end{itemize} - \item Abort notifications - \begin{itemize} - \item Contains a transaction ID of an aborted transaction and the machine ID of the device that created that transaction. - \item Causes a transaction to be aborted, key-values not used in updates. - \end{itemize} - \item Data structure re-size notifications - \begin{itemize} - \item Contains new size of data structure (number of record allowed in the data structure or something like that). - \end{itemize} - \item Server sequence number confirmations. - \begin{itemize} - \item Contains a record ID and the server sequence number for that record that the server reported. - \item Created by any device if that device finds a record with a server sequence number that does not have a server sequence number conformation yet. - \end{itemize} - \item Delete notifications - \begin{itemize} - \item Contain the server sequence number of the record that was deleted. - \item Generated when a device deletes a record. - \end{itemize} - \item New Key notification - \begin{itemize} - \item Contains the name of a new key and the machine ID of the machine that is to arbitrate - \item Generated when a device generates a new (never used) key-value pair. - \end{itemize} -\end{itemize} - -\subsection{\textbf{Pulling the data structure}} -To pull the latest version of the data structure the following is done: -\begin{enumerate} - \item Make a pull request to the server and get all the records sent back. - \item Separate the records by machine ID. - \item For each machine ID, order the records based on that machine IDs clock within each of the records. - \item Check the data structure for any malicious activity (discussed below) -\end{enumerate} - -\subsection{\textbf{Updates}} -Updates take place as follows: -\begin{enumerate} - \item A device pulls the latest version of the data structure. If the device cannot pull the latest version because of network connectivity or some other issues then that device will just work using the local copy of the data structure it has. - \item Check the pulled data structure for any malicious activity (as stated in a section below) if not done already. - \item Check if any records in the current server need to be deleted (have delete notifications in data structure but the delete never took place), if so then delete them. - \item Check that the size of the data structure will not exceed the max size when the new record is inserted. If it does then prepare to delete records by inserting delete payloads in the new record (discussed below). - \item The device makes a record as follows: - \begin{enumerate} - \item Adds its machine ID. - \item Creates a vector clock using the largest clock values from each device it knows and its own largest clock value incremented by 1. - \item Fill the record payload section with the transactions and other types of payloads. - \item Fill the empty space of the record payload with server sequence number confirmations for records that have yet to have their server sequence numbers confirmed. - \item Fill the empty space of the record payload with rescued key-value pairs, transactions, ext (Discussed later). - \item Pad the record to be the same size for all records. - \item Calculate the HMAC of the record and add that to the record - \item Encrypt the record. - \end{enumerate} - \item Send the record to the server for insertion into the device's queue. - \item Issue any server commands such as deletes to the server. -\end{enumerate} - -If there is a connectivity issue then all the records will be held by the local device until connection is resumed then pushed to the server in the order which they occurred. Also the device can only delete records for which there is a server sequence number. At some point the device could run out of records to delete (it hasn't connected to the server in a while) in which case the device will not be able to delete any records. - -\subsection{\textbf{Deletions}} -When deciding which records to delete the following is to be done: -\begin{enumerate} - \item Order all the records in order based on their server sequence numbers - \item Calculate the difference between the current size of the data structure and the minimum size of the data structure (lets call this $m$). Note: count newly inserted records towards the total size of the data structure if doing deletes while doing updates. - \item Delete the oldest m records based on the ordering from step 1. - \begin{itemize} - \item If a record to be deleted has live data in it then the whole data structure needs to be re-sized. - \end{itemize} -\end{enumerate} - -Note this makes that size of the data structure be bounded: -If there are $n$ devices and the data structure has a minimum size of $m$. Then the max size of the data structure is given by $m + n -1$ for the case when all the devices make an update at the same time. - -\subsection{\textbf{Reading a key-value pair}} -When getting a key-value pair the following is done: -\begin{enumerate} - \item A device pulls the latest version of the data structure. If the device cannot pull the latest version because of network connectivity or some other issues then that device will just work using the local copy of the data structure it has. - \item Check the pulled data structure for any malicious activity (as stated in a section below) if not done already. - \item Find the transaction with the largest server sequence number that contains the key-value pair of interest (this is the latest value). -\end{enumerate} - -\subsection{\textbf{Rescuing Transactions, Commits, Aborts, Ext}} -Data should be proactively rescued from the "oldest" records currently in the data structure. Unused space in new records should be used to rescue data from old records so that when it comes time to delete the old records, there are no live pieces of data that need to be rescued. When a piece of data is rescued, it is rescued with its vector clock as well (so that the time of that data can be saved).\\ - -When rescuing transactions and commits: only keep the key-value pair sets that do not have a newer key-value pair set (no other transaction/commits sets that key-value pair later in the future). This means that transactions/commits can shrink in size.\\ - -When rescuing Key Value notifications: save the vector clock and the server sequence number of the notification in the rescued data. - -When deciding which data to rescue the following is to be done: -\begin{enumerate} - \item Order all the records in order based on their server sequence numbers - \item Create an ordered list of currently live transactions, commits, aborts, ext from the oldest $n$ records from step one where the order is based on the age of the data (how old the record is). - \item Randomly select from the list of live transactions, commits, aborts, ext to save. Save as much as can fit in the current new record. The random selection could give higher probability to transactions, commits, aborts, ext from records that are to be deleted sooner. -\end{enumerate} - -\subsection{\textbf{Checking the Data Structure}} -Checking the data structure for consistency is done as follows: -\begin{enumerate} - \item Verify that each record in the data structure has an HMAC that matches the data in the record. - \item Verify that the oldest record the server sent has a server sequence number that is equal to or less than the server sequence number in the most recent delete notification (currently live delete notification) + 1. - \item Make sure that for each device queue the difference between the vector clock value of the device queues clock is at most 1 between 2 consecutive messages for all records with server sequence numbers above the last deleted records server sequence numbers. - \item Verify that no currently live data Structure re-size notification is smaller than the last known data structure size. Data structure can only grow in size. - \item Verify that all the server sequence numbers for the records that are currently present have unique numbers. - \item Verify that all the server sequence numbers for the records have a difference of 1 (no gaps) for all records with server sequence numbers above the last deleted records server sequence numbers. - \item Verify record server sequence numbers against the stated server sequence numbers in the server sequence number notification payloads (make sure the server is not changing the sequence number on the fly). -\end{enumerate} - -\subsection{\textbf{The Arbitrator}} -The arbitrator can: -\begin{enumerate} - \item Send Commits - \item Send Aborts -\end{enumerate} - -\subsubsection{\textbf{Commits}} -Commits have the following properties -\begin{itemize} - \item Agree with the ordering of the server sequence numbers most of the time. - \item Cannot commit an already aborted transaction. - \item Commits state the ordering of key-value pairs. - \item Can disagree with the ordering of server sequence numbers if arbitrator decides to do so. - \item Should occur frequently as to make sure that the commit order matches the server sequence ordering as closely as possible (prevent large divergence of the 2 orderings) -\end{itemize} - -\subsubsection{\textbf{Aborts}} - -\begin{itemize} - \item Aborts are used to show which transactions have been aborted based on the arbitrators decision. - \item Aborts are considered live until an abort acknowledgement is presented. -\end{itemize} - -\subsection{\textbf{Setting Up New Keys (Choosing the Arbitrator)}} -Setting up new keys is done as follows: -\begin{enumerate} - \item Device wishes to generate new key - \item Device inserts a New Key notification into the data structure. -\end{enumerate} -In the case where multiple devices are creating the same key, the key with the smallest vector clock is the only valid one. In the case of a concurrent vector clock, the smallest server sequence number notification is the valid one. - -\subsection{\textbf{Live Status}} -Live Status of entries: -\begin{enumerate} - - \item Delete notifications - \begin{itemize} - \item Live if it deleted the largest known server sequence number to be deleted (most recent delete). - \end{itemize} - - \item Commit notifications - \begin{itemize} - \item Live until all the key-value pair sets in the transaction commit are dead. - \begin{itemize} - \item key-value pairs are dead when a commit for a transaction that sets the same key-value pair occurs with a larger vector clock. - \end{itemize} - \end{itemize} - - \item Abort notifications - \begin{itemize} - \item Live until the device whos machine ID is in the abort notification makes an update to the data structure that contains a vector clock that is more in the future than the vector clock for this abort notification. - \end{itemize} - - \item Data structure re-size notifications - \begin{itemize} - \item Live if it contains the largest target size of the data structure. - \end{itemize} - - \item Server sequence number confirmations. - \begin{itemize} - \item Live until the record that this notification is reporting on is deleted. - \end{itemize} - - \item Transactions - \begin{itemize} - \item Is dead if it is invalid (contains keys-values for multiple arbitrators) - \item Live until a commit or abort notification for this transaction is generated. - \end{itemize} - - \item New Key notification - \begin{itemize} - \item Is dead if there exists a New Key notification that has a server sequence number that is smaller and the same key name. - \end{itemize} - -\end{enumerate} - -\section{\textbf{Server Approach}} - -The servers view of the system is in terms of data slots where each data slot holds a single record, has a monotonically increasing number associated with it (server sequence number) for the record that currently is present in that data slot and can be set or deleted. A server may have a finite amount of memory which it can partition into slots, reusing memory that newly deleted slots used to occupy. - -There are 3 types of requests from a device that the server must respond to: -\begin{enumerate} - \item Pull all current slots. - \item Put a new record in a slot. - \item Delete a slot. -\end{enumerate} - -\subsection{\textbf{Pull all current slots}} -In this case the server will simply send back all active slots (slots that have data) in any order along with each slots server sequence number. It is the job of the devices to order the slots. - -\subsection{\textbf{Put a new record in a slot}} -In this case the server will: -\begin{enumerate} - \item Receive a record data from a device. - \item Put this record data in an empty slot. - \item Assign the just received record the next number in the server sequence numbers. -\end{enumerate} -If more than 1 put request is made at the same time, the server is free to order the requests however it wishes. - -\subsection{\textbf{Delete a slot}} -In this case the server will delete the data in the slot that has the server sequence number that matches the server sequence number in the delete request. The server could delay the delete if it wishes (if it has plenty of space for new slots). - -\section{\textbf{Data Structure Abstraction}} -This section outlines the data structure abstraction that is provided to the IoT application. It is similar to a hash table key-value store. - -Operations on the key-value store: -\begin{itemize} - \item Put operation - \item Get operation - \item Check put status - \item Create New Key Operation. -\end{itemize} - -\subsection{\textbf{Put Operation}} -This operation is described as follows: -\begin{itemize} - \item Has the form: put(Key-value-list, guard) - \item Updates the key-value pairs listed in the key-value list. - \item Has a boolean guard that is passed in that is able to read from keys that are associated with the same arbitrator as the keys being updated - \item Returns an ID for this put (Transaction ID) or an error code if put is formatted incorrectly. - \item Underlying action: Creates a transaction, creates a record and inserts that record in the data structure (doing deletes and other house keeping operations as needed). -\end{itemize} - -\subsection{\textbf{Get Operation}} -\begin{itemize} - \item Has the form: get(key-name) - \item Gets the current value of a key, also returns a machine ID for the arbitrator of that key. - \item Underlying action: Does a pull from the server and resolves the latest value for the specified key (as mentioned above). Also does house keeping work like key rescue and sequence number notification as needed. -\end{itemize} - -\subsection{\textbf{Check put status}} -\begin{itemize} - \item Has the form of a callback. - \item Notifies the application of an aborted transaction. - \item Underlying action: when an abort notification is received then the callback is called. This is checked whenever this application makes changes to the data structure. -\end{itemize} - -\subsection{\textbf{Create New Key Operation}} -\begin{itemize} - \item Has the form: createKey(key-name, machine-id) - \item Creates a new key with an arbitrator at a specific machine ID - \item Underlying action: Creates a new key notification, creates a record and inserts that record in the data structure (doing deletes and other house keeping operations as needed). -\end{itemize} - - - -\section{\textbf{System Guarantees}} -\begin{itemize} - \item Server cannot view data inside records - \item Server cannot forge or modify or create any records - \item Server cannot withhold any records - \item Server cannot reorder records that could not have been ordered differently due to network latency - \item Server cannot delete records unless told to do so. - \item There will always be an obvious key-value pair that is the latest key value pair. - \item The data structure is bounded in size such that $m$ is the minimum size of the data structure, $n$ is the number of devices in the system and $s$ is the current size of the data structure: $m \leq s \leq (m+n-1)$ - \item Data structure can only grow when there are too may key-value pairs (and aborts) than what fit in the current data structure size within reason. - \item No currently valid data can be lost by the system and go undetected. - \item Devices can operate offline and re-sync with the system and get a consistent view of the system - \item If the server tries to hold a device on an older version of the data structure, that device can eventually rejoin the main data structure without problems. - \item Devices that have a transaction aborted will be able to be notified about the abort indefinitely (no time frame when notification must be accepted). - \item Server cannot hold a device on an old version of the data structure and then move them to a newer version of the data structure without being detected (The server sequence numbers would reveal conflicts or gaps or both). - -\end{itemize} - -\section{\textbf{System Correctness}} -The measures of correctness for the system are divided by context and the different system operations as follows: -\begin{itemize} - \item Data Integrity and Authentication - \item Ordering of Records - \item Data Structure Functions -\end{itemize} - -\subsection{\textbf{Data Integrity and Authentication}} -The correctness of the cryptographic aspects of the data structure can be assumed provided that each record is encrypted with one of the client's key and the HMAC of each record does not indicate the data was tampered with. See section 2.7 for more details on how the data structure is verified. - -\subsection{\textbf{Ordering of Records}} -The ordering of the records within the data structure is said to be correct if the total ordering derived from the records by the server sequence numbers does not conflict with the partial ordering derived from the vector clock. - -\subsection{\textbf{Data Structure Functions}} -\subsubsection{\textbf{Put}} -\begin{itemize} - \item From the client side the put operation is said to be correct if the function returns a valid transaction ID for a successful operation or an error code for an unsuccessful operation. - \item From the server side the put operation is correct if the key-value pair changes only when the guard condition evaluates to true. The server should reply with either a transaction ID or and error code depending on the guard condition??? -\end{itemize} - -\subsubsection{\textbf{Get}} -\begin{itemize} - \item For the client the get operation is correct if it returns the value and arbitrator machine ID that corresponds with the input key. Or and error message if no key-value pair exists with that key??? In addition, if any housekeeping work is involved, the get operation must only rescue transactions with a live status. See section 2.10 for details on Live Status. - \item For the server a get operation is correct if the server returns a correctly ordered and untampered version of the data structure when the initial pull is done. -\end{itemize} - -\subsubsection{\textbf{Create New Key}} -\begin{itemize} - \item The client correctly created a new key if it inserts a properly formatted new key notification into the data structure with a valid arbitrator machine ID. - \item The server is said to have correctly added a new key if a new key-value pair with the indicated arbitrator machine ID is inserted into the data structure. Or if it returns an error message for an invalid arbitrator machine ID??? What about collisions??? -\end{itemize} - - -\end{document} \ No newline at end of file diff --git a/version2/doc/iotcloud_informal/makefile b/version2/doc/iotcloud_informal/makefile deleted file mode 100644 index cff4a15..0000000 --- a/version2/doc/iotcloud_informal/makefile +++ /dev/null @@ -1,8 +0,0 @@ -LATEX := pdflatex -halt-on-error - -default: - $(LATEX) iotcloud.tex - -clean: - rm -f *.dvi *.log *.aux *.blg *.bbl *~ - rm -f iotcloud.ps iotcloud.pdf