Add a write up of the state delta resolution algorithm by erikjohnston · Pull Request #3122 · matrix-org/synapse

erikjohnston · 2018-04-19T13:29:56Z

No description provided.

krombel · 2018-04-19T16:19:18Z

docs/state_delta_resolution.tex

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


\WHILE{$pending$ is not empty}

richvdh · 2018-04-20T11:11:13Z

rendered version at https://matrix.org/_matrix/media/v1/download/jki.re/hSmkLkFGVUnrXjtYcjsCUsyS

richvdh · 2018-04-20T11:20:48Z

docs/state_delta_resolution.tex

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


better described as "unconflicted state keys" maybe?

richvdh · 2018-04-20T11:22:12Z

docs/state_delta_resolution.tex

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


richvdh · 2018-04-20T11:24:52Z

docs/state_delta_resolution.tex

+\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}$:


parens around f \cup G ?

richvdh · 2018-04-20T11:27:13Z

docs/state_delta_resolution.tex

+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)$. 


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

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

richvdh · 2018-04-20T11:41:11Z

docs/state_delta_resolution.tex

+\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)$


this could do with clarifying. ITYM:

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

richvdh · 2018-04-20T11:45:17Z

docs/state_delta_resolution.tex

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


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

richvdh · 2018-04-20T11:54:06Z

docs/state_delta_resolution.tex

+\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)


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

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

yup makes sense. more parens ftw.

richvdh · 2018-04-20T11:55:46Z

docs/state_delta_resolution.tex

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


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

richvdh · 2018-04-20T12:55:13Z

docs/state_delta_resolution.tex

+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$.


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

richvdh · 2018-04-20T12:56:29Z

docs/state_delta_resolution.tex

+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.


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.

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))

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

Or redefine it in terms of independence.

richvdh · 2018-04-20T12:56:55Z

docs/state_delta_resolution.tex

+\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:


why is x in a ?

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

richvdh · 2018-04-20T12:59:47Z

docs/state_delta_resolution.tex

+	$c_{f,g}(x)$ depends on $x \in a_{f,g}(x)$, and $r_{f,g}(\alpha_{f,g}(x))$. Now:
+	\[
+		\begin{split}
+		r_{f,g}(\alpha_{f,g}(x))\ =\ & u_{f,g}(\alpha_{f,g}(x)) \cup c_{f,g}(\alpha_{f,g}(x))\\


u is only defined over the unconflicted part of the state key space. I think it's clear what you mean, but it might be good to be more precise here.

richvdh · 2018-04-20T13:02:13Z

docs/state_delta_resolution.tex

+		\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)$.


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 · 2018-04-20T13:03:11Z

docs/state_delta_resolution.tex

+		\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)$.


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

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

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

richvdh · 2018-04-20T13:04:49Z

docs/state_delta_resolution.tex

+		\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)$.


depends on α ?

Yes, if you mean the first "depends on". Though as above its correct to say it depends on a too.

erikjohnston · 2018-04-26T16:29:54Z

Rendered

ara4n · 2019-03-03T20:03:04Z

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)

florianjacob · 2020-04-15T07:06:23Z

For reference why this was closed:

Matthew: “this was written for state resolution v1, and needs to be done for v2”

Add a write up of the state delta resolution algorithm

f7529af

erikjohnston assigned richvdh Apr 19, 2018

krombel reviewed Apr 19, 2018

View reviewed changes

richvdh reviewed Apr 20, 2018

View reviewed changes

richvdh assigned erikjohnston and unassigned richvdh Apr 23, 2018

Clean up and expand on some points

13c5b6e

erikjohnston assigned richvdh and unassigned erikjohnston Apr 26, 2018

richvdh removed their assignment Aug 16, 2018

ara4n mentioned this pull request Jun 3, 2019

Proposal: mitigate extremities accumulation using lazy-transmitted dummy events #5319

Closed

erikjohnston closed this Sep 5, 2019

		\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}$:

Uh oh!

Conversation

erikjohnston commented Apr 19, 2018

Uh oh!

Choose a reason for hiding this comment

Uh oh!

richvdh commented Apr 20, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

erikjohnston commented Apr 26, 2018

Uh oh!

ara4n commented Mar 3, 2019

Uh oh!

florianjacob commented Apr 15, 2020

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

richvdh commented Apr 20, 2018 •

edited

Loading