Re:Katara: Synthesizing CRDTs with Verified Lifting
by alexvoda on Monday September 26, 2022 @05:14AM
(#32980975)
Since it takes LLVM IR as input, why can it not take a subset of Rust or other LLVM supported language?
Re:Katara: Synthesizing CRDTs with Verified Lifting
by shadaj on Friday October 07, 2022 @07:04PM
(#33128031)
Katara author here, you're right! Katara is built on 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!
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.