Automerge Model Checker (AMC)

The Automerge Model Checker provides a library for model checking the Rust implementation of Automerge directly, making some simplifying assumptions along the way, as well as custom applications.

Status

The amc-automerge crate provides a binary for checking general Automerge checking (exercising the public API a bit).

In the process of implementing this checking I think I've found some potential for checking custom applications/data structures built on-top of Automerge. This might be able to help designers of data types check their merge behaviour too!

Current applications

• Counter
  • cargo run --release --bin amc-counter -- check-iterative
  • nix run .#amc-counter -- check-iterative
• Todos
  • cargo run --release --bin amc-todo -- check-iterative
  • nix run .#amc-todo -- check-iterative
• Concurrent moves in a list
  • cargo run --release --bin amc-moves -- check-iterative
  • nix run .#amc-moves -- check-iterative
• Automerge itself
  • cargo run --release --bin amc-automerge -- check-iterative
  • nix run .#amc-automerge -- check-iterative

Design

The Automerge model checker is built on Stateright for doing the actual model checking. AMC provides convenience wrappers for working with automerge documents as well as a more structured way of building the model to be checked. This comes down to two main parts: the Application and the Driver.

The application is responsible for implementing the logic of mutating the automerge document. It takes inputs (think function arguments), executes operations on the document (atomically), and then produces outputs (function return values).

The driver creates the inputs for the application to work with, and can get responses in order to send more inputs too. Each driver instance should implement a single type of workflow that can be performed. This gives each application multiple drivers.

When building the model using the ModelBuilder, AMC will combine applications with logic to handle syncing with a certain method. Drivers get combined with a lightweight wrapper to handle communication with the application. It is at this point developers can specify properties that they want to be evaluated in the model. For instance, a counter should have the value of the sum of increments and decrements (shown in properties of CounterOpts). AMC provides some common properties and helpers in the properties module.

Benchmarking

Benchmarking is performed by the bench.py script, or the bench nix target. Run them with cargo build --release && python bench.py or nix run .#bench respectively (the latter automatically builds the binaries).