These are chat archives for RBMHTechnology/eventuate

11th
Oct 2016
Alexander Semenov
@Tvaroh
Oct 11 2016 09:37
@krasserm what's the correct behavior when adding an already existing node to a tree (same node id, same parent, potentially different payload) in your opinion? Exception/ignore silently/update payload?
Martin Krasser
@krasserm
Oct 11 2016 09:55
Concurrent or after?
Alexander Semenov
@Tvaroh
Oct 11 2016 09:55
after
Martin Krasser
@krasserm
Oct 11 2016 09:55
update payload
Anyway, I strongly recommend following the semantics in the paper
Alexander Semenov
@Tvaroh
Oct 11 2016 09:56
this case is not described there
Martin Krasser
@krasserm
Oct 11 2016 09:57
why?
because this scenario is prevented by different means?
In the end I think there's no way around UPIs ...
Alexander Semenov
@Tvaroh
Oct 11 2016 09:58
probably because it's not concurrent and they do not talk about payload anyway, so nothing to update
Alexander Semenov
@Tvaroh
Oct 11 2016 10:04
what if parent does not exist? Exception / Ignore silently / Put under root?
Martin Krasser
@krasserm
Oct 11 2016 10:07
We already discussed that in context of concurrent addition of node and deletion of its parent. It should have the same behavior then.
not covered in the paper? sure?
Alexander Semenov
@Tvaroh
Oct 11 2016 10:08
this one is covered yes
Martin Krasser
@krasserm
Oct 11 2016 10:09
then it's better to follow the resolution strategy in the paper than mine :smiley:
Alexander Semenov
@Tvaroh
Oct 11 2016 10:10
okay :smile:
There are 4 options (skip, put under root, reappear, compact) in the paper. The last two require tombstones so I won't implement them, the choice of first two will be allowed when creating a tree.
Alexander Semenov
@Tvaroh
Oct 11 2016 13:16
Martin, is it valid to replace an element (remove then add updated) in the set CRDT in the downstream phase? I need to update an edge payload and I'm in the update phase already. Something like this (where edges: ORSet[Edge[A, Id]]):
edges.remove(edges.prepareRemove(existingEdge)).add(edge, timestamp)
Martin Krasser
@krasserm
Oct 11 2016 13:21
I don't think so, because this doesn't guarantee that the element to be removed has been observed at source.
Alexander Semenov
@Tvaroh
Oct 11 2016 13:24
I suspected this... Probably I should split "add child node" (currently it's all downstream) operation and perform this in the prepare phase, right?
and pass "prepared" data to the downstream phase, like in remove
Martin Krasser
@krasserm
Oct 11 2016 13:25
What do the specs say?
Alexander Semenov
@Tvaroh
Oct 11 2016 13:26
there are no specs in the paper, it's kind of informal
Martin Krasser
@krasserm
Oct 11 2016 13:26
hmm ...
this should be covered by the pre(...) and post(...) operations in the paper - a formal specification
Alexander Semenov
@Tvaroh
Oct 11 2016 13:31
alas
Martin Krasser
@krasserm
Oct 11 2016 13:38
ok, so you implement a CRDT with operations that aren't specified. How do you prove correctness?
Alexander Semenov
@Tvaroh
Oct 11 2016 13:39
I don't know. Do you propose to give up?
Martin Krasser
@krasserm
Oct 11 2016 13:39
I can't propose that without having read the paper
I'm currently busy with other things the next few days
In any case, I'd only go for an implementation that is fully specified.
Alexander Semenov
@Tvaroh
Oct 11 2016 13:48
then we need to specify it ourselves
Martin Krasser
@krasserm
Oct 11 2016 14:07
does that mean the specs in the paper aren't sufficient to implement a tree CRDT? What is missing or what do I miss?
Alexander Semenov
@Tvaroh
Oct 11 2016 14:07
there are no specs in the paper, it's all "in words"
Martin Krasser
@krasserm
Oct 11 2016 14:09
and what do you think are the pre(...) and post(...) definitions?
Alexander Semenov
@Tvaroh
Oct 11 2016 14:12
I mean specs in this form: http://image.prntscr.com/image/b39f4822907943229f31e96bd77733a0.png Do you call those pre and post conditions "specs"?
Martin Krasser
@krasserm
Oct 11 2016 14:13
Sure, they are a formal definition of the operations on the tree CRDTs
Alexander Semenov
@Tvaroh
Oct 11 2016 14:16
I see
Alexander Semenov
@Tvaroh
Oct 11 2016 14:26

They are rather obvious, how are they supposed to be helpful? For example, having these:

pre(add(n, m), T ) ≡ ∃(z, m) ∈ T
post(add(n, m), T ) ≡ (m, n) ∈ T
pre(rmv(S), T ) ≡ subtree(S, T )
post(rmv(S), T ) ≡ S ∩ T = {}

how do they help to express a duplicate node addition with a different payload (when we want to update the payload of the existing node)? As I understand I need to handle this in prepare and pass the node timestamps to the downstream where it can be re-added to the underlying OR-set.

Martin Krasser
@krasserm
Oct 11 2016 14:30
Ok, so you're saying these specifications aren't sufficient to implement the tree CRDTs?
Alexander Semenov
@Tvaroh
Oct 11 2016 14:33
I'm not sure. In my understanding, full specs should include atSource and downstream operations. Pre/post conditions do not specify this algorithm, or am I wrong?
Martin Krasser
@krasserm
Oct 11 2016 14:44
pre(...) and post(...) correspond to atSource and downstream and your implementation needs to ensure that these conditions are met. Pre-conditions are evaluated atSource, post-conditions must be achieved downstream.
Alexander Semenov
@Tvaroh
Oct 11 2016 14:49
they must be met at the end of atSource/downstream methods correspondingly, right?
Martin Krasser
@krasserm
Oct 11 2016 14:52
pre(...) must be met prior to atSource I guess
Alexander Semenov
@Tvaroh
Oct 11 2016 14:52
thanks, need to digest it all
Martin Krasser
@krasserm
Oct 11 2016 14:52
you're welcome