version2/doc/iotcloud_formal/iotcloud.tex

   1 \documentclass[11pt]{article}\r
   2 \newcommand{\tuple}[1]{\ensuremath \langle #1 \rangle}\r
   3 \usepackage{color}\r
   4 \usepackage{amsthm}\r
   5 \usepackage{amsmath}\r
   6 \usepackage{graphicx}\r
   7 \usepackage{mathrsfs}\r
   8 \usepackage{amssymb}\r
   9 \usepackage{algpseudocode}% http://ctan.org/pkg/algorithmicx\r
  10 \usepackage[all]{xy}\r
  11 \usepackage{varwidth}\r
  12 \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
  20 \begin{document}\r
  21 \r
  22 \r
  23 \setlength\parindent{0pt} % Removes all indentation from paragraphs - comment this line for an assignment with lots of text\r
  24 \r
  25 \r
  26 \section{\textbf{Introduction}}\r
  27 \r
  28 \r
  29 \r
  30 \r
  31 \r
  32 \section{\textbf{Server}}\r
  33 The server maintains a collection of slots such that each slot contains some data.\r
  34 The operations on the slot are as follows:\r
  35 \begin{itemize}\r
  36     \item Put slot\r
  37     \item Get slot\r
  38     \item Delete Slot\r
  39 \end{itemize}\r
  40 \r
  41 \subsection{\textbf{Server Notation Conventions}}\r
  42 $s \in SN$ is a server sequence number\\\r
  43 $sv \in SV$ is a slot's value\\\r
  44 $slot_s = \tuple{s, sv} \in SL \subseteq SN \times SV$\r
  45 \r
  46 \subsection{\textbf{Server State}}\r
  47 \textit{n = current server sequence number}\\\r
  48 \textit{SL = set of live slots on the server}\\\r
  49 \r
  50 \textbf{Initial Server State}\\\r
  51 $SL = \emptyset$\\\r
  52 $n = 0$\r
  53 \r
  54 \subsection{\textbf{Put Slot}}\r
  55 Put slot is an operation that inserts data into a new slot at the server.\\\r
  56 \r
  57 %Put Function\r
  58 \noindent\fbox{%\r
  59 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
  60 \textbf{Put Function:}\r
  61 \begin{algorithmic}[1]\r
  62 \Function{PutSlotServer}{$sv_p$}\r
  63     \State $s_p \gets n$\r
  64     \State $n \gets n + 1$\r
  65     \State $SL \gets SL \cup \{\tuple{s_p,sv_p}\}$\r
  66 \EndFunction\r
  67 \end{algorithmic}\r
  68 \end{varwidth}% \r
  69 }\r
  70 \r
  71 \subsection{\textbf{Get Slot}}\r
  72 Get slot is an operation that returns all server slots that are greater than some server sequence number.\\\r
  73 \r
  74 % Get Function\r
  75 \noindent\fbox{%\r
  76 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
  77 \textbf{Get Function:}\r
  78 \begin{algorithmic}[1]\r
  79 \Function{GetSlotServer}{$s_g$}\r
  80     \State \Return{$\{\tuple{s, sv} \in SL \mid s \geq s_g\}$}\r
  81 \EndFunction\r
  82 \end{algorithmic}\r
  83 \end{varwidth}% \r
  84 }\r
  85 \r
  86 \subsection{\textbf{Delete Slot}}\r
  87 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
  88 \r
  89 %Delete Function\r
  90 \noindent\fbox{%\r
  91 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
  92 \textbf{Delete Function:}\r
  93 \begin{algorithmic}[1]\r
  94 \Function{DeleteSlotServer}{$s_d$}\r
  95     \State $SD \gets \{\tuple{s, sv} \in SL \mid s \leq s_g\}$\r
  96     \State $SL \gets SL - SD$\r
  97 \EndFunction\r
  98 \end{algorithmic}\r
  99 \end{varwidth}% \r
 100 }\r
 101 \r
 102 \r
 103 \r
 104 \r
 105 \section{\textbf{Client}}\r
 106 The data structure acts as a key store where key-value pairs can be read and set.\r
 107 The data structure exposes the following functions:\r
 108 \begin{itemize}\r
 109     \item Put Transaction\r
 110     \item Get key-value pair\r
 111     \item Create new key\r
 112 \end{itemize}\r
 113 \r
 114 \subsection{\textbf{Client Notation Conventions}}\r
 115 \r
 116 $K$ is the set of all keys.\\\r
 117 $MID$ is the set of the machine IDs of the devices that are in the system.\r
 118 $K_{mid}$ is a set of all keys that have device mid as the arbitrator\\\r
 119 $ssn_s$ is the server sequence number of a record $s$\\\r
 120 $mid_s \in MID$ is the machine ID for the device that created $record_s$.\\\r
 121 $hmac_s$ is the HMAC of $record_s$\\\r
 122 $c_{mid}$ is the latest read clock for a device with machine ID $mid$\\\r
 123 $vc_s = \{c_{mid} | mid \in MID\}$\\\r
 124 $rid_s = \tuple{mid_s, c_{mid_s}}$\r
 125 $k$ is a key entry\\\r
 126 $v$ is a value entry\\\r
 127 $kv_n$ is a key-value entry $\tuple{k_n,v_n} , k \in K$\\\r
 128 \r
 129 $tid_s = \tuple{mid_s,c_{mid_s}}$\\\r
 130 $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
 131 $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}$\\\r
 132 $commit_s = \tuple{tid_s,vc_s}$\\\r
 133 $abort_s = \tuple{tid_s,mid_s,vc_s}$\\\r
 134 $sequence_s = \tuple{rid_s, ssn_s}$\\\r
 135 $delete_s = \tuple{ssn_d}$\\\r
 136 $resize_s = \tuple{x | x \in \mathbb{N}}$\\\r
 137 $newkey_s = \tuple{k_s, vc_s, ssn_s$ or $NULL, mid_s}$\\\r
 138 \r
 139 $payload_s = \{x_1, x_2,..., x_k | \forall k, x_k \in \{$transaction, commit, abort, resize, newkey, sequence, delete$\}\}$\\\r
 140 $rd_s = \tuple{mid_s, vc_s, hmac_s, payload_s}$ \\\r
 141 $record_s = \tuple{ssn_s,rd_s}$\\\r
 142 \r
 143 \subsection{\textbf{Client State}}\r
 144 \textit{s = largest server sequence number pulled from the server by a device} \\\r
 145 \textit{R = set of records pulled from the server so far with their server sequence numbers} \\\r
 146 \textit{RL = set of records that contain live data} \\\r
 147 \r
 148 \subsection{Helper Functions}\r
 149 The following helper functions are needed:\\\r
 150 \r
 151 \r
 152 % Error\r
 153 \noindent\fbox{%\r
 154 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 155 \textbf{ Error:}\r
 156 \begin{algorithmic}[1]\r
 157 \Function{Error}{$msg$}\r
 158     \State $Print(msg)$\r
 159     \State $Halt()$\r
 160 \EndFunction\r
 161 \end{algorithmic}\r
 162 \end{varwidth}% \r
 163 }\r
 164 \r
 165 %Get Payload Items from Record with SSN\r
 166 \noindent\fbox{%\r
 167 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 168 \textbf{Get Payload Items from Record with SSN}:\r
 169 \begin{algorithmic}[1]\r
 170 \Function{GetPayloadItemsWithSSN}{$record_s$}\r
 171     \State $PISSN \gets \emptyset$ \Comment{Set of Payload Items with ssn}\r
 172     \State $\tuple{ssn_s, rd_s} \gets record_s$\r
 173     \State $\tuple{mid_s, vc_s, hmac_s, payload_s} \gets rd_s$\\\r
 174     \r
 175     \ForAll{$payloadItems$ in $payload_s$}\r
 176         \State $PISSN \gets PISSN \cup \{\tuple{payloadItem, ssn_s}\}$\r
 177     \EndFor\\\r
 178     \r
 179     \State \Return {$PISSN$}\r
 180 \EndFunction\r
 181 \end{algorithmic}\r
 182 \end{varwidth}% \r
 183 }\r
 184 \r
 185 %Get rid of record\r
 186 \noindent\fbox{%\r
 187 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 188 \textbf{Get rid of record:}\r
 189 \begin{algorithmic}[1]\r
 190 \Function{GetRid}{$record_s$}\r
 191     \State $\tuple{ssn_s, \tuple{mid_s, \{c_{mid_1}, c_{mid_2}, ... , c_{mid_k}\}, hmac_s, payload_s}} \gets record_s$\r
 192     \State \Return {$\tuple{mid_s, c_{mid_s}}$}\r
 193 \EndFunction\r
 194 \end{algorithmic}\r
 195 \end{varwidth}% \r
 196 }\r
 197 \r
 198 %Get tid of transaction\r
 199 \noindent\fbox{%\r
 200 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 201 \textbf{Get tid of transaction:}\r
 202 \begin{algorithmic}[1]\r
 203 \Function{GetTid}{$transaction_s$}\r
 204     \State $\tuple{ssn_s,\{c_{mid_1}, c_{mid_2}, ... , c_{mid_k}\}, \{kv_1, kv_2,...kv_n\}, guard_s} \gets record_s$\r
 205     \State \Return {$\tuple{mid_s, c_{mid_s}}$}\r
 206 \EndFunction\r
 207 \end{algorithmic}\r
 208 \end{varwidth}% \r
 209 }\r
 210 \r
 211 %Key Value Live\r
 212 %\noindent\fbox{%\r
 213 %\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 214 \textbf{Key Value Live:}\r
 215 \begin{algorithmic}[1]\r
 216 \Function{KeyValueLive}{$keyName_s, transaction_s$}\r
 217     \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\r
 218     \State $AT \gets \emptyset$    \Comment{Set of all Payload Items that are transactions}\r
 219     \State $AC \gets \emptyset$    \Comment{Set of all Payload Items that are commits}\r
 220     \State $AA \gets \emptyset$    \Comment{Set of all Payload Items that are aborts}\r
 221     \State $commitTrans = NULL$\r
 222     \State $tid \gets $ \Call{GetTid}{$transaction_s$}\\\r
 223 \r
 224     \ForAll{$record$ in $R$}\r
 225         \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}\r
 226     \EndFor\\\r
 227     \r
 228     \ForAll{$\tuple{ssn, payload}$ in $API$}\r
 229         \If{$payload$ is a $transaction$}\r
 230             \State $AT \gets AT \cup \{payload\}$\r
 231         \ElsIf{$payload$ is a $commit$}\r
 232             \State $AC \gets AC \cup \{payload\}$\r
 233         \ElsIf{$payload$ is a $abort$}\r
 234             \State $AA \gets AA \cup \{payload\}$\r
 235         \EndIf\r
 236     \EndFor\\\r
 237     \r
 238     \ForAll{$\tuple{tid',mid',vc'}$ in $AA$} \Comment{Has an abort}\r
 239         \If{$tid' = tid$}\r
 240             \State \Return{False}\r
 241         \EndIf\r
 242     \EndFor\\\r
 243 \r
 244     \ForAll{$\tuple{tid',vc'}$ in $AC$} \Comment{Has a commit}\r
 245         \If{$tid' = tid$}\r
 246             \State $commitTrans \gets \tuple{tid',vc'}$\r
 247             \State Break\r
 248         \EndIf\r
 249     \EndFor\\\r
 250     \r
 251     \If{$commitTrans = NULL$}   \r
 252         \State \Return{True} \Comment{If transaction not yet committed then alive}\r
 253     \EndIf\\\r
 254     \r
 255     \State $\tuple{tid_c, vc_c} \gets commitTrans$\r
 256     \ForAll{$trans$ in $AT$}\r
 257         \State $\{mid_t,vc_t ,\{\tuple{k_1, v_1}, \tuple{k_2, v_2},..., \tuple{k_k, v_k}\},guard_t\} \gets trans$\r
 258         \If{$(trans \neq transaction_s) \land (keyName_s = k_n)$}\r
 259             \ForAll{$\tuple{tid_c',vc_c'}$ in $AC$}\r
 260                 \If{$(tid_c = $ \Call{GetTid}{$trans$} $) \land (vc_c' > vc_c)$}\r
 261                     \State \Return{False}\r
 262                 \EndIf\r
 263             \EndFor\r
 264         \EndIf\r
 265     \EndFor\\\r
 266     \r
 267     \State \Return{True}\r
 268     \r
 269 \EndFunction\r
 270 \end{algorithmic}\r
 271 %\end{varwidth}% \r
 272 %}\r
 273 \r
 274 %Sequence Live\r
 275 \noindent\fbox{%\r
 276 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 277 \textbf{Sequence Live}:\r
 278 \begin{algorithmic}[1]\r
 279 \Function{SequenceLive}{$sequence_s, ssn_{s1}$}\r
 280     \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\r
 281     \State $AS \gets \emptyset$    \Comment{Set of all Payload Items that are sequences}\r
 282     \State $StillHasRecord \gets False$\r
 283     \State $\tuple{rid_s, ssn_{s2}} \gets sequence_s$\\\r
 284     \r
 285     \ForAll{$record$ in $R$}\r
 286         \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}\r
 287         \If{$rid_s = $\Call{GetRid}{$record$}}\r
 288             \State $StillHasRecord \gets True$\r
 289         \EndIf\r
 290     \EndFor\\\r
 291     \r
 292     \If{$\lnot StillHasRecord$}  \Comment{The Record does not exists anymore}\r
 293         \State \Return{False}\r
 294     \EndIf\\\r
 295     \r
 296     \ForAll{$\tuple{ssn, payload}$ in $API$}\r
 297         \If{$payload$ is a $sequence$}\r
 298             \State $AS \gets AS \cup \{\tuple{ssn, payload}\}$   \Comment{Extract all sequence payloads}\r
 299         \EndIf\r
 300     \EndFor\\\r
 301     \r
 302     \ForAll{$\tuple{ssn_1', \tuple{rid', ssn_2'}}$ in $AS$}\r
 303         \If{$(rid'=rid_s) \land (ssn_1' > ssn_{s_1})$}\r
 304             \State \Return{False}\r
 305         \EndIf\r
 306     \EndFor \\\r
 307     \State \Return{True}\r
 308 \EndFunction\r
 309 \end{algorithmic}\r
 310 \end{varwidth}% \r
 311 }\r
 312 \r
 313 % Delete Live\r
 314 \noindent\fbox{%\r
 315 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 316 \textbf{Delete Live}:\r
 317 \begin{algorithmic}[1]\r
 318 \Function{DeleteLive}{$delete_s, ssn_s$}\r
 319     \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\r
 320     \State $AD \gets \emptyset$    \Comment{Set of all Payload Items that are deletes}\r
 321     \State $\tuple{ssn_d} \gets delete_s$\\\r
 322     \r
 323     \ForAll{record in R}\r
 324         \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}\r
 325     \EndFor\\\r
 326     \r
 327     \ForAll{$\tuple{ssn, payload}$ in $API$}\r
 328         \If{$payload$ is a $delete$}\r
 329             \State $AD \gets AD \cup \{\tuple{ssn, payload}\}$   \Comment{Extract all delete payloads}\r
 330         \EndIf\r
 331     \EndFor\\\r
 332     \r
 333     \ForAll{delete in AD}\r
 334         \State $\tuple{{ssn_s}', \tuple{{ssn_d}'}} \gets delete$\r
 335         \If{${ssn_d}' > ssn_d$}    \Comment{More recently deleted record}\r
 336             \State \Return{False}\r
 337         \ElsIf{$({ssn_d}'= ssn_d) \land ({ssn_s}' > ssn_s)$} \Comment{More recent delete of same record}\r
 338             \State \Return{False}\r
 339         \EndIf\r
 340     \EndFor \\\r
 341     \State \Return{True}\r
 342 \EndFunction\r
 343 \end{algorithmic}\r
 344 \end{varwidth}% \r
 345 }\r
 346 \r
 347 %Abort Live\r
 348 \noindent\fbox{%\r
 349 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 350 \textbf{Abort Live}:\r
 351 \begin{algorithmic}[1]\r
 352 \Function{AbortLive}{$abort_s$}\r
 353     \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\r
 354     \State $tid \gets NULL$\r
 355     \State $\tuple{tid_s,mid_s,vc_s} \gets abort_s$\\\r
 356 \r
 357     \ForAll{$record$ in $R$}\r
 358         \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}\r
 359     \EndFor\\\r
 360     \r
 361     \ForAll{$\tuple{ssn, payload}$ in $API$} \Comment{Transaction still in data structure}\r
 362         \If{$payload$ is a $transaction$}\r
 363             \State $tid \gets $\Call{GetTid}{$payload$}\r
 364             \If{$tid = tid_s$}\r
 365                 \State Return{True}\r
 366             \EndIf\r
 367         \EndIf\r
 368     \EndFor\\\r
 369     \r
 370     \r
 371     \r
 372     \ForAll{record in R}\r
 373         \State $\tuple{ssn_s',\tuple{mid_s', vc_s', hmac_s', payload_s'}} \gets record$\r
 374         \If{$(mid_s'=mid_s) \land (vc_s' > vc_s)$}\r
 375             \State \Return{False}\r
 376         \EndIf\r
 377     \EndFor\\\r
 378     \State \Return{True}\r
 379 \EndFunction\r
 380 \end{algorithmic}\r
 381 \end{varwidth}% \r
 382 }\r
 383 \r
 384 %Resize Live\r
 385 \noindent\fbox{%\r
 386 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 387 \textbf{Resize Live}:\r
 388 \begin{algorithmic}[1]\r
 389 \Function{ResizeLive}{$resize_s, ssn_s$}\r
 390     \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\r
 391     \State $AR \gets \emptyset$    \Comment{Set of all Payload Items that are resize}\r
 392     \State $\tuple{size} \gets resize_s$\\\r
 393     \r
 394     \ForAll{record in R}\r
 395         \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}\r
 396     \EndFor\\\r
 397     \r
 398     \ForAll{$\tuple{ssn, payload}$ in $API$}\r
 399         \If{$payload$ is a $resize$}\r
 400             \State $AR \gets AR \cup \{\tuple{ssn, payload}\}$   \Comment{Extract all resize payloads}\r
 401         \EndIf\r
 402     \EndFor\\\r
 403     \r
 404     \ForAll{$\tuple{ssn', \tuple{size'}}$ in $AR$}\r
 405         \If{$size' > size$}\r
 406             \State \Return{False}\r
 407         \ElsIf{$(size'=size) \land (ssn' > ssn_s)$}\r
 408             \State \Return{False}\r
 409         \EndIf\r
 410     \EndFor \\\r
 411     \State \Return{True}\r
 412 \EndFunction\r
 413 \end{algorithmic}\r
 414 \end{varwidth}% \r
 415 }\r
 416 \r
 417 %New Key Live\r
 418 \noindent\fbox{%\r
 419 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 420 \textbf{New Key Live:}\r
 421 \begin{algorithmic}[1]\r
 422 \Function{NewKeyLive}{$newkey_s, ssn_r$}\r
 423     \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\r
 424     \State $ANK \gets \emptyset$    \Comment{Set of all Payload Items that are new keys}\r
 425     \State $\tuple{k_s, vc_s, ssn_s, mid_s}\gets newkey_s$\\\r
 426     \r
 427     \If{$ssn_s = NULL$}                    \Comment{Make sure ssn is the correct one}\r
 428         \State $ssn_s \gets ssn_r$\r
 429     \EndIf\\\r
 430     \r
 431     \ForAll{record in R}\r
 432         \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}\r
 433     \EndFor\\\r
 434     \r
 435     \ForAll{$\tuple{ssn', payload'}$ in $API$}\r
 436         \If{$payload'$ is a $newkey$}\r
 437             \State $ANK \gets ANK \cup \{\tuple{ssn', payload'}\}$   \Comment{Extract all new key payloads}\r
 438         \EndIf\r
 439     \EndFor\\\r
 440     \r
 441     \ForAll{$\tuple{ssn', \tuple{k_s', vc_s', ssn_s', mid_s'}}$ in $ANK$}\r
 442         \If{$vc_s' < vc_s$}\r
 443             \State \Return{False}\r
 444         \ElsIf{$\lnot (vc_s' < vc_s) \land (ssn_s' < ssn_s)$}\r
 445             \State \Return{False}\r
 446         \EndIf\r
 447     \EndFor \\\r
 448     \State \Return{True}\r
 449 \EndFunction\r
 450 \end{algorithmic}\r
 451 \end{varwidth}% \r
 452 }\r
 453 \r
 454 %Transaction Live\r
 455 \noindent\fbox{%\r
 456 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 457 \textbf{Transaction Live:}\r
 458 \begin{algorithmic}[1]\r
 459 \Function{TransactionLive}{$transaction_s$}\r
 460     \State $AA \gets \emptyset$    \Comment{Set of all Payload Items that are aborts}\r
 461     \State $AC \gets \emptyset$    \Comment{Set of all Payload Items that are commits}\r
 462     \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\r
 463     \State $tid \gets $ \Call{GetTid}{$transaction_s$}\r
 464     \State $foundCommit \gets False$\\\r
 465     \r
 466     \ForAll{$record$ in $R$}\r
 467         \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}\r
 468     \EndFor\\\r
 469     \r
 470     \ForAll{$\tuple{ssn, payload}$ in $API$}\r
 471         \If{$payload$ is a $abort$}\r
 472             \State $AA \gets AA \cup \{payload\}$\r
 473         \ElsIf{$payload$ is a $commit$}\r
 474             \State $AC \gets AC \cup \{payload\}$\r
 475         \EndIf\r
 476     \EndFor\\\r
 477     \r
 478     \ForAll{$\tuple{tid',mid',vc'}$ in $AA$} \Comment{There is an abort}\r
 479         \If{$tid' = tid$}\r
 480             \State \Return{False}\r
 481         \EndIf\r
 482     \EndFor\\\r
 483     \r
 484     \ForAll{$\tuple{tid',vc'}$ in $AC$} \Comment{There is no commit}\r
 485         \If{$tid' = tid$}\r
 486             \State $foundCommit \gets True$\r
 487             \State Break\r
 488         \EndIf\r
 489     \EndFor\\\r
 490     \r
 491     \If{$\lnot foundCommit$}\r
 492         \State \Return{True}\r
 493     \EndIf\\\r
 494     \r
 495     \State $\tuple{mid',vc' ,kvSet',guard'} \gets transaction_s$ \Comment{All Keys are dead}\r
 496     \ForAll{$\tuple{k',v'}$ in $kvSet'$}\r
 497         \If{\Call{KeyValueLive}{$k', transaction_s$}}\r
 498             \State \Return{True}\r
 499         \EndIf\r
 500     \EndFor\r
 501 \r
 502     \State \Return{False}\r
 503 \r
 504 \EndFunction\r
 505 \end{algorithmic}\r
 506 \end{varwidth}% \r
 507 }\r
 508 \r
 509 %Commit Live\r
 510 \noindent\fbox{%\r
 511 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 512 \textbf{Commit Live:}\r
 513 \begin{algorithmic}[1]\r
 514 \Function{CommitLive}{$commit_s, ssn_s$}\r
 515     \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\r
 516     \State $AT \gets \emptyset$    \Comment{Set of all Payload Items that are transaction}\r
 517     \State $tid' \gets NULL$ \r
 518     \State $\tuple{tid, vc} \gets commit_s$ \\ \r
 519 \r
 520     \ForAll{$record$ in $R$}\r
 521         \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}\r
 522     \EndFor\\\r
 523     \r
 524     \ForAll{$\tuple{ssn, payload}$ in $API$}\r
 525         \If{$payload$ is a $transaction$}\r
 526             \State $tid' \gets$ \Call{GetTid}{$payload$}\r
 527             \If{$tid' = tid$}\r
 528                 \State \Return{True}\r
 529             \EndIf\r
 530         \EndIf\r
 531     \EndFor\\\r
 532 \r
 533     \State \Return{False}\r
 534 \EndFunction\r
 535 \end{algorithmic}\r
 536 \end{varwidth}% \r
 537 }\r
 538 \r
 539 %Is Live\r
 540 \noindent\fbox{%\r
 541 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 542 \textbf{Is Live:}:\r
 543 \begin{algorithmic}[1]\r
 544 \Function{IsLive}{$item_s, ssn_S$}\r
 545     \If{$item_s$ is a $tansaction$}\r
 546         \State \Return{\Call{TransactionLive}{$item_s$}}\r
 547     \r
 548     \ElsIf{$item_s$ is a $commit$}\r
 549         \State \Return{\Call{CommitLive}{$item_s, ssn_s$}}\r
 550     \r
 551     \ElsIf{$item_s$ is a $abort$}\r
 552         \State \Return{\Call{AbortLive}{$item_s$}}\r
 553             \r
 554     \ElsIf{$item_s$ is a $delete$}\r
 555         \State \Return{\Call{DeleteLive}{$item_s, ssn_s$}}\r
 556         \r
 557     \ElsIf{$item_s$ is a $commit$}\r
 558         \State \Return{\Call{ResizeLive}{$item_s, ssn_s$}}\r
 559         \r
 560     \ElsIf{$item_s$ is a $sequence$}\r
 561         \State \Return{\Call{SequenceLive}{$item_s, ssn_s$}}\r
 562         \r
 563     \ElsIf{$item_s$ is a $newkey$}\r
 564         \State \Return{\Call{NewKeyLive}{$item_s, ssn_s$}}\r
 565         \r
 566     \ElsIf{$item_s$ is a $keyvalue$}\r
 567         \State \Return{\Call{KeyValueLive}{$item_s, ssn_s$}}\r
 568     \EndIf\\\r
 569     \r
 570     \State \Return{False}  \Comment{Will never get here}\r
 571 \EndFunction\r
 572 \end{algorithmic}\r
 573 \end{varwidth}% \r
 574 }\r
 575 \r
 576 %Record has live payload data\r
 577 \noindent\fbox{%\r
 578 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 579 \textbf{Record has live payload data:}:\r
 580 \begin{algorithmic}[1]\r
 581 \Function{HasLivePayload}{$record_s, ssn_s$}\r
 582     \State $\tuple{mid_s, vc_s, hmac_s, payload_s} \gets record_s$\r
 583     \ForAll{$item$ in $payload_s$}\r
 584         \If{\Call{IsLive}{$item, ssn_s$}}\r
 585             \State \Return{True}\r
 586         \EndIf\r
 587     \EndFor\r
 588     \State \Return{False}\r
 589 \EndFunction\r
 590 \end{algorithmic}\r
 591 \end{varwidth}% \r
 592 }\r
 593 \r
 594 % Get Data Structure Size\r
 595 \noindent\fbox{%\r
 596 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 597 \textbf{Get Data Structure Size:}\r
 598 \begin{algorithmic}[1]\r
 599 \Function{GetDataStrucSize}{ }\r
 600     \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\r
 601     \State $AR \gets \emptyset$    \Comment{Set of all Payload Items that are resize}\r
 602 \r
 603     \ForAll{record in R}\r
 604         \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}\r
 605     \EndFor\\\r
 606     \r
 607     \ForAll{$\tuple{ssn, payload}$ in $API$}\r
 608         \If{($payload$ is a $resize) \land$ \Call{IsLive}{$payload, ssn$}}\r
 609             \State $\tuple{size'} \gets payload$\r
 610             \State \Return{$size'$}\r
 611         \EndIf\r
 612     \EndFor\\\r
 613     \r
 614     \State \Return{$0$}  \Comment{Get Here only if data structure has no entries}\r
 615 \EndFunction\r
 616 \end{algorithmic}\r
 617 \end{varwidth}% \r
 618 }\r
 619 \r
 620 %Rescue New Key\r
 621 \noindent\fbox{%\r
 622 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 623 \textbf{Rescue New Key:}\r
 624 \begin{algorithmic}[1]\r
 625 \Function{RescueNewKey}{$newKeyPayload, ssn$}\r
 626     \State $\tuple{k', vc', ssn', mid'} \gets newKeyPayload$\r
 627     \State \Return{$\tuple{k', vc', ssn, mid'}$}\r
 628 \EndFunction\r
 629 \end{algorithmic}\r
 630 \end{varwidth}% \r
 631 }\r
 632 \r
 633 %Rescue Transaction\r
 634 \noindent\fbox{%\r
 635 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 636 \textbf{Rescue New Key:}\r
 637 \begin{algorithmic}[1]\r
 638 \Function{RescueTransaction}{$transPayload, ssn$}\r
 639     \State $KVRescue \gets \emptyset$\r
 640     \State $\tuple{mid',vc', KVSet,guard_s} \gets transPayload$\\\r
 641     \r
 642     \ForAll{$\tuple{k,v}$ in $KVSet$}\r
 643         \If{\Call{KeyValueLive}{$k, transPayload$}}\r
 644             \State $KVRescue \gets KVRescue \cup \{\tuple{k,v}\}$\r
 645         \EndIf\r
 646     \EndFor\\\r
 647     \r
 648     \State \Return{$\tuple{mid',vc', KVRescue,guard_s}$}\r
 649 \EndFunction\r
 650 \end{algorithmic}\r
 651 \end{varwidth}% \r
 652 }\r
 653 \r
 654 \r
 655 %Rescue Payload Items\r
 656 \noindent\fbox{%\r
 657 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 658 \textbf{Rescue Payload Items}:\r
 659 \begin{algorithmic}[1]\r
 660 \Function{RescuePayloadItems}{$payload_s$}\r
 661     \State $PIList =$ empty list of $\tuple{ssn, payload}$\r
 662     \State $SpaceRemaining = MaxPayloadSize - $ \Call{GetSize}{$payload_s$}\r
 663     \r
 664     \If{$SpaceRemaining = 0$}\r
 665         \Return{$payload_s$}\r
 666     \EndIf\\\r
 667     \r
 668     \ForAll{record in R}\r
 669         \State $PIList \gets PIList \cup$ \Call{GetPayloadItemsWithSSN}{$record$}\r
 670     \EndFor\\\r
 671     \r
 672     \State Sort $PIList$ by $ssn$ from lowest to highest\\\r
 673     \r
 674     \ForAll{$\tuple{ssn', payload'}$ in $PIList$}\r
 675         \If{\Call{IsLive}{$payload', ssn'$} $\land$ \Call{getRandomBoolean}{ } }\\\r
 676             \r
 677             \If{$payload'$ is a $newkey$}\r
 678                 \State $payload' \gets $ \Call{RescueNewKey}{$payload'$}\r
 679             \ElsIf{$payload'$ is a $transaction$}\r
 680                 \State $payload' \gets $ \Call{RescueTransaction}{$payload'$}\r
 681             \EndIf\\\r
 682         \r
 683             \If{\Call{GetSize}{$payload'$} $ > SpaceRemaining$} \Comment{No more space for resuces in payload}\r
 684                 \State \Return{$payload_s$}\r
 685             \EndIf\r
 686             \r
 687             \State $SpaceRemaining \gets SpaceRemaining -$ \Call{GetSize}{$payload'$}\r
 688             \State $payload_s \gets payload_s \cup \{payload'\}$\r
 689         \EndIf\r
 690     \EndFor\\\r
 691     \State \Return{$payload_s$}\r
 692 \EndFunction\r
 693 \end{algorithmic}\r
 694 \end{varwidth}% \r
 695 }\r
 696 \r
 697 %Pad Payload\r
 698 \noindent\fbox{%\r
 699 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 700 \textbf{Pad Payload}:\r
 701 \begin{algorithmic}[1]\r
 702 \Function{PadPayload}{$payload_s$}    \State $SpaceRemaining =  MaxPayloadSize - $ \Call{GetSize}{$payload_s$}\r
 703     \r
 704     \If{$SpaceRemaining = 0$}\r
 705         \State \Return{$payload_s$}\r
 706     \EndIf\\\r
 707     \State \Return{$payload_s \gets payload_s \cup$ \Call{GenerateFiller}{$SpaceRemaining$}}\r
 708 \EndFunction\r
 709 \end{algorithmic}\r
 710 \end{varwidth}% \r
 711 }\r
 712 \r
 713 %Delete Records\r
 714 \noindent\fbox{%\r
 715 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 716 \textbf{Delete Records (Deletes n records)}:\r
 717 \begin{algorithmic}[1]\r
 718 \Function{Delete}{$num\_of\_records$}\r
 719     \State $RS \gets$ List of all Records sorted by ssn and has form $\tuple{ssn_s, record_s}$\r
 720     \State $n \gets 0$\\\r
 721         \r
 722     \ForAll{$\tuple{ssn_s, record_s}$ in $RS$}\r
 723         \If{\Call{HasLivePayload}{$record_s, ssn_s$}}\r
 724             \State \Return{False}\r
 725         \Else\r
 726             \State \Call{DeleteSlotServer}{$ssn_s$}\r
 727             \State $n \gets n + 1$\r
 728         \EndIf\\\r
 729         \r
 730         \If{$n = num\_of\_records$}\r
 731             \State \textbf{break}\r
 732         \EndIf\r
 733     \EndFor\\\r
 734     \r
 735     \State \Return{True}\r
 736     \r
 737 \EndFunction\r
 738 \end{algorithmic}\r
 739 \end{varwidth}% \r
 740 }\r
 741 \r
 742 %Create Resize Data Structure Payload Item\r
 743 \noindent\fbox{%\r
 744 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 745 \textbf{Create Resize Data Structure Payload Item:}\r
 746 \begin{algorithmic}[1]\r
 747 \Function{MakeResizePayload}{ }\r
 748     \State $rp \gets$ Empty $resize$ payload\r
 749     \State $cs \gets$ \Call{GetDataStrucSize}{ }\r
 750     \State $rp \gets \tuple{cs * 2}$\r
 751     \State \Return{$\{rp\}$}\r
 752 \EndFunction\r
 753 \end{algorithmic}\r
 754 \end{varwidth}% \r
 755 }\r
 756 \r
 757 %Get Arbitrator\r
 758 \noindent\fbox{%\r
 759 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 760 \textbf{Get Arbitrator:}\r
 761 \begin{algorithmic}[1]\r
 762 \Function{GetArbitrator}{$key$}\r
 763     \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\\\r
 764 \r
 765     \ForAll{record in R}\r
 766         \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}\r
 767     \EndFor\\\r
 768     \r
 769     \ForAll{$\tuple{ssn, payload}$ in $API$}\r
 770         \If{($payload$ is a $newkey) \land$ \Call{IsLive}{$payload, ssn$}}\r
 771             \State $\tuple{k', vc', ssn', mid'} \gets payload$\r
 772             \r
 773             \If{$k' = key$}\r
 774                 \State \Return{$mid'$}\r
 775             \EndIf\r
 776         \EndIf\r
 777     \EndFor\\\r
 778     \State \Call{Error}{No arbitrator for key: $key$}\r
 779 \EndFunction\r
 780 \end{algorithmic}\r
 781 \r
 782 \begin{algorithmic}[1]\r
 783 \Function{GetArbitrator}{$guard$}\r
 784     \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\r
 785     \State $\tuple{kvSet, condition} \gets guard$\\\r
 786     \r
 787     \ForAll{record in R}\r
 788         \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}\r
 789     \EndFor\\\r
 790     \r
 791     \ForAll{$\tuple{key, value}$ in $kvSet$}\r
 792         \ForAll{$\tuple{ssn, payload}$ in $API$}\r
 793             \If{($payload$ is a $newkey) \land$ \Call{IsLive}{$payload, ssn$}}\r
 794                 \State $\tuple{k', vc', ssn', mid'} \gets payload$\r
 795                 \If{$k' = key$}\r
 796                     \State \Return{$mid'$}\r
 797                 \EndIf\r
 798             \EndIf\r
 799         \EndFor\r
 800     \EndFor\\\r
 801     \State \Call{Error}{No arbitrator for key: $key$}\r
 802 \EndFunction\r
 803 \end{algorithmic}\r
 804 \r
 805 \end{varwidth}% \r
 806 }\r
 807 \r
 808 %Insert Payload\r
 809 \noindent\fbox{%\r
 810 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 811 \textbf{Insert Payload:}\r
 812 \begin{algorithmic}[1]\r
 813 \Function{InsertPayload}{$payload_s$}\r
 814     \r
 815     \State $numOfRecords \gets |R|+1$\r
 816     \State $targetSize \gets $ \Call{GetDataStrucSize}{ }\r
 817     \State $numToDelete \gets numOfRecords - targetSize$\r
 818     \State $rp \gets NULL$\r
 819     \State $hmac \gets NULL$\r
 820     \State $vc \gets NULL$\r
 821     \State $record \gets NULL$\\\r
 822 \r
 823     \If{\Call{GetSize}{$payload_s$} $> MaxPayloadSize$}\r
 824         \State \Call{Error}{Payload too large}\r
 825     \EndIf\\\r
 826     \r
 827     \If{$numToDelete > 0$}\r
 828         \If{$\lnot$\Call{Delete}{$numToDelete$}}\r
 829             \State $rp \gets$\Call{MakeResizePayload}{ }\r
 830             \If{\Call{GetSize}{$payload_s \cup rp$} $> MaxPayloadSize$}\r
 831                 \State \Call{InsertPayload}{$rp$}\r
 832             \Else\r
 833                 \State $payload_s \gets payload_s \cup rp$\r
 834             \EndIf\r
 835         \EndIf\r
 836     \EndIf\\\r
 837     \r
 838     \State $payload_s \gets$ \Call{RescuePayloadItems}{$payload_s$}\r
 839     \State $payload_s \gets$ \Call{PadPayload}{$payload_s$}\r
 840     \State $vc \gets $ \Call{GenerateVectorClock}{ }\r
 841     \State $hmac \gets$ \Call{GenerateHmac}{$mid, vc, payload_s$}\r
 842     \State $record \gets \tuple{mid,vc,hmac,payload}$\r
 843     \State $record \gets $\Call{Encrypt}{$record$}\r
 844     \State \Call{PutSlotServer}{$record$}\r
 845 \EndFunction\r
 846 \end{algorithmic}\r
 847 \end{varwidth}% \r
 848 }\r
 849 \r
 850 %Check Data Structure for Malicious Activity\r
 851 %\noindent\fbox{%\r
 852 %\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 853 \textbf{Check Data Structure for Malicious Activity:}\r
 854 \begin{algorithmic}[1]\r
 855 \Function{CheckDataStructForValidity}{ }\r
 856     \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\r
 857     \State $ASeq \gets \emptyset$   \Comment{Set of all Payload Items that are sequences}\r
 858     \State $MID \gets \emptyset$   \Comment{Set of all machine IDs}\r
 859     \State $midClocks \gets \emptyset$ \Comment{Set of all clocks for the same machine IDs}\r
 860     \State $oldestDeletedSsn \gets NULL$\r
 861     \State $didFindSsn \gets False$\r
 862     \State $didFindClock \gets False$\r
 863     \State $hmac \gets NULL$\\\r
 864     \r
 865     \State Sort $R$ by $ssn$ from smallest $ssn$ to largest $ssn$\\\r
 866     \r
 867     \ForAll{record in R}\r
 868         \State $\tuple{ssn',\tuple{mid', vc', hmac', payload'}} \gets record$\r
 869         \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}\r
 870         \State $MID \gets MID \cup \{mid'\}$\r
 871     \EndFor\\\r
 872 \r
 873     \ForAll{$record$ in $R$} \Comment{Check HMACs are all valid}\r
 874         \State $\tuple{ssn',\tuple{mid', vc', hmac', payload'}} \gets record$\r
 875         \State $hmac \gets $ \Call{GenerateHmac}{$mid', vc', payload'$}\r
 876         \If{$hmac \neq hmac'$}\r
 877             \State \Call{Error}{HMAC mismatch}\r
 878         \EndIf\r
 879     \EndFor\\\r
 880     \r
 881     \ForAll{$record_1$ in $R$} \Comment{Check no SSN duplicates}\r
 882         \State $\tuple{ssn_1,rData_1} \gets record_1$\r
 883         \ForAll{$record_2$ in $R$}\r
 884             \If{$record_2 \neq record_1$}\r
 885                \State $\tuple{ssn_2,rData_2} \gets record_2$\r
 886                \If{$ssn_2 = ssn_1$}\r
 887                     \State \Call{Error}{Duplicate SSN for different records}\r
 888                \EndIf\r
 889             \EndIf\r
 890         \EndFor\r
 891     \EndFor\\\r
 892     \r
 893     \r
 894     \ForAll{$record_1$ in $R[0:-1]$} \Comment{Check for missing SSN}\r
 895         \State $\tuple{ssn_1,rData_1} \gets record_1$\r
 896         \State $didFindSsn \gets False$\r
 897         \ForAll{$record_2$ in $R[1:]$}\r
 898             \State $\tuple{ssn_2,rData_2} \gets record_2$\r
 899             \If{$ssn_2 = (ssn_1 + 1)$}\r
 900                 \    State $didFindSsn \gets True$\r
 901                 \State Break\r
 902             \EndIf\r
 903         \EndFor\r
 904         \r
 905         \If{$\lnot didFindSsn$}\r
 906             \State \Call{Error}{Missing SSN in SSN sequence.}\r
 907         \EndIf\r
 908     \EndFor\\\r
 909     \r
 910      \ForAll{$\tuple{ssn, payload}$ in $API$}\r
 911         \If{($payload$ is a $delete) \land$ \Call{IsLive}{$payload, ssn$}}\r
 912             \State $\tuple{ssn'} \gets payload$\r
 913             \State $oldestDeleteSsn \gets ssn'$\r
 914         \ElsIf{($payload$ is a $sequence) \land$ \Call{IsLive}{$payload, ssn$}}\r
 915             \State $ASeq \gets ASeq \cup \{payload\}$\r
 916         \EndIf\r
 917     \EndFor\\\r
 918     \r
 919     \r
 920     \ForAll{$record$ in $R$} \Comment{Check SSN's are all valid}\r
 921         \State $\tuple{ssn, rData} \gets record$\r
 922         \ForAll{$\tuple{rid', ssn'}$ in $ASeq$}\r
 923             \If{$(rid' =$ \Call{GetRid}{$record$}$) \land ssn' \neq ssn$}\r
 924                 \State \Call{Error}{SSN mismatch}\r
 925             \EndIf\r
 926         \EndFor\r
 927     \EndFor\\\r
 928     \r
 929     \r
 930     \State $\tuple{ssn, payload} \gets R[0]$ \Comment{Get first record in the sorted R}\r
 931     \If{$ssn > (oldestDeleteSsn + 1) $}\r
 932         \State \Call{Error}{Missing records}\r
 933    \EndIf\\\r
 934     \r
 935     \r
 936     \ForAll{$mid$ in $MID$}\r
 937         \State $midClocks \gets \emptyset$\r
 938         \r
 939         \ForAll{record in R}\r
 940             \State $\tuple{ssn',\tuple{mid', vc', hmac', payload'}} \gets record$\r
 941             \If{$mid' = mid$}\r
 942                 \State $\tuple{c_{mid_1}, c_{mid_2},...,c_{mid_k}} \gets vc'$\r
 943                 \State $midClocks \gets midClocks \cup \{c_{mid_n}|mid_n=mid\}$\r
 944             \EndIf\r
 945         \EndFor\\\r
 946         \r
 947         \State Sort $midClocks$ from smallest clock to largest clock\\\r
 948         \r
 949         \ForAll{$c_1$ in $midClocks[0:-1]$} \Comment{Check for missing SSN}\r
 950             \State $didFindSsn \gets False$\r
 951             \ForAll{$c_2$ in $midClocks[1:]$}\r
 952                 \If{$c_2 = (c_1 + 1)$}\r
 953                     \State $didFindC\r
 954 ock\gets True$\r
 955                     \State Break\r
 956                 \EndIf\r
 957             \EndFor\r
 958         \EndFor\r
 959         \r
 960         \If{$\lnot didFindClock$}\r
 961             \State \Call{Error}{Missing clock in clock sequence for: $mid$.}\r
 962         \EndIf\r
 963     \EndFor\\\r
 964     \r
 965     \State \Comment{If got here then data structure is valid}\r
 966 \EndFunction\r
 967 \end{algorithmic}\r
 968 %\end{varwidth}% \r
 969 %}\r
 970 \r
 971 %Get Latest Data Structure From Server\r
 972 \noindent\fbox{%\r
 973 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 974 \textbf{Get  Latest Data Structure From Server}:\r
 975 \begin{algorithmic}[1]\r
 976 \Function{GetLatestDataStruct}{}\r
 977     \State $largestSsn \gets $ Largest $ssn$ of all $ssn$ in $R$\r
 978     \State $R \gets R \cup $ \Call{GetSlotServer}{$largestSsn + 1$}\r
 979     \State \Call{CheckDataStructForValidity}{ }\r
 980 \EndFunction\r
 981 \end{algorithmic}\r
 982 \end{varwidth}% \r
 983 }\r
 984 \r
 985 %Update Key Value Set\r
 986 \noindent\fbox{%\r
 987 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 988 \textbf{Update Key Value Set:}\r
 989 \begin{algorithmic}[1]\r
 990 \Function{UpdateKVSet}{$currentKV, kvSet$}\r
 991     \State $newKVSet \gets kvSet$\r
 992     \State $foundKey \gets False$\\\r
 993     \r
 994     \ForAll{$\tuple{k,v}$ in $currentKV$}\r
 995         \State $foundKey \gets False$\\\r
 996         \r
 997         \ForAll{$\tuple{k',v'}$ in $kvSet$}\r
 998             \If{$k = k'$}\r
 999                 \State $foundKey \gets True$\r
1000                 \State Break\r
1001             \EndIf\r
1002         \EndFor\\\r
1003         \r
1004         \If{$\lnot foundKey$}\r
1005             \State $newKVSet \gets newKVSet \cup \{\tuple{k,v}\}$\r
1006         \EndIf\r
1007     \EndFor\r
1008     \r
1009     \State \Return{$newKVSet$}\r
1010 \EndFunction\r
1011 \end{algorithmic}\r
1012 \end{varwidth}% \r
1013 }\r
1014 \r
1015 \r
1016 \r
1017 \r
1018 \r
1019 %-Arbitration\r
1020 %   - Insert Commit\r
1021 \r
1022 \r
1023 \subsection{\textbf{Create new key}}\r
1024 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.\r
1025 \r
1026 \noindent\fbox{%\r
1027 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
1028 \textbf{Create new key:}\r
1029 \begin{algorithmic}[1]\r
1030 \Function{CreateNewKey}{$keyName, mid$}\r
1031     \State $vc \gets $ \Call{GenerateVectorClock}{ }\r
1032     \State $newKeyPayload \gets \tuple{keyName, vc, NULL, mid}$\r
1033     \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\\\r
1034 \r
1035     \State \Call{GetLatestDataStruct}{ } \Comment{Update local version of data struct}\\\r
1036 \r
1037     \ForAll{record in R}\r
1038         \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}\r
1039     \EndFor\\\r
1040     \r
1041     \ForAll{$\tuple{ssn, payload}$ in $API$}\r
1042         \If{($payload$ is a $newkey) \land$ \Call{IsLive}{$payload, ssn$}}\r
1043             \State $\tuple{k', vc', ssn', mid'} \gets payload$\r
1044             \r
1045             \If{$k' = key$}\r
1046                 \State \Return{False}\r
1047             \EndIf\r
1048         \EndIf\r
1049     \EndFor\\\r
1050     \r
1051     \State \Call{InsertPayload}{$newKeyPayload$}\r
1052     \State \Return{True}\r
1053 \EndFunction\r
1054 \end{algorithmic}\r
1055 \end{varwidth}% \r
1056 }\r
1057 \r
1058 \subsection{\textbf{Put Transaction}}\r
1059 This operation puts a transaction into the data structure if this transaction fits inside a payload.\r
1060 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.\\\r
1061 \r
1062 %\r
1063 \noindent\fbox{%\r
1064 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
1065 \textbf{Put Transaction:}\r
1066 \begin{algorithmic}[1]\r
1067 \Function{PutTransaction}{$kVUpdates, guard$}\r
1068     \State $mid \gets NULL$\r
1069     \State $vc \gets $ \Call{GenerateVectorClock}{ }\r
1070     \State $transPayload \gets NULL$\\\r
1071 \r
1072     \State \Call{GetLatestDataStruct}{ } \Comment{Update local version of data struct}\\\r
1073 \r
1074     \ForAll{$kv$ in $kVUpdates$}\r
1075         \State $\tuple{k', v'} \gets kv$\r
1076         \r
1077         \If{$mid = NULL$}\r
1078             \State $mid \gets$ \Call{GetArbitrator}{$k'$}\r
1079         \ElsIf{$mid \neq $ \Call{GetArbitrator}{$k'$}}\r
1080             \State \Call{Error}{Multiple Arbitrators}\r
1081         \EndIf\r
1082     \EndFor\\\r
1083     \r
1084     \If{\Call{GetArbitrator}{$guard$} $\neq mid$}\r
1085         \State \Call{Error}{Multiple Arbitrators}\r
1086     \EndIf\\\r
1087     \r
1088     \State $transPayload \gets \tuple{mid, vc, kVUpdates, guard}$\r
1089     \State \Call{InsertPayload}{$transPayload$}\r
1090 \EndFunction\r
1091 \end{algorithmic}\r
1092 \end{varwidth}% \r
1093 }\r
1094 \r
1095 \subsection{\textbf{Get key-value pair}}\r
1096 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.\r
1097 \r
1098 %\noindent\fbox{%\r
1099 %\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
1100 \textbf{Get  Latest Data Structure From Server}:\r
1101 \begin{algorithmic}[1]\r
1102 \Function{GetValueForKey}{$keyName$}\r
1103     \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\r
1104     \State $AT \gets \emptyset$    \Comment{Set of all Payload Items that are transactions}\r
1105     \State $AC \gets \emptyset$    \Comment{Set of all Payload Items that are commits}\r
1106     \State $AA \gets \emptyset$    \Comment{Set of all Payload Items that are aborts}\r
1107     \State $kSet \gets \emptyset$ \Comment{Set of all key names in the system}\r
1108     \State $tid \gets NULL$\r
1109     \State $currentKV \gets \emptyset$\\\r
1110     \r
1111     \State \Call{GetLatestDataStruct}{ } \Comment{Update local version of data struct}\\\r
1112     \r
1113     \ForAll{$record$ in $R$}\r
1114         \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}\r
1115     \EndFor\\\r
1116     \r
1117     \ForAll{$\tuple{ssn, payload}$ in $API$}\r
1118         \If{$payload$ is a $transaction$}\r
1119             \State $AT \gets AT \cup \{\tuple{ssn,payload}\}$\r
1120         \ElsIf{$payload$ is a $commit$}\r
1121             \State $AC \gets AC \cup \{payload\}$\r
1122         \ElsIf{$payload$ is a $abort$}\r
1123             \State $AA \gets AA \cup \{payload\}$\r
1124         \EndIf\r
1125     \EndFor\\\r
1126     \r
1127     \State Sort $AT$ by ssn from oldest to newest\\\r
1128     \r
1129     \ForAll{$trans$ in $AT$} \Comment{Get the latest committed keys}\r
1130         \State $\tuple{mid,vc ,kvSet,guard} \gets trans$\\\r
1131     \r
1132         \ForAll{$\tuple{k,v}$ in $kvSet$} \Comment{Get all key names in the system}\r
1133             \State $kSet \gets kSet \cup \{k\}$\r
1134         \EndFor\\\r
1135 \r
1136         \If{$\lnot $\Call{TransactionLive}{$trans$}} \Comment{Only keep live transactions}\r
1137             \State $AT \gets AT - \{trans\}$\r
1138             \State Continue\r
1139         \EndIf\\\r
1140     \r
1141         \State $tid \gets $ \Call{GetTid}{$trans$}\r
1142         \ForAll{$com$ in $AC$}\r
1143             \State $\tuple{tid', vc'} \gets com$\r
1144             \If{$tid' = tid$}\r
1145                 \ForAll{$\tuple{k,v}$ in $kvSet$}\r
1146                     \If{\Call{KeyValueLive}{$k,trans$}}\r
1147                         \State $currentKV \gets currentKV \cup \{\tuple{k,v}\}$\r
1148                     \EndIf\r
1149                 \EndFor\\\r
1150                 \r
1151                 \State $AT \gets AT - \{trans\}$ \Comment{No need for committed transactions}\r
1152                 \State Break\r
1153             \EndIf\r
1154         \EndFor\r
1155     \EndFor\\\r
1156     \r
1157     \ForAll{$trans$ in $AT$} \Comment{Uncommitted ones only in order from lowest ssn to highest ssn}\r
1158         \State $\tuple{mid,vc ,kvSet,guard} \gets trans$\r
1159         \If{\Call{EvaluateGuard}{$guard, currentKV$}} \Comment{Check if will abort}\r
1160             \State $currentKV \gets $\Call{UpdateKVSet}{$currentKV, kvSet$}\r
1161         \EndIf\r
1162     \EndFor\\\r
1163     \r
1164     \r
1165     \ForAll{$\tuple{k,v}$ in $currentKV$} \Comment{Return the latest guessed value}\r
1166         \If{$k = keyName$}\r
1167             \State \Return{$v$}\r
1168         \EndIf\r
1169     \EndFor\\\r
1170     \r
1171     \State \Return{$NULL$} \Comment{Key was not present}\r
1172     \r
1173 \EndFunction\r
1174 \end{algorithmic}\r
1175 %\end{varwidth}% \r
1176 %}\r
1177 \r
1178 \end{document}\r