4 ms·

Katara: Synthesizing CRDTs with Verified Lifting

86 points by RossBencina 4y ago

RossBencina 4y ago
From the abstract: "In this paper, we present Katara, a program synthesis-based system that takes sequential data type implementations and automatically synthesizes verified CRDT designs from them. Key to this process is a new formal definition of CRDT correctness that combines a reference sequential type with a lightweight ordering constraint that resolves conflicts between non-commutative operations."
jitl 4y ago
The synthesis is amazing! But, I would like to see an attempt to synthesize a rich text CRDT rather than the relatively trivial set & LRW register stuff.
- mlajtos 4y ago
  Doesn't rich text CRDT require messy rules to comply with our collaborative undo-redo mental model?
  - adigau31 4y ago
    Some people have already solved that, like Liveblocks.io Here's an example of Notion-like text editor with multiplayer: https://liveblocks.io/examples/block-text-editor-advanced/nextjs https://liveblocks.io/examples/block-text-editor-advanced/ne... (and yes, it is very complex lol)
    - mlajtos 4y ago
      Nah, Liveblocks.io + Slate is pretty far from Notion-like experience. It doesn't even do local undo/redo.
      - stevenfabre 4y ago
        Liveblocks does support multiplayer undo/redo. We even wrote an interactive blog post about it: https://liveblocks.io/blog/how-to-build-undo-redo-in-a-multiplayer-environment https://liveblocks.io/blog/how-to-build-undo-redo-in-a-multi... Our open-source block-based text editor could support it too with some extra pluming (which we haven’t got to yet). We’re planning to add this in as more and more developers are looking to port this experience into their own products. Is there anything else you’d like this example to support? Thanks for the feedback! :)
        mlajtos 4y ago
        Really nice article. I think the undo/redo for rich text is a tad bit more complicated than undo/redo for objects with properties. For starters, in your demo when user A has selected some word and user B writes a letter in it, user A lost the selection. And this isn't even undo/redo yet, just normal collaborative thing. That "some extra plumbing" you mention is quite big. Please don't get me wrong here – I would love to see you pull it off – Liveblocks.io seems like a good platform from what I read & heard, but you underestimate how hard that problem might be.
        jitl 4y ago
        Notion’s selection and undo/redo with multiplayer are pretty potato. Notion stores selection as grapheme indexes in a text property, so while it won’t lose selection if someone adds/removed characters from a text, your selection won’t make as much sense as one in Google Docs. Likewise with undo/redo or regular typing into the same field - it’s all last-write-wins updates. On the other hand, Notion’s editor does a much better job with CJK input, Android, etc compared to Slate. Slate has a beautiful API design but its implementation suffers outside of ideal conditions. Source: I built this: https://twitter.com/jitl/status/1483918085384028163?s=46&t=SvntQAbT_miucuAq6v9qnA https://twitter.com/jitl/status/1483918085384028163?s=46&t=S...
        stevenfabre 4y ago
        Awesome to hear from the Notion team who really gets this deeply. Slate definitely has its own limitations, especially when used on non desktop devices. Seems like ProseMirror would be a good open source alternative to Slate, what do you think?
peteforde 4y ago
This sounds interesting but makes my eyes glaze, even as someone actively working with CRDTs as an end-user developer. And that's okay! But can someone translate this to mortal? My weak attempt to parse this leaves me with the impression that the goals are conceptually similar to the Elm language compiler, where if you can stay in your lane (so to speak), you are given assurances about immutability and the theoretical impossibility of run-time errors. If I'm way off, well... now you know why I'm asking for an assist. Who is this for, and what do they do with it? Is it a cool proof or something with practical implications?
- jitl 4y ago
  It seems like it could be very practical. The gist is, you give the synthesizer a C++ implementation of a regular plain-old data structure along with a few annotations, and the synthesizer will synthesize a CRDT implementation of that data structure automatically that is provably-correct. The input needs to be in C++ using only a few types like int, set, etc, because the synthesizer's analysis is implemented against LLVM IR. The driving example is taking a trivial implementation of a set, and getting back different CRDT implementation of sets depending on the annotations that guide the synthesis. So, who is this for? A productionized version could be used by feature programmers who want to build new collaborative features. They can "just" write the feature for a single machine, and have the synthesis make it collaborative.
  - alexvoda 4y ago
    Since it takes LLVM IR as input, why can it not take a subset of Rust or other LLVM supported language?
    - shadaj 4y ago
      Katara author here, you're right! Katara is built on Metalift (https://github.com/metalift/metalift https://github.com/metalift/metalift), which is a general purpose framework we've been building at Berkeley to abstract away the logic of analyzing the LLVM IR. The decision to use LLVM was exactly because it is the least-common-denominator for so so many languages, so we are excited to add official support for Rust and friends in the near future!
transfire 4y ago
Hmm… Could you turn the Heap itself into a CRDT?
- toomim 4y ago
  I think so. Some of us in the braid.org group have been discussing how to add OS syscalls to do so.
gtzi 4y ago
For what's worth, Katara means 'curse' in Greek ;)
erichocean 4y ago
Github here: https://github.com/hydro-project/katara https://github.com/hydro-project/katara
iddan 4y ago
Love the Avatar the Last Airbender reference

86 points by RossBencina 4y ago

From the abstract: "In this paper, we present Katara, a program synthesis-based system that takes sequential data type implementations and automatically synthesizes verified CRDT designs from them. Key to this process is a new formal definition of CRDT correctness that combines a reference sequential type with a lightweight ordering constraint that resolves conflicts between non-commutative operations."

jitl 4y ago

The synthesis is amazing! But, I would like to see an attempt to synthesize a rich text CRDT rather than the relatively trivial set & LRW register stuff.

mlajtos 4y ago
Doesn't rich text CRDT require messy rules to comply with our collaborative undo-redo mental model?
- adigau31 4y ago
  Some people have already solved that, like Liveblocks.io Here's an example of Notion-like text editor with multiplayer: https://liveblocks.io/examples/block-text-editor-advanced/nextjs https://liveblocks.io/examples/block-text-editor-advanced/ne... (and yes, it is very complex lol)
  - mlajtos 4y ago
    Nah, Liveblocks.io + Slate is pretty far from Notion-like experience. It doesn't even do local undo/redo.
    - stevenfabre 4y ago
      Liveblocks does support multiplayer undo/redo. We even wrote an interactive blog post about it: https://liveblocks.io/blog/how-to-build-undo-redo-in-a-multiplayer-environment https://liveblocks.io/blog/how-to-build-undo-redo-in-a-multi... Our open-source block-based text editor could support it too with some extra pluming (which we haven’t got to yet). We’re planning to add this in as more and more developers are looking to port this experience into their own products. Is there anything else you’d like this example to support? Thanks for the feedback! :)
      - mlajtos 4y ago
        Really nice article. I think the undo/redo for rich text is a tad bit more complicated than undo/redo for objects with properties. For starters, in your demo when user A has selected some word and user B writes a letter in it, user A lost the selection. And this isn't even undo/redo yet, just normal collaborative thing. That "some extra plumbing" you mention is quite big. Please don't get me wrong here – I would love to see you pull it off – Liveblocks.io seems like a good platform from what I read & heard, but you underestimate how hard that problem might be.
        jitl 4y ago
        Notion’s selection and undo/redo with multiplayer are pretty potato. Notion stores selection as grapheme indexes in a text property, so while it won’t lose selection if someone adds/removed characters from a text, your selection won’t make as much sense as one in Google Docs. Likewise with undo/redo or regular typing into the same field - it’s all last-write-wins updates. On the other hand, Notion’s editor does a much better job with CJK input, Android, etc compared to Slate. Slate has a beautiful API design but its implementation suffers outside of ideal conditions. Source: I built this: https://twitter.com/jitl/status/1483918085384028163?s=46&t=SvntQAbT_miucuAq6v9qnA https://twitter.com/jitl/status/1483918085384028163?s=46&t=S...
        stevenfabre 4y ago
        Awesome to hear from the Notion team who really gets this deeply. Slate definitely has its own limitations, especially when used on non desktop devices. Seems like ProseMirror would be a good open source alternative to Slate, what do you think?

peteforde 4y ago

This sounds interesting but makes my eyes glaze, even as someone actively working with CRDTs as an end-user developer. And that's okay! But can someone translate this to mortal? My weak attempt to parse this leaves me with the impression that the goals are conceptually similar to the Elm language compiler, where if you can stay in your lane (so to speak), you are given assurances about immutability and the theoretical impossibility of run-time errors. If I'm way off, well... now you know why I'm asking for an assist. Who is this for, and what do they do with it? Is it a cool proof or something with practical implications?

jitl 4y ago
It seems like it could be very practical. The gist is, you give the synthesizer a C++ implementation of a regular plain-old data structure along with a few annotations, and the synthesizer will synthesize a CRDT implementation of that data structure automatically that is provably-correct. The input needs to be in C++ using only a few types like int, set, etc, because the synthesizer's analysis is implemented against LLVM IR. The driving example is taking a trivial implementation of a set, and getting back different CRDT implementation of sets depending on the annotations that guide the synthesis. So, who is this for? A productionized version could be used by feature programmers who want to build new collaborative features. They can "just" write the feature for a single machine, and have the synthesis make it collaborative.
- alexvoda 4y ago
  Since it takes LLVM IR as input, why can it not take a subset of Rust or other LLVM supported language?
  - shadaj 4y ago
    Katara author here, you're right! Katara is built on Metalift (https://github.com/metalift/metalift https://github.com/metalift/metalift), which is a general purpose framework we've been building at Berkeley to abstract away the logic of analyzing the LLVM IR. The decision to use LLVM was exactly because it is the least-common-denominator for so so many languages, so we are excited to add official support for Rust and friends in the near future!

transfire 4y ago

Hmm… Could you turn the Heap itself into a CRDT?

toomim 4y ago
I think so. Some of us in the braid.org group have been discussing how to add OS syscalls to do so.

gtzi 4y ago

For what's worth, Katara means 'curse' in Greek ;)

erichocean 4y ago

Github here: https://github.com/hydro-project/katara https://github.com/hydro-project/katara

iddan 4y ago

Love the Avatar the Last Airbender reference