Revisions
authorAli Younis <ayounis@uci.edu>
Tue, 1 Nov 2016 07:12:49 +0000 (00:12 -0700)
committerAli Younis <ayounis@uci.edu>
Tue, 1 Nov 2016 07:12:49 +0000 (00:12 -0700)
doc2/iotcloud.tex

index 9d10557..e80073d 100644 (file)
 \usepackage{amsmath}\r
 \usepackage{graphicx}\r
 \usepackage{mathrsfs}\r
+\usepackage{amssymb}\r
 \usepackage{algpseudocode}% http://ctan.org/pkg/algorithmicx\r
 \usepackage[all]{xy}\r
+\usepackage{varwidth}\r
+\r
 \newtheorem{theorem}{Theorem}\r
 \newtheorem{prop}{Proposition}\r
 \newtheorem{lem}{Lemma}\r
 \newtheorem{defn}{Definition}\r
 \newcommand{\note}[1]{{\color{red} \bf [[#1]]}}\r
 \newcommand{\push}[1][1]{\hskip\dimexpr #1\algorithmicindent\relax}\r
+\newcommand*\xor{\mathbin{\oplus}}\r
+\algnewcommand{\LeftComment}[1]{\Statex \(\triangleright\) #1}\r
 \begin{document}\r
-\section{Approach}\r
-\r
-\subsection{Keys}\r
-\r
-Each device has: user id + password\r
-\r
-Server login is:\r
-hash1(user id), hash1(password)\r
-\r
-Symmetric Crypto keys is:\r
-hash2(user id | password)\r
-\r
-Server has finite length queue of entries + max\_entry\_identifier +\r
-server login key\r
-\r
-\subsection{Entry layout}\r
-Each entry has:\r
-\begin{enumerate}\r
-\item Sequence identifier\r
-\item Random IV (if needed by crypto algorithm)\r
-\item Encrypted payload\r
-\end{enumerate}\r
-\r
-Payload has:\r
-\begin{enumerate}\r
-\item Sequence identifier\r
-\item Machine id (most probably something like a 64-bit random number \r
-that is self-generated by client)\r
-\item HMAC of previous slot\r
-\item Data entries\r
-\item HMAC of current slot\r
-\end{enumerate}\r
-\r
-A data entry can be one of these:\r
-\begin{enumerate}\r
-\item All or part of a Key-value entry\r
-\item Slot sequence entry: Machine id + last message identifier \r
-\newline {The purpose of this is to keep the record of the last slot \r
-from a certain client if a client's update has to expunge that other \r
-client's last entry from the queue. This is kept in the slot until \r
-the entry owner inserts a newer update into the queue.}\r
-\item Queue state entry: Includes queue size \newline {The purpose \r
-of this is for the client to tell if the server lies about the number \r
-of slots in the queue, e.g. if there are 2 queue state entry in the queue, \r
-e.g. 50 and 70, the client knows that when it sees 50, it should expect \r
-at most 50 slots in the queue and after it sees 70, it should expect \r
-50 slots before that queue state entry slot 50 and at most 70 slots. \r
-The queue state entry slot 70 is counted as slot number 51 in the queue.}\r
-\item Collision resolution entry: message identifier + machine id of a\r
-collision winner\r
-\newline {The purpose of this is to keep keep track of the winner of \r
-all the collisions until all clients have seen the particular entry.}\r
-\end{enumerate}\r
-\r
-\subsection{Live status}\r
-\r
-Live status of entries:\r
-\begin{enumerate}\r
-\item Key-Value Entry is dead if either (a) there is a newer key-value pair or (b) it is incomplete.\r
-       \r
-\item Slot sequence number (of either a message version data\r
-or user-level data) is dead if there is a newer slot from the same machine.\r
-\r
-\item Queue state entry is dead if there is a newer queue state entry.\r
-{In the case of queue state entries 50 and 70, this means that queue state \r
-entry 50 is dead and 70 is live. However, not until the number of slots reaches \r
-70 that queue state entry 50 will be expunged from the queue.}\r
-\r
-\item Collision resolution entry is dead if this entry has been seen\r
-by all clients after a collision happens.\r
-\end{enumerate}\r
-\r
-When data is at the end of the queue ready to expunge, if:\r
-\begin{enumerate}\r
-\item The key-value entry is not dead, it must be reinserted at the\r
-beginning of the queue.\r
-\r
-\item If the slot sequence number is not dead, then a message sequence\r
-entry must be inserted.\r
-\r
-\item If the queue state entry is not dead, it must be reinserted at the\r
-beginning of the queue.\r
-\end{enumerate}\r
-\r
-\r
-\paragraph{Reads:}\r
-Client sends a sequence number.  Server replies with either: all data\r
-entries or all newer data entries.\r
-\r
-\paragraph{Writes:}\r
-Client sends slot, server verifies that sequence number is valid,\r
-checks entry hash, and replies with an accept message if all checks\r
-pass.  On success, client updates its sequence number.  On failure,\r
-server sends updates slots to client and client validates those slots.\r
-\r
-\paragraph{Local state on each client:}\r
-A list of machines and the corresponding latest sequence numbers.\r
-\r
-\paragraph{Validation procedure on client:}\r
-\begin{enumerate}\r
-\item Decrypt each new slot in order.\r
-\item For each slot:\r
-    (a) check its HMAC, and\r
-    (b) check that the previous entry HMAC field matches the previous\r
-    entry.\r
-\item Check that the last-message entry for our machine matches the stored HMAC of our last message sent.\r
-\item For all other machines, check that the latest sequence number is\r
-at least as large (never goes backwards).\r
-\item That the queue has a current queue state entry.\r
-\item That the number of entries received is consistent with the size\r
-specified in the queue state entry.\r
-\end{enumerate}\r
-\r
-Key-value entries can span multiple slots.  They aren't valid until\r
-they are complete.\r
-\r
-\subsection{Resizing Queue}\r
-Client can make a request to resize the queue. This is done as a write that combines:\r
-  (a) a slot with the message, and (b) a request to the server. The queue can only be expanded, never contracted; attempting to decrease the size of the queue will cause future clients to throw an error.\r
-\r
-\subsection{Server Algorithm}\r
-$s \in SN$ is a sequence number\\\r
-$sv \in SV$ is a slot's value\\\r
-$slot_s = \tuple{s, sv} \in SL \subseteq SN \times SV$ \\ \\\r
-\textbf{State} \\\r
-\textit{SL = set of live slots on server} \\\r
-\textit{max = maximum number of slots (input only for resize message)} \\\r
-\textit{n = number of slots} \\ \\\r
-\textbf{Helper Function} \\\r
-$MaxSlot(SL_s)= \tuple{s, sv} \mid \tuple{s, sv}\r
-\in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s \geq s_s$ \\\r
-$MinSlot(SL_s)= \tuple{s, sv} \mid \tuple{s, sv} \r
-\in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s \leq s_s$ \\\r
-$SeqN(slot_s = \tuple{s, sv})=s$ \\\r
-$SlotVal(slot_s = \tuple{s, sv})=sv$ \\\r
 \r
-\begin{algorithmic}[1]\r
-\Function{GetSlot}{$s_g$}\r
-\State \Return{$\{\tuple{s, sv} \in SL \mid s \geq s_g\}$}\r
-\EndFunction\r
-\end{algorithmic}\r
 \r
-\begin{algorithmic}[1]\r
-\Function{PutSlot}{$s_p,sv_p,max'$}\r
-\If{$(max' \neq \emptyset)$}  \Comment{Resize}\r
-\State $max \gets max'$\r
-\EndIf\r
-\State $\tuple{s_n,sv_n} \gets MaxSlot(SL)$\Comment{Last sv}\r
-%\State $s_n \gets SeqN(\tuple{s_n,sv_n})$\r
-\If{$(s_p = s_n + 1)$}\r
-       \If{$n = max$}\r
-       \State $\tuple{s_m,sv_m} \gets MinSlot(SL)$\Comment{First sv}\r
-               \State $SL \gets SL - \{\tuple{s_m,sv_m}\}$\r
-       \Else \Comment{$n < max$}\r
-               \State $n \gets n + 1$\r
-       \EndIf\r
-    \State $SL \gets SL \cup \{\tuple{s_p,sv_p}\}$\r
-       \State \Return{$(true,\emptyset)$}\r
-\Else\r
-       \State \Return{$(false,\{\tuple{s,sv}\in SL \mid \r
-    s \geq s_p\})$}\r
-\EndIf\r
-\EndFunction\r
-\end{algorithmic}\r
+\setlength\parindent{0pt} % Removes all indentation from paragraphs - comment this line for an assignment with lots of text\r
+\r
+\r
+\section{\textbf{Introduction}}\r
+\r
+\section{\textbf{Client}}\r
+\r
+\subsection{\textbf{Client Notation Conventions}}\r
+\r
 \r
-\subsection{Client Algorithm}\r
-\subsubsection{Reading Slots}\r
-\textbf{Data Entry} \\\r
 $k$ is key of entry \\\r
 $v$ is value of entry \\\r
-$kv$ is a key-value entry $\tuple{k,v}$, $kv \in DE$ \\\r
-$ss$ is a slot sequence entry $\tuple{id,s_{last}}$, \r
-id + last s of a machine, $ss \in DE$ \\\r
-$qs$ is a queue state entry (contains $max$ size of queue), $qs \in DE$ \\\r
-$cr$ is a collision resolution entry $\tuple{s_{col},id_{col}}$, \r
-s + id of a machine that wins a collision, $cr \in DE$ \\\r
-$de$ is a data entry that can be a $kv$, $ss$, $qs$, or $cr$ \\\r
-$DE$ is a set of all data entries, possibly of different types, in a single message \\\r
-$s \in SN$ is a sequence number \\\r
-$id$ is a machine ID\\\r
+$size$ is a size (target size of the current block chain) \\\r
+$kv$ is a key-value pair $\tuple{k,v}$ \\\r
+$KV$ is a set of $kv$ \\\r
+$id$ is a machine ID \\\r
+$seq$ is a sequence number \\\r
 $hmac_p$ is the HMAC value of the previous slot \\\r
 $hmac_c$ is the HMAC value of the current slot \\\r
-$hmac_{p_g}$ is the HMAC value of the previous slot in procedure $\Call{ProcessSL}{}$ \\\r
-$hmac_{c_g}$ is the HMAC value of the current slot in procedure $\Call{ProcessSL}{}$ \\\r
-$Dat_s = \tuple{s,id,hmac_p,DE,hmac_c}$ \\\r
-$slot_s = \tuple{s, E(Dat_s)} = \r
-\tuple{s, E(\tuple{s,id,hmac_p,DE,hmac_c})}$ \\ \\\r
-\textbf{States} \\\r
-\textit{$d$ = delta between the last $s$ recorded and the first $s$ received} \\\r
-\textit{$id_{self}$ = machine Id of this client} \\\r
-\textit{$max_g$ = maximum number of slots (initially $max_g > 0$)} \\\r
-\textit{$sl_{last}$ = info of last slot in queue = \r
-       $\tuple{s_{last},sv_{last},id_{last}}$ (initially $\emptyset$)} \\\r
-\textit{DT = set of $\tuple{k,v}$ on client} \\\r
-\textit{MS = associative array of $\tuple{id, s_{last}}$ of all clients on client \r
-(initially empty)} \\\r
-\textit{$LV$ = live set of $kv$ entries on client, contains \r
-       $\tuple{kv,s}$ entries} \\\r
-\textit{$SS_{live}$ = live set of $ss$ entries on client} \\\r
-\textit{$CR_{live}$ = live set of $cr$ entries on client} \\\r
-\textit{$MS_g$ = set MS to save all $\tuple{id, s_{last}}$ pairs while\r
-traversing DT after a request to server (initially empty)} \\\r
-\textit{SK = Secret Key} \\\r
-\textit{$SM$ = associative array of $\tuple{s, id}$ of all slots in previous reads\r
-(initially empty)} \\ \\\r
-\textbf{Helper Functions} \\\r
-$MaxSlot(SL_s)= \tuple{s, sv}$ \textit{such that} $\tuple{s, sv}\r
-       \in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s \geq s_s$ \\\r
-$MinSlot(SL_s)= \tuple{s, sv}$ \textit{such that} $\tuple{s, sv} \r
-       \in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s \leq s_s$ \\\r
-$Slot(SL_s,s_s)= \tuple{s, sv}$ \textit{such that} $\tuple{s, sv} \r
-       \in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s = s_s$ \\\r
-$SeqN(\tuple{s, sv})=s$ \\\r
-$SlotVal(\tuple{s, sv})=sv$ \\\r
-$CreateLastSL(s,sv,id)=\tuple{s,sv,id}=sl_{last}$ \\\r
-$Decrypt(SK_s,sv_s)=Dat_s=\tuple{s,id,hmac_p,DE,hmac_c}$ \\\r
-$GetSeqN(Dat_s = \tuple{s,id,hmac_p,DE,hmac_c})=s$ \\\r
-$GetMacId(Dat_s = \tuple{s,id,hmac_p,DE,hmac_c})=id$ \\\r
-$GetPrevHmac(Dat_s = \tuple{s,id,hmac_p,DE,hmac_c})=hmac_p$ \\\r
-$GetCurrHmac(Dat_s = \tuple{s,id,hmac_p,DE,hmac_c})=hmac_c$ \\\r
-$GetDatEnt(Dat_s = \tuple{s,id,hmac_p,DE,hmac_c})=DE$ \\\r
-$GetLiveSS(SS_{live},ss_s)= ss$ \textit{such that} $ss \in SS_{live} \r
-       \wedge \forall ss_s \in SS_{live}, ss = ss_s$ \\\r
-$GetLiveCR(CR_{live},cr_s)= cr$ \textit{such that} $cr \in CR_{live} \r
-       \wedge \forall cr_s \in CR_{live}, cr = cr_s$ \\\r
-$GetLivEntLastS(LV_s,kv_s)= s$ \textit{such that} $\tuple{kv, s} \in LV_s \r
-       \wedge \forall \tuple{kv_s, s_s} \in LV_s, kv_s = kv$ \\\r
-$GetKV($key-value data entry$)=\tuple{k_s,v_s} = kv_s$ \\\r
-$GetSS($slot-sequence data entry$)=\tuple{id_s,s_{s_{last}}} = ss_s$ \\\r
-$GetCR($de$)=\tuple{s_s,id_s} = cr_s$ \\\r
-$Hmac(Dat_s,SK) = hmac_c$ \textit{value computed from $s$, $id$,\r
-$hmac_p$, and $DE$ taken from $Dat_s$} \\\r
-$IsKv(de) = true$ \textit{if $de$ is a $kv$, false otherwise} \\\r
-$IsSs(de) = true$ \textit{if $de$ is a $ss$, false otherwise} \\\r
-$IsQs(de) = true$ \textit{if $de$ is a $qs$, false otherwise} \\\r
-$IsCr(de) = true$ \textit{if $de$ is a $cr$, false otherwise} \\\r
-$GetKey(kv)=k$\Comment{$kv = \tuple{k, v}$} \\\r
-$GetVal(kv)=v$ \\\r
-$GetId(ss)=id$\Comment{$ss = \tuple{id, s_{last}}$} \\\r
-$GetSLast(ss)=s_{last}$ \\\r
-$GetS(cr)=s$\Comment{$cr = \tuple{s, id}$} \\\r
-$GetId(cr)=id$ \\\r
-$GetLastS(sl_{last})=s$\Comment{$sl_{last} = \tuple{s,sv,id}$} \\\r
-$GetSV(sl_{last})=sv$ \\\r
-$GetID(sl_{last})=id$ \\\r
-$GetKeyVal(DT_s,k_s)= \tuple{k, v}$ \textit{such that} $\tuple{k, v} \r
-       \in DT_s \wedge \forall \tuple{k_s, v_s} \in DT_s, k = k_s$ \\\r
-$MaxLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s \r
-       \wedge \forall \tuple{id_s, s_{s_{last}}} \in MS_s, s_{last} \geq s_{s_{last}}$ \\\r
-$MinLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s \r
-       \wedge \forall \tuple{id_s, s_{s_{last}}} \in MS_s, s_{last} \leq s_{s_{last}}$ \\\r
-$MinCRSeqN(CR_s)= s$ \textit{such that} $\tuple{s, id} \in CR_s \r
-       \wedge \forall \tuple{s_s, id_s} \in CR_s, s \leq s_s$ \\\r
-$MaxSMSeqN(SM_s)= s$ \textit{such that} $\tuple{s, id} \in SM_s \r
-       \wedge \forall \tuple{s_s, id_s} \in SM_s, s \geq s_s$ \\\r
+$Guard$ is a set of$ \tuple{k,v,$logical operator$}$ which can be evaluated to a boolean \\\r
 \r
-\begin{algorithmic}[1]\r
-\Procedure{Error}{$msg$}\r
-\State $Print(msg)$\r
-\State $Halt()$\r
-\EndProcedure\r
-\end{algorithmic}\r
+$trans$ is a transaction entry , $\tuple{seq, KV, Guard}$  \\\r
+$lastmsg$ is a last message entry, $\tuple{seq, id}$ \\\r
+$qstate$ is a queue state entry, $\tuple{size}$ \\\r
+$colres$ is a collision resolution entry, $\tuple{id, seq_{old}, seq_{new}, true \lor false}$ \\\r
+$newkey$ is a new key entry, $\tuple{seq, k, id}$, $id$ is ID of arbitrator \\\r
+$commit$ is a commit transaction entry, $\tuple{seq_{trans},KV}$, id is id of arbitrator \\\r
+$abort$ is an abort transaction entry, $\tuple{seq_{abrt},seq_{trans},id_{trans}}$ \\\r
 \r
-\begin{algorithmic}[1]\r
-\Function{GetQueSta}{$DE_s$}\r
-\State $qs_{de} \gets qs$ \textit{such that} $qs \in DE_s, \r
-       de_s \in D \land IsQs(de_s)$\r
-\If{$qs_{de} \neq \emptyset$}\r
-       \State $qs_{ret} \gets qs_{de})$\r
-\Else\r
-       \State $qs_{ret} \gets \emptyset$\r
-\EndIf\r
-\State \Return{$qs_{ret}$}\r
-\EndFunction\r
-\end{algorithmic}\r
 \r
+$de$ is a data entry that can one of: $trans$, $lastmsg$, $qstate$, $colres$, $newkey$, $commit$, $abort$ \\\r
+$DE$ is a set of all data entries, possibly of different types, in a single message, set of $de$\\\r
+\r
+$slotDat = \tuple{seq,id,DE,hmac_p,hmac_c}$ \\\r
+$slot = \tuple{seq, Encrpt(slotDat)}$\\\r
+\r
+\subsection{\textbf{Client State}}\r
+\r
+\subsubsection{Constants}\r
+$LOCAL\_ID$ = machine ID of this client.\\\r
+$RESIZE\_THRESH\_PERCENT$ = percent of slots that need to have live data to trigger a resize.\\\r
+$RESIZE\_PERCENT$ = percent that we should grow the block chain to.\\\r
+$DATA\_ENTRY\_SET\_MAX\_SIZE$ = max size that a data entry set can have (in bytes).\\\r
+$DEAD\_SLOT\_COUNT$ = number of slots to keep dead if possible at the end of the block chain.\\\r
+$MAX\_RESCUE\_SKIPS$ = number of skips that are allowed when saving data entries.\\\r
+\r
+\subsubsection{Primitive Variables}\r
+$max\_size$ = max size of the block chain\\\r
+\r
+\subsubsection{Sets and Lists}\r
+\r
+\r
+$PendingTrans= \tuple{KV, Guard} = \tuple{$set of key value pairs, set of guard conditions$}$.\\\r
+$Arbitrator$ = set of $\tuple{k,id}$ containing the key and its arbitrating device.\\\r
+$LastSlot$ = set of $\tuple{id, seq}$ containing the machine ID and the largest sequence number from that machine ID.\\\r
+$LocalSlots$ = set of slots that are in the clients local buffer (initially $\emptyset$), data is decrypted.\\\r
+$RejectedSlotList$ = ordered list of the sequence numbers of slots that this client tried to insert but were rejected.\\\r
+\r
+\r
+\subsection{Helper Functions}\r
+The following helper functions are needed:\\\r
+\r
+% Get Size\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Get Byte Size:}\\\r
+Get the size in bytes of the thing that is passed in.\\\r
 \begin{algorithmic}[1]\r
-\Function{GetSlotSeq}{$DE_s$}\r
-\State $DE_{ss} \gets \{de | de \in DE_s \land IsSs(de)\}$\r
-\State \Return{$DE_{ss}$}\r
+\Function{GetSize}{$a$}\r
+    \State \Return{Size in bytes of $a$}\r
 \EndFunction\r
-\end{algorithmic}\r
+\end{algorithmic}\end{varwidth}% \r
+}\r
 \r
+% Error\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{ Error:}\\\r
+Prints an error message and halts the execution of the client.\\\r
 \begin{algorithmic}[1]\r
-\Function{GetColRes}{$DE_s$}\r
-\State $DE_{cr} \gets \{de | de \in DE_s \land IsCr(de)\}$\r
-\State \Return{$DE_{cr}$}\r
+\Function{Error}{$msg$}\r
+    \State $Print(msg)$\r
+    \State $Halt()$\r
 \EndFunction\r
-\end{algorithmic}\r
+\end{algorithmic}\end{varwidth}% \r
+}\r
 \r
+% Get Next Sequence Number\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Get Next Sequence Number:}\\\r
+Get the next sequence number for insertion into the block chain.\\\r
 \begin{algorithmic}[1]\r
-\Function{UpdateLastSeqN}{$id_s,s_s,MS_s$}\r
-\State $s_t \gets MS_s[id_s]$\r
-\If{$s_t = \emptyset$}\r
-       \State $MS_s[id_s] = s_s$  \Comment{First occurrence}\r
-\Else\r
-       \If{$id_s = id_{self}$}\r
-               \If{$s_t \neq s_s$}\Comment{Check for mismatch on $s$}\r
-                       \State \Call{Error}{'Mismatch on $s$ for $id_{self}$'}\r
-               \EndIf\r
-       \Else\r
-               \If{$s_t > s_s$}\Comment{Check for rollback on $s$}\r
-                       \State \Call{Error}{'Rollback on $s$ for $id_s$'}\r
-               \EndIf\r
-       \EndIf\r
-       \State $MS_S[id_s] \gets max(s_t, s_s)$\r
-\EndIf\r
-\State \Return{$MS_s$}\r
+\Function{GetNextSeq}{$k$}\r
+    \LeftComment{Get the largest known sequence number}\r
+    \State $seq_{ret} \gets seq$ such that $\tuple{seq, DE}\in LocalSlots \land (\forall \tuple{seq', DE'} \in LocalSlots, seq \geq seq')$\\\r
+    \r
+    \LeftComment{Add one to the largest seq number to generate the new seq number}\r
+    \State \Return{$seq_{ret} + 1$}\r
 \EndFunction\r
 \end{algorithmic}\r
+\end{varwidth}% \r
+}\r
 \r
+% Get Arbitrator\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Get Arbitrator:}\\\r
+Get the arbitrator for a given key.\\\r
 \begin{algorithmic}[1]\r
-\Function{UpdateKVLivEnt}{$LV_s,kv_s,s_s$}\r
-\State $s_t \gets GetLivEntLastS(LV_s,kv_s)$\r
-\If{$s_t = \emptyset$}\r
-       \State $LV_s \gets LV_s \cup \{\tuple{kv_s,s_s}\}$\Comment{First occurrence}\r
-\Else\r
-       \If{$s_s > s_t$}\Comment{Update entry with a later s}\r
-               \State $LV_s \gets (LV_s - \{\tuple{kv_s,s_t}\}) \cup \r
-                       \{\tuple{kv_s,s_s}\}$\r
-       \EndIf\r
-\EndIf\r
-\State \Return{$LV_s$}\r
+\Function{GetArbitrator}{$k$}\r
+    \State $\tuple{k_1,id_1} \gets \tuple{k_2,id_2} $ \textit{such that} $ \tuple{k_2,id_2} \in Arbitrator \land k_2=k$    \r
+    \State \Return{$id_1$}\r
 \EndFunction\r
 \end{algorithmic}\r
+\end{varwidth}% \r
+}\r
+\r
+% Check Transaction arbitrator\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Check Arbitrator for a Transaction:}\\\r
+Check that the arbitrators for a given set are all the same arbitrator.\\\r
+\begin{algorithmic}[1]\r
+\Function{CheckArbitrator}{$PendingTrans_a$}\r
+    \State $id_{arb} \gets NULL$\\\r
+    \State $\tuple{KV_a, Guard_a} \gets PendingTrans_a$\r
+    \r
+    \ForAll{$\tuple{k',v'} \in KV_a$}\r
+        \State $id' \gets$ \Call{GetArbitrator}{$k'$}\\\r
+        \r
+        \If{$id_{arb} = NULL$}  \r
+            \State $id_{arb} \gets id'$\r
+        \ElsIf{$id' \neq id_{arb}$} \Comment{Check all arbitrators are the same}\r
+            \State \Call{Error}{"Multiple arbitrators for key values in transaction."}\r
+        \EndIf\r
+    \EndFor\r
+    \r
+    \ForAll{$\tuple{k',v', lop'} \in Guard_a$}\r
+        \State $id' \gets$ \Call{GetArbitrator}{$k'$}\\\r
+        \r
+        \If{$id_{arb} = NULL$}  \r
+            \State $id_{arb} \gets id'$\r
+        \ElsIf{$id' \neq id_{arb}$} \Comment{Check all arbitrators are the same}\r
+            \State \Call{Error}{"Multiple arbitrators for key values in transaction."}\r
+        \EndIf\r
+    \EndFor\r
+\EndFunction\r
+\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
 \r
+% Get all Commits\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Get all Commits:}\\\r
+Get all commits that are currently in the local block chain.  Iterate over all the local slots and extract all the commits from each slot.\\\r
 \begin{algorithmic}[1]\r
-\Function{AddSSLivEnt}{$SS_{s_{live}},de_s$}\r
-\State $ss_s \gets GetSS(de_s)$\r
-\State $ss_t \gets GetLiveSS(SS_{s_{live}},ss_s)$\r
-\If{$ss_t = \emptyset$}\r
-       \State $SS_{s_{live}} \gets SS_{s_{live}} \cup \{ss_s\}$\Comment{First occurrence}\r
-\EndIf\r
-\State \Return{$SS_{s_{live}}$}\r
+\Function{GetCommits}{$ $}\r
+    \State $ComSet \gets \emptyset$ \Comment{Set of the commits}\\\r
+        \r
+    \LeftComment{Iterate over all the slots saved locally}\r
+    \ForAll{$\tuple{s_1', \tuple{seq_2',id',DE',hmac_p',hmac_c'}} \in LocalSlots$}\r
+        \State $ComSet \gets ComSet \cup \{c |c \in DE',c$is a $commit\}$\r
+    \EndFor\r
+    \State \Return{$ComSet$}\r
 \EndFunction\r
 \end{algorithmic}\r
+\end{varwidth}% \r
+}\r
 \r
+% Get all aborts\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Get all aborts:}\\\r
+Get all aborts that are currently in the local block chain.  Iterate over all the local slots and extract all the aborts from each slot.\\\r
 \begin{algorithmic}[1]\r
-\Function{AddCRLivEnt}{$CR_{s_{live}},cr_s$}\r
-\State $cr_t \gets GetLiveCR(CR_{s_{live}},cr_s)$\r
-\If{$cr_t = \emptyset$}\r
-       \State $CR_{s_{live}} \gets CR_{s_{live}} \cup \{cr_s\}$\Comment{First occurrence}\r
-\EndIf\r
-\State \Return{$CR_{s_{live}}$}\r
+\Function{GetAborts}{$ $}\r
+    \State $AbrtSet \gets \emptyset$ \Comment{Set of the aborts}\\\r
+        \r
+    \LeftComment{Iterate over all the slots saved locally}\r
+    \ForAll{$\tuple{s_1', \tuple{seq_2',id',DE',hmac_p',hmac_c'}} \in LocalSlots$}\r
+        \State $AbrtSet \gets AbrtSet \cup \{c |c \in DE',c$is a $abort\}$\r
+    \EndFor\r
+    \State \Return{$AbrtSet$}\r
 \EndFunction\r
 \end{algorithmic}\r
+\end{varwidth}% \r
+}\r
 \r
+% Get all Queue States\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Get all queue states:}\\\r
+Get all qstates that are currently in the local block chain.  Iterate over all the local slots and extract all the qstates from each slot.\\\r
 \begin{algorithmic}[1]\r
-\Function{UpdateSSLivEnt}{$SS_{s_{live}},MS_s$}\r
-\State $s_{s_{min}} \gets MinLastSeqN(MS_s)$\r
-\ForAll{$ss_s \in SS_{s_{live}}$}\r
-       \State $s_{s_{last}} \gets GetSLast(ss_s)$\r
-       \If{$s_{s_{min}} > s_{s_{last}}$}\Comment{Remove if dead}\r
-               \State $SS_{s_{live}} \gets SS_{s_{live}} - \{ss_s\}$           \r
-       \EndIf\r
-\EndFor\r
-\State \Return{$SS_{s_{live}}$}\r
+\Function{GetQStates}{$ $}\r
+    \State $QSet \gets \emptyset$ \Comment{Set of the qstates}\\\r
+        \r
+    \LeftComment{Iterate over all the slots saved locally}\r
+    \ForAll{$\tuple{s_1', \tuple{seq_2',id',DE',hmac_p',hmac_c'}} \in LocalSlots$}\r
+        \State $QSet \gets QSet \cup \{c |c \in DE',c$is a $qstate\}$\r
+    \EndFor\r
+    \State \Return{$QSet$}\r
 \EndFunction\r
 \end{algorithmic}\r
+\end{varwidth}% \r
+}\r
 \r
+% Check Queue State Live\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Check Queue State Live:}\\\r
+A queue state is dead if there is another queue state data entry that has a larger queue state.\\\r
 \begin{algorithmic}[1]\r
-\Function{UpdateCRLivEnt}{$CR_{s_{live}},MS_s$}\r
-\State $s_{s_{min}} \gets MinLastSeqN(MS_s)$\r
-\ForAll{$cr_s \in CR_{s_{live}}$}\r
-       \State $s_s \gets GetS(cr_s)$\r
-       \If{$s_{s_{min}} > s_s$}\Comment{Remove if dead}\r
-               \State $CR_{s_{live}} \gets CR_{s_{live}} - \{cr_s\}$   \r
-       \EndIf\r
-\EndFor\r
-\State \Return{$CR_{s_{live}}$}\r
+\Function{CheckQStateLive}{$qstate_a$}\r
+    \State $\tuple{size_a} \gets qstate_a$\r
+    \State $AllQStates \gets$ \Call{GetQState}{} \Comment{Get all the qstates} \\\r
+    \r
+    \If{$\exists \tuple{size'} \in AllQStates, size' > size_a$}\r
+        \State \Return{false}\r
+    \EndIf\r
+    \State \Return{true}\r
+    \r
 \EndFunction\r
 \end{algorithmic}\r
+\end{varwidth}% \r
+}\r
 \r
+% Check Commit Live\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Check Commit Live:}\\\r
+A commit is dead if for every key value pair in the commit there is a commit with a larger transaction sequence number that has a key value pair with the same key.\\\r
+\begin{algorithmic}[1]\r
+\Function{CheckCommitLive}{$commit_a$}\r
+    \State $\tuple{seq_{a_{trans}},KV_a} \gets commit_a$\r
+    \State $KSet \gets \{k|\tuple{k,v} \in KV\}$\r
+    \State $AllCommits \gets$ \Call{GetCommits}{} \Comment{Get all the commits} \\\r
+    \r
+    \LeftComment{Iterate all commits that are newer in time}\r
+    \ForAll{$\tuple{seq_{trans}',KV'}\in AllCommits, seq_{trans}' > seq_{a_{trans}}$}\r
+        \State $KVSet \gets KVSet \setminus \{k|\tuple{k,v} \in KV'\}$\\\r
+        \r
+        \If{$KVSet = \emptyset$}\r
+            \State \Return{false} \Comment{All keys have a newer commit}\r
+        \EndIf\r
+    \EndFor\r
+    \State \Return{true} \Comment{If got here then some keys still live}\r
+\EndFunction\r
+\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
+\r
+% Check Last Message Live\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Check Last Message Live:}\\\r
+The last message is dead if the device in question pushed a slot that has a larger sequence number than the one recorded in the last message data entry. \\\r
 \begin{algorithmic}[1]\r
-\Function{UpdateSM}{$SM_s,CR_s$}\Comment{Remove if dead}\r
-\State $s_{cr_{min}} \gets MinCRSeqN(CR_s)$\r
-       \State $SM_s \gets SM_s - \{\tuple{s_s,id_s} \mid \tuple{s_s,id_s}\r
-               \in SM_s \wedge s_s < s_{cr_{min}}\}$\r
-\State \Return{$CR_{s_{live}}$}\r
+\Function{CheckLastMsgLive}{$lastmsg_a$}\r
+    \State $\tuple{seq_a, id_a} \gets lastmsg_a$\\\r
+    \r
+    \If{$\exists \tuple{id', seq'} \in LastSlot, id'=id_a \land seq' > seq_a$}\r
+        \State \Return{false}\r
+    \EndIf\r
+    \State \Return{True}    \r
 \EndFunction\r
 \end{algorithmic}\r
+\end{varwidth}% \r
+}\r
 \r
+%Check Collision Resolution Live\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Check Collision Resolution Live:}\\\r
+Check if a collision resolution data entry is live or not.  This done by checking if all clients that we know about have seen the collision resolution entry.  This is checked by seeing if all devices have inserted a message with a larger sequence number into the block chain.\\\r
 \begin{algorithmic}[1]\r
-\Procedure{CheckLastSeqN}{$MS_s,MS_t,d$}\r
-\For {$\tuple{id, s_t}$ in $MS_t$}\Comment{Check $MS_t$ based on the newer $MS_s$}\r
-       \State $s_s \gets MS_s[id]$\r
-       \If{$d \land s_s = \emptyset$}\r
-       \State \Call{Error}{'Missing $s$ for machine $id$'}\r
-       \ElsIf{$id = id_{self}$ and $s_s \neq s_t$}\r
-               \State \Call{Error}{'Invalid last $s$ for this machine'}\r
-       \ElsIf{$id \neq id_{self}$ and $s_{s_{last}} < s_{t_{last}}$}\r
-       \State \Call{Error}{'Invalid last $s$ for machine $id$'}\r
-    \Else\r
-               \State $MS_t[id] \gets s_s$\r
-       \EndIf\r
-\EndFor\r
-\EndProcedure\r
+\Function{CheckColResLive}{$colres_a$}\r
+    \State $\tuple{id_a, seq_{a_{old}}, seq_{a_{new}}, equal_a} \gets colres_a$\\\r
+    \r
+    \If{$\forall \tuple{id', seq'} \in LastSlot, seq' \geq seq_{a_{new}}$}\r
+        \State \Return{false}\r
+    \EndIf\r
+    \State \Return{true}\r
+\EndFunction\r
 \end{algorithmic}\r
+\end{varwidth}% \r
+}\r
 \r
+% Check New Key Live\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Check New Key Live:}\\\r
+A new key data entry is always live.\\\r
 \begin{algorithmic}[1]\r
-\Procedure{CheckCollision}{$MS_s,SM_s,cr_s$}\r
-\If{$cr_s \neq \emptyset$}\r
-       \State $s_s \gets GetS(cr_s)$\r
-       \State $id_s \gets GetId(cr_s)$\r
-       \State $s_{s_{last}} \gets GetLastSeqN(MS_s,id_s)$\r
-       \If{$s_{s_{last}} < s_s$}\r
-               \State $id_t \gets SM_s[s_s]$\r
-               \If{$id_s \neq id_t$}\r
-                       \State \Call{Error}{'Invalid $id$ for this slot update'}\r
-               \EndIf\r
-       \EndIf\r
-\EndIf\r
-\EndProcedure\r
+\Function{CheckNewkeyLive}{$newkey_a$}\r
+    \State \Return{True}    \r
+\EndFunction\r
 \end{algorithmic}\r
+\end{varwidth}% \r
+}\r
 \r
+% Check Abort Live\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Check Abort Live:}\\\r
+Check if an abort data entry is live or not.  Abort is dead if the device whos transaction was aborted sees the abort.  This is checked by seeing if that device inserted a slot into the block chain which has a sequence number that is larger than the aborts sequence number.\\\r
 \begin{algorithmic}[1]\r
-\Function{ValidSlotsRange}{$s_{s_{min}}$}\r
-\State $s_{s_{last}} \gets MaxSMSeqN(SM)$\r
-\If{$s_{s_{min}} \leq s_{s_{last}}$}\r
-       \State \Call{Error}{'Server sent old slots'}\r
-\EndIf\r
-\State \Return{$s_{s_{min}} > s_{s_{last}} + 1$}\r
+\Function{CheckAbortLive}{$abort_a$}\r
+    \State $\tuple{seq_{a_{abrt}}, seq_{a_{trans}},id_a} \gets abort_a$\\\r
+    \r
+    \LeftComment{The device whos transaction was aborted saw the abort}\r
+    \If{$\exists \tuple{id', seq'} \in LastSlot, id'=id_a \land seq' > seq_{a_{abrt}}$}\r
+        \State \Return{false}\r
+    \EndIf\r
+    \State \Return{True}    \r
 \EndFunction\r
 \end{algorithmic}\r
+\end{varwidth}% \r
+}\r
 \r
-\begin{algorithmic}[1]\r
-\Procedure{CheckNumSlots}{$|SL_s|,sz_s$}\r
-\If{$|SL_s| \neq sz_s$}\r
-       \State \Call{Error}{'Actual number of slots does not match expected'}\r
-\EndIf\r
-\EndProcedure\r
-\end{algorithmic}\r
+% Check Transaction Live\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Check Transaction Live:}\\\r
+A transaction is dead if there is an abort for that transaction or if there is a commit for that transaction or a transaction that came after this transaction.  Since transactions must be commited in order of there insertion, seeing a transaction that is commited and has a larger sequence number than the transaction in question means that the transaction in question was commited at some point.\\\r
+\begin{algorithmic}[1]\r
+\Function{CheckTransLive}{$trans_a$}\r
+    \State $\tuple{seq_a, KV_a, Guard_a} \gets trans_a$\r
+    \State $AllCommits \gets$ \Call{GetCommits}{} \Comment{Get all the commits}\r
+    \State $AllAborts \gets$ \Call{GetAborts}{} \Comment{Get all the aborts} \\\r
+    \r
+    \If{$\exists \tuple{seq_{abrt}',seq_{trans}',id'} \in AllAborts, seq_{trans}' = seq_a$}\r
+        \State \Return{false}\r
+    \ElsIf{$\exists \tuple{seq_{trans}',KV'} \in AllCommits, seq_{trans}' \geq seq_a$}\r
+        \State \Return{false}\r
+    \EndIf\r
+    \State \Return{true}\r
+\EndFunction\r
+\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
 \r
-\begin{algorithmic}[1]\r
-\Function{StoreLastSlot}{$MS_s,sl_l,s_s,sv_s,id_s$}\r
-\State $s_{min} \gets MinLastSeqN(MS_s)$\r
-\If{$s_{min} \neq \emptyset \land s_{min} = s_s$}\Comment{$MS$ initially empty}\r
-       \State $sl_l \gets CreateLastSL(s_s,sv_s,id_s)$\r
-\EndIf\r
-\State \Return{$sl_l$}\r
+% Check Live\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Check Live:}\\\r
+Checks if a data entry is live based on its type.\\\r
+\begin{algorithmic}[1]\r
+\Function{CheckLive}{$datentry$}\r
+    \If{$datentry$ is a $commit$}\r
+        \State \Return{\Call{CheckCommitLive}{$datentry$}}\\r
+    \ElsIf{$datentry$ is a $abort$}\r
+        \State \Return{\Call{CheckAbortLive}{$datentry$}}\\r
+    \ElsIf{$datentry$ is a $trans$}\r
+        \State \Return{\Call{CheckTransLive}{$datentry$}}\\r
+    \ElsIf{$datentry$ is a $lastmsg$}\r
+        \State \Return{\Call{CheckLastMsgLive}{$datentry$}}\\r
+    \ElsIf{$datentry$ is a $colres$}\r
+        \State \Return{\Call{CheckColResLive}{$datentry$}}\\r
+    \ElsIf{$datentry$ is a $qstate$}\r
+        \State \Return{\Call{CheckQStateLive}{$datentry$}}\r
+    \ElsIf{$datentry$ is a $newkey$}\r
+        \State \Return{\Call{CheckNewkeyLive}{$datentry$}}\r
+    \Else\r
+        \State \Call{Error}{"Unknown data entry type."}\r
+    \EndIf\r
 \EndFunction\r
 \end{algorithmic}\r
+\end{varwidth}% \r
+}\r
+\r
+% Slot Has Live\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Slot Has Live:}\\\r
+Check if the slot has any live data entries in it. Do this by looking at all the data entries in the slot and checking if they are live\\\r
+\begin{algorithmic}[1]\r
+\Function{SlotHasLive}{$slot_a$}\r
+    \State $\tuple{s_1, \tuple{seq_2,id,DE,hmac_p,hmac_c}} \in LocalSlots$\r
+    \r
+    \ForAll{$datentry \in DE$}\r
+        \If{\Call{CheckLive}{$datentry$}} \Comment{an entry is alive}\r
+            \State \Return{true}\r
+        \EndIf\r
+    \EndFor\r
+    \r
+    \State \Return{false} \Comment{All entries were dead}    \r
+\EndFunction\r
+\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
 \r
+% Calculate Resize Threshold\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Calculate Resize Threshold:}\\\r
+Calculate a threshold for how many slots need to have live data entries in them for a resize to take place.\\\r
 \begin{algorithmic}[1]\r
-\Function{ValidHmacChain}{$Dat_s,s_s,hmac_{p_s},sl_l$}\r
-       \State $hmac_{p_{stored}} \gets GetPrevHmac(Dat_s)$\r
-       \If {$ \neg(s_s = 0 \land hmac_{p_s} = 0)$}\r
-               \State $s_l \gets GetLastS(sl_l)$\r
-               \If {$(s_s > s_l + 1) \land (hmac_{p_{stored}} \neq hmac_{p_s})$}\r
-                       \State \Call{Error}{'Invalid previous HMAC value'}\r
-               \EndIf\r
-       \EndIf\r
-       \If{$Hmac(Dat_s,SK) \neq GetCurrHmac(Dat_s)$ }\r
-               \State \Call{Error}{'Invalid current HMAC value'}\r
-       \EndIf\r
-       \State $hmac_{p_s} \gets Hmac(Dat_s,SK)$\Comment{Update $hmac_{p_s}$ for next check}\r
-\State \Return{$hmac_{p_s}$}\r
+\Function{CalcResizeThresh}{$maxsize$}\r
+    \State \Return{$\left \lfloor {maxsize * RESIZE\_THRESH\_PERCENT} \right \rfloor$}\r
 \EndFunction\r
 \end{algorithmic}\r
+\end{varwidth}% \r
+}\r
 \r
+% Calculate Block Chain New Size\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Calculate Block Chain New Size:}\\\r
+Calculate the new size of the block chain which we need if we are to resize the data structure.\\\r
 \begin{algorithmic}[1]\r
-\Function{UpdateDT}{$DT_s,DE_s,LV_s,s_s$}\r
-\State $DE_{s_{kv}} \gets \{de_s | de_s \in DE_s \land IsKv(de_s)\}$\r
-\ForAll{$de_s \in DE_{s_{kv}}$}\r
-       \State $kv_s \gets GetKV(de_s)$\r
-       \State $LV_s \gets \Call{UpdateKVLivEnt}{LV_s,kv_s,s_s}$\r
-       \State $k_s \gets GetKey(kv_s)$\r
-       \State $\tuple{k_s,v_t} \gets GetKeyVal(DT_s,k_s)$\r
-       \If{$\tuple{k_s,v_t} = \emptyset$}\r
-               \State $DT_s \gets DT_s \cup \{\tuple{k_s,v_s}\}$\r
-       \Else\r
-               \State $DT_s \gets (DT_s - \{\tuple{k_s,v_t}\}) \cup \r
-                       \{\tuple{k_s,v_s}\}$\r
-       \EndIf\r
-\EndFor\r
-\State \Return{$DT_s$}\r
+\Function{CalcNewSize}{$maxsize$}\r
+    \State \Return{$\left \lceil {maxsize * RESIZE\_THRESH\_PERCENT} \right \rceil$}\r
 \EndFunction\r
 \end{algorithmic}\r
+\end{varwidth}% \r
+}\r
 \r
+% Should Resize\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Should Resize:}\\\r
+Check if the block should resize based on some metric of how many slots in the block chain are filled with live data. \\\r
 \begin{algorithmic}[1]\r
-\Function{InitExpSize}{$s_{min}$}\r
-\If{$s_{min} < max_g$}\Comment{Check whether $SL$ is full on server}\r
-       \State $sz_s \gets s_{min}$\r
-\Else\r
-       \State $sz_s \gets max_g$\r
-\EndIf\r
-\State \Return{$sz_s$}\r
+\Function{ShouldResize}{$ $}\r
+    \State $LiveSlots \gets \{slot_s|slot_s \in LocalSlots \land $\Call{SlotHasLive}{$slot_s$}$\}$\r
+    \State $resizethreshold \gets $ \Call{CalcResizeThresh}{$max\_size$}\r
+    \State \Return{$|LiveSlots| \geq resizethreshold$} \Comment{If passes threshold then resize}\r
 \EndFunction\r
 \end{algorithmic}\r
+\end{varwidth}% \r
+}\r
 \r
+% Create Queue State \r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Create Queue State:}\\\r
+Generate a queue state data entry.\\\r
 \begin{algorithmic}[1]\r
-\Function{UpdateExpSize}{$sz_s$}\r
-\State $sz_s \gets sz_s + 1$\r
-\If{$sz_s > max_g$}\Comment{Expected size $\leq max_g$}\r
-       \State $sz_s \gets max_g$\r
-\EndIf\r
-\State \Return{$sz_s$}\r
+\Function{CreateQState}{$size_a$}\r
+    \State \Return{$\tuple{size_a}$}    \r
 \EndFunction\r
 \end{algorithmic}\r
+\end{varwidth}% \r
+}\r
 \r
+% Generate Transaction\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Create Transaction:}\\\r
+Generate a transaction data entry.\\\r
 \begin{algorithmic}[1]\r
-\Function{UpdateQS}{$Dat_s,max_s$}\r
-\State $DE_s \gets GetDatEnt(Dat_s)$\r
-\State $qs_s \gets \Call{GetQueSta}{DE_s}$\Comment{Handle qs}\r
-\If{$qs_s \neq \emptyset \land qs_s > max_s$}\r
-       \State $max_s \gets qs_s$\r
-\EndIf\r
-\State \Return{$max_s$}\r
+\Function{CreateTrans}{$pendingtrans_a, seq_a$}\r
+    \State $\tuple{KV_a, Guard_a} \gets pendingtrans_a$\r
+    \State \Return{$\tuple{seq_a, KV_a, Guard_a}$}    \r
 \EndFunction\r
 \end{algorithmic}\r
+\end{varwidth}% \r
+}\r
 \r
-\begin{algorithmic}[1]\r
-\Procedure{UpdateCR}{$DE_s$}\r
-\State $DE_{s_{cr}} \gets \Call{GetColRes}{DE_s}$\Comment{Handle cr}\r
-\If{$DE_{s_{cr}} \neq \emptyset$}\r
-       \ForAll{$de_{s_{cr}} \in DE_{s_{cr}}$}\r
-               \State $cr_s \gets GetCR(de_{s_{cr}})$\r
-               \State $\Call{CheckCollision}{MS,SM,cr_s}$\r
-               \State $CR_{live} \gets \Call{AddCRLivEnt}{CR_{live},cr_s}$\r
-       \EndFor\r
-\EndIf\r
-\EndProcedure\r
-\end{algorithmic}\r
 \r
+% Data Entry Set Has Space \r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Data Entry Set Has Space :}\\\r
+Checks if a data entry set has enough space for a new data entry to be inserted.\\\r
 \begin{algorithmic}[1]\r
-\Function{UpdateSS}{$DE_s,MS_s$}\r
-\State $DE_{s_{ss}} \gets \Call{GetSlotSeq}{DE_s}$\Comment{Handle ss}\r
-\If{$DE_{s_{ss}} \neq \emptyset$}\r
-       \ForAll{$de_{s_{ss}} \in DE_{s_{ss}}$}\r
-               \State $\tuple{id_d,s_{d_{last}}} \gets GetSS(de_{s_{ss}})$\r
-               \State $MS_s \gets \Call{UpdateLastSeqN}{id_d,s_{d_{last}},MS_s}$\r
-               \State $SS_{live} \gets \Call{AddSSLivEnt}{SS_{live},de_{s_{ss}}}$\r
-       \EndFor\r
-\EndIf\r
-\State \Return{$MS_s$}\r
+\Function{DEHasSpace}{$DE_a, de_a$}\r
+    \State $newsize \gets $ \Call{GetSize}{$DE_a$}\r
+    \State $newsize \gets newsize +$ \Call{GetSize}{$de_a$}\r
+    \State \Return{$newsize \leq DATA\_ENTRY\_SET\_MAX\_SIZE$}\r
 \EndFunction\r
 \end{algorithmic}\r
+\end{varwidth}% \r
+}\r
 \r
-\begin{algorithmic}[1]\r
-\Procedure{ProcessSL}{$SL_g$}\r
-\State $MS_g \gets \emptyset$\r
-\State $\tuple{s_{g_{min}},sv_{g_{min}}} \gets MinSlot(SL_g)$\r
-\State $\tuple{s_{g_{max}},sv_{g_{max}}} \gets MaxSlot(SL_g)$\r
-\State $d \gets \Call{ValidSlotsRange}{s_{g_{min}}}$\r
-\State $sz \gets \Call{InitExpSize}{s_{g_{min}}}$\r
-\For{$s_g \gets s_{g_{min}}$ \textbf{to} $s_{g_{max}}$}\Comment{Process slots \r
-       in $SL_g$ in order}\r
-       \State $\tuple{s_g,sv_g} \gets Slot(SL_g,s_g)$\r
-       \State $Dat_g \gets Decrypt(SK,sv_g)$\r
-       \State $id_g \gets GetMacId(Dat_g)$\r
-       \State $SM \gets SM \cup \{\tuple{s_g,id_g}\}$\r
-       \State $s_{g_{in}} \gets GetSeqN(Dat_g)$\r
-    \If{$s_g \neq s_{g_{in}}$}\r
-               \State \Call{Error}{'Invalid sequence number'}\r
-       \EndIf\r
-       \State $hmac_{p_g} \gets \Call{ValidHmacChain}{Dat_g,s_g,hmac_{p_g},sl_{last}}$\r
-       \State $sz \gets \Call{UpdateExpSize}{sz}$\r
-       \State $max_g \gets \Call{UpdateQS}{Dat_g,max_g}$\Comment{Handle qs}\r
-       \State $MS_g \gets \Call{UpdateLastSeqN}{id_g,s_g,MS_g}$\Comment{Handle last s}\r
-       \State $MS_g \gets \Call{UpdateSS}{DE_g,MS_g}$\Comment{Handle ss}\r
-       %\State $DE_{g_{ss}} \gets \Call{GetSlotSeq}{DE_g}$\Comment{Handle ss}\r
-       %\If{$DE_{g_{ss}} \neq \emptyset$}\r
-       %       \ForAll{$de_{g_{ss}} \in DE_{g_{ss}}$}\r
-       %               \State $\tuple{id_d,s_{d_{last}}} \gets GetSS(de_{g_{ss}})$\r
-       %               \State $MS_g \gets \Call{UpdateLastSeqN}{id_d,s_{d_{last}},MS_g}$\r
-       %               \State $SS_{live} \gets \Call{AddSSLivEnt}{SS_{live},de_{g_{ss}}}$\r
-       %       \EndFor\r
-       %\EndIf\r
-       \State $\Call{UpdateCR}{DE_g}$\Comment{Handle cr}\r
-       %\State $DE_{g_{cr}} \gets \Call{GetColRes}{DE_g}$\Comment{Handle cr}\r
-       %\If{$DE_{g_{cr}} \neq \emptyset$}\r
-       %       \ForAll{$de_{g_{cr}} \in DE_{g_{cr}}$}\r
-       %               \State $cr_g \gets GetCR(de_{g_{cr}})$\r
-       %               \State $\Call{CheckCollision}{MS,SM,cr_g}$\r
-       %               \State $CR_{live} \gets \Call{AddCRLivEnt}{CR_{live},cr_g}$\r
-       %       \EndFor\r
-       %\EndIf\r
-       \State $sl_{last} \gets \Call{StoreLastSlot}{MS,sl_{last},s_g,sv_g,id_g}$\r
-       \State $DT \gets \Call{UpdateDT}{DT,DE_g,LV,s_g}$\r
-\EndFor\r
-\State $\Call{CheckLastSeqN}{MS_g,MS,d}$\r
-\State $\Call{CheckNumSlots}{|SL_g|,sz}$\r
-\State $\Call{UpdateSSLivEnt}{SS_{live},MS}$\r
-\State $\Call{UpdateCRLivEnt}{CR_{live},MS}$\r
-\State $\Call{UpdateSM}{SM,CR_{live}}$\r
-\EndProcedure\r
-\end{algorithmic}\r
 \r
-\begin{algorithmic}[1]\r
-\Procedure{GetKVPairs}{}\r
-\State $s_g \gets GetLastSeqN(MS,id_{self}) + 1$\r
-\State $SL_c \gets \Call{GetSlot}{s_g}$\r
-\State $\Call{ProcessSL}{SL_c}$\Comment{Process slots and update DT}\r
-\EndProcedure\r
-\end{algorithmic}\r
 \r
+% Create Rescued Commit\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Create Rescued Date Entry:}\\\r
+Generate the data entry rescued version of the entry.  For some data entry types such as commits, the entry is not rescued as is.  For commits only the key-value pairs that are most recent (no newer commit that has those key values in it).\\\r
 \begin{algorithmic}[1]\r
-\Function{Get}{$k_g$}  \Comment{Interface function to get a value}\r
-\State $\tuple{k_s,v_s} \gets \tuple{k,v}$ \textit{such that} $\tuple{k,v} \r
-       \in DT \land k = k_g$\r
-\State \Return{$v_s$}\r
+\Function{CreateRescuedCommit}{$commit_a$}\r
+    \State $AllCommits \gets $ \Call{GetCommits}{}\r
+    \State $\tuple{seq_{a_{trans}},KV_a} \gets de_a$\r
+    \State $NewKV \gets KV_a$\\\r
+\r
+    \LeftComment{Get rid of all key values that have newer commits}\r
+    \ForAll{$\tuple{k_a, v_a} \in KV_a$}\r
+        \LeftComment{Iterate over all commits that are newer than the rescue commit}\r
+        \ForAll{$\tuple{seq', KV'} \in AllCommits, seq' > seq_{a_{trans}}$}\r
+            \If{$\exists \tuple{k', v'} \in KV', k' = k_a$}\r
+                \State $NewKV \gets NewKV \setminus \tuple{k_a, v_a}$\r
+                \State Break\r
+            \EndIf\r
+        \EndFor\r
+    \EndFor\r
+    \State \Return{$\tuple{seq_{a_{trans}}, NewKV}$}\r
 \EndFunction\r
 \end{algorithmic}\r
+\end{varwidth}% \r
+}\r
 \r
-\subsubsection{Writing Slots}\r
-\textbf{States} \\\r
-\textit{$cp$ = data entry $DE$ maximum size/capacity} \\\r
-\textit{$ck_p$ = counter of $kv \in KV$ for putting pairs (initially 0)} \\\r
-\textit{$ck_g$ = counter of $kv \in KV$ for getting pairs (initially 0)} \\\r
-\textit{$cs_p$ = counter of $ss \in SS$ for putting pairs (initially 0)} \\\r
-\textit{$cs_g$ = counter of $ss \in SS$ for getting pairs (initially 0)} \\\r
-\textit{$cc_p$ = counter of $cr \in CR$ for putting pairs (initially 0)} \\\r
-\textit{$cc_g$ = counter of $cr \in CR$ for getting pairs (initially 0)} \\\r
-\textit{$hmac_{c_p}$ = the HMAC value of the current slot in procedure \r
-$\Call{PutDataEntries}{}$} \\\r
-\textit{$hmac_{p_p}$ = the HMAC value of the previous slot \r
-($hmac_{p_p} = \emptyset$ for the first slot) in procedure \r
-$\Call{PutDataEntries}{}$} \\\r
-\textit{$id_{self}$ = machine Id of this client} \\\r
-\textit{$sl_{last}$ = info of last slot in queue = \r
-       $\tuple{s_{last},sv_{last},id_{last}}$ (initially $\emptyset$)} \\\r
-\textit{$sz$ = expected size of received slots from server} \\\r
-\textit{$th_p$ = threshold number of dead slots for a resize to happen} \\\r
-\textit{$m'_p$ = offset added to $max$ for resize} \\\r
-\textit{$reinsert_{qs}$ = boolean to decide $qs$($max_g$) reinsertion} \\\r
-\textit{$KV$ = set of $\tuple{ck, \tuple{k,v}}$ of kv entries on client} \\\r
-\textit{$SS$ = set of $\tuple{cs, \tuple{id,s_{last}}}$ of ss entries on client} \\\r
-\textit{$CR$ = set of $\tuple{cc, \tuple{s_{col},id_{col}}}$ of cr entries on client} \\\r
-\textit{$SL_p$ = set of returned slots on client} \\\r
-\textit{SK = Secret Key} \\ \\\r
-\textbf{Helper Functions} \\\r
-$CreateDat(s,id,hmac_p,DE,hmac_c)=Dat_s=\tuple{s,id,hmac_p,DE,hmac_c}$ \\\r
-$CreateSS(id_s,s_{s_{last}})=\tuple{id_s,s_{s_{last}}} = ss_s$ \\\r
-$CreateQS(max'_s)=qs_s$ \\\r
-$CreateCR(s_s,id_s)=\tuple{s_s,id_s} = cr_s$ \\\r
-$Encrypt(Dat_s,SK_s)=sv_s$ \\\r
-$GetColSeqN(SL_s,s_s)= \tuple{s, sv}$ \textit{such that} $\tuple{s, sv}\r
-\in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s = s_s$ \\\r
-$GetKVPair(KV_s,k_s)= \tuple{ck,\tuple{k, v}}$ \textit{such that} \r
-$\tuple{ck,\tuple{k, v}} \in KV_s \wedge\r
-\forall \tuple{ck_s,\tuple{k_s, v_s}} \in KV_s, k = k_s$ \\\r
 \r
+% Create Rescued Date Entry\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Create Rescued Date Entry:}\\\r
+Generate the data entry rescued version of the entry.  For some data entry types such as commits, the entry is not rescued as is.  For commits only the key-value pairs that are most recent (no newer commit that has those key values in it).\\\r
 \begin{algorithmic}[1]\r
-\Function{Put}{$KV_s,\tuple{k_s,v_s}$}  \Comment{Interface function to update a key-value pair}\r
-\State $\tuple{ck_s,\tuple{k_s,v_t}} \gets GetKVPair(KV_s,k_s)$\r
-\If{$\tuple{ck_s,\tuple{k_s,v_t}} = \emptyset$}\r
-       \State $KV_s \gets KV_s \cup \{\tuple{ck_p, \tuple{k_s,v_s}}\}$\r
-       \State $ck_p \gets ck_p + 1$\r
-\Else\r
-       \State $KV_s \gets (KV_s - \{\tuple{ck_s, \tuple{k_s,v_t}}\}) \cup \r
-       \{\tuple{ck_s, \tuple{k_s,v_s}}\}$\r
-\EndIf\r
-\State \Return{$KV_s$}\r
-\EndFunction\r
-\end{algorithmic}\r
+\Function{CreateRescuedEntry}{$de_a$}\r
 \r
-\begin{algorithmic}[1]\r
-\Function{PutSSPair}{$SS_s,\tuple{id_s,s_{s_{last}}}$}\Comment{Insert a set of $ss$ entries}\r
-\State $SS_s \gets SS_s \cup \{\tuple{cs_p, \tuple{id_s,s_{s_{last}}}}\}$\r
-\State $cs_p \gets cs_p + 1$\r
-\State \Return{$SS_s$}\r
-\EndFunction\r
-\end{algorithmic}\r
+    \If{$de_a$is a $commit$}\r
+        \State \Return{\Call{CreateRescuedCommit}{$de_a$}}\r
+    \EndIf\r
+    \r
+    \State \Return{$de_a$} \Comment{No Modification needed}\r
 \r
-\begin{algorithmic}[1]\r
-\Function{PutCRPair}{$CR_s,\tuple{s_s,id_s}$}\Comment{Insert a set of $cr$ entries}\r
-\State $CR_s \gets CR_s \cup \{\tuple{cc_p, \tuple{s_s,id_s}}\}$\r
-\State $cc_p \gets cc_p + 1$\r
-\State \Return{$CR_s$}\r
 \EndFunction\r
 \end{algorithmic}\r
+\end{varwidth}% \r
+}\r
 \r
-\begin{algorithmic}[1]\r
-\Function{CheckResize}{$MS_s,th_s,max_t,m'_s$}\r
-\State $s_{last_{min}} \gets MinLastSeqN(MS_s)$\r
-\State $s_{last_{max}} \gets MaxLastSeqN(MS_s)$\r
-\State $n_{live} \gets s_{last_{max}} - s_{last_{min}} + 1$\Comment{Number of live slots}\r
-\State $n_{dead} \gets max_t - n_{live}$\r
-\If{$n_{dead} \leq th_s$}\r
-       \State $max'_s \gets max_t + m'_s$\r
-\Else\r
-       \State $max'_s \gets \emptyset$\r
-\EndIf\r
-\State \Return{$max'_s$}\r
-\EndFunction\r
-\end{algorithmic}\r
 \r
-\begin{algorithmic}[1]\r
-\Function{CheckSLFull}{$MS_s,max_t$}\Comment{Check if $ss$ is needed}\r
-\State $s_{last_{min}} \gets MinLastSeqN(MS_s)$\r
-\State $s_{last_{max}} \gets MaxLastSeqN(MS_s)$\r
-\State $n_{live} \gets s_{last_{max}} - s_{last_{min}}$\Comment{Number of live slots}\r
-\State $n_{dead} \gets max_t - n_{live}$\r
-\State \Return {$n_{dead} = 0$}\r
-\EndFunction\r
-\end{algorithmic}\r
+% Mandatory Rescue\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Mandatory Rescue:}\\\r
+This rescue is mandatory before any types of data entries (excpet queue states) can be placed into the data entry section of the new slot.  Returns the data entry Set or null if the first slot could not be cleared (the live data in that slot could not fit in this current slot). \\\r
+\begin{algorithmic}[1]\r
+\Function{MandatoryRescue}{$DE_a$}\r
+    \State $smallestseq \gets seq$ such that $\tuple{seq, DE}\in LocalSlots \land (\forall \tuple{seq', DE'} \in LocalSlots, seq \leq seq')$\r
+    \State $cseq \gets smallestseq$\\\r
+    \r
+    \LeftComment{Check the least slots to rescue and live entries}\r
+    \While{$cseq < (smallestseq + DEAD\_SLOT\_COUNT)$}\r
+        \State $currentslot \gets s'$ such that $\tuple{s',DE'} \in LocalSlots \land s' = cseq$\r
+        \State $\tuple{seq', \tuple{seq_2',id',DE',hmac_p',hmac_c'}} \gets currentslot$\\\r
+        \r
+        \ForAll{$de \in DE'$} \Comment{Iterate over all the entries}\r
+            \If{\Call{CheckLive}{$de$}} \Comment{data entry is live}\r
+                \State $de \gets $ \Call{CreateRescuedEntry}{de} \Comment{Resize entry if needed}\r
+                \If{\Call{DEHasSpace}{$DE_a, de$}}\r
+                    \State $DE_a \gets DE_a \cup de$ \Comment{Had enough space to add it}\r
+                \ElsIf{$currentseq = smallestseq$}\r
+                    \State \Return{$NULL$}\r
+                \Else\r
+                    \State \Return{$DE_a$}\r
+                \EndIf\r
+            \EndIf\r
+        \EndFor\\\r
+        \r
+        \State $cseq \gets cseq+1$ \Comment{Move onto the next slot}\r
+    \EndWhile\r
+    \r
+    \State \Return{$DE_a$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
 \r
-\begin{algorithmic}[1]\r
-\Function{HandleCollision}{$SL_s,s_s$}\r
-\If{$SL_s = \emptyset$}\r
-       \State \Call{Error}{'No slots received from server'}\r
-\EndIf\r
-\State $\tuple{s_{col},sv_{col}} \gets GetColSeqN(SL_s,s_s)$\r
-\State $Dat_{col} \gets Decrypt(SK,sv_{col})$\r
-\State $id_{col} \gets GetMacId(Dat_{col})$\r
-\State $cr_s \gets CreateCR(s_{col},id_{col})$\r
-\State $\Call{ProcessSL}{SL_s}$\r
-\State \Return{$cr_s$}\r
-\EndFunction\r
-\end{algorithmic}\r
 \r
-\begin{algorithmic}[1]\r
-\Procedure{CheckLastSlot}{$sl_{s_{last}}$}\r
-\State $s_s \gets GetLastS(sl_{s_{last}})$\r
-\State $sv_s \gets GetSV(sl_{s_{last}})$\r
-\State $Dat_s \gets Decrypt(SK,sv_s)$\r
-\State $DE_s \gets GetDatEnt(Dat_s)$\r
-\ForAll{$de_s \in DE_s$}\r
-       \State $live \gets \Call{CheckLiveness}{s_s,de_s}$\r
-       \If{$live$}\r
-               \If{$type(de_s) = ``kv"$}\r
-                       \State $\tuple{k_s,v_s} \gets GetKV(de_s)$\r
-                       \State $KV \gets \Call{PutKVPair}{KV,\tuple{k_s,v_s}}$\r
-               \ElsIf{$type(de_s) = ``ss"$}\r
-                       \State $\tuple{id_s,s_{s_{last}}} \gets GetSS(de_s)$\r
-                       \State $SS \gets \Call{PutSSPair}{SS,\tuple{id_s,s_{s_{last}}}}$\r
-               \ElsIf{$type(de_s) = ``cr"$}\r
-                       \State $\tuple{s_s,id_s} \gets GetCR(de_s)$\r
-                       \State $CR \gets \Call{PutCRPair}{CR,\tuple{s_s,id_s}}$\r
-               \ElsIf{$type(de_s) = ``qs"$}\r
-                       \State $reinsert_{qs} \gets true$\r
-               \EndIf\r
-       \EndIf\r
-\EndFor\r
-\EndProcedure\r
-\end{algorithmic}\r
 \r
-\begin{algorithmic}[1]\r
-\Function{CheckLiveness}{$s_s,de_s$}\r
-\State $live \gets true$\r
-\If{$de_s = kv$}\r
-       \State $s_l \gets GetLivEntLastS(LV,de_s)$\r
-       \If{$s_l = \emptyset \lor s_s < s_l$}\r
-               \State $live \gets false$\r
-       \EndIf\r
-\ElsIf{$de_s = ss$}\r
-       \State $ss_s \gets GetSS(de_s)$\r
-       \State $ss_l \gets GetLiveSS(SS_{live},ss_s)$\r
-       \If{$ss_l = \emptyset$}\r
-               \State $live \gets false$\r
-       \EndIf\r
-\ElsIf{$de_s = cr$}\r
-       \State $cr_s \gets GetCR(de_s)$\r
-       \State $cr_l \gets GetLiveCR(CR_{live},cr_s)$\r
-       \If{$cr_l = \emptyset$}\r
-               \State $live \gets false$\r
-       \EndIf\r
-\ElsIf{$de_s = qs$}\r
-       \State $qs_s \gets GetQS(de_s)$\r
-       \If{$qs_s \neq max_g$}\r
-               \State $live \gets false$\r
-       \EndIf\r
-\Else\r
-       \State \Call{Error}{'Unrecognized $de$ type'}\r
-\EndIf\r
-\State \Return{$live$}\r
-\EndFunction\r
-\end{algorithmic}\r
 \r
-\begin{algorithmic}[1]\r
-\Function{CreateSlotSeq}{$sl_s$}\r
-\State $id_s \gets GetID(sl_s)$\r
-\State $s_{s_{last}} \gets GetLastS(sl_s)$\r
-\State $ss_s \gets CreateSS(id_s,s_{s_{last}})$\r
-\State \Return{$\tuple{ss_s}$}\r
-\EndFunction\r
-\end{algorithmic}\r
+% Try Insert Transaction\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Try Insert Transaction:}\\\r
+Try to insert a transaction into the block chain.\\\r
+\begin{algorithmic}[1]\r
+\Function{TryInsertTransaction}{$pendingtrans_a, forceresize$}\r
+    \State $DE \gets \emptyset$ \Comment{The data entries for this slot}\r
+    \State $seq \gets $ \Call{GetNextSeq}{} \Comment{Get the sequence number for this slot}\r
+    \State $newsize \gets 0$\r
+    \State $trans \gets$ \Call{CreateTrans}{$pendingtrans_a, seq$}\r
+    \State $transinserted \gets false$\r
+    \r
+    \State $resize \gets $ \Call{ShouldResize}{ } \Comment{Check if we should resize}\r
+    \State $resize \gets resize \lor forceresize$\r
+    \If{$resize$}\r
+        \State $newsize \gets$ \Call{CalcNewSize}{$max\_size$}\r
+        \State $DE \gets DE \cup \{$\Call{CreateQState}{$newsize$}$\}$\r
+    \EndIf\\\r
+    \r
+    \r
+    \r
+    \r
+    %\If{$RejectedSlotList \neq \emptyset$}   \r
+    %\EndIf\r
+    \r
+    % Arbitrate\r
+    \r
+    \State $DE \gets$ \Call{MandatoryRescue}{$DE$} \Comment{Round 1 of rescue}\r
+    \If{$DE = NULL$}\r
+        \LeftComment{Data was going to fall off the end so try again with a forced resize}\r
+        \State \Return{\Call{TryInsertTransaction}{$trans_a, true$}}\r
+    \EndIf\\\r
+    \r
+    \If{\Call{DEHasSpace}{$DE, trans$}} \Comment{transaction fits}\r
+        \State $DE \gets DE \cup trans$\r
+        \State $transinserted \gets true$\r
+    \EndIf\r
+    \r
+    \r
+    \r
+\EndFunction\r
+\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
 \r
-\begin{algorithmic}[1]\r
-\Function{AddQueSta}{$DE_s,max'_s,cp_s$}\Comment{Insert a $qs$}\r
-\State $DE_{ret} \gets \emptyset$\r
-\State $qs_s \gets max'_s$\r
-\State $DE_{ret} \gets DE_s \cup \{qs_s\}$\r
-\State $cp_s \gets cp_s - 1$\r
-\State \Return{$\tuple{DE_{ret},cp_s}$}\r
-\EndFunction\r
-\end{algorithmic}\r
 \r
-\begin{algorithmic}[1]\r
-\Function{GetKVPairs}{$DE_s,KV_s,cp_s$}\r
-\State $DE_{ret} \gets \emptyset$\r
-\If{$|KV_s| \leq cp_s$}\Comment{$KV$ set can span multiple slots}\r
-       \State $DE_{ret} \gets DE_s \cup\r
-       \{\tuple{k_s,v_s} \mid \tuple{ck_s,\tuple{k_s,v_s}} \in KV_s\}$\r
-\Else\r
-       \State $DE_{ret} \gets DE_s \cup\r
-       \{\tuple{k_s,v_s} \mid \tuple{ck_s,\tuple{k_s,v_s}} \in KV_s,\r
-               ck_g \leq ck_s < ck_g + cp_s\}$\r
-\EndIf\r
-\State \Return{$\tuple{DE_{ret}}$}\r
-\EndFunction\r
-\end{algorithmic}\r
 \r
+\subsection{Client Interfaces}\r
+\r
+% Put KV pair\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Put Key Value Pair:}\\\r
+Puts a key value pair into the key value pair buffer\\\r
 \begin{algorithmic}[1]\r
-\Function{GetSSPairs}{$DE_s,SS_s,cp_s$}\r
-\State $DE_{ret} \gets \emptyset$\r
-\If{$|SS_s| \leq cp_s$}\Comment{$SS$ set can span multiple slots}\r
-       \State $DE_{ret} \gets DE_s \cup\r
-       \{\tuple{id_s,s_{s_{last}}} \mid \tuple{cs_s,\tuple{id_s,s_{s_{last}}}} \in SS_s\}$\r
-       \State $cp_s \gets cp_s - |SS_s|$\r
-\Else\r
-       \State $DE_{ret} \gets DE_s \cup\r
-       \{\tuple{id_s,s_{s_{last}}} \mid \tuple{cs_s,\tuple{id_s,s_{s_{last}}}} \in SS_s,\r
-               cs_g \leq cs_s < cs_g + cp_s\}$\r
-       \State $cp_s \gets 0$\r
-\EndIf\r
-\State \Return{$\tuple{DE_{ret},cp_s}$}\r
+\Function{PutKeyValue}{$k,v$}\r
+    \State $\tuple{seq, KV, Guard} \gets PendingTrans$\\\r
+    \r
+    \LeftComment{Check if KV already has a key value pair for the specified key}\r
+    \State $DSet \gets \{\tuple{k_1,v_1} | \tuple{k_1,v_1} \in KV \land k_1 = k\}$\\\r
+    \r
+    \If{$DSet \neq \emptyset$}\r
+        \State \Call{Error}{"Value for key already in most recent update"}\r
+    \EndIf\\\r
+        \r
+    \State $KV \gets KV \cup \{\tuple{k,v}\}$ \Comment{Add key value pair}\r
+    \State $PendingTrans \gets \tuple{seq, KV, Guard}$\r
+    \State \Call{CheckArbitrator}{$PendingTrans$} \Comment{Check that the transaction still valid}\r
 \EndFunction\r
 \end{algorithmic}\r
+\end{varwidth}% \r
+}\r
+\r
 \r
+% Put guard condition\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Put Guard:}\\\r
+Puts a guard transaction into the key value update.  A guard is a key value with a logical operator ($lop$).\\\r
+\begin{algorithmic}[1]\r
+\Function{PutGuard}{$k,v, lop$}\r
+    \State $\tuple{seq, KV, Guard} \gets PendingTrans$\\\r
+    \r
+    \If{$\tuple{k,v, lop} \in Guard$}\r
+        \State \Return{} \Comment{Already have guard condition in update}\r
+    \EndIf\\\r
+    \r
+    \State $Guard \gets Guard \cup \{\tuple{k,v,lop}\}$\r
+    \State $PendingTrans \gets \tuple{seq, KV, Guard}$\r
+    \State \Call{CheckArbitrator}{$PendingTrans$} \Comment{Check that the transaction still valid}\r
+\EndFunction    \r
+\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
+\r
+\r
+% Transaction Start\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{ Transaction Start:}\\\r
+Starts a transaction.  Clears out the key value pair update buffer.\\\r
 \begin{algorithmic}[1]\r
-\Function{GetCRPairs}{$DE_s,CR_s,cp_s$}\r
-\State $DE_{ret} \gets \emptyset$\r
-\If{$|CR_s| \leq cp_s$}\Comment{$CR$ set can span multiple slots}\r
-       \State $DE_{ret} \gets DE_s \cup\r
-       \{\tuple{s_s,id_s} \mid \tuple{cc_s,\tuple{s_s,id_s}} \in CR_s\}$\r
-       \State $cp_s \gets cp_s - |CR_s|$\r
-\Else\r
-       \State $DE_{ret} \gets DE_s \cup\r
-       \{\tuple{s_s,id_s} \mid \tuple{cc_s,\tuple{s_s,id_s}} \in CR_s,\r
-               cc_g \leq cc_s < cc_g + cp_s\}$\r
-       \State $cp_s \gets 0$\r
-\EndIf\r
-\State \Return{$\tuple{DE_{ret},cp_s}$}\r
+\Function{TransactionStart}{$ $}\r
+    \LeftComment{Reset the key value update buffer}\r
+    \State $KVUpdate \gets \tuple{\emptyset, \emptyset}$\r
 \EndFunction\r
 \end{algorithmic}\r
+\end{varwidth}% \r
+}\r
 \r
+% Transaction Commit\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{ Transaction Commit:}\\\r
+Commits the transaction into the block chain.  Keeps attempting to insert the transaction into the block chain until it succeeds.\r
 \begin{algorithmic}[1]\r
-\Procedure{PutDataEntries}{$th_p,m'_p$}\r
-\State $success_p \gets false$\r
-\State $CR_p \gets \emptyset$\r
-\While{$\neg success_p$}\r
-       \State $DE_p \gets \emptyset$\r
-       \State $s_p \gets MaxLastSeqN(MS)$\r
-       \State $cp_p \gets cp$\r
-       \State $max'_p \gets \Call{CheckResize}{MS,th_p,max_g,m'_p}$\r
-       \If{$max'_p \neq \emptyset$}\Comment{Add a qs entry}\r
-               \State $\tuple{DE_p,cp_p} \gets \Call{AddQueSta}{DE_p,max'_p,cp_p}$\r
-               \State $reinsert_{qs} \gets false$\r
-       \Else\Comment{Check if there is $qs$ reinsertion}\r
-               \If{$reinsert_{qs}$}\r
-                       \State $\tuple{DE_p,cp_p} \gets \Call{AddQueSta}{DE_p,max_g,cp_p}$\r
-                       \State $reinsert_{qs} \gets false$\r
-               \EndIf\r
-       \EndIf\r
-       \If{$SS \neq \emptyset$}\Comment{Add $ss$ entries}\r
-               \State $\tuple{DE_p,cp_p} \gets \Call{GetSSPairs}{DE_p,SS,cp_p}$\r
-       \EndIf\r
-       \If{$CR \neq \emptyset$}\Comment{Add $cr$ entries}\r
-               \State $\tuple{DE_p,cp_p} \gets \Call{GetCRPairs}{DE_p,CR,cp_p}$\r
-       \EndIf\r
-       \State $\tuple{DE_p,cp_p} \gets \Call{GetKVPairs}{DE_p,KV,cp_p}$\Comment{Add $kv$ entries}\r
-       \State $hmac_{c_p} \gets Hmac(DE_p,SK)$\r
-       \State $Dat_p \gets CreateDat(s_p,id_{self},hmac_{p_p},DE_p,hmac_{c_p})$\r
-       \State $hmac_{p_p} \gets hmac_{c_p}$\r
-       \State $sv_p \gets Encrypt(Dat_p,SK)$\r
-       \State $\tuple{success_p,SL_p} \gets \Call{PutSlot}{s_p,sv_p,max'_p}$\r
-       \If{$\neg success_p$}\r
-               \State $cr_p \gets \Call{HandleCollision}{SL_p,s_p}$\r
-               \State $\tuple{s_{p_{col}},id_{p_{col}}} \gets GetCR(cr_p)$\r
-               \State $CR \gets \Call{PutCRPair}{CR,\tuple{s_{p_{col}},id_{p_{col}}}}$\r
-       \EndIf\r
-\EndWhile\r
-\State $MS \gets \Call{UpdateLastSeqN}{id_{self},s_p,MS}$\r
-\If{$|DE_p| = cp$}\Comment{Update set counters}\r
-       \State $ck_g \gets ck_g + cp_p$\Comment{Middle of set}\r
-       \State $cs_g \gets cs_g + |SS|$\r
-       \State $cc_g \gets cc_g + |CR|$\r
-\Else\Comment{End of set}\r
-       \State $ck_g \gets 0$\r
-       \State $cs_g \gets 0$\r
-       \State $cc_g \gets 0$\r
-\EndIf\r
-\State $need_p \gets \Call{CheckSLFull}{MS,max_g}$\r
-\If{$need_p$}\Comment{SL on server is full}\r
-       \State $\Call{CheckLastSlot}{sl_{last}}$\Comment{Salvage entries from expunged slot}\r
-       \State $ss_p \gets \Call{CreateSlotSeq}{sl_{last}}$\r
-       \State $\tuple{id_p,s_{p_{last}}} \gets GetSS(ss_p)$\r
-       \State $SS \gets \Call{PutSSPair}{SS,\tuple{id_p,s_{p_{last}}}}$\Comment{Add ss}\r
-\EndIf\r
-\EndProcedure\r
+\Function{Transaction Commit}{$ $}\r
+    \State $success \gets False$\r
+    \r
+    \While{$\lnot success$}\r
+        \State $success \gets$\r
+    \EndWhile\r
+    \r
+    \r
+\EndFunction\r
 \end{algorithmic}\r
-\r
-%\note{Lots of problems with PutDataEntries: (1) What happens if lose network connectivity after adding the key value pair, but before reinserting the last slot?  You probably need to create space first and then insert your data entry...  (2) What if reinsertlastslot kicks something else important out?  What if the server rejects our update because it is out of date?  At the very least, any putdataentries function w/o a loop is wrong!}\r
-\r
-%\note{General comments...  Work on structuring things to improve readability...  This include names of functions/variables, how things are partitioned into functions, adding useful comments,...}\r
-  \r
-%\note{Also Missing liveness state definition in algorithm...}\r
-\r
-\r
-\subsection{Formal Guarantees}\r
-\subsubsection{Definitions}\r
-\r
-\begin{defn}[Message]\r
-A message $\mathsf{t}$, is the tuple \r
-\begin{center}\r
-$\mathsf{t = \tuple{s, E(Dat_s)}}$ \\\r
-$\mathsf{Dat_t = \tuple{s,id,hmac_p, DE,hmac_c}}$\r
-\end{center}\r
-containing $\mathsf{s}$ as sequence number and $\mathsf{Dat_t}$ as its \r
-encrypted contents. $\mathsf{Dat_t}$ consists of $\mathsf{s}$, \r
-$\mathsf{id}$ as machine ID of the sender, $\mathsf{hmac_p}$ as HMAC \r
-from a previous message, $\mathsf{DE}$ as set of data entries, and \r
-$\mathsf{hmac_c}$ as HMAC from message $\mathsf{t}$ respectively.\r
-\end{defn}\r
-\r
-\begin{defn}[Equality]\r
-Two messages $\mathsf{t}$ and $\mathsf{u}$ are equal if their $\mathsf{s}$, \r
-and $\mathsf{Dat_t}$ are exactly the same.\r
-\end{defn}\r
-\r
-\begin{defn}[Parent]\r
-A parent of a message $\mathsf{t}$ is the message $\mathsf{p_t}$, \r
-unique by the correctness of HMACs in $\mathsf{Dat_t}$, such that \r
-$\mathsf{hmac_p(t) = hmac_c(p_t)}$.\r
-\end{defn}\r
-\r
-\begin{defn}[Chain]\r
-A chain of messages with length $\mathsf{n \ge 1}$ is a message sequence \r
-$\mathsf{R = (r_s, r_{s+1}, ..., r_{s+n-1})}$ such that for every sequence \r
-number $\mathsf{s < k \le s+n-1}$, $\mathsf{r_k}$ has sequence number \r
-$\mathsf{k}$ and is the parent of $\mathsf{r_{k-1}}$.\r
-\end{defn}\r
-\r
-\begin{defn}[Partial sequence]\r
-A partial sequence $\mathsf{P}$ is a sequence of messages, no two \r
-with the same sequence number, that can be divided into disjoint chains.\r
-\end{defn}\r
-\r
-\begin{defn}[Total sequence]\r
-A total sequence $\mathsf{T =}$ $\mathsf{(t_1, t_2, ..., t_n)}$ with \r
-length $\mathsf{n}$ is a chain of messages that starts at $\mathsf{s = 1}$.\r
-\end{defn}\r
-\r
-\begin{defn}[Path]\r
-The path of a message $\mathsf{t}$ is the chain that starts at $\mathsf{s = 1}$ \r
-and whose last message is $\mathsf{t}$. The uniqueness of a path follows \r
-from the uniqueness of a parent.\r
-\end{defn}\r
-\r
-\begin{defn}[Consistency]\r
-A partial sequence $\mathsf{P}$ is consistent with a total sequence \r
-$\mathsf{T}$ of length $\mathsf{n}$ if for every message $\mathsf{p \in P}$ \r
-with $\mathsf{s_p \leq n}$, $\mathsf{t_{s_p} = p}$. This implies that \r
-$\mathsf{\{p \in P | s_p \le n\}}$ is a partial sequence of $\mathsf{T}$.\r
-\end{defn}\r
-\r
-\begin{defn}[Transitive closure]\r
-Transitive closure set at sequence number $\mathsf{s_n}$ is a set \r
-$\mathsf{\mathscr{S}}$ of clients comprising a connected component of an \r
-undirected graph, where two clients are connected by an edge if they both \r
-received the same message $\mathsf{t}$ with sequence number $\mathsf{s_t > s_n}$.\r
-\end{defn}\r
-\r
-\subsubsection{Lemmas and Proofs}\r
-\r
-\begin{prop}\r
-\label{prop:parentmessage}\r
-Every client $\mathsf{J}$ who sends a message $\mathsf{t}$ \r
-has parent $\mathsf{p_t}$ as its latest stored message, and \r
-$\mathsf{s_t = s_{p_t} + 1}$. \r
-\end{prop}\r
-\begin{proof} True by definition, because $J$ sets \r
-$\mathsf{hmac_p(t) = hmac_c(p_t)}$ and \r
-$\mathsf{s_t = }$ $\mathsf{s_{p_t + 1}}$ when a message \r
-is sent. \r
-\end{proof}\r
-\r
-\begin{prop} \r
-\label{prop:rejectedmessage}\r
-If a rejected message entry is added to the set $\mathsf{CR}$ \r
-at sequence number $\mathsf{s}$, the message will remain in $\mathsf{CR}$ \r
-until every client has seen it. \r
-\end{prop}\r
-\begin{proof} Every $\mathsf{CR}$ entry $\mathsf{cr}$ remains in the queue until it \r
-reaches the tail, and is refreshed by the next sender $\mathsf{J}$ at that time if \r
-$\mathsf{min(MS) > s_{cr}}$; that is, until every client has sent a message with \r
-sequence number greater than $\mathsf{s_{cr}}$. Because every client who sends a \r
-message with sequence number $\mathsf{s}$ has the state of the set $\mathsf{SL}$ at \r
-$\mathsf{s - 1}$, this client will have seen the message at $\mathsf{s_{cr}}$. \r
-\end{proof}\r
-\r
-\begin{figure}[h]\r
-  \centering\r
-      \xymatrix{ & & L \\\r
-\dots \ar[r] & q \ar[dr]_{J} \ar[r]^{K} & l_1 \ar[r] & l_2 \ar[r] & \dots \ar[r] & m \ar[r] & \dots \ar[r] & l_n = u \\\r
-& & r_1 \ar[r] & r_2 \ar[r] & \dots \ar[r] & r_m = t \\\r
-& & R\r
-\save "2,3"."2,8"*+\frm{^\}}\r
-\save "3,3"."3,6"*+\frm{_\}}\r
-\restore\r
-\restore\r
+\end{varwidth}% \r
 }\r
-\caption{By \textbf{Lemma \ref{lem:twomessages}}, receiving both $t$ and $u$ here is impossible.}\r
-\end{figure}\r
-\r
-\begin{lem}\r
-\label{lem:twomessages}\r
-Two messages are received without errors by a client $\mathsf{C}$; \r
-call them $\mathsf{t}$ and $\mathsf{u}$ such that $\mathsf{s_t \le s_u}$. \r
-Then $\mathsf{t}$ is in the path of $\mathsf{u}$. \r
-\end{lem}\r
-\begin{proof}\r
-Assume that there are some pairs of messages $\mathsf{(t,u)}$ that violate this lemma. \r
-Take a specific $\mathsf{(t,u)}$ such that $\mathsf{s_u}$ is minimized, and \r
-$\mathsf{s_t}$ is maximized for this choice of $\mathsf{s_u}$. We will show that $\mathsf{C}$\r
-cannot receive both $\mathsf{t}$ and $\mathsf{u}$ without throwing an error.\r
-\r
-Clearly $\mathsf{C}$ will throw an error if $\mathsf{s_t = s_u}$. So \r
-$\mathsf{s_t < s_u}$. Additionally, if $\mathsf{C}$ receives $\mathsf{u}$ before \r
-$\mathsf{t}$, this will cause it to throw an error, so $\mathsf{t}$ is received \r
-before $\mathsf{u}$. We will prove that an error occurs upon receipt of $\mathsf{u}$.\r
-\r
-Let $\mathsf{r_1}$ be the earliest member of the path of $\mathsf{t}$ that is \r
-not in the path of $\mathsf{u}$, and $\mathsf{q}$ be its parent. Message \r
-$\mathsf{q}$, the last common ancestor of $\mathsf{t}$ and $\mathsf{u}$, must exist, \r
-since all clients and the server were initialized with the same state. Let \r
-$\mathsf{l_1}$ be the successor of $\mathsf{q}$ that is in the path of $\mathsf{u}$; \r
-we know $\mathsf{l_1 \neq r_1}$. Let $\mathsf{R = (r_1, r_2, \dots, r_{|R|} = t)}$ be \r
-the distinct portion of the path of $\mathsf{t}$, and similarly let $\mathsf{L}$ \r
-be the distinct portion of the path of $\mathsf{l_{|L|} = u}$.\r
-\r
-Let $\mathsf{J}$ be the client who sent $\mathsf{r_1}$; that is, such that \r
-$\mathsf{{id_{self}}_J = GetMacID(r_1)}$, and $\mathsf{K}$ be the client who \r
-sent $\mathsf{l_1}$. Because no client can send two messages with the same sequence number, and \r
-$\mathsf{s_{r_1} = s_{l_1} = s_q + 1}$, $\mathsf{J \neq K}$.\r
-\r
-We also know the following facts: \r
-\r
-\begin{prop} \r
-\label{prop:bothmessages}\r
-No client sends both a message in $\mathsf{(r_2,...,t)}$ and a message in $\mathsf{(l_2,...,u)}$. \r
-\end{prop}\r
-\r
-\begin{proof}\r
-To send a message $\mathsf{p}$ that is the parent of some other \r
-message, one must have received the parent of $\mathsf{p}$. Since \r
-$\mathsf{u}$ is the message with smallest sequence number received by any \r
-client that violates Lemma \ref{lem:twomessages}, no client receives both a message \r
-in $\mathsf{r}$ and a message in $\mathsf{l}$. \r
-\end{proof}\r
-\r
-\begin{prop} \r
-\label{prop:seqnumb}\r
-$\mathsf{C}$ does not receive any message with a\r
-sequence number strictly between $\mathsf{s_t}$ and $\mathsf{s_u}$. \r
-\end{prop}\r
-\r
-\begin{proof} If there were such a message with sequence number smaller than \r
-$\mathsf{s_u}$, it would contradict the assumption that $\mathsf{u}$ is the \r
-message with the least sequence number that violates Lemma \ref{lem:twomessages}. \r
-\end{proof}\r
-\r
-There are two cases:\r
-\begin{itemize}\r
-\item Case 1: $\mathsf{J}$ did not send a message in $\mathsf{L}$. Then, where $\mathsf{s_{t_J}}$ \r
-is the greatest sequence number of the messages that client $\mathsf{J}$ sent in \r
-the path of message $\mathsf{t}$, $\mathsf{s_{t_J} > s_{q_J} = s_{u_J}}$.\r
-\begin{itemize}\r
-\item Case 1.1: $\mathsf{C}$ never updates its slot sequence list $\mathsf{SS}$ \r
-between receiving $\mathsf{t}$ and receiving $\mathsf{u}$; this can only happen if \r
-$\mathsf{s_t = s_u - 1}$. Since $\mathsf{t}$ is not the parent of $\mathsf{u}$, \r
-$\mathsf{hmac_p(u) \neq hmac_c(t)}$, causing $\mathsf{C}$ to throw an error.\r
-\item Case 1.2: Case 1.1 does not occur; therefore, $\mathsf{C}$ must update \r
-its slot sequence list $\mathsf{SS}$ at some point between receiving $\mathsf{t}$ \r
-and $\mathsf{u}$. \r
-The latest sequence number of $\mathsf{J}$ decreases during this time, which \r
-means it must decrease when some message is received, which means $\mathsf{C}$ \r
-throws an error in the $\mathsf{CheckLastSeqN()}$ subroutine.\r
-\end{itemize}\r
-\r
-\item Case 2: $\mathsf{J}$ sent at least one message in $\mathsf{L}$. Call the \r
-first one $\mathsf{m}$. We know that $\mathsf{s_m > s_{r_1}}$, since \r
-$\mathsf{J \neq K}$ and $\mathsf{m \neq l_1}$. Message $\mathsf{r_1}$ must be sent \r
-either before or after $\mathsf{m}$.\r
-\begin{itemize}\r
-\item Case 2.1: Client $\mathsf{J}$ sends $\mathsf{m}$, and then $\mathsf{r_1}$. \r
-Before sending $\mathsf{m}$, the greatest sequence number of a message that \r
-$\mathsf{J}$ has received, $\mathsf{{s_{last}}_J}$, must be equal to \r
-$\mathsf{s_m - 1 \ge s_{r_1}}$. Since $\mathsf{{s_{last}}_J}$ never decreases, \r
-client $\mathsf{J}$ cannot then send a message with sequence number \r
-$\mathsf{s_{r_1}}$, a contradiction.\r
-\item Case 2.2: Client $\mathsf{J}$ sends $\mathsf{r_1}$, and then $\mathsf{m}$. \r
-Let $\mathsf{X = (r_1 = x_1, \dots , x_n)}$ be the list of messages $\mathsf{J}$ sends \r
-starting before $\mathsf{r_1}$ and ending before $m$; clearly these all have sequence \r
-number $\mathsf{s_p = s_q + 1}$.\r
-\begin{itemize}\r
-\item Case 2.2.1: Some message in $\mathsf{X}$ was accepted. Before sending $\mathsf{m}$, \r
-$\mathsf{J}$'s value in $\mathsf{MS_J}$ for its own latest sequence number would \r
-be strictly greater than $\mathsf{s_{q_J}}$. If there is a sequence of messages with \r
-contiguous sequence numbers that $\mathsf{J}$ receives between $\mathsf{r_1}$ and \r
-$\mathsf{m}$, $\mathsf{J}$ throws an error for a similar reason as Case 1.1. Otherwise, \r
-when preparing to send $\mathsf{m}$, $\mathsf{J}$ would have received an update of its \r
-own latest sequence number as at most $\mathsf{s_{q_J}}$. $J$ throws an error before \r
-sending $\mathsf{p}$, because its own latest sequence number decreases.\r
-\item Case 2.2.2: All messages in $\mathsf{X}$ were rejected, making $\mathsf{m}$ \r
-the first message of $\mathsf{J}$ that is accepted after $\mathsf{r_1}$.\r
-\r
-We will show that $\mathsf{C}$ sees $\mathsf{r_1}$. Assume not. Then $\mathsf{(r_2, ..., u)}$ \r
-must have at least $\mathsf{{max_g}_C} \geq 2$ messages for $\mathsf{r_1}$ to fall off the \r
-end of the queue. Consider the sender of $\mathsf{r_3}$ and call it $\mathsf{H}$. \r
-$\mathsf{H \neq J}$ by Proposition \ref{prop:bothmessages} and the existence of $\mathsf{m}$. \r
-Since $\mathsf{H \neq J}$, then by Proposition \ref{prop:bothmessages} it could not also \r
-have sent a message in $\mathsf{(l_2,..., u)}$. Therefore, $\mathsf{s_{u_H} < s_q + 2 = s_{t_H}}$, \r
-so upon receipt of $\mathsf{u}$, $\mathsf{C}$ will throw an error by the decrease in a \r
-last sequence number similar to Case 1, a contradiction.\r
-\r
-Now that we know that $\mathsf{C}$ sees $\mathsf{r_1}$, note that C receives $\mathsf{u}$ \r
-immediately after $\mathsf{t}$ by Proposition \ref{prop:seqnumb}. Therefore, \r
-$\mathsf{C}$ could not have seen a message after $\mathsf{t}$ with sequence number less \r
-than $\mathsf{s_m}$. In the $\mathsf{PutDataEntries()}$ subroutine, $\mathsf{J}$ adds every \r
-$\mathsf{cr}$ entry that contains sequence number $\mathsf{s}$ and machine ID \r
-$\mathsf{id}$ of the messsages that win in the collisions before $\mathsf{m}$ into \r
-$\mathsf{CR}$; $\mathsf{CR}$ keeps the collection of live $\mathsf{cr}$ entries, namely\r
-those which not all clients have seen. Hence, for every $\mathsf{i}$, $\mathsf{1 \leq i < |X|}$, \r
-the collision winner that has collided with $\mathsf{x_i}$ will be recorded appropriately. Since all the $\mathsf{cr}$ entries that record the results of the collisions before $\mathsf{p}$ will also be seen when $\mathsf{u}$ \r
-is received, and $\mathsf{C}$ sees $\mathsf{r_1}$, ${l_1}$ will be recorded in a $\mathsf{cr}$ entry as the winner in the \r
-collision against ${r_1}$.\r
-\r
-When $\mathsf{C}$ receives $\mathsf{u}$, if $\mathsf{C}$ \r
-has seen the $\mathsf{cr}$ entry that records the collision at index $\mathsf{s_q + 1}$, it will throw \r
-an error from the mismatch of $\mathsf{\tuple{s_q+1, id_J}}$ with \r
-$\mathsf{\tuple{s_q+1, id_K}}$ in the corresponding $\mathsf{cr}$ entry.\r
-\r
-\end{itemize}\r
-\end{itemize}\r
-\r
-\end{itemize}\r
-\end{proof}\r
-\r
-\begin{lem} \r
-\label{lem:pathmessages}\r
-If there are two messages $\mathsf{t}$ and $\mathsf{u}$, with \r
-$\mathsf{s_t \leq s_u}$, such that $\mathsf{t}$ is in the path of $\mathsf{u}$, \r
-then for any message $\mathsf{p}$ with $\mathsf{s_p \leq s_t}$, iff $\mathsf{p}$ is in \r
-the path of $\mathsf{t}$, it is in the path of $\mathsf{u}$. \r
-\end{lem}\r
-\r
-\begin{proof}\r
-If $\mathsf{s_t = s_u}$ or $\mathsf{s_p = s_t}$, then we are done, because the two \r
-relevant messages are the same. If they are different messages, then:\r
-\begin{itemize}\r
-\item Reverse direction: The definition of $\mathsf{t}$ being in the path of \r
-$\mathsf{u}$ is the existence of a message sequence $\mathsf{(\dots, t, \dots, u)}$ \r
-such that each message except $\mathsf{u}$ is the parent of the succeeding message. \r
-The path of $\mathsf{u}$ must contain some message with sequence number $\mathsf{s_p}$; \r
-because $\mathsf{p}$ is in the path of $\mathsf{u}$, this message is $\mathsf{p}$ \r
-itself. The path of $\mathsf{t}$ is then the prefix of this path ending at $\mathsf{t}$, \r
-which clearly contains $\mathsf{p}$.\r
-\r
-\item Forward direction: The path of $\mathsf{t}$ is a substring of the path of \r
-$\mathsf{u}$, so if the path of $\mathsf{t}$ contains $\mathsf{p}$, so does the path \r
-of $\mathsf{u}$.\r
-\end{itemize}\r
-\end{proof}\r
-\r
-\begin{theorem}\r
-Suppose that there is a transitive closure set $\mathsf{\mathscr{S}}$ of clients, \r
-at sequence number $\mathsf{s_n}$. Then there is some total sequence $\mathsf{T}$ of \r
-length $\mathsf{n}$ such that every client $\mathsf{C}$ in $\mathsf{\mathscr{S}}$ \r
-sees a partial sequence $\mathsf{P_C}$ consistent with $\mathsf{T}$. \r
-\end{theorem}\r
-\r
-\begin{proof}\r
-\r
-The definition of consistency of $\mathsf{P_C}$ with $\mathsf{T}$ is that every message \r
-$\mathsf{p \in P_C}$ with sequence number $\mathsf{s_p \le s_n}$ is equal to the message \r
-in that slot in $\mathsf{T}$. Let $\mathsf{C_1}$ be some client in the transitive closure \r
-set, with partial sequence $\mathsf{P_{C_1}}$, and let $\mathsf{u}$ be some message with \r
-$\mathsf{s_u > s_n}$ that $\mathsf{C_1}$ shares with another client. Then let $\mathsf{T}$ \r
-be the portion of the path of $\mathsf{u}$ ending at sequence number $\mathsf{s_n}$ and \r
-$\mathsf{t}$ be the message at that sequence number. Clearly, by Lemma \ref{lem:twomessages}, \r
-$\mathsf{P_{C_1}}$ is consistent with $\mathsf{T}$. We will show that, for every other client \r
-$\mathsf{D}$ with partial sequence $\mathsf{P_D}$, $\mathsf{P_D}$ has some message whose path \r
-includes $\mathsf{t}$. Because $\mathsf{D}$ is in the transitive closure, there is a sequence \r
-of clients $\mathsf{\mathscr{C} = (C_1, C_2, ..., D)}$ from $\mathsf{C_1}$ to $\mathsf{D}$, \r
-where each shares an edge with the next.\r
-We prove by induction that $\mathsf{P_D}$ has a message whose path includes $\mathsf{t}$.\r
-\begin{itemize}\r
-\item Base case: $\mathsf{P_{C_1}}$ includes $\mathsf{u}$, whose path includes $\mathsf{t}$.\r
-\r
-\item Inductive step: Each client in $\mathsf{\mathscr{C}}$ has a partial sequence with a message \r
-that includes $\mathsf{t}$ if the previous client does. Suppose $\mathsf{P_{C_k}}$ has \r
-a message $\mathsf{w}$ with a path that includes $\mathsf{t}$, and shares message $\mathsf{x}$ \r
-with $\mathsf{P_{C_{k+1}}}$ such that $\mathsf{s_x > s_n}$. By Lemma \ref{lem:twomessages}, \r
-$\mathsf{w}$ or $\mathsf{x}$, whichever has the least sequence number, is in the path of the other, \r
-and therefore by Lemma \ref{lem:pathmessages}, $\mathsf{t}$ is in the path of $\mathsf{x}$.\r
-\r
-\item Let $\mathsf{z}$ be the message of $\mathsf{D}$ whose path includes $\mathsf{t}$. \r
-By Lemma \ref{lem:twomessages}, every message in $\mathsf{P_D}$ with sequence number smaller \r
-than $\mathsf{s_w}$ is in the path of $\mathsf{z}$. Since $\mathsf{t}$ is in the path of \r
-$\mathsf{z}$, every message in $\mathsf{P_D}$ with smaller sequence number than \r
-$\mathsf{s_t = s_n}$ is in $\mathsf{T}$. \r
-Therefore, $\mathsf{P_D}$ is consistent with $\mathsf{T}$.\r
-\r
-\end{itemize}\r
-\end{proof}\r
-\r
-\subsection{Future Work}\r
-\paragraph{Support Messages}\r
-  A message is dead once receiving machine sends an entry with a newer\r
-  sequence identifier\r
-\r
-\paragraph{Persistent data structures}\r
-       Root object w/ fields\r
-       Other objects can be reachable from root\r
-       Each object has its own entries\r
-       Dead objects correspond to dead \r
-\r
-\paragraph{Multiple App Sharing}\r
-\r
-Idea is to separate subspace of entries...  Shared with other cloud...\r
+\r
 \end{document}\r