From badc54d22aba7e160c63ca95ce442e2333094603 Mon Sep 17 00:00:00 2001 From: Ali Younis Date: Thu, 13 Oct 2016 19:54:24 -0700 Subject: [PATCH] Formal Edits --- version2/doc/iotcloud_formal/iotcloud.tex | 191 +++++++++++++++++++++- 1 file changed, 182 insertions(+), 9 deletions(-) diff --git a/version2/doc/iotcloud_formal/iotcloud.tex b/version2/doc/iotcloud_formal/iotcloud.tex index b13d030..17c03f0 100644 --- a/version2/doc/iotcloud_formal/iotcloud.tex +++ b/version2/doc/iotcloud_formal/iotcloud.tex @@ -187,11 +187,6 @@ The following helper functions are needed:\\ \end{varwidth}% } - -\textbf{Get Transaction Arbitrator}:\\ -\textbf{Transaction Live}:\\ -\textbf{Commit Live}:\\ - %Sequence Live \noindent\fbox{% \begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} @@ -317,15 +312,192 @@ The following helper functions are needed:\\ \end{varwidth}% } +%Is Live +\noindent\fbox{% +\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} +\textbf{Is Live:}: +\begin{algorithmic}[1] +\Function{IsLive}{$item_s, ssn_S$} + \If{$item_s$ is a $tansaction$} + \State \Return{\Call{TransactionLive}{$item_s, ssn_s$}} + + \ElsIf{$item_s$ is a $commit$} + \State \Return{\Call{CommitLive}{$item_s, ssn_s$}} + + \ElsIf{$item_s$ is a $abort$} + \State \Return{\Call{AbortLive}{$item_s$}} + + \ElsIf{$item_s$ is a $delete$} + \State \Return{\Call{DeleteLive}{$item_s, ssn_s$}} + + \ElsIf{$item_s$ is a $commit$} + \State \Return{\Call{ResizeLive}{$item_s, ssn_s$}} + + \ElsIf{$item_s$ is a $sequence$} + \State \Return{\Call{SequenceLive}{$item_s, ssn_s$}} + + \ElsIf{$item_s$ is a $newkey$} + \State \Return{\Call{NewKeyLive}{$item_s, ssn_s$}} + + \ElsIf{$item_s$ is a $keyvalue$} + \State \Return{\Call{KeyValueLive}{$item_s, ssn_s$}} + \EndIf\\ + + \State \Return{False} \Comment{Will never get here} +\EndFunction +\end{algorithmic} +\end{varwidth}% +} +%Record has live payload data +\noindent\fbox{% +\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} +\textbf{Record has live payload data:}: +\begin{algorithmic}[1] +\Function{HasLivePayload}{$record_s, ssn_s$} + \State $\tuple{mid_s, vc_s, hmac_s, payload_s} \gets record_s$ + \ForAll{$item$ in $payload_s$} + \If{\Call{IsLive}{$item, ssn_s$}} + \State \Return{True} + \EndIf + \EndFor + \State \Return{False} +\EndFunction +\end{algorithmic} +\end{varwidth}% +} -\textbf{Evaluate Guard Condition:}\\ +% Get Data Structure Size +\noindent\fbox{% +\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} +\textbf{Get Data Structure Size:} +\begin{algorithmic}[1] +\Function{GetDataStrucSize}{ } + \State $API \gets \emptyset$ \Comment{Set of all Payload Items} + \State $AR \gets \emptyset$ \Comment{Set of all Payload Items that are resize} + \ForAll{record in R} + \State $API \gets API \cup$ \Call{GetPayloadItemsWithSSN}{record} + \EndFor\\ + + \ForAll{$\tuple{ssn, payload}$ in $API$} + \If{($payload$ is a $resize) \land$ \Call{IsLive}{$payload, ssn$}} + \State $\tuple{size'} \gets payload$ + \State \Return{$size'$} + \EndIf + \EndFor\\ + + \State \Return{$0$} \Comment{Get Here only if data structure has no entries} +\EndFunction +\end{algorithmic} +\end{varwidth}% +} -\textbf{Get Latest Data Structure From Server:}\\ -\textbf{Delete Records:}\\ -\textbf{Check Data Structure for Malicious Activity:} +%Rescue Payload Items +\noindent\fbox{% +\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} +\textbf{Rescue Payload Items}: +\begin{algorithmic}[1] +\Function{RescuePayloadItems}{$payload_s$} + \State $PIList =$ empty list of $\tuple{ssn, payload}$ + \State $SpaceRemaining = MaxPayloadSize - $ \Call{GetSize}{$payload_s$} + + \If{$SpaceRemaining = 0$} + \Return{$payload_s$} + \EndIf\\ + + \ForAll{record in R} + \State $PIList \gets PIList \cup$ \Call{GetPayloadItemsWithSSN}{$record$} + \EndFor\\ + + \State Sort $PIList$ by $ssn$ from lowest to highest\\ + + \ForAll{$\tuple{ssn', payload'}$ in $PIList$} + \If{\Call{IsLive}{$payload', ssn'$} $\land$ \Call{getRandomBoolean}{ } } + + \If{\Call{GetSize}{$payload'$} $ > SpaceRemaining$} \Comment{No more space for resuces in payload} + \State \Return{$payload_s$} + \EndIf + + \State $SpaceRemaining \gets SpaceRemaining -$ \Call{GetSize}{$payload'$} + \State $payload_s \gets payload_s \cup payload'$ + \EndIf + \EndFor\\ + \State \Return{$payload_s$} +\EndFunction +\end{algorithmic} +\end{varwidth}% +} +%Pad Payload +\noindent\fbox{% +\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} +\textbf{Pad Payload}: +\begin{algorithmic}[1] +\Function{PadPayload}{$payload_s$} + \State $SpaceRemaining = MaxPayloadSize - $ \Call{GetSize}{$payload_s$} + + \If{$SpaceRemaining = 0$} + \State \Return{$payload_s$} + \EndIf\\ + \State \Return{$payload_s \gets payload_s \cup$ \Call{GenerateFiller}{$SpaceRemaining$}} +\EndFunction +\end{algorithmic} +\end{varwidth}% +} + +%Delete Records +\noindent\fbox{% +\begin{varwidth}{\dimexpr\linewidth-2\fboxsep-2\fboxrule\relax} +\textbf{Delete Records (Deletes n records)}: +\begin{algorithmic}[1] +\Function{Delete}{$num\_of\_records$} + \State $RS \gets$ List of all Records sorted by ssn and has form $\tuple{ssn_s, record_s}$ + \State $n \gets 0$\\ + + \ForAll{$\tuple{ssn_s, record_s}$ in $RS$} + \If{\Call{HasLivePayload}{$record_s, ssn_s$}} + \State \Call{ResizeDataStruc}{ } + \State \Return{False} + \Else + \State \Call{DeleteSlotServer}{$ssn_s$} + \State $n \gets n + 1$ + \EndIf\\ + + \If{$n = num\_of\_records$} + \State \textbf{break} + \EndIf + \EndFor\\ + + \State \Return{True} + +\EndFunction +\end{algorithmic} +\end{varwidth}% +} + + + + +\textbf{Evaluate Guard Condition:}\\ +\textbf{Get Latest Data Structure From Server:}\\ +\textbf{Check Data Structure for Malicious Activity:}\\ +\textbf{Resize Data Structure:}\\ +\textbf{Get Transaction Arbitrator}:\\ +\textbf{Transaction Live}:\\ +\textbf{Commit Live}:\\ +\textbf{New Key Live}:\\\ +\textbf{Key Value Live}:\\\ + +%-Rescues +% - Need to Change Transaction sizes +%-Deletes +%-Resize +%-Puts +%-Gets +%-New Key +%-Arbitration +%-Check Data Structure \subsection{\textbf{Put Transaction}} @@ -334,4 +506,5 @@ The following helper functions are needed:\\ \subsection{\textbf{Get key-value pair}} \subsection{\textbf{Create new key}} + \end{document} -- 2.34.1