Updates
authorAli Younis <ayounis@uci.edu>
Mon, 17 Oct 2016 03:52:11 +0000 (20:52 -0700)
committerAli Younis <ayounis@uci.edu>
Mon, 17 Oct 2016 03:52:11 +0000 (20:52 -0700)
version2/doc/iotcloud_formal/iotcloud.tex
version2/doc/iotcloud_informal/iotcloud.out

index 8239655..d4e201a 100644 (file)
@@ -102,10 +102,6 @@ Delete slot is an operation that deletes all live slots that have server sequenc
 \r
 \r
 \r
-\r
-\r
-\r
-\r
 \section{\textbf{Client}}\r
 The data structure acts as a key store where key-value pairs can be read and set.\r
 The data structure exposes the following functions:\r
@@ -132,7 +128,7 @@ $kv_n$ is a key-value entry $\tuple{k_n,v_n} , k \in K$\\
 \r
 $tid_s = \tuple{mid_s,c_{mid_s}}$\\\r
 $guard_s = \tuple{\{kv_1, kv_2, ... ,kv_n | \exists mid \in MID, \forall n, kv_n[k] \in K_{mid}\},$ boolean condition using $ \{kv_1, kv_2, ... ,kv_n\}} $\\\r
-$transaction_s = \{mid_s,vc_{s_t} ,\{kv_1, kv_2,...kv_n | \exists mid \in MID, mid = guard_s[mid], \forall n, kv_n[k] \in K_{mid}\},guard_s\}$\\\r
+$transaction_s = \tuple{mid_s,vc_{s_t} ,\{kv_1, kv_2,...kv_n | \exists mid \in MID, mid = guard_s[mid], \forall n, kv_n[k] \in K_{mid}\},guard_s}$\\\r
 $commit_s = \tuple{tid_s,vc_s}$\\\r
 $abort_s = \tuple{tid_s,mid_s,vc_s}$\\\r
 $sequence_s = \tuple{rid_s, ssn_s}$\\\r
@@ -153,10 +149,10 @@ $record_s = \tuple{ssn_s,rd_s}$\\
 The following helper functions are needed:\\\r
 \r
 \r
-%Throw Error\r
+% Error\r
 \noindent\fbox{%\r
 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
-\textbf{Throw Error:}\r
+\textbf{ Error:}\r
 \begin{algorithmic}[1]\r
 \Function{Error}{$msg$}\r
     \State $Print(msg)$\r
@@ -166,28 +162,6 @@ The following helper functions are needed:\\
 \end{varwidth}% \r
 }\r
 \r
-%Error Message\r
-\begin{algorithmic}[1]\r
-\Procedure{Error}{$msg$}\r
-\State $Print(msg)$\r
-\State $Halt()$\r
-\EndProcedure\r
-\end{algorithmic}\r
-\r
-\r
-%Get Latest Data Structure From Server\r
-\noindent\fbox{%\r
-\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
-\textbf{Get  Latest Data Structure From Server}:\r
-\begin{algorithmic}[1]\r
-\Function{GetLatestDataStruct}{}\r
-    \State $largestSsn \gets $ Largest $ssn$ of all $ssn$ in $R$\r
-    \State $R \gets R \cup $ \Call{GetSlotServer}{$largestSsn + 1$}\r
-\EndFunction\r
-\end{algorithmic}\r
-\end{varwidth}% \r
-}\r
-\r
 %Get Payload Items from Record with SSN\r
 \noindent\fbox{%\r
 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
@@ -208,10 +182,10 @@ The following helper functions are needed:\\
 \end{varwidth}% \r
 }\r
 \r
-%Get rid For Record\r
+%Get rid of record\r
 \noindent\fbox{%\r
 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
-\textbf{Get rid For Record}:\r
+\textbf{Get rid of record:}\r
 \begin{algorithmic}[1]\r
 \Function{GetRid}{$record_s$}\r
     \State $\tuple{ssn_s, \tuple{mid_s, \{c_{mid_1}, c_{mid_2}, ... , c_{mid_k}\}, hmac_s, payload_s}} \gets record_s$\r
@@ -221,6 +195,82 @@ The following helper functions are needed:\\
 \end{varwidth}% \r
 }\r
 \r
+%Get tid of transaction\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Get tid of transaction:}\r
+\begin{algorithmic}[1]\r
+\Function{GetTid}{$transaction_s$}\r
+    \State $\tuple{ssn_s,\{c_{mid_1}, c_{mid_2}, ... , c_{mid_k}\}, \{kv_1, kv_2,...kv_n\}, guard_s} \gets record_s$\r
+    \State \Return {$\tuple{mid_s, c_{mid_s}}$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
+\r
+%Key Value Live\r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Key Value Live:}\r
+\begin{algorithmic}[1]\r
+\Function{KeyValueLive}{$keyName_s, transaction_s$}\r
+    \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\r
+    \State $AT \gets \emptyset$    \Comment{Set of all Payload Items that are transactions}\r
+    \State $AC \gets \emptyset$    \Comment{Set of all Payload Items that are commits}\r
+    \State $AA \gets \emptyset$    \Comment{Set of all Payload Items that are aborts}\r
+    \State $commitTrans = NULL$\r
+    \State $tid \gets $ \Call{GetTid}{$transaction_s$}\\\r
+\r
+    \ForAll{$record$ in $R$}\r
+        \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}\r
+    \EndFor\\\r
+    \r
+    \ForAll{$\tuple{ssn, payload}$ in $API$}\r
+        \If{$payload$ is a $transaction$}\r
+            \State $AT \gets AT \cup \{payload\}$\r
+        \ElsIf{$payload$ is a $commit$}\r
+            \State $AC \gets AC \cup \{payload\}$\r
+        \ElsIf{$payload$ is a $abort$}\r
+            \State $AA \gets AA \cup \{payload\}$\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \ForAll{$\tuple{tid',mid',vc'}$ in $AA$} \Comment{Has an abort}\r
+        \If{$tid' = tid$}\r
+            \State \Return{False}\r
+        \EndIf\r
+    \EndFor\\\r
+\r
+    \ForAll{$\tuple{tid',vc'}$ in $AC$} \Comment{Has a commit}\r
+        \If{$tid' = tid$}\r
+            \State $commitTrans \gets \tuple{tid',vc'}$\r
+            \State Break\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \If{$commitTrans = NULL$}   \r
+        \State \Return{True} \Comment{If transaction not yet committed then alive}\r
+    \EndIf\\\r
+    \r
+    \State $\tuple{tid_c, vc_c} \gets commitTrans$\r
+    \ForAll{$trans$ in $AT$}\r
+        \State $\{mid_t,vc_t ,\{\tuple{k_1, v_1}, \tuple{k_2, v_2},..., \tuple{k_k, v_k}\},guard_t\} \gets trans$\r
+        \If{$(trans \neq transaction_s) \land (keyName_s = k_n)$}\r
+            \ForAll{$\tuple{tid_c',vc_c'}$ in $AC$}\r
+                \If{$(tid_c = $ \Call{GetTid}{$trans$} $) \land (vc_c' > vc_c)$}\r
+                    \State \Return{False}\r
+                \EndIf\r
+            \EndFor\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \State \Return{True}\r
+    \r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
+\r
 %Sequence Live\r
 \noindent\fbox{%\r
 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
@@ -300,14 +350,32 @@ The following helper functions are needed:\\
 \textbf{Abort Live}:\r
 \begin{algorithmic}[1]\r
 \Function{AbortLive}{$abort_s$}\r
+    \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\r
+    \State $tid \gets NULL$\r
     \State $\tuple{tid_s,mid_s,vc_s} \gets abort_s$\\\r
+\r
+    \ForAll{$record$ in $R$}\r
+        \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}\r
+    \EndFor\\\r
+    \r
+    \ForAll{$\tuple{ssn, payload}$ in $API$} \Comment{Transaction still in data structure}\r
+        \If{$payload$ is a $transaction$}\r
+            \State $tid \gets $\Call{GetTid}{$payload$}\r
+            \If{$tid = tid_s$}\r
+                \State Return{True}\r
+            \EndIf\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \r
+    \r
     \ForAll{record in R}\r
         \State $\tuple{ssn_s',\tuple{mid_s', vc_s', hmac_s', payload_s'}} \gets record$\r
         \If{$(mid_s'=mid_s) \land (vc_s' > vc_s)$}\r
-            \State \Return{True}\r
+            \State \Return{False}\r
         \EndIf\r
     \EndFor\\\r
-    \State \Return{False}\r
+    \State \Return{True}\r
 \EndFunction\r
 \end{algorithmic}\r
 \end{varwidth}% \r
@@ -383,6 +451,91 @@ The following helper functions are needed:\\
 \end{varwidth}% \r
 }\r
 \r
+%Transaction Live\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Transaction Live:}\r
+\begin{algorithmic}[1]\r
+\Function{TransactionLive}{$transaction_s$}\r
+    \State $AA \gets \emptyset$    \Comment{Set of all Payload Items that are aborts}\r
+    \State $AC \gets \emptyset$    \Comment{Set of all Payload Items that are commits}\r
+    \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\r
+    \State $tid \gets $ \Call{GetTid}{$transaction_s$}\r
+    \State $foundCommit \gets False$\\\r
+    \r
+    \ForAll{$record$ in $R$}\r
+        \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}\r
+    \EndFor\\\r
+    \r
+    \ForAll{$\tuple{ssn, payload}$ in $API$}\r
+        \If{$payload$ is a $abort$}\r
+            \State $AA \gets AA \cup \{payload\}$\r
+        \ElsIf{$payload$ is a $commit$}\r
+            \State $AC \gets AC \cup \{payload\}$\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \ForAll{$\tuple{tid',mid',vc'}$ in $AA$} \Comment{There is an abort}\r
+        \If{$tid' = tid$}\r
+            \State \Return{False}\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \ForAll{$\tuple{tid',vc'}$ in $AC$} \Comment{There is no commit}\r
+        \If{$tid' = tid$}\r
+            \State $foundCommit \gets True$\r
+            \State Break\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \If{$\lnot foundCommit$}\r
+        \State \Return{True}\r
+    \EndIf\\\r
+    \r
+    \State $\tuple{mid',vc' ,kvSet',guard'} \gets transaction_s$ \Comment{All Keys are dead}\r
+    \ForAll{$\tuple{k',v'}$ in $kvSet'$}\r
+        \If{\Call{KeyValueLive}{$k', transaction_s$}}\r
+            \State \Return{True}\r
+        \EndIf\r
+    \EndFor\r
+\r
+    \State \Return{False}\r
+\r
+\EndFunction\r
+\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
+\r
+%Commit Live\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Commit Live:}\r
+\begin{algorithmic}[1]\r
+\Function{CommitLive}{$commit_s, ssn_s$}\r
+    \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\r
+    \State $AT \gets \emptyset$    \Comment{Set of all Payload Items that are transaction}\r
+    \State $tid' \gets NULL$ \r
+    \State $\tuple{tid, vc} \gets commit_s$ \\ \r
+\r
+    \ForAll{$record$ in $R$}\r
+        \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}\r
+    \EndFor\\\r
+    \r
+    \ForAll{$\tuple{ssn, payload}$ in $API$}\r
+        \If{$payload$ is a $transaction$}\r
+            \State $tid' \gets$ \Call{GetTid}{$payload$}\r
+            \If{$tid' = tid$}\r
+                \State \Return{True}\r
+            \EndIf\r
+        \EndIf\r
+    \EndFor\\\r
+\r
+    \State \Return{False}\r
+\EndFunction\r
+\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
+\r
 %Is Live\r
 \noindent\fbox{%\r
 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
@@ -390,7 +543,7 @@ The following helper functions are needed:\\
 \begin{algorithmic}[1]\r
 \Function{IsLive}{$item_s, ssn_S$}\r
     \If{$item_s$ is a $tansaction$}\r
-        \State \Return{\Call{TransactionLive}{$item_s, ssn_s$}}\r
+        \State \Return{\Call{TransactionLive}{$item_s$}}\r
     \r
     \ElsIf{$item_s$ is a $commit$}\r
         \State \Return{\Call{CommitLive}{$item_s, ssn_s$}}\r
@@ -464,6 +617,41 @@ The following helper functions are needed:\\
 \end{varwidth}% \r
 }\r
 \r
+%Rescue New Key\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Rescue New Key:}\r
+\begin{algorithmic}[1]\r
+\Function{RescueNewKey}{$newKeyPayload, ssn$}\r
+    \State $\tuple{k', vc', ssn', mid'} \gets newKeyPayload$\r
+    \State \Return{$\tuple{k', vc', ssn, mid'}$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
+\r
+%Rescue Transaction\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Rescue New Key:}\r
+\begin{algorithmic}[1]\r
+\Function{RescueTransaction}{$transPayload, ssn$}\r
+    \State $KVRescue \gets \emptyset$\r
+    \State $\tuple{mid',vc', KVSet,guard_s} \gets transPayload$\\\r
+    \r
+    \ForAll{$\tuple{k,v}$ in $KVSet$}\r
+        \If{\Call{KeyValueLive}{$k, transPayload$}}\r
+            \State $KVRescue \gets KVRescue \cup \{\tuple{k,v}\}$\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \State \Return{$\tuple{mid',vc', KVRescue,guard_s}$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
+\r
+\r
 %Rescue Payload Items\r
 \noindent\fbox{%\r
 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
@@ -484,7 +672,13 @@ The following helper functions are needed:\\
     \State Sort $PIList$ by $ssn$ from lowest to highest\\\r
     \r
     \ForAll{$\tuple{ssn', payload'}$ in $PIList$}\r
-        \If{\Call{IsLive}{$payload', ssn'$} $\land$ \Call{getRandomBoolean}{ } }\r
+        \If{\Call{IsLive}{$payload', ssn'$} $\land$ \Call{getRandomBoolean}{ } }\\\r
+            \r
+            \If{$payload'$ is a $newkey$}\r
+                \State $payload' \gets $ \Call{RescueNewKey}{$payload'$}\r
+            \ElsIf{$payload'$ is a $transaction$}\r
+                \State $payload' \gets $ \Call{RescueTransaction}{$payload'$}\r
+            \EndIf\\\r
         \r
             \If{\Call{GetSize}{$payload'$} $ > SpaceRemaining$} \Comment{No more space for resuces in payload}\r
                 \State \Return{$payload_s$}\r
@@ -703,7 +897,7 @@ The following helper functions are needed:\\
         \ForAll{$record_2$ in $R[1:]$}\r
             \State $\tuple{ssn_2,rData_2} \gets record_2$\r
             \If{$ssn_2 = (ssn_1 + 1)$}\r
-                \State $didFindSsn \gets True$\r
+                \    State $didFindSsn \gets True$\r
                 \State Break\r
             \EndIf\r
         \EndFor\r
@@ -736,7 +930,7 @@ The following helper functions are needed:\\
     \State $\tuple{ssn, payload} \gets R[0]$ \Comment{Get first record in the sorted R}\r
     \If{$ssn > (oldestDeleteSsn + 1) $}\r
         \State \Call{Error}{Missing records}\r
-    \EndIf\\\r
+   \EndIf\\\r
     \r
     \r
     \ForAll{$mid$ in $MID$}\r
@@ -756,7 +950,8 @@ The following helper functions are needed:\\
             \State $didFindSsn \gets False$\r
             \ForAll{$c_2$ in $midClocks[1:]$}\r
                 \If{$c_2 = (c_1 + 1)$}\r
-                    \State $didFindClock\gets True$\r
+                    \State $didFindC\r
+ock\gets True$\r
                     \State Break\r
                 \EndIf\r
             \EndFor\r
@@ -773,25 +968,61 @@ The following helper functions are needed:\\
 %\end{varwidth}% \r
 %}\r
 \r
+%Get Latest Data Structure From Server\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Get  Latest Data Structure From Server}:\r
+\begin{algorithmic}[1]\r
+\Function{GetLatestDataStruct}{}\r
+    \State $largestSsn \gets $ Largest $ssn$ of all $ssn$ in $R$\r
+    \State $R \gets R \cup $ \Call{GetSlotServer}{$largestSsn + 1$}\r
+    \State \Call{CheckDataStructForValidity}{ }\r
+\EndFunction\r
+\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
+\r
+%Update Key Value Set\r
+\noindent\fbox{%\r
+\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Update Key Value Set:}\r
+\begin{algorithmic}[1]\r
+\Function{UpdateKVSet}{$currentKV, kvSet$}\r
+    \State $newKVSet \gets kvSet$\r
+    \State $foundKey \gets False$\\\r
+    \r
+    \ForAll{$\tuple{k,v}$ in $currentKV$}\r
+        \State $foundKey \gets False$\\\r
+        \r
+        \ForAll{$\tuple{k',v'}$ in $kvSet$}\r
+            \If{$k = k'$}\r
+                \State $foundKey \gets True$\r
+                \State Break\r
+            \EndIf\r
+        \EndFor\\\r
+        \r
+        \If{$\lnot foundKey$}\r
+            \State $newKVSet \gets newKVSet \cup \{\tuple{k,v}\}$\r
+        \EndIf\r
+    \EndFor\r
+    \r
+    \State \Return{$newKVSet$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\end{varwidth}% \r
+}\r
 \r
 \r
 \r
-\textbf{Transaction Live}:\\\r
-\textbf{Commit Live}:\\\r
-\textbf{Key Value Live}:\\\r
 \r
 \r
-%-Rescues\r
-%    - Need to Change Transaction sizes\r
-%    - Need to Change New Key ssn in transaction\r
-%-Gets\r
 %-Arbitration\r
 %   - Insert Commit\r
-%-Check Data Structure\r
-\r
 \r
 \r
 \subsection{\textbf{Create new key}}\r
+This operation creates a key and assigns an arbitrator to arbitrate on that new key.  In the case where more than one clients concurrently try to create the same new key, the client that inserted the newkey payload with the lowest ssn will be the client to generate the key, all other clients generation attempts would be invalid.\r
+\r
 \noindent\fbox{%\r
 \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
 \textbf{Create new key:}\r
@@ -862,10 +1093,86 @@ If by adding this transaction the data structure size exceeds the proposed max d
 }\r
 \r
 \subsection{\textbf{Get key-value pair}}\r
+This operation gets the latest key value pair from the data structure.  This is done by starting at the last known committed key value pairs then extrapolating into the future of uncommitted transactions till the transaction with the largest ssn is reached.  Everytime a new transaction is evaluated, it is evaluated against the current best guess of key value pairs based on the transactions up to the transaction being evaluated (by ssn).  This allows each client to "guess" what the latest value for a specified key will be even when the arbitrator has not stepped in yet to arbitrate.\r
 \r
+%\noindent\fbox{%\r
+%\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}\r
+\textbf{Get  Latest Data Structure From Server}:\r
+\begin{algorithmic}[1]\r
+\Function{GetValueForKey}{$keyName$}\r
+    \State $API \gets \emptyset$   \Comment{Set of all Payload Items}\r
+    \State $AT \gets \emptyset$    \Comment{Set of all Payload Items that are transactions}\r
+    \State $AC \gets \emptyset$    \Comment{Set of all Payload Items that are commits}\r
+    \State $AA \gets \emptyset$    \Comment{Set of all Payload Items that are aborts}\r
+    \State $kSet \gets \emptyset$ \Comment{Set of all key names in the system}\r
+    \State $tid \gets NULL$\r
+    \State $currentKV \gets \emptyset$\\\r
+    \r
+    \State \Call{GetLatestDataStruct}{ } \Comment{Update local version of data struct}\\\r
+    \r
+    \ForAll{$record$ in $R$}\r
+        \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record}\r
+    \EndFor\\\r
+    \r
+    \ForAll{$\tuple{ssn, payload}$ in $API$}\r
+        \If{$payload$ is a $transaction$}\r
+            \State $AT \gets AT \cup \{\tuple{ssn,payload}\}$\r
+        \ElsIf{$payload$ is a $commit$}\r
+            \State $AC \gets AC \cup \{payload\}$\r
+        \ElsIf{$payload$ is a $abort$}\r
+            \State $AA \gets AA \cup \{payload\}$\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \State Sort $AT$ by ssn from oldest to newest\\\r
+    \r
+    \ForAll{$trans$ in $AT$} \Comment{Get the latest committed keys}\r
+        \State $\tuple{mid,vc ,kvSet,guard} \gets trans$\\\r
+    \r
+        \ForAll{$\tuple{k,v}$ in $kvSet$} \Comment{Get all key names in the system}\r
+            \State $kSet \gets kSet \cup \{k\}$\r
+        \EndFor\\\r
 \r
-\r
-\r
-\r
+        \If{$\lnot $\Call{TransactionLive}{$trans$}} \Comment{Only keep live transactions}\r
+            \State $AT \gets AT - \{trans\}$\r
+            \State Continue\r
+        \EndIf\\\r
+    \r
+        \State $tid \gets $ \Call{GetTid}{$trans$}\r
+        \ForAll{$com$ in $AC$}\r
+            \State $\tuple{tid', vc'} \gets com$\r
+            \If{$tid' = tid$}\r
+                \ForAll{$\tuple{k,v}$ in $kvSet$}\r
+                    \If{\Call{KeyValueLive}{$k,trans$}}\r
+                        \State $currentKV \gets currentKV \cup \{\tuple{k,v}\}$\r
+                    \EndIf\r
+                \EndFor\\\r
+                \r
+                \State $AT \gets AT - \{trans\}$ \Comment{No need for committed transactions}\r
+                \State Break\r
+            \EndIf\r
+        \EndFor\r
+    \EndFor\\\r
+    \r
+    \ForAll{$trans$ in $AT$} \Comment{Uncommitted ones only in order from lowest ssn to highest ssn}\r
+        \State $\tuple{mid,vc ,kvSet,guard} \gets trans$\r
+        \If{\Call{EvaluateGuard}{$guard, currentKV$}} \Comment{Check if will abort}\r
+            \State $currentKV \gets $\Call{UpdateKVSet}{$currentKV, kvSet$}\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \r
+    \ForAll{$\tuple{k,v}$ in $currentKV$} \Comment{Return the latest guessed value}\r
+        \If{$k = keyName$}\r
+            \State \Return{$v$}\r
+        \EndIf\r
+    \EndFor\\\r
+    \r
+    \State \Return{$NULL$} \Comment{Key was not present}\r
+    \r
+\EndFunction\r
+\end{algorithmic}\r
+%\end{varwidth}% \r
+%}\r
 \r
 \end{document}\r
index 4241fc5..14b3549 100644 (file)
@@ -24,3 +24,9 @@
 \BOOKMARK [2][-]{subsection.4.4}{Create New Key Operation}{section.4}% 24
 \BOOKMARK [1][-]{section.5}{System Guarantees}{}% 25
 \BOOKMARK [1][-]{section.6}{System Correctness}{}% 26
+\BOOKMARK [2][-]{subsection.6.1}{Data Integrity and Authentication}{section.6}% 27
+\BOOKMARK [2][-]{subsection.6.2}{Ordering of Records}{section.6}% 28
+\BOOKMARK [2][-]{subsection.6.3}{Data Structure Functions}{section.6}% 29
+\BOOKMARK [3][-]{subsubsection.6.3.1}{Put}{subsection.6.3}% 30
+\BOOKMARK [3][-]{subsubsection.6.3.2}{Get}{subsection.6.3}% 31
+\BOOKMARK [3][-]{subsubsection.6.3.3}{Create New Key}{subsection.6.3}% 32