3 ms·
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 ann
by 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 agoSince it takes LLVM IR as input, why can it not take a subset of Rust or other LLVM supported language?
- shadaj 4y agoKatara 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!