Modeling CRDTs in Alloy – the importance of idempotence
1–9 of 9 posts
Re: Modeling CRDTs in Alloy – the importance of idempotence
#2Nice article! The statement of idempotence is a little nonstandard, I think -- I'm used to it being stated as `merge(a, a) = a`. The form in the article makes more sense if you have set of operations acting on a state, so that `apply(apply(st, a), a) = apply(st, a)` -- but this follows from the more usual merge law above, since `apply(apply(st, a), a) = apply(st, merge(a, a)` by the laws of monoid actions, then `apply(st, merge(a, a)) = apply(st, a)` by (standard) idempotence.
Re: Modeling CRDTs in Alloy – the importance of idempotence
#3Nice article! The statement of idempotence is a little nonstandard, I think -- I'm used to it being stated as `merge(a, a) = a`. The form in the article makes more sense if you have set of operations acting on a state, so that `apply(apply(st, a), a) = apply(st, a)` -- but this follows from the more usual merge law above, since `apply(apply(st, a), a) = apply(st, merge(a, a)` by the laws of monoid actions, then `appl…
They're talking about idempotence of `merge(a, _ )` (under function composition), whereas you're talking about idempotence of `a` (with composition given by `merge`). Same property, different object.
Re: Modeling CRDTs in Alloy – the importance of idempotence
#4For those like me who didn't know what Alloy is, it looks like it's a general purpose constraint solver for testing correctness in range of different algorithms.
Re: Modeling CRDTs in Alloy – the importance of idempotence
#5Nice article! The statement of idempotence is a little nonstandard, I think -- I'm used to it being stated as `merge(a, a) = a`. The form in the article makes more sense if you have set of operations acting on a state, so that `apply(apply(st, a), a) = apply(st, a)` -- but this follows from the more usual merge law above, since `apply(apply(st, a), a) = apply(st, merge(a, a)` by the laws of monoid actions, then `appl…
They're talking about idempotence of `merge(a, _ )` (under function composition), whereas you're talking about idempotence of `a` (with composition given by `merge`). Same property, different object.
Right, but then for commutativity I would expect them to use `merge(merge(a, b), c) = merge(merge(a, c), b)`, whereas what they actually have is the usual `merge(a, b) = merge(b, a)`. They're sort of mixing and matching from the axioms of monoids[^] and the axioms of actions (what you're referring to as "function composition").
[^] (well, properly, semilattices, because that's what state-based CRDTs are based on. But semilattices are "just" commutative idempontent monoids ^_^)
Re: Modeling CRDTs in Alloy – the importance of idempotence
#6> ... engineers who worked on Google Wave (which also used OT) also struggled with this… I remember reading a quote a while back that said something along the lines of "I wish I could have those years of my life back, and I wouldn't recommend anyone else try syncing this way."
I think you're (mis)quoting me. I made a comment like that on the webpage for ShareJS back in 2011 which eventually made it into the wikipedia article on operational transform.
If I remember correctly, what I actually said was that it took us about 2 years to implement the OT algorithms we used for Google Wave. And if we rewrote it again today from scratch, it would take just as long a second time because there's no standard, reusable libraries that implement collaborative editing in a pluggable way that any application can use. The collaborative editing engine that powered Google Wave was bespoke, and if we rewrote it today we'd need to write another bespoke collaborative editing engine from scratch.
Thats why I wrote ShareJS, and later ShareDB and more recently why I've been working with CRDTs. I love generic collaborative editing libraries is because of the hope that they'll bridge this gap, and make generic tools that can work in any application. I was right on the money with Figma - as I understand it, it took them about 2 years to build the collaborative editing code that sits underneath their application, because there still aren't enough truly great libraries to use for building software like this.
Re: Modeling CRDTs in Alloy – the importance of idempotence
#7> ... engineers who worked on Google Wave (which also used OT) also struggled with this… I remember reading a quote a while back that said something along the lines of "I wish I could have those years of my life back, and I wouldn't recommend anyone else try syncing this way." I think you're (mis)quoting me. I made a comment like that on the webpage for ShareJS back in 2011 which eventually made it into the wikipedia…
Thanks for the pointer. I looked for that quote for a while and couldn't find it. Go figure that it would be on a page I literally linked from the post.
Now that I have it, I'm going to edit the post to make it less misremembered.
Re: Modeling CRDTs in Alloy – the importance of idempotence
#8There is a talk that gives a good overview on Alloy and how useful using something like this is:
"Finding bugs without running or even looking at code" by Jay Parlar https://www.youtube.com/watch?v=FvNRlE4E9QQ
Re: Modeling CRDTs in Alloy – the importance of idempotence
#9For those like me who didn't know what Alloy is, it looks like it's a general purpose constraint solver for testing correctness in range of different algorithms. https://alloytools.org/
It is a modeling language based on relations and constraints. It is very friendly and feels like writing SQL schemas or classes. Given a model and its constraints Alloy can use a SAT solver to find valid instances. This is used to check model properties.
It can be used to model not only algorithms but principally concepts.
I always use Alloy before starting a new design.