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{algpseudocode}% http://ctan.org/pkg/algorithmicx\r
   9 \usepackage[all]{xy}\r
  10 \newtheorem{theorem}{Theorem}\r
  11 \newtheorem{prop}{Proposition}\r
  12 \newtheorem{lem}{Lemma}\r
  13 \newtheorem{defn}{Definition}\r
  14 \newcommand{\note}[1]{{\color{red} \bf [[#1]]}}\r
  15 \newcommand{\push}[1][1]{\hskip\dimexpr #1\algorithmicindent\relax}\r
  16 \begin{document}\r
  17 \r
  18 \r
  19 \setlength\parindent{0pt} % Removes all indentation from paragraphs - comment this line for an assignment with lots of text\r
  20 \r
  21 \r
  22 \section{\textbf{Introduction}}\r
  23 \r
  24 \r
  25 \r
  26 \r
  27 \r
  28 \r
  29 \r
  30 \section{\textbf{Server}}\r
  31 The server maintains a collection of slots such that each slot contains some data.\r
  32 The operations on the slot are as follows:\r
  33 \begin{itemize}\r
  34     \item Put slot\r
  35     \item Get slot\r
  36     \item Delete Slot\r
  37 \end{itemize}\r
  38 \r
  39 \subsection{\textbf{Server Notation Conventions}}\r
  40 $s \in SN$ is a server sequence number\\\r
  41 $sv \in SV$ is a slot's value\\\r
  42 $slot_s = \tuple{s, sv} \in SL \subseteq SN \times SV$\r
  43 \r
  44 \subsection{\textbf{Server State}}\r
  45 \textit{n = current server sequence number}\\\r
  46 \textit{SL = set of live slots on the server}\\\r
  47 \r
  48 \textbf{Initial Server State}\\\r
  49 $SL = \emptyset$\\\r
  50 $n = 0$\r
  51 \r
  52 \subsection{\textbf{Put Slot}}\r
  53 Put slot is an operation that inserts data into a new slot at the server.\\\r
  54 \r
  55 \textbf{Put Function:}\r
  56 \begin{algorithmic}[1]\r
  57 \Function{PutSlotServer}{$sv_p$}\r
  58     \State $s_p \gets n$\r
  59     \State $n \gets n + 1$\r
  60     \State $SL \gets SL \cup \{\tuple{s_p,sv_p}\}$\r
  61 \EndFunction\r
  62 \end{algorithmic}\r
  63 \r
  64 \r
  65 \subsection{\textbf{Get Slot}}\r
  66 Get slot is an operation that returns all server slots that are greater than some server sequence number.\\\r
  67 \r
  68 \textbf{Get Function:}\r
  69 \begin{algorithmic}[1]\r
  70 \Function{GetSlotServer}{$s_g$}\r
  71     \State \Return{$\{\tuple{s, sv} \in SL \mid s \geq s_g\}$}\r
  72 \EndFunction\r
  73 \end{algorithmic}\r
  74 \r
  75 \subsection{\textbf{Delete Slot}}\r
  76 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
  77 \r
  78 \textbf{Delete Function:}\r
  79 \begin{algorithmic}[1]\r
  80 \Function{DeleteSlotServer}{$s_d$}\r
  81     \State $SD \gets \{\tuple{s, sv} \in SL \mid s \leq s_g\}$\r
  82     \State $SL \gets SL - SD$\r
  83 \EndFunction\r
  84 \end{algorithmic}\r
  85 \r
  86 \r
  87 \r
  88 \r
  89 \r
  90 \r
  91 \r
  92 \r
  93 \section{\textbf{Client}}\r
  94 The data structure acts as a key store where key-value pairs can be read and set.\r
  95 The data structure exposes the following functions:\r
  96 \begin{itemize}\r
  97     \item Put Transaction\r
  98     \item Get key-value pair\r
  99     \item Create new key\r
 100 \end{itemize}\r
 101 \r
 102 \subsection{\textbf{Client Notation Conventions}}\r
 103 $mid_s \in MID$ is the machine ID for the device that created $record_s$.\\\r
 104 $hmac_s$ is the HMAC of $record_s$\\\r
 105 $c_{mid}$ is the latest read clock for a device with machine ID $mid$\\\r
 106 $vc_s = \{c_{mid} | mid \in MID\}$\\\r
 107 \r
 108 \r
 109 $payload_s = \{x_1, x_2,..., x_k | \forall k, x_k \in \{$transaction, commit, abort, resize, new-key, sequence, delete$\}\}$\\\r
 110 $record_s = \tuple{mid_s, vc_s, hmac_s, payload_s}$ \\\r
 111 \r
 112 \subsection{\textbf{Client State}}\r
 113 \textit{s = largest server sequence number pulled from the server by a device} \\\r
 114 \r
 115 \r
 116 \subsection{Helper Functions}\r
 117 The following helper functions are needed:\\\r
 118 \r
 119 \textbf{Get Latest Data Structure From Server:}\\\r
 120 \textbf{Delete Records:}\\\r
 121 \textbf{Check Data Structure for Malicious Activity:}\r
 122 \r
 123 \r
 124 \subsection{\textbf{Put Transaction}}\r
 125 \r
 126 \r
 127 \r
 128 \subsection{\textbf{Get key-value pair}}\r
 129 \subsection{\textbf{Create new key}}\r
 130 \r
 131 \end{document}\r