Add a write up of the state delta resolution algorithm #3122

Open
wants to merge 2 commits into
from
+276 −0

Conversation

Projects
None yet
Member

erikjohnston commented Apr 19, 2018

 No description provided.
 Add a write up of the state delta resolution algorithm 
 f7529af 

krombel reviewed Apr 19, 2018

 \begin{algorithmic} \STATE $to\_recalculate \leftarrow \text{empty set of state keys}$ \STATE $pending \leftarrow G_\delta$ \WHILE{$pending$ is empty}

krombel Apr 19, 2018

Contributor

\WHILE{$pending$ is not empty}

Member

richvdh reviewed Apr 20, 2018

 \end{split} \end{equation} which we call state maps, for $F, G \subset K$. We can then compute the set of all unconflicted events":

richvdh Apr 20, 2018

Member

better described as "unconflicted state keys" maybe?

 \begin{split} u_{f,g} : U_{f,g} \longrightarrow &\ E\\ x \longmapsto &\ \begin{cases} f(x), & \text{if}\ f \in F \\

richvdh Apr 20, 2018

Member

x \in F

 \end{equation} which gets the unconflicted event for a given state key. We can also define a function on $C_{f,g} = F \cup G \setminus U_{f,g}$:

richvdh Apr 20, 2018

Member

parens around f \cup G ?

erikjohnston Apr 20, 2018

Author Member

yup

 We can also define a function on $C_{f,g} = F \cup G \setminus U_{f,g}$: \begin{equation} c_{f,g}: C_{f,g} \rightarrow E \end{equation} which is used to resolve conflicts between $f$ and $g$. Note that $c_{f,g}$ is either $f(x)$ or $g(x)$.

richvdh Apr 20, 2018

Member

ITYM $c_{f,g}(x)$ is either ...

I don't think it's true that c_{f,g} is either f or g

erikjohnston Apr 20, 2018

Author Member

yup

 \end{equation} which we call the resolved state of $f$ and $g$. \begin{lemma} $\forall x \in U_{f,g} \ s.t.\ g(x) = g'(x)$ then $r_{f,g}(x) = r_{f,g'}(x)$

richvdh Apr 20, 2018

Member

this could do with clarifying. ITYM:

if $\forall x (g(x) = g'(x)), x \in U_{f_g}$, then ...

richvdh reviewed Apr 20, 2018

 \end{split} \end{equation} which we call the resolved state of $f$ and $g$. \begin{lemma}

richvdh Apr 20, 2018

Member

it looks like you're about to prove this, which is confusing. Suggest just stating it rather than making it a Lemma.

richvdh reviewed Apr 20, 2018

 \alpha: E \rightarrow \mathbb{P}(K) \end{equation} to be the mapping of an event to the type/state keys needed to auth the event, and \begin{equation} \alpha_{f,g}(x) = \alpha f(x) \cup \alpha g(x)

richvdh Apr 20, 2018

Member

what's going on here? what does \alpha f(x) mean?

erikjohnston Apr 20, 2018

Author Member

\alpha f(x) = \alpha(f(x)), i.e. for the event in the state f, \alpha f(x) are its auth state keys

richvdh Apr 20, 2018

Member

yup makes sense. more parens ftw.

 Further, we can define \begin{equation} a_{f,g}(x) = \bigcup_{n=0}^\infty (\alpha_{f,g})^n(x)

richvdh Apr 20, 2018

Member

can't you use something other than a? (or something other than \alpha?) They look pretty similar.

richvdh reviewed Apr 20, 2018

 Further, we can define \begin{equation} a_{f,g}(x) = \bigcup_{n=0}^\infty (\alpha_{f,g})^n(x) \end{equation} to be the auth chain of $f(x)$ and $g(x)$. This is well defined as there are a finite number of elements in $F \cup G$ and $a_{f,g} \rightarrow F \cup G$.

richvdh Apr 20, 2018

Member

I think more to the point, α → F ∩ G

richvdh reviewed Apr 20, 2018

 a_{f,g}(x) = \bigcup_{n=0}^\infty (\alpha_{f,g})^n(x) \end{equation} to be the auth chain of $f(x)$ and $g(x)$. This is well defined as there are a finite number of elements in $F \cup G$ and $a_{f,g} \rightarrow F \cup G$. If we consider the implementation of $c_{f,g}$ in Synapse we can see that it depends not only on the values of $x$, but also on the resolved state of their auth events, i.e. $r_{f,g}(\alpha_{f,g}(x))$. By depends on" we mean that if those are the same for different values of $f$ and $g$, then the result of $c_{f,g}(x)$ is the same.

richvdh Apr 20, 2018

Member

I'm failing to grok the By depends on sentence. "those are the same": which are the same?

the term "depends on" is used heavily in the later proofs, so I think this needs defining more precisely.

erikjohnston Apr 20, 2018

Author Member

By depends on I mean, say: c_f(x) depends on r_f(x), then forall g where r_f(x) = r_g(x) then c_g(x) = c_f(x).

Its basically saying that c could be written as a pure function from f(x), g(x) and r_{f,g}(\alpha_{f,g}(x))

richvdh Apr 20, 2018

Member

(i'd be tempted to abuse a proportionality symbol \propto to represent the 'depends on' relationship.

Or redefine it in terms of independence.

richvdh reviewed Apr 20, 2018

 \end{lemma} \begin{proof} $c_{f,g}(x)$ depends on $x \in a_{f,g}(x)$, and $r_{f,g}(\alpha_{f,g}(x))$. Now:

Member

why is x in a ?

erikjohnston Apr 20, 2018

Author Member

a_{f,g}(x) = x \cup \alpha_{f,g}(x) \cup (\alpha_{f,g})^2(x) \cup ...

richvdh reviewed Apr 20, 2018

richvdh Apr 20, 2018

Member

could you be consistent about c_{f,g}\alpha_{f,g}(x) vs c_{f,g}(\alpha_{f,g}(x)) ? (with my preference heavily on the former). It's particularly weird to see r with extra parens in the same sentence as c without.

richvdh reviewed Apr 20, 2018

 \begin{split} r_{f,g}(\alpha_{f,g}(x))\ =\ & u_{f,g}(\alpha_{f,g}(x)) \cup c_{f,g}(\alpha_{f,g}(x))\\ \end{split} \] but by definition $u_{f,g}(\alpha_{f,g}(x))$ depends only on $\alpha_{f,g}(x)$, so $r_{f,g}(\alpha_{f,g}(x))$ depends on $a_{f,g}(x)$ and $c_{f,g}\alpha_{f,g}(x)$.

richvdh Apr 20, 2018

Member

I think s/depends on a/depends on α/

richvdh Apr 20, 2018

Member

could you split the result of what r(...) depends on to a separate \begin{equation}, since you're about to use it for induction?

erikjohnston Apr 20, 2018

Author Member

Err, yes, (though α is a subset of a, so its correct to say that it depends on a)

richvdh reviewed Apr 20, 2018

 \end{split} \] but by definition $u_{f,g}(\alpha_{f,g}(x))$ depends only on $\alpha_{f,g}(x)$, so $r_{f,g}(\alpha_{f,g}(x))$ depends on $a_{f,g}(x)$ and $c_{f,g}\alpha_{f,g}(x)$. By induction, $c_{f,g}\alpha_{f,g}(x)$ depends on $a_{f,g}(x)$ and $c_{f,g}(\alpha_{f,g})^n(x), \forall n$. Since $(\alpha_{f,g})^n(x)$ repeats and we know $c_{f,g}$ is well defined, we can infer that $c_{f,g}(x)$ depends only on $\bigcup_{n=0}^\infty (\alpha_{f,g})^n(x) = a_{f,g}(x)$.

Member

depends on α ?

erikjohnston Apr 20, 2018

Author Member

Yes, if you mean the first "depends on". Though as above its correct to say it depends on a too. richvdh assigned erikjohnston and unassigned richvdhApr 23, 2018

 Clean up and expand on some points 
 13c5b6e 
Member Author

Member

ara4n commented Mar 3, 2019

 this would help with #1760 (i think?) as faster state res means that the number of extremities which need to be resolved is less of a consideration (especially if their intermediary resolution results have been cached and can be built on)

Open