1 \documentclass[11pt]{article}
\r
2 \newcommand{\tuple}[1]{\ensuremath \langle #1 \rangle}
\r
6 \usepackage{graphicx}
\r
7 \usepackage{mathrsfs}
\r
9 \usepackage{algpseudocode}% http://ctan.org/pkg/algorithmicx
\r
10 \usepackage[all]{xy}
\r
11 \usepackage{varwidth}
\r
13 \newtheorem{theorem}{Theorem}
\r
14 \newtheorem{prop}{Proposition}
\r
15 \newtheorem{lem}{Lemma}
\r
16 \newtheorem{defn}{Definition}
\r
17 \newcommand{\note}[1]{{\color{red} \bf [[#1]]}}
\r
18 \newcommand{\push}[1][1]{\hskip\dimexpr #1\algorithmicindent\relax}
\r
19 \newcommand*\xor{\mathbin{\oplus}}
\r
23 \setlength\parindent{0pt} % Removes all indentation from paragraphs - comment this line for an assignment with lots of text
\r
26 \section{\textbf{Introduction}}
\r
34 \section{\textbf{Server}}
\r
35 The server maintains a collection of slots such that each slot contains some data.
\r
36 The operations on the slot are as follows:
\r
43 \subsection{\textbf{Server Notation Conventions}}
\r
44 $s \in SN$ is a server sequence number\\
\r
45 $sv \in SV$ is a slot's value\\
\r
46 $slot_s = \tuple{s, sv} \in SL \subseteq SN \times SV$
\r
48 \subsection{\textbf{Server State}}
\r
49 \textit{n = current server sequence number}\\
\r
50 \textit{SL = set of live slots on the server}\\
\r
52 \textbf{Initial Server State}\\
\r
56 \subsection{\textbf{Put Slot}}
\r
57 Put slot is an operation that inserts data into a new slot at the server.\\
\r
61 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}
\r
62 \textbf{Put Function:}
\r
63 \begin{algorithmic}[1]
\r
64 \Function{PutSlotServer}{$sv_p$}
\r
65 \State $s_p \gets n$
\r
66 \State $n \gets n + 1$
\r
67 \State $SL \gets SL \cup \{\tuple{s_p,sv_p}\}$
\r
73 \subsection{\textbf{Get Slot}}
\r
74 Get slot is an operation that returns all server slots that are greater than some server sequence number.\\
\r
78 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}
\r
79 \textbf{Get Function:}
\r
80 \begin{algorithmic}[1]
\r
81 \Function{GetSlotServer}{$s_g$}
\r
82 \State \Return{$\{\tuple{s, sv} \in SL \mid s \geq s_g\}$}
\r
88 \subsection{\textbf{Delete Slot}}
\r
89 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
93 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}
\r
94 \textbf{Delete Function:}
\r
95 \begin{algorithmic}[1]
\r
96 \Function{DeleteSlotServer}{$s_d$}
\r
97 \State $SD \gets \{\tuple{s, sv} \in SL \mid s \leq s_g\}$
\r
98 \State $SL \gets SL - SD$
\r
111 \section{\textbf{Client}}
\r
112 The data structure acts as a key store where key-value pairs can be read and set.
\r
113 The data structure exposes the following functions:
\r
115 \item Put Transaction
\r
116 \item Get key-value pair
\r
117 \item Create new key
\r
120 \subsection{\textbf{Client Notation Conventions}}
\r
122 $K$ is the set of all keys.\\
\r
123 $MID$ is the set of the machine IDs of the devices that are in the system.
\r
124 $K_{mid}$ is a set of all keys that have device mid as the arbitrator\\
\r
125 $ssn_s$ is the server sequence number of a record $s$\\
\r
126 $mid_s \in MID$ is the machine ID for the device that created $record_s$.\\
\r
127 $hmac_s$ is the HMAC of $record_s$\\
\r
128 $c_{mid}$ is the latest read clock for a device with machine ID $mid$\\
\r
129 $vc_s = \{c_{mid} | mid \in MID\}$\\
\r
130 $rid_s = \tuple{mid_s, c_{mid_s}}$
\r
131 $k$ is a key entry\\
\r
132 $v$ is a value entry\\
\r
133 $kv_n$ is a key-value entry $\tuple{k_n,v_n} , k \in K$\\
\r
135 $tid_s = \tuple{mid_s,c_{mid_s}}$\\
\r
136 $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
137 $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
138 $commit_s = \tuple{tid_s,vc_s}$\\
\r
139 $abort_s = \tuple{tid_s,mid_s,vc_s}$\\
\r
140 $sequence_s = \tuple{rid_s, ssn_s}$\\
\r
141 $delete_s = \tuple{ssn_d}$\\
\r
142 $resize_s = \tuple{x | x \in \mathbb{N}}$\\
\r
143 $newkey_s = \tuple{k_s, vc_s, ssn_s$ or $-1, mid_s}$\\
\r
145 $payload_s = \{x_1, x_2,..., x_k | \forall k, x_k \in \{$transaction, commit, abort, resize, newkey, sequence, delete$\}\}$\\
\r
146 $rd_s = \tuple{mid_s, vc_s, hmac_s, payload_s}$ \\
\r
147 $record_s = \tuple{ssn_s,rd_s}$\\
\r
149 \subsection{\textbf{Client State}}
\r
150 \textit{s = largest server sequence number pulled from the server by a device} \\
\r
151 \textit{R = set of records pulled from the server so far with their server sequence numbers} \\
\r
152 \textit{RL = set of records that contain live data} \\
\r
154 \subsection{Helper Functions}
\r
155 The following helper functions are needed:\\
\r
157 %Get Payload Items from Record with SSN
\r
159 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}
\r
160 \textbf{Get Payload Items from Record with SSN}:
\r
161 \begin{algorithmic}[1]
\r
162 \Function{GetPayloadItemsWithSSN}{$record_s$}
\r
163 \State $PISSN \gets \emptyset$ \Comment{Set of Payload Items with ssn}
\r
164 \State $\tuple{ssn_s, rd_s} \gets record_s$
\r
165 \State $\tuple{mid_s, vc_s, hmac_s, payload_s} \gets rd_s$\\
\r
167 \ForAll{$payloadItems$ in $payload_s$}
\r
168 \State $PISSN \gets PISSN \cup \tuple{payloadItem, ssn_s}$
\r
171 \State \Return {$PISSN$}
\r
177 %Get rid For Record
\r
179 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}
\r
180 \textbf{Get rid For Record}:
\r
181 \begin{algorithmic}[1]
\r
182 \Function{GetRid}{$record_s$}
\r
183 \State $\tuple{ssn_s, \tuple{mid_s, \{c_{mid_1}, c_{mid_2}, ... , c_{mid_k}\}, hmac_s, payload_s}} \gets record_s$
\r
184 \State \Return {$\tuple{mid_s, c_{mid_s}}$}
\r
191 \textbf{Get Transaction Arbitrator}:\\
\r
192 \textbf{Transaction Live}:\\
\r
193 \textbf{Commit Live}:\\
\r
197 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}
\r
198 \textbf{Sequence Live}:
\r
199 \begin{algorithmic}[1]
\r
200 \Function{SequenceLive}{$sequence_s, ssn_{s1}$}
\r
201 \State $API \gets \emptyset$ \Comment{Set of all Payload Items}
\r
202 \State $AS \gets \emptyset$ \Comment{Set of all Payload Items that are sequences}
\r
203 \State $StillHasRecord \gets False$
\r
204 \State $\tuple{rid_s, ssn_{s2}} \gets sequence_s$\\
\r
206 \ForAll{$record$ in $R$}
\r
207 \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}
\r
208 \If{$rid_s = $\Call{GetRid}{$record$}}
\r
209 \State $StillHasRecord \gets True$
\r
213 \If{$\lnot StillHasRecord$} \Comment{The Record does not exists anymore}
\r
214 \State \Return{False}
\r
217 \ForAll{$\tuple{ssn, payload}$ in $API$}
\r
218 \If{$payload$ is a $sequence$}
\r
219 \State $AS \gets AS \cup \{\tuple{ssn, payload}\}$ \Comment{Extract all sequence payloads}
\r
223 \ForAll{$\tuple{ssn_1', \tuple{rid', ssn_2'}}$ in $AS$}
\r
224 \If{$(rid'=rid_s) \land (ssn_1' > ssn_{s_1})$}
\r
225 \State \Return{False}
\r
228 \State \Return{True}
\r
236 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}
\r
237 \textbf{Delete Live}:
\r
238 \begin{algorithmic}[1]
\r
239 \Function{DeleteLive}{$delete_s, ssn_s$}
\r
240 \State $API \gets \emptyset$ \Comment{Set of all Payload Items}
\r
241 \State $AD \gets \emptyset$ \Comment{Set of all Payload Items that are deletes}
\r
242 \State $\tuple{ssn_d} \gets delete_s$\\
\r
244 \ForAll{record in R}
\r
245 \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}
\r
248 \ForAll{$\tuple{ssn, payload}$ in $API$}
\r
249 \If{$payload$ is a $delete$}
\r
250 \State $AD \gets AD \cup \{\tuple{ssn, payload}\}$ \Comment{Extract all delete payloads}
\r
254 \ForAll{delete in AD}
\r
255 \State $\tuple{{ssn_s}', \tuple{{ssn_d}'}} \gets delete$
\r
256 \If{${ssn_d}' > ssn_d$} \Comment{More recently deleted record}
\r
257 \State \Return{False}
\r
258 \ElsIf{$({ssn_d}'= ssn_d) \land ({ssn_s}' > ssn_s)$} \Comment{More recent delete of same record}
\r
259 \State \Return{False}
\r
262 \State \Return{True}
\r
270 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}
\r
271 \textbf{Abort Live}:
\r
272 \begin{algorithmic}[1]
\r
273 \Function{AbortLive}{$abort_s$}
\r
274 \State $\tuple{tid_s,mid_s,vc_s} \gets abort_s$\\
\r
275 \ForAll{record in R}
\r
276 \State $\tuple{ssn_s',\tuple{mid_s', vc_s', hmac_s', payload_s'}} \gets record$
\r
277 \If{$(mid_s'=mid_s) \land (vc_s' > vc_s)$}
\r
278 \State \Return{True}
\r
281 \State \Return{False}
\r
289 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}
\r
290 \textbf{Resize Live}:
\r
291 \begin{algorithmic}[1]
\r
292 \Function{ResizeLive}{$resize_s, ssn_s$}
\r
293 \State $API \gets \emptyset$ \Comment{Set of all Payload Items}
\r
294 \State $AR \gets \emptyset$ \Comment{Set of all Payload Items that are resize}
\r
295 \State $\tuple{size} \gets resize_s$\\
\r
297 \ForAll{record in R}
\r
298 \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}
\r
301 \ForAll{$\tuple{ssn, payload}$ in $API$}
\r
302 \If{$payload$ is a $resize$}
\r
303 \State $AR \gets AR \cup \{\tuple{ssn, payload}\}$ \Comment{Extract all resize payloads}
\r
307 \ForAll{$\tuple{ssn', \tuple{size'}}$ in $AR$}
\r
308 \If{$size' > size$}
\r
309 \State \Return{False}
\r
310 \ElsIf{$(size'=size) \land (ssn' > ssn_s)$}
\r
311 \State \Return{False}
\r
314 \State \Return{True}
\r
322 \textbf{Evaluate Guard Condition:}\\
\r
325 \textbf{Get Latest Data Structure From Server:}\\
\r
326 \textbf{Delete Records:}\\
\r
327 \textbf{Check Data Structure for Malicious Activity:}
\r
330 \subsection{\textbf{Put Transaction}}
\r
334 \subsection{\textbf{Get key-value pair}}
\r
335 \subsection{\textbf{Create new key}}
\r