Merging changes
[iotcloud.git] / doc / iotcloud.tex
index 49f0b2ad0b4dd55b332b923e87f392b124108133..c2b7de8f2f86bf7268621750c2f3ffa68e7d7708 100644 (file)
@@ -254,33 +254,27 @@ $MinLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s
 \EndProcedure\r
 \end{algorithmic}\r
 \r
+\note{Don't include ``such that'' in the argument of a function...}\r
+\r
 \begin{algorithmic}[1]\r
 \Function{ValidHmac}{$DE_s,SK_s,hmac_{stored}$}\r
 \State $hmac_{computed} \gets Hmac(DE_s,SK_s)$\r
-\If{$hmac_{stored} = hmac_{computed}$}\r
-       \State $valid \gets true$\r
-\Else\r
-       \State $valid \gets false$\r
-\EndIf\r
-\State \Return{$valid$}\r
+\State \Return {$hmac_{stored} = hmac_{computed}$}\r
 \EndFunction\r
 \end{algorithmic}\r
 \r
 \begin{algorithmic}[1]\r
 \Function{ValidPrevHmac}{$DE_s,hmac_{p_s},hmac_{p_{sto}}$}\r
 \If{$hmac_{p_s} = \emptyset$}\Comment{First slot - no previous HMAC}\r
-       \State $valid \gets true$\r
+       \State \Return $true$\r
 \Else\r
-       \If{$hmac_{p_{sto}} = hmac_{p_s}$}\r
-               \State $valid \gets true$\r
-       \Else\r
-               \State $valid \gets false$\r
-       \EndIf\r
+       \State \Return {$hmac_{p_{sto}} = hmac_{p_s}$}\r
 \EndIf\r
-\State \Return{$valid$}\r
 \EndFunction\r
 \end{algorithmic}\r
 \r
+\note{So if a slot has a null previous hmac, everything is fine?  What if it isn't the first slot?}\r
+\r
 \begin{algorithmic}[1]\r
 \Function{GetQueSta}{$Dat_s$}\r
 \State $DE_s \gets GetDatEnt(DE_s)$\r
@@ -409,7 +403,6 @@ $MinLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s
 \ForAll{$de_s \in DE_s$}\r
        \If{$de_s$ \textit{such that} $de_s \in D \land de_s = kv$}\r
                \State $\tuple{k_s,v_s} \gets GetKV(de_s)$\r
-               \State $k_s \gets GetKey(\tuple{k_s,v_s})$\r
                \State $\tuple{k_s,v_t} \gets GetKeyVal(DT_s,k_s)$\r
                \If{$\tuple{k_s,v_t} = \emptyset$}\r
                        \State $DT_s \gets DT_s \cup \{\tuple{k_s,v_s}\}$\r
@@ -493,7 +486,6 @@ $MinLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s
 \Function{GetValFromKey}{$k_g$}\r
 \State $\tuple{k_s,v_s} \gets \tuple{k,v}$ \textit{such that} $\tuple{k,v} \r
        \in DT \land k = k_g$\r
-\State $v_s \gets GetVal(\tuple{k_s,v_s})$\r
 \State \Return{$v_s$}\r
 \EndFunction\r
 \end{algorithmic}\r
@@ -545,14 +537,13 @@ $\tuple{ck,\tuple{k, v}} \in KV_s \wedge
 \forall \tuple{ck_s,\tuple{k_s, v_s}} \in KV_s, k = k_s$ \\\r
 \r
 \begin{algorithmic}[1]\r
-\Function{PutKVPair}{$KV_s,\tuple{k_s,v_s}$}\r
-\State $k_s \gets GetKey(\tuple{k_s,v_s})$\r
-\State $\tuple{ck_s,\tuple{k_s,v_t}} \gets GetKV(KV_s,k_s)$\r
+\Function{PutKVPair}{$\tuple{k_s,v_s}$}\r
+\State $\tuple{ck_s,\tuple{k_s,v_t}} \gets GetKV(KV,k_s)$\r
 \If{$\tuple{ck_s,\tuple{k_s,v_t}} = \emptyset$}\r
-       \State $KV_s \gets KV_s \cup \{\tuple{ck_p, \tuple{k_s,v_s}}\}$\r
+       \State $KV \gets KV \cup \{\tuple{ck_p, \tuple{k_s,v_s}}\}$\r
        \State $ck_p \gets ck_p + 1$\r
 \Else\r
-       \State $KV_s \gets (KV_s - \{\tuple{ck_s, \tuple{k_s,v_t}}\}) \cup \r
+       \State $KV \gets (KV - \{\tuple{ck_s, \tuple{k_s,v_t}}\}) \cup \r
        \{\tuple{ck_s, \tuple{k_s,v_s}}\}$\r
 \EndIf\r
 \State \Return{$KV_s$}\r
@@ -580,12 +571,7 @@ $\tuple{ck,\tuple{k, v}} \in KV_s \wedge
 \State $s_{last_{max}} \gets MaxLastSeqN(MS_s)$\r
 \State $n_{live} \gets s_{last_{max}} - s_{last_{min}}$\Comment{Number of live slots}\r
 \State $n_{dead} \gets max'_t - n_{live}$\r
-\If{$n_{dead} = 0$}\r
-       \State $need \gets true$\r
-\Else\r
-       \State $need \gets false$\r
-\EndIf\r
-\State \Return{$need$}\r
+\State \Return {$n_{dead} = 0$}\r
 \EndFunction\r
 \end{algorithmic}\r
 \r
@@ -610,16 +596,23 @@ $\tuple{ck,\tuple{k, v}} \in KV_s \wedge
 \end{algorithmic}\r
 \r
 \begin{algorithmic}[1]\r
-\Function{ReinsertLastSlot}{$need_s,sl_{s_{last}},max'_s$}\r
-\If{$need_s$}\r
-       \State $s_s \gets GetLastS(sl_{s_{last}})$\r
-       \State $sv_s \gets GetSV(sl_{s_{last}})$\r
-       \State $\tuple{stat_s,SL_s} \gets \Call{PutSlot}{s_s,sv_s,max'_s}$\r
-       \State $cr_s \gets \Call{HandleCollision}{\tuple{stat_s,SL_s}}$\r
-\EndIf\r
-\State \Return{$cr_s$}\r
+\Function{ReinsertLastSlot}{$MS_s,SK_s,sl_{s_{last}},max'_s,hmac_{p_s}$}\r
+\State $s_s \gets MaxLastSeqN(MS_s)$\r
+\State $sv_s \gets GetSV(sl_{s_{last}})$\r
+\State $Dat_s \gets Decrypt(SK,sv_s)$\r
+\State $DE_s \gets GetDatEnt(Dat_s)$\r
+\State $hmac_{c_s} \gets Hmac(DE_s,SK_s)$\r
+\State $Dat_s \gets CreateDat(s_s,id_{self},hmac_{p_s},DE_p,hmac_{c_s})$\r
+\State $hmac_{p_s} \gets hmac_{c_s}$\r
+\State $\tuple{stat_s,SL_s} \gets \Call{PutSlot}{s_s,sv_s,max'_s}$   \r
+\State $cr_s \gets \Call{HandleCollision}{\tuple{stat_s,SL_s}}$\r
+\State \Return{$\tuple{cr_s,hmac_{p_p}}$}\r
 \EndFunction\r
 \end{algorithmic}\r
+\note{Shouldn't this function do something pretty sophisticated about seeing what data we actually need to keep from the last slot and not just insert the entire thing?}\r
+\r
+\note{Probably best to just not call this function if $need_s$ is false and not pass in such parameters.  It makes it harder to read.}\r
+\r
 \r
 \begin{algorithmic}[1]\r
 \Function{GetDEPairs}{$KV_s,max'_s,need_s,sl_s$}\r
@@ -674,10 +667,20 @@ $\tuple{ck,\tuple{k, v}} \in KV_s \wedge
 \State $sv_p \gets Encrypt(Dat_p,SK)$\r
 \State $\tuple{stat_p,SL_p} \gets \Call{PutSlot}{s_p,sv_p,max'_p}$\r
 \State $cr_p \gets \Call{HandleCollision}{\tuple{stat_p,SL_p}}$\r
-\State $cr_{p_{last}} \gets \Call{ReinsertLastSlot}{need_p,sl_{last},max'_p}$\r
+\If{$need_p$}\r
+       \State $\tuple{cr_{p_{last}},hmac_{p_p}} \gets \r
+       \Call{ReinsertLastSlot}{MS,SK,sl_{last},max'_p,hmac_{p_p}}$\r
+\EndIf\r
 \EndProcedure\r
 \end{algorithmic}\r
 \r
+\note{Lots of problems with PutDataEntries: (1) What happens if lose network connectivity after adding the key value pair, but before reinserting the last slot?  You probably need to create space first and then insert your data entry...  (2) What if reinsertlastslot kicks something else important out?  What if the server rejects our update because it is out of date?  At the very least, any putdataentries function w/o a loop is wrong!}\r
+\r
+\note{General comments...  Work on structuring things to improve\r
+  readability...  This include names of functions/variables, how\r
+  things are partitioned into functions, adding useful comments,...}\r
+\r
+\r
 \subsection{Formal Guarantees}\r
 \r
 \textit{To be completed ...}\r