From 7dbaf953f6ccb82abbbfa62062a06193cbcc45dc Mon Sep 17 00:00:00 2001 From: Ali Younis Date: Tue, 11 Oct 2016 15:38:34 -0700 Subject: [PATCH] Formal Version --- .gitignore | 13 +- version2/doc/iotcloud.out | 9 -- version2/doc/iotcloud_formal/iotcloud.tex | 131 ++++++++++++++++++ version2/doc/{ => iotcloud_formal}/makefile | 0 version2/doc/iotcloud_informal/iotcloud.out | 26 ++++ .../doc/{ => iotcloud_informal}/iotcloud.tex | 0 version2/doc/iotcloud_informal/makefile | 8 ++ 7 files changed, 174 insertions(+), 13 deletions(-) delete mode 100644 version2/doc/iotcloud.out create mode 100644 version2/doc/iotcloud_formal/iotcloud.tex rename version2/doc/{ => iotcloud_formal}/makefile (100%) create mode 100644 version2/doc/iotcloud_informal/iotcloud.out rename version2/doc/{ => iotcloud_informal}/iotcloud.tex (100%) create mode 100644 version2/doc/iotcloud_informal/makefile diff --git a/.gitignore b/.gitignore index f32907e..9702a6a 100644 --- a/.gitignore +++ b/.gitignore @@ -23,7 +23,12 @@ doc/algpseudocode.sty doc/iotcloud.aux doc/iotcloud.log doc/iotcloud.pdf -version2/doc/iotcloud.aux -version2/doc/iotcloud.log -version2/doc/iotcloud.pdf -version2/doc/iotcloud.out +version2/doc/iotcloud_formal/iotcloud.aux +version2/doc/iotcloud_formal/iotcloud.log +version2/doc/iotcloud_formal/iotcloud.pdf +version2/doc/iotcloud_formal/iotcloud.out +version2/doc/iotcloud_informal/iotcloud.aux +version2/doc/iotcloud_informal/iotcloud.log +version2/doc/iotcloud_informal/iotcloud.pdf +version2/doc/iotcloud_informal/iotcloud.out + diff --git a/version2/doc/iotcloud.out b/version2/doc/iotcloud.out deleted file mode 100644 index 25677b4..0000000 --- a/version2/doc/iotcloud.out +++ /dev/null @@ -1,9 +0,0 @@ -\BOOKMARK [1][-]{section.1}{Introduction}{}% 1 -\BOOKMARK [1][-]{section.2}{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}{Updates}{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}{Checking the Graph}{section.2}% 8 -\BOOKMARK [2][-]{subsection.2.6}{Live Status}{section.2}% 9 diff --git a/version2/doc/iotcloud_formal/iotcloud.tex b/version2/doc/iotcloud_formal/iotcloud.tex new file mode 100644 index 0000000..6615895 --- /dev/null +++ b/version2/doc/iotcloud_formal/iotcloud.tex @@ -0,0 +1,131 @@ +\documentclass[11pt]{article} +\newcommand{\tuple}[1]{\ensuremath \langle #1 \rangle} +\usepackage{color} +\usepackage{amsthm} +\usepackage{amsmath} +\usepackage{graphicx} +\usepackage{mathrsfs} +\usepackage{algpseudocode}% http://ctan.org/pkg/algorithmicx +\usepackage[all]{xy} +\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} +\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.\\ + +\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} + + +\subsection{\textbf{Get Slot}} +Get slot is an operation that returns all server slots that are greater than some server sequence number.\\ + +\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} + +\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.\\ + +\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} + + + + + + + + +\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} + +\subsection{\textbf{Client Notation Conventions}} +$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\}$\\ + + +$payload_s = \{x_1, x_2,..., x_k | \forall k, x_k \in \{$transaction, commit, abort, resize, new-key, sequence, delete$\}\}$\\ +$record_s = \tuple{mid_s, vc_s, hmac_s, payload_s}$ \\ + +\subsection{\textbf{Client State}} +\textit{s = largest server sequence number pulled from the server by a device} \\ + + +\subsection{Helper Functions} +The following helper functions are needed:\\ + +\textbf{Get Latest Data Structure From Server:}\\ +\textbf{Delete Records:}\\ +\textbf{Check Data Structure for Malicious Activity:} + + +\subsection{\textbf{Put Transaction}} + + + +\subsection{\textbf{Get key-value pair}} +\subsection{\textbf{Create new key}} + +\end{document} diff --git a/version2/doc/makefile b/version2/doc/iotcloud_formal/makefile similarity index 100% rename from version2/doc/makefile rename to version2/doc/iotcloud_formal/makefile diff --git a/version2/doc/iotcloud_informal/iotcloud.out b/version2/doc/iotcloud_informal/iotcloud.out new file mode 100644 index 0000000..4241fc5 --- /dev/null +++ b/version2/doc/iotcloud_informal/iotcloud.out @@ -0,0 +1,26 @@ +\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 diff --git a/version2/doc/iotcloud.tex b/version2/doc/iotcloud_informal/iotcloud.tex similarity index 100% rename from version2/doc/iotcloud.tex rename to version2/doc/iotcloud_informal/iotcloud.tex diff --git a/version2/doc/iotcloud_informal/makefile b/version2/doc/iotcloud_informal/makefile new file mode 100644 index 0000000..cff4a15 --- /dev/null +++ b/version2/doc/iotcloud_informal/makefile @@ -0,0 +1,8 @@ +LATEX := pdflatex -halt-on-error + +default: + $(LATEX) iotcloud.tex + +clean: + rm -f *.dvi *.log *.aux *.blg *.bbl *~ + rm -f iotcloud.ps iotcloud.pdf -- 2.34.1