martinkl · HackerTrans

Replaying immutable events in a deterministic order doesn't fit so well with Automerge; Automerge is more designed for apps where you can represent the mutable state of your application as an Automerge doc. https://livestore.dev/ might be a better fit for you.

martinkl

2 anni fadiscuss

Oh hi Andrew! It's been ages, hope you're well!

martinkl

2 anni fadiscuss

Hi there, good to hear from you! :)

martinkl

2 anni fadiscuss

Thank you! To your point about industrial use, yes – this is interesting. For example, Actyx makes a software system for coordination within a factory floor, and Ditto performs sync between devices of cabin crew on an aircraft. These are nice examples of industrial local-first systems.

martinkl

4 anni fadiscuss

Hi there! Martin here.

I agree that for most engineers, getting into formal proof is intimidatingly hard and perhaps not a good use of time, because lighter-weight specification languages and model-checking can help develop a good understanding of a system's behaviour with a much lower time investment.

But the intended audience for this post was not engineers working on production systems; it was intended for researchers studying distributed algorithms (e.g. consensus algorithms), and researchers who already know proof assistants and want to know how to use their skills to verify distributed algorithms. Note that this post appeared on a blog called "Machine Logic", not "Practical Distributed Systems Engineering"!

I have personally got a lot of value out of formal verification because the distributed algorithms I work on (CRDTs) are sometimes so subtle that without a proof of correctness, I simply don't believe that they are correct. I have several times developed algorithms that I believed to be correct, only later to find out that I was wrong. Here's a case study of one such example: https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-969.pdf

For people like myself, who are designing such algorithms, I believe that formal proof is worth the effort. But most people are not in this situation.

martinkl

4 anni fadiscuss

Hi, one of the authors here. You're right that in order to ensure that you won't receive timestamps lower than some threshold, you need to know all the nodes in the system, and you need to hear from all of them (if even just one node is unreachable, that will be enough to hold up the process). That's quite a big assumption to make, but unfortunately there doesn't really seem to be a good way around it. Lots of CRDT algorithms have this problem of requiring causal stability for garbage collection.

Using a consensus protocol is possible, and would have the advantage that it only requires communication with a quorum (typically a majority of nodes), rather than all nodes. However, it has the downside that now a node cannot generate timestamps independently any more — generating a timestamp would then also require a round trip to a quorum, making the algorithm a lot more expensive.

martinkl

4 anni fadiscuss

Not quite a MOOC, but if you like video, I published my lecture series here (same as what I teach to Cambridge undergraduates): https://www.youtube.com/playlist?list=PLeKd45zvjcDFUEv_ohr_H...

martinkl

4 anni fadiscuss

Martin here. I cited your paper in the related work section. It's a good start, but it does not cover everything that's required to achieve BFT — in particular, the issue that an operation may be valid in some contexts and invalid in others, and all correct nodes need to agree on whether an operation is valid or not.

If you have more details on the caveats you have discovered, it would be great if you could write them up so that others can learn from your experience!

martinkl

5 anni fadiscuss

Hello, Martin here :) I use the Paper app (https://wetransfer.com/paper) on an iPad, then transfer the images to a computer, do a little post-processing in Gimp and ImageMagick, and then drop the images into PowerPoint. You might be able to present directly from the Paper app, but it's more designed for drawing than for presenting.

comments