-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
-% Short Sectioned Assignment\r
-% LaTeX Template\r
-% Version 1.0 (5/5/12)\r
-%\r
-% This template has been downloaded from:\r
-% http://www.LaTeXTemplates.com\r
-%\r
-% Original author:\r
-% Frits Wenneker (http://www.howtotex.com)\r
-%\r
-% License:\r
-% CC BY-NC-SA 3.0 (http://creativecommons.org/licenses/by-nc-sa/3.0/)\r
-%\r
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
-\r
-%----------------------------------------------------------------------------------------\r
-% PACKAGES AND OTHER DOCUMENT CONFIGURATIONS\r
-%----------------------------------------------------------------------------------------\r
-\r
-\documentclass[paper=letter, fontsize=11pt]{scrartcl} % A4 paper and 11pt font size\r
-\r
-\usepackage[T1]{fontenc} % Use 8-bit encoding that has 256 glyphs\r
-\usepackage{fourier} % Use the Adobe Utopia font for the document - comment this line to return to the LaTeX default\r
-\usepackage[english]{babel} % English language/hyphenation\r
-\usepackage{amsmath,amsfonts,amsthm} % Math packages\r
+\documentclass[11pt]{article}\r
+\newcommand{\tuple}[1]{\ensuremath \langle #1 \rangle}\r
+\usepackage{color}\r
+\usepackage{amsthm}\r
+\usepackage{amsmath}\r
\usepackage{graphicx}\r
-\usepackage{lipsum} % Used for inserting dummy 'Lorem ipsum' text into the template\r
-\usepackage{hyperref}\r
+\usepackage{mathrsfs}\r
\usepackage{amssymb}\r
-\usepackage{listings}\r
-\usepackage[]{algorithm2e}\r
-\usepackage{algpseudocode}\r
-\usepackage{enumerate}\r
-\usepackage[table,xcdraw]{xcolor}\r
-\usepackage{sectsty} % Allows customizing section commands\r
-\usepackage{float}\r
-\usepackage{caption}\r
-\usepackage{gensymb} % to used degree symbol \r
-\usepackage{siunitx} \r
-\usepackage{enumitem}\r
-\r
-\usepackage[sc]{mathpazo}\r
-\allsectionsfont{ \normalfont\scshape} % Make all sections the default font and small caps\r
-\usepackage{fancyhdr} % Custom headers and footers\r
-\pagestyle{fancyplain} % Makes all pages in the document conform to the custom headers and footers\r
-\fancyhead{} % No page header - if you want one, create it in the same way as the footers below\r
-\fancyfoot[L]{} % Empty left footer\r
-\fancyfoot[C]{} % Empty center footer\r
-\fancyfoot[R]{\thepage} % Page numbering for right footer\r
-\renewcommand{\headrulewidth}{0pt} % Remove header underlines\r
-\renewcommand{\footrulewidth}{0pt} % Remove footer underlines\r
-\setlength{\headheight}{13.6pt} % Customize the height of the header\r
-\r
-\numberwithin{equation}{section} % Number equations within sections (i.e. 1.1, 1.2, 2.1, 2.2 instead of 1, 2, 3, 4)\r
-\numberwithin{figure}{section} % Number figures within sections (i.e. 1.1, 1.2, 2.1, 2.2 instead of 1, 2, 3, 4)\r
-\numberwithin{table}{section} % Number tables within sections (i.e. 1.1, 1.2, 2.1, 2.2 instead of 1, 2, 3, 4)\r
+\usepackage{algorithm}\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
+\algnewcommand{\algorithmicgoto}{\textbf{go to}}%\r
+\algnewcommand{\Goto}[1]{\algorithmicgoto~\ref{#1}}%\r
+\r
+\r
+\begin{document}\r
+\r
\r
\setlength\parindent{0pt} % Removes all indentation from paragraphs - comment this line for an assignment with lots of text\r
\r
-%----------------------------------------------------------------------------------------\r
-% TITLE SECTION\r
-%----------------------------------------------------------------------------------------\r
-\newcommand{\horrule}[1]{\rule{\linewidth}{#1}} % Create horizontal rule command with 1 argument of height\r
\r
-\title{ \r
-\normalfont \normalsize \r
-\textsc{University of California Irvine} \\ % Your university, school and/or department name(s)\r
-\textsc{Prgramming Language Research Group} \\ [25pt]\r
-\horrule{0.5pt} \\[0.4cm] % Thin top horizontal rule\r
-\huge IoTCloud Version 2.0\\ % The assignment title\r
-\horrule{2pt} \\[0.5cm] % Thick bottom horizontal rule\r
-}\r
+\section{\textbf{Introduction}}\r
\r
-\author{Authors} % Your name\r
\r
+\section{Approach}\r
\r
-\date{\normalsize\today} % Today's date or a custom date\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
\r
-\begin{document}\r
+\subsection{The Arbitrator}\r
+Each key has an arbitrator that makes the final decision when it comes to whether a specific transaction containing that key updates the state of the system or is aborted. This ensures that clients can make offline updates and then push those updates to the server at a later time. The arbitrator then tries to merge those updates and if possible will commit them into the current working state of the system. If not possible then the arbitrator will abort that transaction. The arbitrator arbitrates on transactions in order of transaction sequence number.\r
\r
-\maketitle % Print the title\r
\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+\section{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
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Get Slot:}\\\r
+Returns to the client the slots that have a sequence number that is greater than or equal to the sequence number that is in the request.\r
+\begin{algorithmic}[1]\r
+\Function{GetSlot}{$s_g$} throws $Server\_Connection\_Timeout$, $Server\_Response\_Timeout$\r
+\State \Return{$\{\tuple{s, sv} \in SL \mid s \geq s_g\}$}\r
+\EndFunction\r
+\end{algorithmic}%\end{varwidth}% \r
+%}\r
\r
\r
-%---------------------------------------------------------------------------------------\r
-% Custom Stuff\r
-%---------------------------------------------------------------------------------------\r
-\newcommand{\tab}[1]{\hspace{.2\textwidth}\rlap{#1}}\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Get Slot:}\\\r
+Puts a slot in the server memory if the slot has the correct sequence number. Also resizes the server memory if needed.\r
+\begin{algorithmic}[1]\r
+\Function{PutSlot}{$s_p,sv_p,max'$} throws $Server\_Connection\_Timeout$, $Server\_Response\_Timeout$\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}%\end{varwidth}% \r
+%}\r
\r
\r
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\r
+\section{Client Algorithm}\r
\r
+\subsection{\textbf{Client Notation Conventions}}\r
+$k$ is key of entry \\\r
+$v$ is value of entry \\\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
+$G$ is a set of $kv$ that is the guard \\\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
\r
-\section{\textbf{Introduction}}\r
+$colres$ is a collision resolution entry, $\tuple{id, seq_{old}, seq_{new}, true \lor false}$ \\\r
+$lastmsg$ is a last message entry, $\tuple{seq, id}$ \\\r
+$qstate$ is a queue state entry, $\tuple{size}$ \\\r
+$newkey$ is a new key entry, $\tuple{k, id}$, $id$ is ID of arbitrator \\\r
+$abort$ is an abort transaction entry, $\tuple{seq_{clientlocal}, seq_{server}, id, arb, seq_{arb}}$ \\\r
+$transpart$ is a transaction part entry, $\tuple{Dat,arb,seq_{clientLocal}, seq_{server}, id, partnum, isLast}$\\\r
+$compart$ is a commit part entry, $\tuple{Dat,seq_{trans}, seq_{server}, id, partnum, isLast}$\\\r
+\r
+$de$ is a data entry that can one of: $transpart$, $lastmsg$, $qstate$, $colres$, $newkey$, $compart$, $abort$ \\\r
+$DE$ is a set of all data entries, possibly of different types, in a single message, set of $de$\\\r
+\r
+\r
+$pendingTransaction$ is a pending transaction, $\tuple{KV, G, id, seq_{clientLocal}}$ \\\r
+$Transaction$ is a Transaction container that houses transaction parts together, $\tuple{Parts, KV, G,seq_{local}, seq_{server},id, arb}$\\\r
+$Commit$ is a commit container that houses commit parts together, $\tuple{Parts, KV, seq_{trans}, seq_{server},id}$\r
+$ArbitrationRound$ is a commit and a group of aborts where all the aborts must be sent before the commit, $\tuple{commit, AbortSet, SentSet}$\r
+\r
+$status$ is the status of a transaction and can be: $aborted, pending, committed, sentpartial, sentfully, noeffect$\r
+$TransStatus$ is the status of a transaction, $\tuple{status}$\\\r
+\r
+$slotDat = \tuple{seq,id,DE,hmac_p,hmac_c}$ \\\r
+$slot = \tuple{seq, Encrpt(slotDat)}$\\\r
+\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
+$MAX\_ROUND\_SIZE$ = max number of parts that an arbitration round can have before being full. \\\r
+\r
+\subsubsection{Primitive Variables}\r
+$max\_size$ = max size of the block chain.\\\r
+$clntTransactionNum \gets 0$ = current client transaction number that this client created.\\\r
+$newPendingTransaction$ = transaction being built.\\\r
+$arbitrationSeqNum \gets 0$ = sequence number used by the arbitrator to label the commits and aborts it creates\\\r
+$hadPartialSendToServer gets false$ = if the last attempt to send the server had a recieve timeout.\\\r
+\r
+\r
+\subsubsection{Sets and Lists}\r
+\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 sequence number of the last slot.\\\r
+$Arbitrator$ = set of $\tuple{k,id}$ containing the key and its arbitrating device.\\ne 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
+$CommittedKV$ = set of committed key value pairs (initially $\emptyset$).\\\r
+$SpeculatedKV$ = set of speculated key value pairs (initially $\emptyset$).\\\r
+$PendingTransactionQueue$ = queue of transactions that need to be sent.\\\r
+$LastTransactionArbitrated$ = set of $\tuple{id, seq}$ with the last sequence number an arbitrator arbitrated on.\\\r
+$LiveTransactions$ = set of transactions with their parts.\\\r
+$LiveCommits$ = set of live commits and their parts.\\\r
+$OfflineTransAtServer$ = set of transactions that were sent to the server but were arbitrated through local communication.\\ \r
+$SendArbQueue$ = queue of arbitration rounds that have yet to be sent to the server.\\\r
+$LastTransSeenMid$ = Last transaction seen from a specific machine from the server.\\\r
+$LastArbLocalArbitrated$ = Last local sequence number seen from a client.\\\r
+$LastCommitSeenFromArbitrator$ = last commit seen from a specific arbitrator.\\\r
+\r
+\subsection{Helper Functions}\r
+The following helper functions are needed:\\\r
+\r
+$MaxSlot(SL_s)= \tuple{s, sv} \mid \tuple{s, sv} \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} \in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s \leq s_s$ \\\r
+$DecodeParts(transpart)= $ Converts the part data into KV sets and Guard Condition sets.\\\r
+$DecodeParts(compart)= $ Converts the part data into a KV set.\\\r
+$GenerateParts(Commit)= $ Fills the commit with parts generated by its content.\\\r
+$GenerateParts(Transaction)= $ Fills the transaction with parts generated by its content.\\\r
+$SetTransStatus(TransStatus, Transaction_Identifier) = $ saves a transaction status.\\ \r
+$ChangeTransStatus(TransStatus, newStatus) = $ changes a transaction status.\\ \r
+$GetTransStatus(Transaction_Identifier) = $ gets a transaction status.\\ \r
+$DeleteTransStatus(Transaction_Identifier) = $ delete a transaction status.\\ \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{GetSize}{$a$}\r
+ \State \Return{Size in bytes of $a$}\r
+\EndFunction\r
+\end{algorithmic}\r
+%\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{Error}{$msg$}\r
+ \State $Print(msg)$\r
+ \State $Halt()$\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{CalcResizeThresh}{$maxsize$}\r
+ \State $lower \gets \left \lfloor {maxsize * RESIZE\_THRESH\_PERCENT} \right \rfloor - 1$\r
+ \State \Return{$lower + $\Call{Random}{$maxsize - lower$}}\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{CalcNewSize}{$maxsize$}\r
+ \State \Return{$\left \lceil {maxsize * RESIZE\_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{ShouldResize}{$ $}\r
+ \State $LiveSlots \gets \{slot_s|slot_s \in LocalSlots \land $\Call{SlotHasLive}{$slot_s$}$\}$\r
+ \State \Return{$|LiveSlots| \geq $\Call{CalcResizeThresh}{$max\_size$}} \r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\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{DEHasSpace}{$DE_a, de_a$}\r
+ \State $newsize \gets $ \Call{GetSize}{$DE_a$} $ + $ \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
+% 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{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
+% Get Arbitrator KV\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Get Arbitrator for KV Set:}\\\r
+Get the arbitrator for a given key value set.\r
+\begin{algorithmic}[1]\r
+\Function{GetArbitratorKV}{$KV_a$} \r
+ \State \Return{$id'$ such that $\exists \tuple{k',v'} \in KV_a, id' =$ \Call{GetArbitrator}{$k'$}}\r
+\EndFunction\r
+\end{algorithmic}\r
+%\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{GetNextSeq}{$k$}\r
+ \LeftComment{Get the largest known sequence number}\r
+ \State $seq_{ret} \gets seq$ such that $\tuple{id, seq}\in LastSlot \land (\forall \tuple{id', seq'} \in LastSlo, 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
+% Create Collision\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Create ColRes:}\\\r
+Generate a colres data entry.\r
+\begin{algorithmic}[1]\r
+\Function{CreateColRes}{$is_a, seq_{a_{old}}, seq_{a_{new}}, isequal_a$}\r
+ \State \Return{$\tuple{id_a, seq_{a_{old}}, seq_{a_{new}},}isequal_a$}\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+% Check and Create Last Message Data Entry\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Check and Create Last Message Data Entry:}\\\r
+Check if a last message entry needs to be created for this slot and if so create it. The check is done by checking if there are any newer slots with the same id or if there is already a last message slot with a newer sequence number.\r
+\begin{algorithmic}[1]\r
+\Function{CheckCreateLastMsgEntry}{$seq_a, id_a$}\r
+ \State $AllLastMsg \gets$ \Call{GetLastMsg}{}\\\r
+ \r
+ \LeftComment{Already Has one}\r
+ \If{$\exists \tuple{seq', id'} \in AllLastMsg, id_a=id' \land seq'=seq_a$}\r
+ \State \Return{$\emptyset$}\r
+ \EndIf\\\r
+ \r
+ \LeftComment{Not latest slot from that client}\r
+ \If{$\exists \tuple{seq_1', \tuple{seq_2',id',DE',hmac_p',hmac_c'}} \in LocalSlots, id_a=id' \land seq_1'>seq_a$}\r
+ \State \Return{$\emptyset$}\\\r
+ \EndIf\\\r
+ \r
+ \State \Return{$\{\tuple{seq_a, id_a}\}$}\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+%Evaluate Guard\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Evaluate Guard:}\\\r
+Evaluate Guard Condition checks if all the KV pairs in the guard condition match the declared KV pairs.\r
+\begin{algorithmic}[1]\r
+\Function{EvaluateGuard}{$G_a, KV_a$}\r
+\r
+ \If{$\exists \tuple{k_G, v_G} \in G_a, \tuple{k_{KV},v_{KV}} \in KV_a, k_G=K_{KV} \land v_G \neq v_{KV}$}\r
+ \State \Return{False}\r
+ \EndIf\r
+ \r
+ \State \Return{True}\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{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',id',DE',hmac_p',hmac_c'}} \in LocalSlots$}\r
+ \ForAll{$a' \in DE', a'$ is a $abort$}\r
+ \State $\tuple{seq_l', seq_s', id', arb', seq_{arb}'} \gets a'$\r
+ \State $AbrtSet \gets AbrtSet \cup \{seq_l', seq_s', id', arb', seq_{arb}', seq'\}$\r
+ \EndFor\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{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',id',DE',hmac_p',hmac_c'}} \in LocalSlots$}\r
+ \ForAll{$q' \in DE', q'$ is a $qstate$}\r
+ \State $\tuple{size'} \gets q'$\r
+ \State $QSet \gets QSet \cup \{\tuple{size', seq'}\}$\r
+ \EndFor\r
+ \EndFor\r
+ \State \Return{$QSet$}\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+% Get all New Keys\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Get all new keys:}\\\r
+Get all new keys that are currently in the local block chain. Iterate over all the local slots and extract all the new keys from each slot.\r
+\begin{algorithmic}[1]\r
+\Function{GetNewKeys}{$ $}\r
+ \State $NKSet \gets \emptyset$ \Comment{Set of the new keys}\\\r
+ \r
+ \LeftComment{Iterate over all the slots saved locally}\r
+ \ForAll{$\tuple{s_1', \tuple{seq',id_1',DE',hmac_p',hmac_c'}} \in LocalSlots$}\r
+ \ForAll{$nk' \in DE', nk'$ is a $newkey$}\r
+ \State $\tuple{k', id_2'} \gets nk'$\r
+ \State $NKSet \gets NKSet \cup \{\tuple{k', id_2', seq'}\}$\r
+ \EndFor\r
+ \EndFor\r
+ \State \Return{$NKSet$}\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+% Get all Collision Resolutions\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Get all collision resolutions:}\\\r
+Get all the collision resolution entries fron the slots. \r
+\begin{algorithmic}[1]\r
+\Function{GetColRes}{$ $}\r
+ \State $CRSet \gets \emptyset$ \Comment{Set of the new keys}\\\r
+ \r
+ \LeftComment{Iterate over all the slots saved locally}\r
+ \ForAll{$\tuple{s_1', \tuple{seq',id_1',DE',hmac_p',hmac_c'}} \in LocalSlots$}\r
+ \ForAll{$cr' \in DE', nk'$ is a $colres$}\r
+ \State $\tuple{id', seq_{old}', seq_{new}', local'} \gets cr'$\r
+ \State $CRSet \gets CRSet \cup \{\tuple{id', seq_{old}', seq_{new}', local', seq'}\}$\r
+ \EndFor\r
+ \EndFor\r
+ \State \Return{$CRSet$}\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+% Get all Last Messages States\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Get all last message data entries:}\\\r
+Get all last msg that are currently in the local block chain. Iterate over all the local slots and extract all the last msg from each slot.\r
+\begin{algorithmic}[1]\r
+\Function{GetLastMsg}{$ $}\r
+ \State $LMSet \gets \emptyset$ \Comment{Set of the last msg}\\\r
+ \r
+ \LeftComment{Iterate over all the slots saved locally}\r
+ \ForAll{$\tuple{s_1', \tuple{seq_1',id_1',DE',hmac_p',hmac_c'}} \in LocalSlots$}\r
+ \ForAll{$lm' \in DE', lm'$ is a $lastmsg$}\r
+ \State $\tuple{seq_2', id_2'} \gets lm'$\r
+ \State $LMSet \gets LMSet \cup \{\tuple{seq_2', id_2', seq_1'}\}$\r
+ \EndFor\r
+ \EndFor\r
+ \State \Return{$LMSet$}\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}%\r
+%}\r
+\r
+% Get all Transaction Parts\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Get all the transaction part entries:}\\\r
+Get all the transaction parts from the slots.\r
+\begin{algorithmic}[1]\r
+\Function{GetTransParts}{$ $}\r
+ \State $TPSet \gets \emptyset$ \r
+ \r
+ \LeftComment{Iterate over all the slots saved locally}\r
+ \ForAll{$\tuple{s_1', \tuple{seq_1',id_1',DE',hmac_p',hmac_c'}} \in LocalSlots$}\r
+ \ForAll{$tp' \in DE', tp'$ is a $transpart$}\r
+ \State $\tuple{Dat',arb',seq_{clientLocal}', seq_{server}', id', partnum', isLast'} \gets tp'$\r
+ \State $TPSet \gets TPSet \cup \{\tuple{Dat',arb',seq_{clientLocal}', seq_{server}', id', partnum', isLast', seq_1'}\}$\r
+ \EndFor\r
+ \EndFor\r
+ \State \Return{$TPSet$}\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}%\r
+%}\r
+\r
+% Get all Commit Parts\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Get all the commit part entries:}\\\r
+Get all the commit parts from the slots.\r
+\begin{algorithmic}[1]\r
+\Function{GetComParts}{$ $}\r
+ \State $CPSet \gets \emptyset$ \r
+ \r
+ \LeftComment{Iterate over all the slots saved locally}\r
+ \ForAll{$\tuple{s_1', \tuple{seq_1',id_1',DE',hmac_p',hmac_c'}} \in LocalSlots$}\r
+ \ForAll{$cp' \in DE', cp'$ is a $compart$}\r
+ \State $\tuple{Dat',seq_{trans}', seq_{server}', id', partnum', isLast'} \gets cp'$\r
+ \State $CPSet \gets CPSet \cup \{\tuple{Dat',seq_{trans}', seq_{server}', id', partnum', isLast', seq_1'}\}$\r
+ \EndFor\r
+ \EndFor\r
+ \State \Return{$CPSet$}\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}%\r
+%}\r
+\r
+\r
+\r
+\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{CheckQStateLive}{$qstate_a, seq_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', seq'} \in AllQStates, size' > size_a$}\r
+ \State \Return{false}\r
+ \ElsIf{$\exists \tuple{size', seq'} \in AllQStates, size' = size_a \land seq' > seq_a$}\r
+ \State \Return{false}\r
+ \EndIf\r
+ \State \Return{true}\r
+ \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{CheckLastMsgLive}{$lastmsg_a$}\r
+ \State $\tuple{seq_a, id_a} \gets lastmsg_a$\\\r
+ \State $AllLastMsg \gets$ \Call{GetLastMsg}{} \Comment{Get all the last messages} \\\r
+ \r
+ \If{$\exists \tuple{seq_1', id', seq_2'} \in AllLastMsg, id'=id_a \land seq_1' > seq_a$}\r
+ \State \Return{false}\r
+ \ElsIf{$\exists \tuple{seq_1', id', seq_2'} \in AllLastMsg, id'=id_a \land seq_1' = seq_a \land seq_2' > seq_a$}\r
+ \State \Return{false}\r
+ \EndIf\r
+ \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 unless there is a resuced version of the new key that is newer.\r
+\begin{algorithmic}[1]\r
+\Function{CheckNewkeyLive}{$newkey_a, seq$}\r
+ \State $\tuple{k_a, id_a} \gets newkey_a$\r
+ \State $AllNewKeys \gets$ \Call{GetNewKeys}{} \Comment{Get all the new keys} \\\r
+ \r
+ \If{$\exists \tuple{k', id', seq'} \in AllNewKeys, k'=k_a \land id'=id_a \land seq' > seq$}\r
+ \State \Return{False}\r
+ \ElsIf{$\exists \tuple{k', id', seq'} \in AllNewKeys, k'=k_a \land id'\neq id_a \land seq' > seq$}\r
+ \State \Return{False} \Comment{Delete an attempt to insert a new key that already exists}\r
+ \EndIf\r
+ \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{CheckAbortLive}{$abort_a, seq_a$}\r
+ \State $\tuple{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$}\r
+ \State \Return{false}\r
+ \Else\r
+ \State $AllAborts \gets$ \Call{GetAborts}{} \Comment{Get all the aborts} \\\r
+ \If{$\exists \tuple{seq_{trans}',id_{trans}', seq'} \in AllAborts, seq_{a_{trans}} = seq_{trans}' \land id_a = id_{trans}' \land seq' > seq_a$}\r
+ \State \Return{false}\r
+ \EndIf\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
+\Function{CheckColResLive}{$colres_a, seq_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
+ \r
+ \State $AllColRes \gets$ \Call{GetColRes}{}\r
+ \If{$\exists \tuple{id', seq_{old}', seq_{new}', local', seq'} \in AllColRes, id'=id_a \land seq_{old}'= seq_{a_{old}} \land seq_{new}'= seq_{a_{new}} \land local'=equal_a \land seq_2' > seq_a$}\r
+ \State \Return{false}\r
+ \EndIf\r
+ \r
+ \State \Return{true}\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+%Check Transaction Part Live\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Check Transaction Part Live:}\\\r
+Check if a transaction part is live or not.\r
+\begin{algorithmic}[1]\r
+\Function{CheckTransPartLive}{$transpart_a, seq_a$}\r
+ \State $\tuple{Dat, arb,seq_{clientLocal}, seq_{server}, id, partnum,isLast} \gets transpart_a$\r
+ \r
+ \If{$\exists \tuple{id',seq'} \in LastTransactionArbitrated \land id'=arb land seq' \geq seq_{server}$}\r
+ \State \Return{False}\r
+ \EndIf\r
+ \r
+ \State $AllTransParts \gets$ \Call{GetTransParts}{} \r
+ \If{$\exists \tuple{Dat',arb',seq_{clientLocal}', seq_{server}', id', partnum', isLast', seq'} \in AllTransParts, seq_{server} = seq_{server}' \land partnum' = partnum \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 Commit Part Live\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Check Commit Part Live:}\\\r
+Check if a commit part is live or not.\r
+\begin{algorithmic}[1]\r
+\Function{CheckCommitPartLive}{$commitpart_a, seq_a$}\r
+ \State $\tuple{Dat,seq_t, seq_s, id, partnum, isLast, seq} \gets commitpart_a$\r
+ \State $AllComParts \gets $ \Call{GetComParts}{}\\\r
+ \r
+ \If{$\exists \tuple{Dat',seq_t', seq_s', id, partnum', isLast', seq'} \in AllComParts, seq_s = seq_s' \land partnum'= partnum \land seq' > seq_a$}\r
+ \State \Return{False}\r
+ \EndIf\r
+ \r
+ \ForAll{$\tuple{P, KV, seq_t, seq_s,id} \in LiveCommits$}\r
+ \If{$commitpart_a \in P$}\r
+ \State \Return{True}\r
+ \EndIf\r
+ \EndFor\r
+ \r
+ \State \Return{False}\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\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, seq$}\r
+ \If{$datentry$ is a $compart$}\r
+ \State \Return{\Call{CheckCommitPartLive}{$datentry, seq$}}\\r
+ \ElsIf{$datentry$ is a $abort$}\r
+ \State \Return{\Call{CheckAbortLive}{$datentry, seq$}}\\r
+ \ElsIf{$datentry$ is a $transpart$}\r
+ \State \Return{\Call{CheckTransPartLive}{$datentry,seq$}}\\r
+ \ElsIf{$datentry$ is a $lastmsg$}\r
+ \State \Return{\Call{CheckLastMsgLive}{$datentry, seq$}}\\r
+ \ElsIf{$datentry$ is a $colres$}\r
+ \State \Return{\Call{CheckColResLive}{$datentry, seq$}}\\r
+ \ElsIf{$datentry$ is a $qstate$}\r
+ \State \Return{\Call{CheckQStateLive}{$datentry, seq$}}\r
+ \ElsIf{$datentry$ is a $newkey$}\r
+ \State \Return{\Call{CheckNewkeyLive}{$datentry, seq$}}\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{seq_1, \tuple{seq_2,id,DE,hmac_p,hmac_c}} \in LocalSlots$\r
+ \r
+ \ForAll{$datentry \in DE$}\r
+ \If{\Call{CheckLive}{$datentry, seq_1$}} \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
+% Rejected Messages\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Rejected Messages:}\\\r
+\begin{algorithmic}[1]\r
+\Function{RejectedMessages}{$DE_a$}\r
+ \State $seq_{old} \gets seq$ such that $\tuple{seq} \in RejectedSlotList \land \forall \tuple{seq'} \in RejectedSlotList, seq \geq seq'$\r
+ \State $prev \gets -1$\\\r
+ \r
+ \If{$|RejectedSlotList| \geq REJECTED\_THRESH$}\r
+ \State $seq_{new} \gets seq$ such that $\tuple{seq} \in RejectedSlotList \land \forall \tuple{seq'} \in RejectedSlotList, seq \leq seq'$\\\r
+ \State $colres \gets $ \Call{CreateColRes}{$LOCAL\_ID, seq_{old}, seq_{new}, false$} \r
+ \State \Return{$DE_a \cup \{colres\}$}\r
+ \EndIf\\\r
+ \r
+ \ForAll{$\tuple{seq} \in RejectedSlotList$ sorted by $seq$}\r
+ \If{$\exists \tuple{seq',Dat'} \in LocalSlots$}\r
+ \State Break\r
+ \EndIf\r
+ \State $prev \gets seq$\r
+ \EndFor\\\r
+ \r
+ \If{$prev \neq -1$}\r
+ \State $DE_a \gets DE_a \cup$ \Call{CreateColRes}{$LOCAL\_ID, seq_{old}, prev, false$}\r
+ \EndIf\\\r
+ \r
+ \State $RejectedSlotList \gets \{\tuple{seq}| \tuple{seq} \in RejectedSlotList, seq > prev\}$\\\r
+ \r
+ \ForAll{$\tuple{seq} \in RejectedSlotList$ sorted by $seq$}\r
+ \State $DE_a \gets DE_a \cup$ \Call{CreateColRes}{$LOCAL\_ID, seq,seq, false$}\r
+ \EndFor\\\r
+ \r
+ \State \Return{$DE_a$}\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\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
+ \State $DE' \gets DE' \cup$ \Call{CheckCreateLastMsgEntry}{$seq', id'$} \Comment{Get the last message too if we need it}\\\r
+ \r
+ \ForAll{$de \in DE'$} \Comment{Iterate over all the entries}\r
+ \If{\Call{CheckLive}{$de, cseq$}} \Comment{data entry is live}\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{$\tuple{$true$,DE_a}$}\r
+ \Else\r
+ \State \Return{$\tuple{$false$,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{$\tuple{$false$,DE_a}$}\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+% Optional Rescue\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Optional Rescue:}\\\r
+This rescue is not mandatory. This is trying to fill the remaining portion of the slot with rescued data so that no space is wasted. If we encounter a data entry that does not fit move on to the next, maybe that one will fit. Do this until we skipped too many live data entries.\r
+\begin{algorithmic}[1]\r
+\Function{OptionalRescue}{$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 $largestseq \gets seq$ such that $\tuple{seq, DE}\in LocalSlots \land (\forall \tuple{seq', DE'} \in LocalSlots, seq \geq seq')$\r
+\r
+ \State $numofskips \gets 0$\r
+ \State $cseq \gets smallestseq$\\\r
+ \r
+ \LeftComment{Check the least slots to rescue and live entries}\r
+ \While{$cseq < largestseq$}\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, cseq$}} \Comment{data entry is live}\r
+ \State $de \gets $ \Call{CreateRescuedEntry}{de} \Comment{Resize entry if needed}\\\r
+ \r
+ \If{$de \in DE_a$} \Comment{Already being rescued}\r
+ \State Continue\r
+ \EndIf\\\r
+ \r
+ \If{\Call{DEHasSpace}{$DE_a, de$}}\r
+ \State $DE_a \gets DE_a \cup de$ \Comment{Had enoug space to add it}\r
+ \ElsIf{$numofskips \geq MAX\_RESCUE\_SKIPS$}\r
+ \State \Return{$DE_a$}\r
+ \Else\r
+ $numofskips \gets numofskips +1$\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
+% Create New Slot\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Create New Slot:}\\\r
+Create a slot and encrypt it.\r
+\begin{algorithmic}[1]\r
+\Function{CreateNewSlot}{$seq_a, DE_a$}\r
+ \State $\tuple{seq, SDE} \gets \tuple{seq', SDE'}$ such that $\tuple{seq', SDE'}\in LocalSlots \land (\forall \tuple{seq'', DE''} \in LocalSlots, seq' \geq seq'')$\r
+ \State $\tuple{seq,id,DE,hmac_p,hmac_c} \gets SDE$\r
+ \State $newhmac \gets $ \Call{GenerateHmac}{$seq_a, LOCAL\_ID, DE_a, hmac_p$}\r
+ \State $newSDE \gets \tuple{seq,LOCAL\_ID,DE_a,hmac_c,newhmac}$\r
+ \State $encryptnewSDE \gets $\Call{Encrypt}{newSDE}\r
+ \State \Return{$\tuple{seq_a, encryptnewSDE}$}\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+\r
+\r
+\r
+\r
+\r
+\r
+\r
+\r
+\r
+\r
+\r
+\r
+% Fill Slot\r
+%% \noindent\fbox{%\r
+%% \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+% \begin{algorithm}\r
+\textbf{Fill Slot:}\\\r
+Fill a slot with data that needs to be inserted into the block chain.\r
+\begin{algorithmic}[1]\r
+\Function{FillSlot}{$newkey_a $}\r
+ \State $resize \gets False$\r
+ \State $newsize \gets 0$\r
+ \r
+ \State $DE \gets \emptyset$ \Comment{The data entries for this slot} \label{resetMarker}\r
+ \State $seq \gets $ \Call{GetNextSeq}{} \Comment{Get the sequence number for this slot}\r
+\r
+ \r
+ \State $resize \gets resize \lor $ \Call{ShouldResize}{ } \Comment{Check if we should resize}\r
+ \If{$resize$}\r
+ \State $newsize \gets$ \Call{CalcNewSize}{$max\_size$}\r
+ \State $DE \gets DE \cup \{$\Call{CreateQState}{$newsize$}$\}$\r
+ \EndIf\\\r
+ \r
+ \If{$RejectedSlotList \neq \emptyset$} \r
+ \State $DE \gets$ \Call{RejectedMessages}{$DE$}\r
+ \EndIf\\\r
+\r
+ \State $\tuple{needRezize,DE} \gets$ \Call{MandatoryRescue}{$DE$} \Comment{Round 1 of rescue}\r
+ \If{$needRezize \land \lnot resize$}\r
+ \LeftComment{Data was going to fall off the end so try again with a forced resize}\r
+ \State $resize \gets $ true\r
+ \State \Goto{resetMarker}\r
+ \EndIf\\\r
+ \r
+ \If{$newkey_a \neq NULL \land $\Call{DEHasSpace}{$DE, newkey_a$}}\r
+ \State $DE \gets DE \cup \{newkey_a\}$\r
+ \EndIf\\\r
+ \r
+ \ForAll{$\tuple{commit, AbortSet, SentSet} \in ArbitrationRound$ in order of insertion}\r
+ \ForAll{$abort \in (AbortSet \setminus SentSet)$} \r
+ \State $\tuple{seq_{clientlocal}, seq_{server}, id, arb, seq_{arb}} \gets abort$\r
+ \State $abort \gets \tuple{seq_{clientlocal}, seq, id, arb, seq_{arb}}$ \Comment{Set sequence number}\r
+ \r
+ \If{\Call{DEHasSpace}{$De, abort$}}\r
+ \State $DE \gets DE \cup abort$\r
+ \Else\r
+ \State \Goto{EndArb}\r
+ \EndIf\r
+ \EndFor\r
+ \r
+ \If{$commit \neq NULL$}\r
+ \If{\Call{DEHasSpace}{$De, commit$}}\r
+ \State $DE \gets DE \cup commit$\r
+ \Else\r
+ \State \Goto{EndArb}\r
+ \EndIf\r
+ \EndIf\r
+ \EndFor \label{EndArb}\r
+ \r
+ \r
+ \If{$|PendingTransactionQueue| > 0$}\r
+ \State $\tuple{\tuple{P, KV, G,seq_l, seq_s,id, arb}, Sent, hadTimeout} \gets PendingTransactionQueue.peak()$\r
+ \r
+ \If{$(|Sent| = 0 \land \lnot hadTimeout) \lor (seq_s = -1)$}\r
+ \State $seq_s \gets seq$\r
+ \ForAll{$part \in P$}\r
+ \State $\tuple{Dat,arb,seq_{cl}, seq_{server}, id, partnum, isLast} \gets part$\r
+ \State $part \gets \tuple{Dat,arb,seq_{cl}, seq, id, partnum, isLast}$\r
+ \EndFor\r
+ \EndIf\r
+ \r
+ \ForAll{$part \in (P \setminus Sent)$}\r
+ \If{\Call{DEHasSpace}{$De, part$}}\r
+ \State $DE \gets DE \cup part$\r
+ \Else\r
+ \State \Goto{EndTrans}\r
+ \EndIf\r
+ \EndFor\r
+ \EndIf \label{EndTrans}\r
+ \r
+\r
+ \LeftComment{Rescue data to fill slot data entry section}\r
+ \State $DE \gets$ \Call{OptionalRescue}{$DE$}\\\r
+ \State $newslot \gets $\Call{CreateNewSlot}{$seq, DE$}\r
+ \State \Return{$\tuple{newslot,DE, newsize}$} \r
+\EndFunction\r
+\end{algorithmic}\r
+% \end{algorithm}\r
+\r
+% %\end{varwidth}% \r
+% } \r
+\r
+\r
+\r
+\r
+\r
+\r
+\r
+\r
+% Send to Server\r
+%% \noindent\fbox{%\r
+%% \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+% \begin{algorithm}\r
+\textbf{Send to Server:}\\\r
+Send local data to server if there is any local data that needs to be sent.\r
+\algblock[TryCatchFinally]{try}{endtry}\r
+\algcblock[TryCatchFinally]{TryCatchFinally}{finally}{endtry}\r
+\algcblockdefx[TryCatchFinally]{TryCatchFinally}{catch}{endtry}\r
+ [1]{\textbf{catch} #1}\r
+ {\textbf{end try}}\r
+\r
+\begin{algorithmic}[1]\r
+\Function{SendToServer}{$slot_a, newsize_a$} throws $Server\_Connection\_Timeout$, $Server\_Response\_Timeout$\r
+ \State $\tuple{seq_a, DE_A} \gets slot_a$\r
+ \State $EDE_a \gets $ \Call{Encrypt}{$DE_A$}\r
+ \State $slot_a \gets \tuple{seq_a, EDE_a}$\r
+ \State $\tuple{success, NewSlots} \gets$ \Call{PutSlot}{$seq_a, newslot, newsize_a$}\\\r
+ \r
+ \If{$success$}\r
+ \State $RejectedSlotList \gets \emptyset$\r
+ \State \Return{$\tuple{true, \{newslot\}}$}\r
+ \Else\r
+ \If{$|newslots| = 0$}\r
+ \State \Call{Error}{"Server rejected but did not send any slots"}\r
+ \EndIf\\\r
+ \r
+ \State $NewSlots_{decrypt} \gets \emptyset$\r
+ \ForAll{$\tuple{seq', EDat'} \in NewSlots$}\r
+ \State $DDat \gets $ \Call{Decrypt}{$EDat'$}\r
+ \State $NewSlots_{decrypt} \gets NewSlots_{decrypted} \cup \tuple{seq',DDat}$\r
+ \EndFor\\\r
+ \r
+ \If{$hadPartialSendToServer$}\r
+ \r
+ \If{$\exists \tuple{seq_1, \tuple{seq_2,id,DE,hmac_p,hmac_c}} \in NewSlots_{decrypt}, id=LOCAL\_ID \land seq_2 = seq_a$}\r
+ \Return{$\tuple{true, NewSlots_{decrypted}}$}\r
+ \EndIf\\\r
+ \r
+ \If{$\exists \tuple{seq_1, \tuple{seq_2,id,DE,hmac_p,hmac_c}} \in NewSlots_{decrypt}, \exists \tuple{seq', id'} \in DE, \tuple{seq', id'}$ is a $ \land id'=LOCAL\_ID \land seq'=seq_a$}\r
+ \Return{$\tuple{true, NewSlots_{decrypted}}$}\r
+ \EndIf\r
+ \EndIf\\\r
+ \r
+ \State $RejectedSlotList \gets RejectedSlotList \cup \{seq_a\}$\r
+ \State \Return{$\tuple{false, NewSlots_{decrypted}}$}\r
+ \EndIf\\\r
+ \r
+\EndFunction\r
+\end{algorithmic}\r
+% \end{algorithm}\r
+% %\end{varwidth}% \r
+% }\r
+\r
+\r
+\r
+\r
+\r
+\r
+\r
+% Send to Server\r
+%% \noindent\fbox{%\r
+%% \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+% \begin{algorithm}\r
+\textbf{Send to Server:}\\\r
+Send local data to server if there is any local data that needs to be sent.\r
+\algblock[TryCatchFinally]{try}{endtry}\r
+\algcblock[TryCatchFinally]{TryCatchFinally}{finally}{endtry}\r
+\algcblockdefx[TryCatchFinally]{TryCatchFinally}{catch}{endtry}\r
+ [1]{\textbf{catch} #1}\r
+ {\textbf{end try}}\r
+\r
+\begin{algorithmic}[1]\r
+\Function{SendToServer}{$NewKey_a$}\r
+ \State $SlotDE \gets \emptyset$\r
+ \r
+ \try\r
+ \While{$|PendingTransactionQueue| > 0 \lor |SendArbQueue| > 0 \lor NewKey_a \neq NULL$}\r
+ \State $\tuple{slot, SlotDE, newsize} \gets $ \Call{FillSlot}{$NewKey_a$}\r
+ \State $\tuple{inserted, NewSlots} \gets $ \Call{SendToServer}{$slot, newsize$} \r
+ \If{$inserted$} \r
+ \State $NewKey_a \gets NULL$\r
+ \r
+ \r
+ \ForAll{$\tuple{commit, AbortSet, SentSet} \in ArbitrationRound$}\r
+ \State $ArbitrationRound \gets ArbitrationRound \setminus \tuple{commit, AbortSet, SentSet}$\r
+ \State $SentSet \gets SentSet \cup \{e| e\in(\{commit\} \cup AbortSet) \land e \in SlotDE\}$\r
+ \r
+ \LeftComment{Add Back to the set if not done sending}\r
+ \If{$(commit=NULL \land |AbortSet| \neq |SentSet|) \land (commit \neq NULL \land (|AbortSet|+1) \neq |SentSet|)$}\r
+ \State $ArbitrationRound \gets ArbitrationRound \cup \tuple{commit, AbortSet, SentSet}$\r
+ \EndIf\r
+ \EndFor\r
+\r
+ \r
+ \ForAll{$\tuple{\tuple{P, KV, G,seq_l, seq_s,id, arb},SentSet,hadTimeout} \in PendingTransactionQueue$ where $\exists p \in P, p \in SlotDE$}\r
+ \State $pos \gets PendingTransactionQueue.remove(\setminus \{\tuple{\tuple{P, KV, G,seq_l, seq_s,id, arb},SentSet,hadTimeout})$\r
+ \State $SentSet \gets SentSet \cup \{p|p \in P \land p \in SlotDE\}$\\\r
+ \r
+ \If{$|SentSet| > 0 \land id = LOCAL\_ID$}\r
+ \State $TransStatus \gets $ \Call{GetTransStatus}{$id,seq_l$}\r
+ \State \Call{ChangeTransStatus}{$TransStatus,sentfully$}\r
+ \EndIf\\\r
+ \r
+ \If{$|P| \neq |SentSet|$}\r
+ \State $PendingTransactionQueue.insert(pos, \{\tuple{\tuple{P, KV, G,seq_l, -1,id, arb},SentSet,false})$\r
+ \ElsIf{$id = LOCAL\_ID$}\r
+ \State $TransStatus \gets $ \Call{GetTransStatus}{$id,seq_l$}\r
+ \State \Call{ChangeTransStatus}{$TransStatus,sentfully$}\r
+ \State \Call{DeleteTransStatus}{$id,seq_l$}\r
+ \EndIf \r
+ \EndFor \r
+ \Else\r
+ \ForAll{$\tuple{\tuple{P, KV, G,seq_l, seq_s,id, arb},SentSet,hadTimeout} \in PendingTransactionQueue$ where $\exists p \in P, p \in SlotDE$}\r
+ \If{$|Sent| = 0$}\r
+ \State $PendingTransactionQueue.replace(\{\tuple{\tuple{P, KV, G,seq_l, seq_s,id, arb},SentSet,hadTimeout},\tuple{\tuple{P, KV, G,seq_l, -1,id, arb},SentSet,hadTimeout})\}$\r
+ \EndIf\r
+ \EndFor\r
+ \EndIf\r
+ \r
+ \r
+ \State \Call{ValidateAndUpdate}{$NewSlots$} \r
+ \EndWhile\r
+ \catch{$Server\_Connection\_Timeout$} \r
+ \ForAll{$\tuple{\tuple{P, KV, G,seq_l, seq_s,id, arb},SentSet,hadTimeout} \in PendingTransactionQueue$ where $\exists p \in P, p \in SlotDE$}\r
+ \If{$|Sent| = 0$}\r
+ \State $PendingTransactionQueue.replace(\{\tuple{\tuple{P, KV, G,seq_l, seq_s,id, arb},SentSet,hadTimeout}, \tuple{\tuple{P, KV, G,seq_l, -1,id, arb},SentSet,hadTimeout})$\r
+ \EndIf\r
+ \EndFor\r
+ \r
+ \State \textbf{rethrowException}\\\r
+ \r
+ \catch{$Server\_Response\_Timeout$}\r
+ \State $hadPartialSendToServer \gets True$\r
+ \ForAll{$\tuple{\tuple{P, KV, G,seq_l, seq_s,id, arb},SentSet,hadTimeout} \in PendingTransactionQueue$ where $\exists p \in P, p \in SlotDE$}\r
+ \State $PendingTransactionQueue.replace(\{\tuple{\tuple{P, KV, G,seq_l, seq_s,id, arb},SentSet,hadTimeout}, \tuple{\tuple{P, KV, G,seq_l, -1,id, arb},SentSet,True})$\r
+ \EndFor\r
+ \State \textbf{rethrowException}\r
+ \endtry\r
+ \r
+ \State \Return{$NewKey_a = NULL$}\r
+\EndFunction\r
+\end{algorithmic}\r
+% \end{algorithm}\r
+\r
+% %\end{varwidth}% \r
+% }\r
+\r
+\r
+\r
+\r
+% Check Slot Hmacs\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Check Slot HMACs:}\\\r
+Check that each slot has not been tampered with by checking that the stored HMAC matches the calculated HMAC. Also check thatthe slot number reported by the server matches the slot number of the actual slot.\r
+\begin{algorithmic}[1]\r
+\Function{CheckSlotsHmacAndSeq}{$Slots_a$}\r
+ \ForAll{$slot_a \in Slots_a$}\r
+ \State $\tuple{seq_{a_1}, \tuple{seq_{a_2},id_a,DE_a,hmac_{a_p},hmac_{a_c}}} \gets slot_a$\r
+ \State $calchmac \gets $ \Call{GenerateHmac}{$seq_{a_2}, id_a, DE_a, hmac_{a_p}$}\r
+ \r
+ \If{$seq_{a_1} \neq seq_{a_2}$}\r
+ \State \Call{Error}{"Slot sequence number mismatch"}\r
+ \ElsIf{$calchmac \neq hmac_{a_c}$}\r
+ \State \Call{Error}{"Slot HMAC mismatch"}\r
+ \EndIf\r
+ \EndFor\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+% Check HMAC Chain\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Check HMAC Chain:}\\\r
+Check that the HMAC chain has not been violated.\r
+\begin{algorithmic}[1]\r
+\Function{CheckHmacChain}{$Slots_a$}\r
+ \State $SlotsList \gets Slots_a$ sorted by sequence number\\ \r
+ \r
+ \LeftComment{Check all new slots}\r
+ \ForAll{$index \in [2: |SlotsList|]$}\r
+ \State $\tuple{seq_{a_1}, \tuple{seq_{a_2},id_a,DE_a,hmac_{a_p},hmac_{a_c}}} \gets SlotList[i-1]$\r
+ \State $\tuple{seq_{b_1}, \tuple{seq_{b_2},id_b,DE_b,hmac_{b_p},hmac_{b_c}}} \gets SlotList[i]$\r
+ \r
+ \If{$hmac_{b_p} \neq hmac_{b_c}$}\r
+ \State \Call{Error}{"Invalid previous HMAC."}\r
+ \EndIf \r
+ \EndFor\\\r
+ \r
+ \LeftComment{Check against slots that we already have in the block chain}\r
+ \If{$|LocalSlots| \neq 0$}\r
+ \State $\tuple{seq, SDE} \gets $\Call{MaxSlot}{$LocalSlots$}\r
+ \State $\tuple{seq{last_2},id_{last},DE_{last},hmac_{last_p},hmac_{last_c}} \gets SDE$\r
+ \State $\tuple{seq_{a_1}, \tuple{seq_{a_2},id_a,DE_a,hmac_{a_p},hmac_{a_c}}} \gets SlotList[1]$\\\r
+\r
+ \If{$(seq_{last_2} + 1) = seq_{a_1} \land hmac_{a_p} \neq hmac_{last_c}$} \r
+ \State \Call{Error}{"Invalid previous HMAC."}\r
+ \EndIf\r
+ \EndIf\r
+ \r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+% Check For Old Slots\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Check For Old Slots:}\\\r
+Check if the slots are not new. Checks if the "new" slots are actually new or if they are older than the most recent slot that we have.\r
+\begin{algorithmic}[1]\r
+\Function{CheckOldSlots}{$Slots_a$}\r
+ \State $\tuple{seq_{new}, Dat_{new}} \gets$ \Call{MinSlot }{$Slots_a$} \Comment{Get the oldest new slot}\r
+ \State $\tuple{seq_{local}, Dat_{local}} \gets$ \Call{MaxSlot }{$LocalSlots$} \Comment{Get the newest slot seen}\\\r
+ \r
+ \If{$seq_{new} \leq seq_{local}$} \Comment{The slots were not newer than what was already seen}\r
+ \State \Call{Error}{"Server sent old slots."}\r
+ \EndIf\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+% Check Size With Gap\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Check Size With Gap:}\\\r
+Checks that the block chain size is correct when there is a gap in the block chain. This check makes sure that the server is not hiding any information from the client. If there is a gap and there is only 1 queue state in the new slot entries then there must have at least that many slots since the old slot entry must have been purged. If there is more than 1 queue state then the block chain is still growing check the smallest max size and there should be at least that many slots. \r
+\begin{algorithmic}[1]\r
+\Function{CheckSizeWithGap}{$Slots_a$} \r
+ %\State $QSSet \gets $ \Call{GetQStateWithSeq}{$Slots_a$}\r
+ %\State $\tuple{seq_{max}, size_{max}} \gets \tuple{seq, size}$ such that $\tuple{seq, size} \in QSSet \land \forall \tuple{seq', size'} \in QSSet, size \geq size'$ \Comment{Get largest size}\r
+ %\State $\tuple{seq_{min}, size_{min}} \gets \tuple{seq, size}$ such that $\tuple{seq, size} \in QSSet \land \forall \tuple{seq', size'} \in QSSet , size \leq size'$ \Comment{Get smallest size}\r
+ \r
+ \State $QSet \gets $ \Call{GetQState}{$Slots_a$}\r
+ \State $size_{max} \gets size$ such that $size \in QSet \land \forall size' \in QSet, size \geq size'$ \r
+ \State $size_{min} \gets size$ such that $size \in QSet \land \forall size' \in QSet, size \leq size'$ \r
+ \State $Slots_{oldmax} \gets \emptyset$\\\r
+\r
+ \r
+ \LeftComment{If only 1 max size then we must have all the slots for that size}\r
+ \If{$(|QSSet| = 1) \land (|Slots_a| \neq size_{max})$}\r
+ \State \Call{Error}{"Missing Slots"}\r
+ \EndIf\\\r
+ \r
+ \LeftComment{We definitely have all the slots}\r
+ \If$|Slots_a| = size_{max}$\r
+ \State \Return{} \Comment{We have all the slots}\r
+ \EndIf\\\r
+ \r
+ \LeftComment{We must have at least this many slots}\r
+ \If$|Slots_a| < size_{min}$\r
+ \State \Call{Error}{"Missing Slots"}\r
+ \EndIf\\\r
+\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+% Check Size\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Check Size:}\\\r
+\begin{algorithmic}[1]\r
+\Function{CheckSize}{$Slots_a$} \r
+ \State $\tuple{seq_{old_{max}}, Dat_{old_{max}}} \gets $ \Call{MaxSlot}{$LocalSlots$}\r
+ \State $\tuple{seq_{new_{max}}, Dat_{new_{max}}} \gets $ \Call{MinSlot}{$Slots_a$}\\\r
+ \r
+ \If{$(seq_{old_{max}} + 1) = seq_{new_{max}}$}\r
+ \LeftComment{No Gap so cannot say anything about the size}\r
+ \State \Return{} \r
+ \Else \r
+ \LeftComment{Has a gap so we need to do checks}\r
+ \State \Call{CheckSizeWithGap}{$Slots_a$}\r
+ \EndIf\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+% Process New Key Data Entry\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Process New Key Entry:}\\\r
+Process a queue state entry. Adds a key to the key arbitrator set.\r
+\begin{algorithmic}[1]\r
+\Function{ProcessNewkey}{$newkey_a$}\r
+ \State $Arbitrator \gets Arbitrator \cup \{newkey_a\}$\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+% Process Collision Resolution Entry\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Process Queue State Entry:}\\\r
+Process a collision resolution entry.\r
+\begin{algorithmic}[1]\r
+\Function{ProcessColres}{$colres_a, NewSlots_a$}\r
+ \State $\tuple{id_a, seq_{a_{old}}, seq_{a_{new}}, isequal_a}$\r
+ \State $AllSlots \gets LocalSlots \cup NewSlots_a$\r
+ \State $index \gets seq_{a_{old}}$\\\r
+ \r
+ \While{$index <= seq_{a_{new}}$}\r
+ \State $slt \gets \tuple{seq' Dat'}$ such that $\tuple{seq' Dat'} \in AllSlots \land seq'=index$\r
+ \r
+ \If{$\exists \tuple{seq' Dat'} \in AllSlots, seq' = index$}\r
+ \State $\tuple{seq, Dat} \gets \tuple{seq' Dat'}$ such that $\tuple{seq' Dat'} \in AllSlots \land seq'=index$\r
+ \State $\tuple{seq,id,DE,hmac_p,hmac_c} \gets Dat$\r
+ \If{$isequal_a \neq (id=id_a)$}\r
+ \State \Call{Error}{"Trying to insert rejected messages for slot"}\r
+ \EndIf\r
+ \EndIf\\\r
+ \State $index \gets index + 1$\r
+ \EndWhile\r
+ \r
+ \r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+% Process Queue State Data Entry\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Process Queue State Entry:}\\\r
+Process a queue state entry. Updates the max size of the block chain.\r
+\begin{algorithmic}[1]\r
+\Function{ProcessQState}{$qstate_a$}\r
+ \State $\tuple{size_a} \gets qstate_a$\r
+ \State $max\_size \gets size_a$ \Comment{Update the max size we can have}\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+% Process Transaction Part Entry\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Process Transaction Part Entry:}\\\r
+Process a new Transaction Part Entry.\r
+\begin{algorithmic}[1]\r
+\Function{ProcessTransPart}{$TransactionPart_a$}\r
+ \State $\tuple{Dat,arb,seq_{clientLocal}, seq_{server}, id, partnum, isLast} \gets TransactionPart_a$\r
+ \State $Transaction \gets NULL$\\\r
+ \r
+ \If{$\exists \tuple{id',seq'} \in LastTransactionArbitrated \land id'=arb land seq' \geq seq_{server}$}\r
+ \State \Return{}\r
+ \EndIf\\\r
+ \r
+ \If{$\exists \tuple{Parts', KV', G',seq_{clientlocal}', seq_{server}',id', arb'} \in LiveTransactions, seq_{server}' = seq_{server}$}\r
+ \State $Transaction \gets \tuple{Parts', KV', G',seq_{clientlocal}', seq_{server}',id', arb'} \in LiveTransactions$such that$ seq_{server}' = seq_{server}$\r
+ \State $LiveTransactions \gets LiveTransactions \setminus \{Transaction\}$\r
+ \Else\r
+ \State $Transaction \gets \tuple{\emptyset, \emptyset, \emptyset, seq_{clientlocal}, seq_{server},id, arb}$\r
+ \EndIf\\\r
+ \r
+ \State $\tuple{Parts, KV, G,seq_{local}, seq_{server},id, arb} \gets Transaction$\r
+ \State $Parts \gets Parts \cup TransactionPart_a$\\\r
+ \r
+ \If{$\exists \tuple{Dat,arb,seq_{clientLocal}, seq_{server}, id, partnum, isLast} \in Parts \land isLast \land |Parts| = partnum$}\r
+ \State $\tuple{KV, G} \gets $\Call{DecodeParts}{$Parts$}\r
+ \EndIf\r
+ \r
+ \State $Transactin \gets \tuple{Parts, KV, G,seq_{local}, seq_{server},id,arb}$.\r
+ \State $LiveTransactions \gets LiveTransactions \cup \{Transaction\}$\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+% Process Abort Entry\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Process Abort Entry:}\\\r
+Process a new Abort Entry.\r
+\begin{algorithmic}[1]\r
+\Function{ProcessAbort}{$abort_a$}\r
+ \State $\tuple{seq_{cl}, seq_{s}, id, arb, seq_{arb}} \gets abort_a$\r
+ \r
+ \If{$\lnot(\exists \tuple{id',seq'} \in LastArbLocalArbitrated, id'=id \land seq' > seq_{arb})$}\r
+ \State $LastArbLocalArbitrated\gets \tuple{\tuple{id',seq'}|\tuple{id',seq'} \in LastArbLocalArbitrated, id' \neq id} \cup \{\tuple{id, }\}$\r
+ \EndIf\r
+ \r
+ \If{$\lnot(\exists \tuple{id',seq'} \in LastTransactionArbitrated, id'=id \land seq' > seq_{s})$}\r
+ \State $LastTransactionArbitrated \gets \tuple{\tuple{id',seq'}|\tuple{id',seq'} \in LastTransactionArbitrated, id' \neq id} \cup \{\tuple{id, seq_{s}}\}$\r
+ \EndIf \r
+ \r
+ \If{$id = LOCAL\_ID$}\r
+ \State $TransStatus \gets $ \Call{GetTransStatus}{$id, seq_{cl}$}\r
+ \State \Call{ChangeTransStatus}{$TransStatus,abort$}\r
+ \State \Call{DeleteTransStatus}{$id, seq_{cl}$}\r
+ \EndIf\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+% Process Commit Part Entry\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Process Commit Part Entry:}\\\r
+Process a new Commit Part Entry.\r
+\begin{algorithmic}[1]\r
+\Function{ProcessCommitPart}{$CommitPart_a$}\r
+ \State $\tuple{Dat,seq_t, seq_s, id, partnum, isLast} \gets CommitPart_a$\r
+ \State $Commit \gets NULL$\\\r
+ \r
+ \If{$\exists \tuple{P', KV', seq_t', seq_s',id'} \in LiveCommits, seq_s' = seq_s$}\r
+ \State $Commit \gets \tuple{P', KV', seq_t', seq_s',id} \in LiveCommits$ such that$ seq_{s}' = seq_{s}$\r
+ \State $LiveCommits \gets LiveCommits \setminus \{Commit\}$\r
+ \Else\r
+ \State $Commit \gets \tuple{\emptyset, \emptyset, seq_t, seq_s,id}$\r
+ \EndIf\\\r
+ \r
+ \State $\tuple{P, KV, seq_t, seq_s,id} \gets Commit$\r
+ \State $P \gets P \cup CommitPart_a$\\\r
+ \r
+ \If{$\exists \tuple{Dat',seq_t', seq_s', id', partnum', isLast'} \in P \land isLast' \land |P| = partnum$}\r
+ \State $KV \gets $\Call{DecodeParts}{$P$}\r
+ \EndIf\\\r
+ \r
+ \State $Commit \gets \tuple{P, KV, seq_t, seq_s,id}$\r
+ \State $LiveCommits \gets LiveCommits \cup \{Commit\}$\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+% Update Last Message\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Process Commit Data Entry:}\\\r
+Process a commit entry. Updates the local copy of commits.\r
+\begin{algorithmic}[1]\r
+\Function{UpdateLastMessage}{$seq_a, id_a, updateinglocal_a, MachinesSeen$}\r
+ \State $\tuple{id_{old}, seq_{old}} \gets \tuple{id', seq'}$ such that $\tuple{id', seq'} \in LastSlot \land id'=id$\\\r
+ \r
+ \If{$id_a = LOCAL\_ID$}\r
+ \If{$hadPartialSendToServer$}\r
+ \If{$\lnot updateinglocal_a \land (seq_a < seq_{old})$}\r
+ \LeftComment{This client did not make any updates so its latest sequence number should not change}\r
+ \State \Call{Error}{"Mismatch on local machine sequence number"}\r
+ \EndIf\r
+ \Else\r
+ \If{$\lnot updateinglocal_a \land (seq_a \neq seq_{old})$}\r
+ \LeftComment{This client did not make any updates so its latest sequence number should not change}\r
+ \State \Call{Error}{"Mismatch on local machine sequence number"}\r
+ \EndIf\r
+ \EndIf\r
+ \Else\r
+ \If{$seq_{old} > seq_a$}\r
+ \State \Call{Error}{"Rollback on remote machine sequence number"}\r
+ \EndIf\r
+ \EndIf\\\r
+ \r
+ \State $LastSlot \gets LastSlot \setminus \{\tuple{id, seq} | \tuple{id, seq} \in LastSlot, id=id_a\}$\r
+ \State $LastSlot \gets LastSlot \cup \{\tuple{id_a, seq_a}\}$\r
+ \State $MachinesSeen \gets MachinesSeen \setminus \{id_a\}$\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+% Process Process Data Entry\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Process Data Entry:}\\\r
+Process the data entry based on what kind of entry it is.\r
+\begin{algorithmic}[1]\r
+\Function{ProcessDatEntry}{$slot_a, NewSlots_a,MachinesSeen$}\r
+ \If{$datentry_a$ is a $compart$}\r
+ \State \Call{ProcessCommitPart}{$dataentry_a$}\r
+ \r
+ \ElsIf{$datentry_a$ is a $abort$}\r
+ \LeftComment{Do Nothing in this case}\r
+ \r
+ \ElsIf{$datentry_a$ is a $transpart$}\r
+ \State \Call{ProcessTransPart}{$dataentry_a$}\r
+ \r
+ \ElsIf{$datentry_a$ is a $lastmsg$}\r
+ \State $\tuple{seq_a, id_a} \gets dataentry_a$\r
+ \State \Call{UpdateLastMessage}{$seq_a, id_a, false, MachinesSeen$}\r
+ \r
+ \ElsIf{$datentry_a$ is a $colres$}\r
+ \State \Call{ProcessColres}{$dataentry_a, NewSlots_a$}\r
+ \r
+ \ElsIf{$datentry_a$ is a $qstate$}\r
+ \State \Call{ProcessQState}{$dataentry_a$}\r
+ \r
+ \ElsIf{$datentry_a$ is a $newkey$}\r
+ \State \Call{ProcessNewkey}{$dataentry_a$}\r
+ \Else\r
+ \State \Call{Error}{"Unknown data entry type."}\r
+ \EndIf\r
+ \r
+ \State \Return{$LstSlt_a$} \r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+% Update Committed Table\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Update Committed Key value Table:}\\\r
+Update the table of committed Key Value Pairs based on commits that we received.\r
+\begin{algorithmic}[1]\r
+\Function{UpdateCommitTable}{$ $} \r
+ \r
+ \State $ArbSet \gets \{id'| \tuple{P, KV, seq_t, seq_s,id'} \in LiveCommits\}$\r
+ \r
+ \ForAll{$id \in ArbSet$}\r
+ \State $Commits \gets \{\tuple{P, KV, seq_t, seq_s,id'}| \tuple{P, KV, seq_t, seq_s,id'} \in LiveCommits \land id' = id\}$\r
+ \r
+ \State $lastComSeenSeq \gets -1$\r
+ \If{$\exists \tuple{id',seq'} \in LastCommitSeenFromArbitrator, id'=id$}\r
+ \State $lastComSeenSeq \gets seq$ such that $\tuple{id',seq'} \in LastCommitSeenFromArbitrator, id'=id$\r
+ \EndIf\\\r
+ \r
+ \ForAll{$\tuple{P, KV, seq_t, seq_s,id} \in Commits$ sorted by $seq_s$ where $seq_s > lastComSeenSeq$}\r
+\r
+ \If{$(\forall \tuple{D',seq_t', seq_s', id', pn', isLast'} \in P, \lnot isLast')\lor(\exists \tuple{D',seq_t', seq_s', id', pn', isLast'} \in P,isLast') \land |P| \neq pn)$}\r
+ \If{$\forall \tuple{P', KV', seq_t', seq_s',id'} \in Commits, seq_s' < seq_s$}\r
+ \State Break \Comment{This is the last slot so ignore it}\r
+ \Else\r
+ \State Continue\r
+ \EndIf\r
+ \EndIf\\\r
+ \r
+ \If{$\lnot(\exists \tuple{id',seq'} \in LastArbLocalArbitrated, id'=id \land seq' > seq_s)$}\r
+ \State $LastArbLocalArbitrated\gets \tuple{\tuple{id',seq'}|\tuple{id',seq'} \in LastArbLocalArbitrated, id' \neq id} \cup \{\tuple{id, seq_s}\}$\r
+ \EndIf\r
+ \r
+ \State $LastCommitSeenFromArbitrator \gets \{ \tuple{id',seq'}| \tuple{id',seq'} \in LastCommitSeenFromArbitrator,id' \neq id\} \cup \{\tuple{id, seq_s}\}$\r
+\r
+ \If{$\lnot(\exists \tuple{id',seq'} \in LastTransactionArbitrated, id'=id \land seq' > seq_{t})$}\r
+ \State $LastTransactionArbitrated \gets \tuple{\tuple{id',seq'}|\tuple{id',seq'} \in LastTransactionArbitrated, id' \neq id} \cup \{\tuple{id, seq_{t}}\}$\r
+ \EndIf \r
+ \r
+ \LeftComment{Update Committed Table}\r
+ \State $CommittedKV \gets \{\tuple{k,v}| \tuple{k,v} \in CommittedKV \land \forall \tuple{k',v'} \in KV, k\neq k' \} \cup KV$ \r
+ \State $LiveCommits \gets LiveCommits \cup \tuple{P, KV, seq_t, seq_s,id}$\\\r
+ \r
+ \ForAll{$\tuple{P, KV, seq_t, seq_s,id} \in LiveCommits$}\r
+ \LeftComment{All Key Values in this commit have been overridden by a newer commit} \r
+ \If{$\forall \tuple{k,v} \in KV, \exists \tuple{P', KV', seq_t', seq_s',id'} \in LiveCommits, \exists \tuple{k',v'} \in KV', k'=k \land seq_s' > seq_s$}\r
+ \State $LiveCommits \gets LiveCommits \setminus \{\tuple{P, KV, seq_t, seq_s,id}\}$\r
+ \EndIf\r
+ \EndFor \r
+ \EndFor\r
+ \EndFor\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+% Update Speculative Table\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Update Speculated Key value Table:}\\\r
+Update the table of speculative Key Value Pairs based on commits that we received.\r
+\begin{algorithmic}[1]\r
+\Function{UpdateSpeculativeKV}{$ $}\r
+ \State $SpecKV \gets CommittedKV$\\\r
+ \r
+ \ForAll{$\tuple{P, KV, G,seq_{cl}, seq_s,id, arb} \in LiveTransactions$ sorted by $seq_s$}\r
+ \If{$\forall \tuple{D',arb',seq_{l}', seq_{s}', id', pn', isLast'} \in P, \lnot isLast'$}\r
+ \State Continue\r
+ \ElsIf{$(\exists \tuple{D',arb',seq_{l}', seq_{s}', id', pn', isLast'} \in P,isLast') \land |P| \neq pn$}\r
+ \State Continue\r
+ \EndIf\\\r
+ \r
+ \If{\Call{EvaluateGuard}{$G, SpecKV$}}\r
+ \State $SpecKV\gets \{\tuple{k',v'}| \tuple{k',v'} \in SpecKV \land \forall \tuple{k,v} \in KV, k' \neq k\}\cup KV$\r
+ \EndIf\r
+ \EndFor\\\r
+ \r
+ \ForAll{$\tuple{KV, G, id, seq} \in PendingTransactionQueue$ sorted by $seq$}\r
+ \If{\Call{EvaluateGuard}{$G, SpecKV$}}\r
+ \State $SpecKV\gets \{\tuple{k',v'}| \tuple{k',v'} \in SpecKV \land \forall \tuple{k,v} \in KV, k' \neq k\}\cup KV$\r
+ \EndIf\r
+ \EndFor\\\r
+ \r
+ \State $SpeculatedKV \gets SpecKV$\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+% Compact Arbitration Rounds\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Compact Arbitration Rounds:}\\\r
+Compact Arbitration Rounds to reduce the amount of data needed to be sent to the server.\r
+\begin{algorithmic}[1]\r
+\Function{CompactArbitrationRounds}{$ $}\r
+ \If{$|SendArbQueue| < 2$}\r
+ \State \Return{False}\r
+ \EndIf\\\r
+ \r
+ \State $didMergeWithCommit \gets False$\r
+ \r
+ \While{$|SendArbQueue| > 1$}\r
+ \State $\tuple{c_1, A_1, S_1} \gets SendArbQueue.peak(|SendArbQueue|)$\r
+ \State $\tuple{c_2, A_2, S_2} \gets SendArbQueue.peakEnd(|SendArbQueue| - 1)$\\\r
+ \r
+ \If{$|S_1| \neq 0 \lor |S_2| \neq 0$}\r
+ \State \Return{$didMergeWithCommit$}\r
+ \EndIf\\\r
+ \r
+ \If{$c_2 = NULL$}\r
+ \If{$|A_1| + |A_2| > MAX\_ROUND\_SIZE$}\r
+ \State \Return{$didMergeWithCommit$}\r
+ \EndIf \r
+ \State $SendArbQueue.remove(|SendArbQueue|)$\r
+ \State $SendArbQueue.remove(|SendArbQueue|)$\r
+ \State $SendArbQueue \gets SendArbQueue \cup \tuple{c_1, A_1 \cup A_2, \emptyset}$\r
+ \Else\r
+ \State $\tuple{P_1, KV_1, seq_{1_t}, seq_{1_s},id_1} \gets c_1$\r
+ \State $\tuple{P_2, KV_2, seq_{2_t}, seq_{2_s},id_2} \gets c_2$\r
+ \State $newKV \gets \{\tuple{k_2,v_2}| \tuple{k_2,v_2} \in KV_2 \land \forall \tuple{k_1,v_1} \in KV_1 \land k_1 \neq k_2\} \cup KV_1$\r
+ \State $NewCom \gets \tuple{P_1, newKV, seq_{1_t}, seq_{1_s},id_1}$\r
+ \State \Call{GenerateParts}{$NewCom$}\r
+ \State $\tuple{P_1, newKV, seq_{1_t}, seq_{1_s},id_1} \gets NewCom$\\\r
+ \r
+ \If{$|P_1| > MAX\_ROUND\_SIZE$}\r
+ \State \Return{$didMergeWithCommit$}\r
+ \EndIf\\\r
+ \r
+ \State $SendArbQueue.remove(|SendArbQueue|)$\r
+ \State $SendArbQueue.remove(|SendArbQueue|)$\r
+ \State $SendArbQueue \gets SendArbQueue \cup \tuple{newCom, A_1 \cup A_2, \emptyset}$\r
+ \State $didMergeWithCommit \gets True$\r
+ \EndIf\r
+ \EndWhile \r
+ \r
+ \State \Return{$didMergeWithCommit$}\r
+ \r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+% Arbitrate From Server\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Arbitrate Form Server:}\\\r
+Arbitrate on the transactions that were received from the server\r
+\begin{algorithmic}[1]\r
+\Function{ArbitrateFromServer}{$ $}\r
+ \r
+ \State $KVCom \gets \emptyset$\r
+ \State $KVTmp \gets CommittedKV$\r
+ \State $lastTransCommitted = 0$\r
+ \State $AbortSet \gets \emptyset$\r
+ \State $NewCom \gets NULL$\r
+ \r
+ \State $TransArb \gets \{\tuple{P, KV, G,seq_{l}, seq_{s},id,arb}|\tuple{p, KV, G,seq_{l}, seq_{s},id,arb} \in LiveTransactions \land arb = LOCAL\_ID\}$\\\r
+ \r
+ \ForAll{$\tuple{P, KV, G,seq_{cl}, seq_{s},id,arb} \in Transarb$ sorted by $seq_{s}$}\r
+ \r
+ \If{$\forall \tuple{D',arb',seq_{l}', seq_{s}', id', pn', isLast'} \in P, \lnot isLast'$}\r
+ \State Break\r
+ \ElsIf{$(\exists \tuple{D',arb',seq_{l}', seq_{s}', id', pn', isLast'} \in P,isLast') \land |P| \neq pn$}\r
+ \State Break\r
+ \ElsIf{$\exists \tuple{id', seq_{l}'} \in OfflineTransAtServer, id' = id\land seq_{cl}' = seq_{cl} $}\r
+ \State Break\r
+ \EndIf\\\r
+ \r
+ \State $LastTransSeenMid \gets \{\tuple{id',seq'}|\tuple{id',seq'} \in LastTransSeenMid \land id'\neq id\} \cup \{\tuple{id, seq_s}\}$\\\r
+ \r
+ \r
+ \If{\Call{EvaluateGuard}{$G, KVTmp$}}\r
+ \State $KVTmp \gets \{\tuple{k',v'} |\tuple{k',v'} \in KVTmp \land \forall \tuple{k,v} \in KV, k' \neq k\}\cup KV$\r
+ \State $KVCom \gets \{\tuple{k',v'} |\tuple{k',v'} \in KVCom \land \forall \tuple{k,v} \in KV, k' \neq k\}\cup KV$\r
+ \State $lastTransCommitted \gets seq_{s}$ \r
+ \Else\r
+ \State $newAbort \gets \tuple{seq_{cl}, seq_{s}, id, arb, arbitrationSeqNum}$\r
+ \State $AbortSet \gets AbortSet \cup newAbort$\r
+ \State $arbitrationSeqNum \gets arbitrationSeqNum + 1$\r
+ \State \Call{ProcessAbort}{$newAbort$}\r
+ \EndIf\r
+ \EndFor\r
+ \r
+ \If{$|KVCom| \neq 0$}\r
+ \State $NewCom \gets \tuple{\emptyset, KVCom, lastTransCommitted, arbitrationSeqNum,id}$\r
+ \State \Call{GenerateParts}{$NewCom$}\r
+ \State $arbitrationSeqNum \gets arbitrationSeqNum + 1$\r
+ \ForAll{$compart \in NewCom$}\r
+ \State \Call{ProcessCommitPart}{compart}\r
+ \EndFor\r
+ \EndIf\r
+ \r
+ \If{$|KVCom| \neq 0 \lor |AbortSet| \neq 0$}\r
+ \State $ArbitrationQueue \gets ArbitrationQueue \cup \tuple{NewCom, AbortSet, \emptyset}$\r
+ \r
+ \If{\Call{CompactArbitrationRounds}{$ $}}\r
+ \State $\tuple{NewCom, AbortSet, \emptyset} \gets ArbitrationQueue.peakEnd()$\r
+ \ForAll{$compart \in NewCom$}\r
+ \State \Call{ProcessCommitPart}{compart}\r
+ \EndFor\r
+ \EndIf\r
+ \EndIf \r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+\r
+\r
+% Arbitrate From Local\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Arbitrate from local:}\\\r
+Arbitrate on the transactions that were received from the local.\r
+\begin{algorithmic}[1]\r
+\Function{ArbitrateFromLocal}{$Transaction_a$}\r
+ \State $\tuple{Parts, KV, G,seq_l, seq_s,id, arb} \gets Transaction_a$\\\r
+ \r
+ \If{$id \neq LOCAL\_ID$} \Comment{If is arbitrator}\r
+ \State \Return{$\tuple{False, False}$}\r
+ \EndIf\\\r
+ \r
+ \LeftComment{transaction is complete}\r
+ \If{$\forall \tuple{D',arb',seq_{l}', seq_{s}', id', pn', isLast'} \in P, \lnot isLast'$}\r
+ \State \Return{$\tuple{False, False}$}\r
+ \ElsIf{$(\exists \tuple{D',arb',seq_{l}', seq_{s}', id', pn', isLast'} \in P,isLast') \land |P| \neq pn$}\r
+ \State \Return{$\tuple{False, False}$}\r
+ \EndIf\\\r
+ \r
+ \If{$id \neq LOCAL\_ID$}\r
+ \If{$\exists \tuple{id',seq'} \in LastTransSeenMid, id'=id \land seq' > seq_l$}\r
+ \State \Return{$\tuple{False, False}$} \Comment{Already seen this transaction}\r
+ \EndIf\r
+ \EndIf\\\r
+ \r
+ \If{\Call{EvaluateGuard}{$G, CommittedKV$}} \r
+ \State $NewCom \gets \tuple{\emptyset, KV, seq_s, arbitrationSeqNum,id}$\r
+ \State \Call{GenerateParts}{$NewCom$}\r
+ \State $arbitrationSeqNum \gets arbitrationSeqNum + 1$\r
+ \ForAll{$compart \in NewCom$}\r
+ \State \Call{ProcessCommitPart}{compart}\r
+ \EndFor\\\r
+ \r
+ \State $ArbitrationQueue \gets ArbitrationQueue \cup \tuple{NewCom, \emptyset, \emptyset}$\r
+ \If{\Call{CompactArbitrationRounds}{$ $}}\r
+ \State $\tuple{NewCom, AbortSet, \emptyset} \gets ArbitrationQueue.peakEnd()$\r
+ \ForAll{$compart \in NewCom$}\r
+ \State \Call{ProcessCommitPart}{compart}\r
+ \EndFor\r
+ \EndIf\r
+ \r
+ \r
+ \If{$id = LOCAL\_ID$}\r
+ \State $TransStatus \gets $ \Call{GetTransStatus}{$id,seq_l$}\r
+ \State \Call{ChangeTransStatus}{$TransStatus,committed$}\r
+ \State \Call{DeleteTransStatus}{$id,seq_l$}\r
+ \EndIf\r
+ \r
+ \State \Call{UpdateCommittedKV}{}\r
+ \State \Call{UpdateLiveTransactionsAndStatuses}{}\r
+ \State \Call{UpdateSpeculativeKV}{} \r
+ \State \Return{$\tuple{True, True}$} \r
+ \Else\r
+ \r
+ \If{$id = LOCAL\_ID$}\r
+ \State $TransStatus \gets $ \Call{GetTransStatus}{$id,seq_l$}\r
+ \State \Call{ChangeTransStatus}{$TransStatus,aborted$}\r
+ \State \Call{DeleteTransStatus}{$id,seq_l$}\r
+ \Else\r
+ \State $newAbort \gets \tuple{seq_{cl}, seq_{s}, id, arb, arbitrationSeqNum}$\r
+ \State $arbitrationSeqNum \gets arbitrationSeqNum + 1$\r
+ \State \Call{ProcessAbort}{$newAbort$} \r
+ \State $ArbitrationQueue \gets ArbitrationQueue \cup \tuple{NULL, \{newAbort\}, \emptyset}$\r
+ \r
+ \If{\Call{CompactArbitrationRounds}{$ $}}\r
+ \State $\tuple{NewCom, AbortSet, \emptyset} \gets ArbitrationQueue.peakEnd()$\r
+ \ForAll{$compart \in NewCom$}\r
+ \State \Call{ProcessCommitPart}{compart}\r
+ \EndFor\r
+ \EndIf\r
+ \EndIf \r
+ \EndIf\r
+ \r
+ \State \Call{UpdateCommittedKV}{}\r
+ \State \Call{UpdateLiveTransactionsAndStatuses}{}\r
+ \State \Call{UpdateSpeculativeKV}{} \r
+ \State \Return{$\tuple{True, False}$}\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+% Update Live Transaction and Statuses\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Update Live Transactions And Statuses:}\\\r
+Update the live transactions and the transaction statuses.\r
+\begin{algorithmic}[1]\r
+\Function{UpdateLiveTransactionsAndStatuses}{$ $}\r
+ \ForAll{$\tuple{P, KV, G,seq_l, seq_s,id, arb} \in LiveTransactions$}\r
+ \If{$\exists \tuple{id',seq'} \in LastTransactionArbitrated, id=id' \land seq' > seq_s$}\r
+ \If{$id = LOCAL\_ID$}\r
+ \State $TransStatus \gets $ \Call{GetTransStatus}{$id,seq_l$}\r
+ \State \Call{ChangeTransStatus}{$TransStatus,committed$}\r
+ \State \Call{DeleteTransStatus}{$id,seq_l$}\r
+ \EndIf\r
+ \EndIf\r
+ \EndFor\r
+ \State $LiveTransactions \gets \{\tuple{P, KV, G,seq_l, seq_s,id, arb}| \tuple{P, KV, G,seq_l, seq_s,id, arb} \in LiveTransactions \land \forall \tuple{id',seq'} \in LastTransactionArbitrated, id'\neq id \lor seq_s > seq'\}$\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+% Validate and Update \r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Validate Update:}\\\r
+Validate the block chain and insert into the local block chain.\r
+\begin{algorithmic}[1]\r
+\Function{ValidateUpdate}{$NewSlots_a, updatinglocal_a$}\r
+ \State $\tuple{seq_{oldest}, Dat_{oldest}} \gets$ \Call{MinSlot}{$NewSlots_a$}\r
+ \State $\tuple{seq_{newest}, Dat_{newest}} \gets$ \Call{MaxSlot}{$NewSlots_a$}\r
+ \State $\tuple{seq_{local}, Dat_{local}} \gets$ \Call{MaxSlot}{$LocalSlots$}\r
+ \State $MachinesSeen \gets \{id'|\tuple{id',seq'} \in LastSlot\}$\\\r
+ \r
+ \State \Call{CheckSlotsHmacAndSeq}{$NewSlots_a$}\r
+ \State \Call{CheckHmacChain}{$NewSlots_a$}\r
+ \State \Call{CheckOldSlots}{$NewSlots_a$}\r
+ \State \Call{CheckSize}{$NewSlots_a$}\\\r
+ \r
+ \ForAll{$slot_a \in NewSlots_a$ in order of sequence number} \r
+ \State $\tuple{seq_{a_1}, \tuple{seq_{a_2},id_a,DE_a,hmac_{a_p},hmac_{a_c}}} \gets slot_a$\r
+ \State \Call{UpdateLastMessage}{$seq_{a_1}, id_a, updatinglocal_a, MachinesSeen$}\\\r
+ \r
+ \ForAll{$de_a \in DE_a$}\r
+ \State \Call{ProccessDatEntry}{$de_a, NewSlots_a, MachinesSeen$}\r
+ \EndFor\\\r
+ \r
+ \State $LocalSlots \gets LocalSlots \cup \{slot_a\}$ \Comment{Add to local Chain}\r
+ \EndFor\\\r
+ \r
+ \If{$seq_{oldest} > (seq_{local} +1) \land MachinesSeen \neq \emptyset$}\r
+ \LeftComment{There was a gap so there should be a complete set of information on each previously seen client}\r
+ \State \Call{Error}{"Missing records for machines"}\r
+ \EndIf\\\r
+ \r
+ \State \Call{DeleteLocalSlots}{ } \Comment{Delete old slots from local}\r
+ \r
+ \State \Call{ArbitrateFromServer}{}\r
+ \State \Call{UpdateCommittedKV}{}\r
+ \State \Call{UpdateLiveTransactionsAndStatuses}{}\r
+ \State \Call{UpdateSpeculativeKV}{}\r
+ \r
+ \State $offlineTransactionAtServer \gets \emptyset$\r
+ \State $hadPartialSendToServer \gets false$\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+% Accept from local \r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Accept from Local:}\\\r
+The local transaction handling accept.\r
+\begin{algorithmic}[1]\r
+\Function{AcceptFromLocal}{$seq_a, transaction_a$}\r
+ \State $arbitrated \gets false$\r
+ \State $committed \gets false$\r
+ \State $ReturnSet \gets \emptyset$\\\r
+ \r
+ \If{$transaction_a \neq NULL$}\r
+ \State $\tuple{arbitrated, committed} \gets $ \Call{ArbitrateFromLocal}{$transaction_a$} \r
+ \State $\tuple{P, KV, G,seq_l, seq_s,id, arb} \gets transaction_a$\r
+ \If{$seq_s \neq -1$}\r
+ \State $OfflineTransAtServer \gets OfflineTransAtServer \cup \{\tuple{id, seq_l}\}$\r
+ \EndIf\r
+ \State \Call{UpdateCommittedKV}{}\r
+ \State \Call{UpdateLiveTransactionsAndStatuses}{}\r
+ \State \Call{UpdateSpeculativeKV}{}\r
+ \EndIf\\\r
+ \r
+ \State $AllAborts \gets$ \Call{GetAborts}{} \Comment{Get all the aborts} \\\r
+ \State $ReturnSet \gets ReturnSet \cup \{\tuple{seq_l', seq_s', id', arb', seq_{arb}'}|\tuple{seq_l', seq_s', id', arb', seq_{arb}', seq'} \in A \land id'=LOCAL\_ID \land seq_l' > seq_a\}$\r
+ \State $ReturnSet \gets ReturnSet \cup \{p'|p'\in P' \land \tuple{P', KV', seq_t', seq_s',id'} \in LiveCommits \land id'=LOCAL\_ID \land seq_s' > seq_a\}$\r
+ \State \Return{$\tuple{arbitrated, committed,ReturnSet}$} \r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+\r
+% Send to local \r
+%% \noindent\fbox{%\r
+%% \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Send To Local:}\\\r
+Send transaction to local to be arbitrated on or not.\r
+\begin{algorithmic}[1]\r
+\Function{SendToLocal}{$transaction_a$}\r
+ \State $\tuple{P, KV, G,seq_l, seq_s,id, arb} \gets transaction_a$\r
+ \If{Cannot communicate locally with client $id$}\r
+ \State \Return{$False$}\r
+ \EndIf\r
+\r
+\r
+ \State $seq_{lastseen} \gets seq'$ such that $\tuple{id',seq'} \in LastArbLocalArbitrated \land id'=id$\r
+ \State $\tuple{arbitrated, committed,ReturnSet} \gets $\Call{AcceptFromLocal}{$seq_{lastseen}, transaction_a$}\\\r
+\r
+ \ForAll{$e \in ReturnSet$}\r
+ \If{$e$ is an $abort$}\r
+ \State \Call{ProcessAbort}{$e$}\r
+ \Else\r
+ \State \Call{ProcessCommitPart}{$e$}\r
+ \EndIf\r
+ \EndFor\\\r
+ \r
+ \State \Call{UpdateCommittedKV}{}\r
+ \State \Call{UpdateLiveTransactionsAndStatuses}{}\r
+ \State \Call{UpdateSpeculativeKV}{}\\\r
+ \r
+ \State $TransStatus \gets $ \Call{GetTransStatus}{$id,seq_l$}\r
+ \If{$arbitrated$}\r
+ \If{$committed$}\r
+ \State \Call{ChangeTransStatus}{$TransStatus,committed$}\r
+ \Else\r
+ \State \Call{ChangeTransStatus}{$TransStatus,aborted$}\r
+ \EndIf\r
+ \ElsIf{$\exists \tuple{seq_l', seq_s', id', arb', seq_{arb}'} \in ReturnSet, \tuple{seq_l', seq_s', id', arb', seq_{arb}'}$ is an $abort \land id' = LOCAL\_ID \land seq_l' = seq_l$}\r
+ \State \Call{ChangeTransStatus}{$TransStatus,aborted$}\r
+ \Else\r
+ \State \Call{ChangeTransStatus}{$TransStatus,committed$} \r
+ \EndIf\r
+ \r
+ \State \Call{DeleteTransStatus}{$id,seq_l$}\r
+ \State \Return{$True$}\r
+\EndFunction\r
+\end{algorithmic}\r
+% %\end{varwidth}% \r
+% }\r
+\r
+\r
+\subsection{Client Interfaces}\r
+\r
+\r
+\r
+\r
+% Update\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Update}\\\r
+Sync with the server and get all the latest slots.\r
+\r
+\algblock[TryCatchFinally]{try}{endtry}\r
+\algcblock[TryCatchFinally]{TryCatchFinally}{finally}{endtry}\r
+\algcblockdefx[TryCatchFinally]{TryCatchFinally}{catch}{endtry}\r
+ [1]{\textbf{catch} #1}\r
+ {\textbf{end try}}\r
+\r
+\begin{algorithmic}[1]\r
+\Function{UpdateFromServer}{$ $}\r
+ \State $NewSlots_{decrypt} \gets \emptyset$\r
+ \State $\tuple{seq, Dat} \gets $ \Call{MaxSlot}{$LocalSlots$}\\\r
+ \r
+ \try\r
+ \State $NewSlots \gets$ \Call{GetSlots}{$seq$}\\\r
+ \r
+ \ForAll{$\tuple{seq', EDat'} \in NewSlots$}\r
+ \State $DDat \gets $ \Call{Decrypt}{$EDat'$}\r
+ \State $NewSlots_{decrypt} \gets NewSlots_{decrypted} \cup \tuple{seq',DDat}$\r
+ \EndFor\\\r
+ \r
+ \State \Call{ValidateAndUpdate}{$NewSlots_{decrypt}$} \r
+ \State \Call{SendToServer}{$Null$}\r
+ \State \Return{$True$} \r
+ \catch{$Exception$}\r
+ \LeftComment{Do nothing here}\r
+ \endtry\r
+ \r
+ \State \Return{$False$}\r
+ \r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+% Update from local\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Update from local}\\\r
+Get the latest from a client through local communication.\r
+\begin{algorithmic}[1]\r
+\Function{UpdateFromLocal}{$id_a$}\r
+ \If{Cannot communicate locally with client $id$}\r
+ \State \Return{}\r
+ \EndIf\r
+ \r
+ \State $seq_{lastseen} \gets seq'$ such that $\tuple{id',seq'} \in LastArbLocalArbitrated \land id'=id_a$\r
+ \State $\tuple{arbitrated, committed,ReturnSet} \gets $\Call{AcceptFromLocal}{$seq_{lastseen}, transaction_a$}\\\r
+\r
+ \ForAll{$e \in ReturnSet$}\r
+ \If{$e$ is an $abort$}\r
+ \State \Call{ProcessAbort}{$e$}\r
+ \Else\r
+ \State \Call{ProcessCommitPart}{$e$}\r
+ \EndIf\r
+ \EndFor\\\r
+ \r
+ \State \Call{UpdateCommittedKV}{}\r
+ \State \Call{UpdateLiveTransactionsAndStatuses}{}\r
+ \State \Call{UpdateSpeculativeKV}{}\\\r
+\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+\r
+%Create New Key \r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Create New Key:}\\\r
+Creates a new key and specifies which machine ID is the arbitrator. If there is already a new key entry in the block chain for this key name then do not insert into the chain, another client got there first.\r
+\begin{algorithmic}[1]\r
+\Function{Transaction Commit}{$k_a, id_a$}\r
+ \State $success \gets false$\\\r
+ \While{$\lnot success$}\r
+ \If{$\exists \tuple{k',id'} \in Arbitrator, k' = k_a$}\r
+ \State \Return{$false$} \Comment{Key already created}\r
+ \EndIf\\\r
+ \r
+ \State $success \gets$ \Call{SendToServer}{$\tuple{k_a, id_a}$}\r
+ \EndWhile\r
+ \r
+ \State \Return{$true$} \Comment{If got here then insertion was correct}\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \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.\r
+\begin{algorithmic}[1]\r
+\Function{TransactionStart}{$ $}\r
+ \State $newPendingTransaction \gets \tuple{\emptyset, \emptyset, LOCAL\_ID,clntTransactionNum}$\r
+ \State $clntTransactionNum \gets clntTransactionNum + 1$\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\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{PutKeyValue}{$k,v$}\r
+ \State $\tuple{KV, G,id, seq_{clientLocal}} \gets newPendingTransaction$\r
+ \State $KV \gets \{\tuple{k',v'}| \tuple{k,v} \in KV, k \neq k'\}\cup \{\tuple{k,v}\}$ \r
+ \State $ArbSet \gets \{arb| \exists \tuple{k',v'} \in (KV \cup G), arb=$\Call{GetArbitrator}{$k'$}$\}$\r
+ \If{$|ArbSet| > 1$}\r
+ \State \Call{Error}{"Multiple arbitrators for key values in transaction."}\r
+ \EndIf\r
+ \State $newPendingTransaction \gets \tuple{KV, G,id, seq_{clientLocal}}$\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 a transaction.\r
+\r
+\algblock[TryCatchFinally]{try}{endtry}\r
+\algcblock[TryCatchFinally]{TryCatchFinally}{finally}{endtry}\r
+\algcblockdefx[TryCatchFinally]{TryCatchFinally}{catch}{endtry}\r
+ [1]{\textbf{catch} #1}\r
+ {\textbf{end try}}\r
+\begin{algorithmic}[1]\r
+\Function{TransactionCommit}{$ $}\r
+ \State $\tuple{KV, G,id, seq_{clientLocal}} \gets newPendingTransaction$\r
+ \r
+ \If{$|KV| = 0$} \Comment{Nothing To Update}\r
+ \State $TransStatus \gets \tuple{noeffect}$ \r
+ \State \Return{$TransStatus$}\r
+ \EndIf\r
+ \State $transArb \gets $\Call{GetArbitratorKV}{$KV$}\r
+ \r
+ \If{$transArb = LOCAL\_ID$}\r
+ \State \Call{ArbitrateFromLocal}{$\tuple{\emptyset, KV, G,seq_{clientLocal},-1,LOCAL\_ID,transArb}$}\r
+ \State \Call{UpdateCommittedKV}{}\r
+ \State \Call{UpdateLiveTransactionsAndStatuses}{}\r
+ \State \Call{UpdateSpeculativeKV}{} \r
+ \Else\r
+ \State $TransStatus \gets \tuple{pending}$ \r
+ \State \Call{SetTransStatus}{$LOCAL\_ID, seq_{clientLocal}, TransStatus$}\r
+ \r
+ \State $newTrans \gets \tuple{\emptyset, KV, G,seq_{clientLocal},-1,LOCAL\_ID,transArb}$\r
+ \State \Call{GenerateParts}{newTrans} \r
+ \State $PendingTransactionQueue.push(\tuple{newTrans, \emptyset, false}$ \r
+ \EndIf\r
+ \r
+ \State $newPendingTransaction \gets \tuple{\emptyset, \emptyset, LOCAL\_ID,clntTransactionNum}$\r
+ \State $clntTransactionNum \gets clntTransactionNum + 1$\r
+\r
+ \try\r
+ \State \Call{SendToServer}{$NULL$}\r
+ \catch{$Exception$} \r
+ \ForAll{$transaction \in PendingTransactionQueue$}\r
+ \If{\Call{SendToLocal}{$transaction$}}\r
+ \State $PendingTransactionQueue.remove(transaction)$\r
+ \EndIf\r
+ \EndFor\r
+ \endtry\r
+ \r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+% Get KV Pair Committed\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Get KV Pair Committed:}\\\r
+Get the value for the key which have been committed.\r
+\begin{algorithmic}[1]\r
+\Function{GetCommit}{$k_a$}\r
+ \If{$\exists \tuple{k,v} \in CommittedKV \land k \neq k_a$}\r
+ \State \Return{$NULL$}\r
+ \EndIf\r
+ \State \Return{$v$ such that $\tuple{k,v} \in CommittedKV \land k = k_a$}\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+% Get KV Pair Committed Atomic\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Get KV Pair Committed Atomic:}\\\r
+Get the value for the key which have been committed and add it to the guard condition of the current pending transaction.\r
+\begin{algorithmic}[1]\r
+\Function{GetCommitAtomic}{$k_a$}\r
+ \State $val \gets NULL$\r
+ \If{$\exists \tuple{k,v} \in CommittedKV \land k = k_a$}\r
+ \State $val \gets v$ such that $\tuple{k,v} \in CommittedKV \land k = k_a$\r
+ \EndIf\\\r
+ \r
+ \State $\tuple{KV, G, seq_{clientLocal}} \gets newPendingTransaction$\r
+ \State $G \gets G \cup \{\tuple{k_a,val}\}$\r
+ \State $ArbSet \gets \{arb| \exists \tuple{k',v'} \in (KV \cup G), arb=$\Call{GetArbitrator}{$k'$}$\}$\r
+ \If{$|ArbSet| > 1$}\r
+ \State \Call{Error}{"Multiple arbitrators for key values in transaction."}\r
+ \EndIf\r
+ \State $newPendingTransaction \gets \tuple{KV, G, seq_{clientLocal}}$\r
+ \State \Return{$val$}\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+% Get KV Pair Speculative \r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Get KV Pair Speculative:}\\\r
+Get the value for the key which have been speculated on.\r
+\begin{algorithmic}[1]\r
+\Function{GetSpeculated}{$k_a$}\r
+ \If{$\exists \tuple{k,v} \in SpeculatedKV \land k \neq k_a$}\r
+ \State \Return{$NULL$}\r
+ \EndIf\r
+ \State \Return{$v$ such that $\tuple{k,v} \in SpeculatedKV \land k = k_a$}\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
+% Get KV Pair Speculative Atomic\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Get KV Pair Speculative Atomic:}\\\r
+Get the value for the key which have been speculative and add it to the guard condition of the current pending transaction.\r
+\begin{algorithmic}[1]\r
+\Function{GetSpeculatedAtomic}{$k_a$}\r
+ \State $val \gets NULL$\r
+ \If{$\exists \tuple{k,v} \in SpeculatedKV \land k = k_a$}\r
+ \State $val \gets v$ such that $\tuple{k,v} \in SpeculatedKV \land k = k_a$\r
+ \EndIf\\\r
+ \r
+ \State $\tuple{KV, G, id,seq_{clientLocal}} \gets newPendingTransaction$\r
+ \State $G \gets G \cup \{\tuple{k_a,val}\}$\r
+ \State $ArbSet \gets \{arb| \exists \tuple{k',v'} \in (KV \cup G), arb=$\Call{GetArbitrator}{$k'$}$\}$\r
+ \If{$|ArbSet| > 1$}\r
+ \State \Call{Error}{"Multiple arbitrators for key values in transaction."}\r
+ \EndIf\r
+ \State $newPendingTransaction \gets \tuple{KV, G, seq_{clientLocal}}$\r
+ \State \Return{$val$}\r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
\r
-\section{\textbf{Device Approach}}\r
-\r
-\subsection{\textbf{Records}}\r
-Each record has the following information included in it:\r
-\begin{itemize}\r
- \item Machine ID of the device creating the record\r
- \item The vector clock using the largest clock values from each device it knows and its own largest clock value incremented by 1.\r
- \item Data payload\r
- \item HMAC of the record.\r
-\end{itemize}\r
- \r
-Records can be identified by the machine ID and the local machine clock, hereby referred to as the record ID.\r
-\r
-\subsubsection{\textbf{Types of Payloads}}\r
-The different types of record payloads are:\r
-\begin{itemize}\r
-\r
- \item Transactions\r
- \begin{itemize}\r
- \item Contains:\r
- \begin{itemize}\r
- \item Transaction ID\r
- \item key-value pair gets (reads)\r
- \item A guard condition (boolean condition) that can be evaluated on the key-value gets.\r
- \item A set of key-value pairs that are to be updated if the guard condition is met.\r
- \item Can only get and set key-value pairs that are from 1 arbitrator. Getting and/or setting key-value pairs from more than 1 arbitrator causes the transaction to be invalid and dead.\r
- \end{itemize}\r
- \end{itemize}\r
- \item Commit notifications\r
- \begin{itemize}\r
- \item Contains the commit of a single transaction, the whole transaction.\r
- \item There is 1 commit per transaction.\r
- \item Generated by the arbitrator for the set of key-value gets and sets in the transaction.\r
- \end{itemize}\r
- \item Abort notifications\r
- \begin{itemize}\r
- \item Contains a transaction ID of an aborted transaction and the machine ID of the device that created that transaction.\r
- \item Causes a transaction to be aborted, key-values not used in updates.\r
- \end{itemize}\r
- \item Data structure re-size notifications\r
- \begin{itemize}\r
- \item Contains new size of data structure (number of record allowed in the data structure or something like that).\r
- \end{itemize}\r
- \item Server sequence number confirmations.\r
- \begin{itemize}\r
- \item Contains a record ID and the server sequence number for that record that the server reported.\r
- \item Created by any device if that device finds a record with a server sequence number that does not have a server sequence number conformation yet.\r
- \end{itemize}\r
- \item Delete notifications\r
- \begin{itemize}\r
- \item Contain the server sequence number of the record that was deleted.\r
- \item Generated when a device deletes a record.\r
- \end{itemize}\r
- \item New Key notification\r
- \begin{itemize}\r
- \item Contains the name of a new key and the machine ID of the machine that is to arbitrate\r
- \item Generated when a device generates a new (never used) key-value pair.\r
- \end{itemize}\r
-\end{itemize}\r
-\r
-\subsection{\textbf{Pulling the data structure}}\r
-To pull the latest version of the data structure the following is done:\r
-\begin{enumerate}\r
- \item Make a pull request to the server and get all the records sent back.\r
- \item Separate the records by machine ID.\r
- \item For each machine ID, order the records based on that machine IDs clock within each of the records.\r
- \item Check the data structure for any malicious activity (discussed below)\r
-\end{enumerate}\r
-\r
-\subsection{\textbf{Updates}}\r
-Updates take place as follows:\r
-\begin{enumerate}\r
- \item A device pulls the latest version of the data structure. If the device cannot pull the latest version because of network connectivity or some other issues then that device will just work using the local copy of the data structure it has.\r
- \item Check the pulled data structure for any malicious activity (as stated in a section below) if not done already.\r
- \item Check if any records in the current server need to be deleted (have delete notifications in data structure but the delete never took place), if so then delete them.\r
- \item Check that the size of the data structure will not exceed the max size when the new record is inserted. If it does then prepare to delete records by inserting delete payloads in the new record (discussed below).\r
- \item The device makes a record as follows:\r
- \begin{enumerate}\r
- \item Adds its machine ID.\r
- \item Creates a vector clock using the largest clock values from each device it knows and its own largest clock value incremented by 1.\r
- \item Fill the record payload section with the transactions and other types of payloads.\r
- \item Fill the empty space of the record payload with server sequence number confirmations for records that have yet to have their server sequence numbers confirmed.\r
- \item Fill the empty space of the record payload with rescued key-value pairs, transactions, ext (Discussed later).\r
- \item Pad the record to be the same size for all records.\r
- \item Calculate the HMAC of the record and add that to the record\r
- \item Encrypt the record.\r
- \end{enumerate}\r
- \item Send the record to the server for insertion into the device's queue.\r
- \item Issue any server commands such as deletes to the server.\r
-\end{enumerate}\r
-\r
-If there is a connectivity issue then all the records will be held by the local device until connection is resumed then pushed to the server in the order which they occurred. Also the device can only delete records for which there is a server sequence number. At some point the device could run out of records to delete (it hasn't connected to the server in a while) in which case the device will not be able to delete any records.\r
-\r
-\subsection{\textbf{Deletions}}\r
-When deciding which records to delete the following is to be done:\r
-\begin{enumerate}\r
- \item Order all the records in order based on their server sequence numbers\r
- \item Calculate the difference between the current size of the data structure and the minimum size of the data structure (lets call this $m$). Note: count newly inserted records towards the total size of the data structure if doing deletes while doing updates.\r
- \item Delete the oldest m records based on the ordering from step 1. \r
- \begin{itemize}\r
- \item If a record to be deleted has live data in it then the whole data structure needs to be re-sized.\r
- \end{itemize}\r
-\end{enumerate}\r
-\r
-Note this makes that size of the data structure be bounded:\r
-If there are $n$ devices and the data structure has a minimum size of $m$. Then the max size of the data structure is given by $m + n -1$ for the case when all the devices make an update at the same time. \r
-\r
-\subsection{\textbf{Reading a key-value pair}}\r
-When getting a key-value pair the following is done:\r
-\begin{enumerate}\r
- \item A device pulls the latest version of the data structure. If the device cannot pull the latest version because of network connectivity or some other issues then that device will just work using the local copy of the data structure it has.\r
- \item Check the pulled data structure for any malicious activity (as stated in a section below) if not done already.\r
- \item Find the transaction with the largest server sequence number that contains the key-value pair of interest (this is the latest value).\r
-\end{enumerate}\r
-\r
-\subsection{\textbf{Rescuing Transactions, Commits, Aborts, Ext}}\r
-Data should be proactively rescued from the "oldest" records currently in the data structure. Unused space in new records should be used to rescue data from old records so that when it comes time to delete the old records, there are no live pieces of data that need to be rescued. When a piece of data is rescued, it is rescued with its vector clock as well (so that the time of that data can be saved).\\\r
-\r
-When rescuing transactions and commits: only keep the key-value pair sets that do not have a newer key-value pair set (no other transaction/commits sets that key-value pair later in the future). This means that transactions/commits can shrink in size.\\\r
-\r
-When rescuing Key Value notifications: save the vector clock and the server sequence number of the notification in the rescued data.\r
-\r
-When deciding which data to rescue the following is to be done:\r
-\begin{enumerate}\r
- \item Order all the records in order based on their server sequence numbers\r
- \item Create an ordered list of currently live transactions, commits, aborts, ext from the oldest $n$ records from step one where the order is based on the age of the data (how old the record is).\r
- \item Randomly select from the list of live transactions, commits, aborts, ext to save. Save as much as can fit in the current new record. The random selection could give higher probability to transactions, commits, aborts, ext from records that are to be deleted sooner.\r
-\end{enumerate}\r
-\r
-\subsection{\textbf{Checking the Data Structure}}\r
-Checking the data structure for consistency is done as follows:\r
-\begin{enumerate}\r
- \item Verify that each record in the data structure has an HMAC that matches the data in the record.\r
- \item Verify that the oldest record the server sent has a server sequence number that is equal to or less than the server sequence number in the most recent delete notification (currently live delete notification) + 1.\r
- \item Make sure that for each device queue the difference between the vector clock value of the device queues clock is at most 1 between 2 consecutive messages for all records with server sequence numbers above the last deleted records server sequence numbers.\r
- \item Verify that no currently live data Structure re-size notification is smaller than the last known data structure size. Data structure can only grow in size.\r
- \item Verify that all the server sequence numbers for the records that are currently present have unique numbers.\r
- \item Verify that all the server sequence numbers for the records have a difference of 1 (no gaps) for all records with server sequence numbers above the last deleted records server sequence numbers.\r
- \item Verify record server sequence numbers against the stated server sequence numbers in the server sequence number notification payloads (make sure the server is not changing the sequence number on the fly).\r
-\end{enumerate}\r
-\r
-\subsection{\textbf{The Arbitrator}}\r
-The arbitrator can:\r
-\begin{enumerate}\r
- \item Send Commits\r
- \item Send Aborts\r
-\end{enumerate}\r
-\r
-\subsubsection{\textbf{Commits}}\r
-Commits have the following properties\r
-\begin{itemize}\r
- \item Agree with the ordering of the server sequence numbers most of the time.\r
- \item Cannot commit an already aborted transaction.\r
- \item Commits state the ordering of key-value pairs.\r
- \item Can disagree with the ordering of server sequence numbers if arbitrator decides to do so.\r
- \item Should occur frequently as to make sure that the commit order matches the server sequence ordering as closely as possible (prevent large divergence of the 2 orderings)\r
-\end{itemize}\r
- \r
-\subsubsection{\textbf{Aborts}}\r
-\r
-\begin{itemize}\r
- \item Aborts are used to show which transactions have been aborted based on the arbitrators decision.\r
- \item Aborts are considered live until an abort acknowledgement is presented.\r
-\end{itemize}\r
- \r
-\subsection{\textbf{Setting Up New Keys (Choosing the Arbitrator)}}\r
-Setting up new keys is done as follows:\r
-\begin{enumerate}\r
- \item Device wishes to generate new key\r
- \item Device inserts a New Key notification into the data structure.\r
-\end{enumerate}\r
-In the case where multiple devices are creating the same key, the key with the smallest vector clock is the only valid one. In the case of a concurrent vector clock, the smallest server sequence number notification is the valid one.\r
- \r
-\subsection{\textbf{Live Status}}\r
-Live Status of entries:\r
-\begin{enumerate}\r
-\r
- \item Delete notifications\r
- \begin{itemize}\r
- \item Live if it deleted the largest known server sequence number to be deleted (most recent delete).\r
- \end{itemize}\r
- \r
- \item Commit notifications\r
- \begin{itemize}\r
- \item Live until all the key-value pair sets in the transaction commit are dead.\r
- \begin{itemize}\r
- \item key-value pairs are dead when a commit for a transaction that sets the same key-value pair occurs with a larger vector clock.\r
- \end{itemize}\r
- \end{itemize}\r
- \r
- \item Abort notifications\r
- \begin{itemize}\r
- \item Live until the device whos machine ID is in the abort notification makes an update to the data structure that contains a vector clock that is more in the future than the vector clock for this abort notification.\r
- \end{itemize}\r
- \r
- \item Data structure re-size notifications\r
- \begin{itemize}\r
- \item Live if it contains the largest target size of the data structure.\r
- \end{itemize}\r
- \r
- \item Server sequence number confirmations.\r
- \begin{itemize}\r
- \item Live until the record that this notification is reporting on is deleted.\r
- \end{itemize}\r
- \r
- \item Transactions\r
- \begin{itemize}\r
- \item Is dead if it is invalid (contains keys-values for multiple arbitrators)\r
- \item Live until a commit or abort notification for this transaction is generated.\r
- \end{itemize}\r
- \r
- \item New Key notification\r
- \begin{itemize}\r
- \item Is dead if there exists a New Key notification that has a server sequence number that is smaller and the same key name.\r
- \end{itemize}\r
- \r
-\end{enumerate}\r
-\r
-\section{\textbf{Server Approach}}\r
-\r
-The servers view of the system is in terms of data slots where each data slot holds a single record, has a monotonically increasing number associated with it (server sequence number) for the record that currently is present in that data slot and can be set or deleted. A server may have a finite amount of memory which it can partition into slots, reusing memory that newly deleted slots used to occupy.\r
-\r
-There are 3 types of requests from a device that the server must respond to:\r
-\begin{enumerate}\r
- \item Pull all current slots.\r
- \item Put a new record in a slot.\r
- \item Delete a slot.\r
-\end{enumerate}\r
-\r
-\subsection{\textbf{Pull all current slots}}\r
-In this case the server will simply send back all active slots (slots that have data) in any order along with each slots server sequence number. It is the job of the devices to order the slots.\r
-\r
-\subsection{\textbf{Put a new record in a slot}}\r
-In this case the server will:\r
-\begin{enumerate}\r
- \item Receive a record data from a device.\r
- \item Put this record data in an empty slot.\r
- \item Assign the just received record the next number in the server sequence numbers.\r
-\end{enumerate}\r
-If more than 1 put request is made at the same time, the server is free to order the requests however it wishes.\r
-\r
-\subsection{\textbf{Delete a slot}}\r
-In this case the server will delete the data in the slot that has the server sequence number that matches the server sequence number in the delete request. The server could delay the delete if it wishes (if it has plenty of space for new slots).\r
-\r
-\section{\textbf{System Guarantees}}\r
-\begin{itemize}\r
- \item Server cannot view data inside records\r
- \item Server cannot forge or modify or create any records\r
- \item Server cannot withhold any records\r
- \item Server cannot reorder records that could not have been ordered differently due to network latency\r
- \item Server cannot delete records unless told to do so.\r
- \item There will always be an obvious key-value pair that is the latest key value pair.\r
- \item The data structure is bounded in size such that $m$ is the minimum size of the data structure, $n$ is the number of devices in the system and $s$ is the current size of the data structure: $m \leq s \leq (m+n-1)$\r
- \item Data structure can only grow when there are too may key-value pairs (and aborts) than what fit in the current data structure size within reason.\r
- \item No currently valid data can be lost by the system and go undetected.\r
- \item Devices can operate offline and re-sync with the system and get a consistent view of the system\r
- \item If the server tries to hold a device on an older version of the data structure, that device can eventually rejoin the main data structure without problems.\r
- \item Devices that have a transaction aborted will be able to be notified about the abort indefinitely (no time frame when notification must be accepted).\r
- \item Server cannot hold a device on an old version of the data structure and then move them to a newer version of the data structure without being detected (The server sequence numbers would reveal conflicts or gaps or both).\r
-\r
-\end{itemize}\r
- \r
-\section{System Correctness}\r
-\r
-\end{document}
\ No newline at end of file
+\end{document}\r
projects / iotcloud.git / blobdiff