Synthesize CRDTs that mirror your existing data types!

Katara is a program synthesis engine that can automatically generate CRDT designs that mirror the behavior of a sequential data type annotated with a conflict resolution policy for non-commutative operations. See our paper for more information!

Setup

Install (with Nix)

To get a development environment up and running, one option is to use Nix, which can automatically pull and build the necessary dependencies. First, you'll need to install Nix. Note that this will require temporary root access as Nix sets up a daemon to handle builds, and will set up a separate volume for storing build artifacts if on macOS.

Once you've got Nix installed, you'll need to enable flakes.

Then, all you have to do is navigate to the Metalift directory and run the following command:

$ nix develop

This will build all of Metalift's dependencies and drop you into a temporary shell with all the dependencies available.

Note: you still will need to install Racket and Rosette separately. There is a solution for doing this through Nix, but it requires nix-ld to be installed and is generally not recommended unless you run NixOS.

Install (without Nix)

You'll need the following dependencies installed to use Katara:

• Python 3.8 with Poetry
• Rosette
• CVC5
• LLVM 11

We use Poetry for dependency management. To set up the environment, simply install Poetry, run poetry install, and then poetry shell to enter an environment with the dependencies installed.

Build the LLVM Pass

We currently support LLVM 11

Run the following to build the LLVM pass for processing branch instructions (works for LLVM 11):

cd llvm-pass
mkdir build
cd build
cmake ..
make 
cd ../..

This pass is called in tests/compile-add-blocks.

Synthesizing CRDTs

The first step to synthesizing a CRDT is to compile the sequential reference. We have provided a set of benchmark sequential data types in the tests/ folder. These can be compiled by entering the folder and running compile-all:

cd tests
./compile-all
cd ..

Then, from the base directory of the project, we can run the synthesis benchmarks defined in tests/synthesize_crdt.py (in the benchmarks variable). Each benchmark is configured with the sequential data type to process, the ordering constraing as defined in our paper (opOrder), flags to enable synthesis of non-idempotent operations, and type hints to optimize the synthesis process. With a benchmark configured, we can run it as

python -m tests.synthesize_crdt synth <BENCHMARK NAME>

For example, we can synthesize for the 2P-Set benchmark with

python -m tests.synthesize_crdt synth 2p_set

In general, you can use the following command structure:

python -m tests.synthesize_crdt <mode> <benchmark> [--fixed] [--first <N>] [--repeat <N>]

Where:

• <mode> is either synth for bounded synthesis with pruning or synth-unbounded for direct unbounded synthesis.
• <benchmark> is the name of the benchmark or all to run all benchmarks.
• --fixed (optional) uses a fixed lattice structure instead of exploring all structures.
• --first <N> (optional) synthesizes the first N structures.
• --repeat <N> (optional) specifies the number of repetitions for the synthesis process.