Modeling CRDTs in Alloy – the importance of idempotence(bytes.zone)
bytes.zone
Modeling CRDTs in Alloy – the importance of idempotence
https://bytes.zone/posts/modeling-crdts-in-alloy-introduction-and-the-importance-of-idempotence/
8 comments
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.
Now that I have it, I'm going to edit the post to make it less misremembered.
For 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/
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.
It can be used to model not only algorithms but principally concepts.
I always use Alloy before starting a new design.
Nice 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.
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 ^_^)
[^] (well, properly, semilattices, because that's what state-based CRDTs are based on. But semilattices are "just" commutative idempontent monoids ^_^)
There 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
"Finding bugs without running or even looking at code" by Jay Parlar https://www.youtube.com/watch?v=FvNRlE4E9QQ
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.