Stateful Property Testing a CRDT with jetCheck

Background

Property-based testing is a powerful technique for making general claims about the behavior of a system and verifying that those claims hold true. This relies on combinatorics to drive the tests themselves, generating randomized, valid inputs to the system and asserting against the resulting state. The technique was arguably popularized by the Haskell QuickCheck library.

A presentation by Benjamin C. Pierce titled "Principles of Synchronization" (see the CERN CDS record for the video) and the corresponding paper titled "Mysteries of Dropbox" (located at the University of Pennsylvania site) can offer an idea of how effective the technique can be to discovering problematic behavior in a real-world system. 

JetBrains developed a property-based testing Java library named jetCheck (the repository can be found on GitHub) as part of the IntelliJ IDE project. Crucially, it supports verifying stateful systems by inputing a set of custom commands that interact with the system. A random sequence of those commands is executed against the system with assertions that certain properties hold true. If the custom commands are deterministic, jetCheck can shrink the total sequence of commands down to a minimal subsequence that reproduces a verification failure.

Example

To help demonstrate the jetCheck library by example, the system under test is an arbitrary state-based Add-Wins set CRDT (Conflict-free Replicated Data Type) implementation. Details such as the mechanism for establishing causality are abstracted away for simplicity. Its interface is in Listing 1.

/**
 * An interface for an Add-Wins CRDT datatype in which removes only affect causally preceding adds.
 */
public interface AWSet<T> {

    /**
     * Returns a unique string identifier for this AWOR set, used for distinguishing it from other sets and aid in debugging.
     */
    String getId();

    /**
     * Adds a value to the set, if it is not already present in the set.
     *
     * @param value The value to add to the set.
     * @return A set with this value added.
     */
    AWSet<T> add(T value);

    /**
     * Removes the value from the set, if the value is already present in the set.
     *
     * @param value The value to remove.
     * @return A set with this value removed.
     */
    AWSet<T> remove(T value);

    /**
     * Merges this set with the other, with a bias for add operations.
     * If an element was removed from one of the sets and later re-added to that same set,
     * while concurrently the element was removed from the other set,
     * then in the merged set the element is present.
     *
     * @param other The set to be merged with this one.
     */
    void merge(AWSet<T> other);

    /**
     * Determines if the set contains the given value.
     *
     * @param value The value whose presence is to be determined.
     * @return True if the value is an element of the set. False, otherwise.
     */
    boolean contains(T value);

    /**
     * Returns the elements of the set, with any causality metadata removed.
     *
     * @return The elements of the set.
     */
    Set<T> values();

    /**
     * Determines whether the sets are equivalent, taking into account both the set elements and causality-tracking metadata, e.g., dots.
     *
     * @return True, if the values of the causality metadata and values of the set are equal.
     */
    boolean causallyEqual(AWSet<T> other);
}

Listing 1 - Interface of the Add-Wins set.

The property-based test is written in Groovy (with Spock) and is contained in Listing 2. If an exception is thrown, jetCheck assumes that a property was violated and verification fails. Since in Groovy assertions are always executed and throw an exception on failure, the test makes use of the “assert” keyword.

Should a test iteration fail, a descriptive error message is printed and describes shrunk (if possible) steps that lead to the failure and outputs a seed number to re-run the same sequence if required for debugging:

To re-run the minimal failing case, run
  PropertyChecker.customized().rechecking("8Y7Ysx7R7LamCAEBDw==")
    .checkScenarios(...)
To re-run the test with all intermediate shrinking steps, use `recheckingIteration(-920137639009002735L, 1)` instead for last iteration, or `withSeed(-920137639009002735L)` for all iterations

The test itself declares four commands: Add, Remove, Merge and Add-Wins. first three commands are self-explanatory and correspond directly to the set operations defined by the interface. On the other hand, the Add-Wins command exercises a specific property of the set: that on merge, where there is a concurrent add and remove of an element, the add prevails, keeping the element in the set.

import org.jetbrains.annotations.NotNull
import org.jetbrains.jetCheck.Generator
import org.jetbrains.jetCheck.ImperativeCommand
import org.jetbrains.jetCheck.PropertyChecker
import spock.lang.Specification

import java.util.concurrent.ThreadLocalRandom
import java.util.function.Supplier

import static org.jetbrains.jetCheck.Generator.asciiIdentifiers
import static org.jetbrains.jetCheck.Generator.sampledFrom
import static org.jetbrains.jetCheck.ImperativeCommand.Environment

class AWORSetPropertyTest extends Specification {

    def "AW set property test"() {
        given:
        def replicas = 10
        def sets = (1..replicas).collect {
            new AWSetImpl<String>("n${it}")
        }

        and:
        def commands = sets.collect { set -> [new Add(set), new Remove(set)] }.flatten()
        commands.addAll([new Merge(sets), new AddWins(sets)])
        Generator generator = sampledFrom(commands)

        Supplier<ImperativeCommand> commandSupplier = new Supplier<ImperativeCommand>() {
            @Override
            ImperativeCommand get() {
                new ImperativeCommand() {
                    @Override
                    void performCommand(@NotNull Environment env) {
                        env.executeCommands(generator)
                        new Merge(sets).performCommand(env)
                    }
                }
            }
        }

        when:
        PropertyChecker.customized().checkScenarios(commandSupplier)

        Set<String> remainingObservedValues = sets.collect { it.values() }.flatten() as Set<String>

        then:
        sets.every {
            it.values() == remainingObservedValues
        }
    }

    abstract class SetCommand implements ImperativeCommand {

        protected String add(Environment env, AWSet<String>... set) {
            String value = env.generateValue(asciiIdentifiers(), null)
            set.each {
                env.logMessage("Adding value ${value} to set ${it.id}")
                it.add(value)
            }
            value
        }

        protected void remove(Environment env, AWSet<String> set, String value = null) {
            List<String> existingValues = set.values()
            if (value != null && existingValues.empty) {
                throw new IllegalArgumentException("Cannot remove pre-determined value ${value} from an empty set.")
            } else if (!existingValues.empty) {
                if (value == null) {
                    value = existingValues.get(ThreadLocalRandom.current().nextInt(existingValues.size()))
                }

                env.logMessage("Removing value ${value} from set ${set.id}")

                if (!existingValues.contains(value)) {
                    throw new IllegalArgumentException("Cannot remove value ${value} as it is not contained by the set.")
                }

                set.remove(value)
                value
            }
            null
        }
    }

    class Add extends SetCommand {

        final AWSet<String> set

        Add(AWSet<String> set) {
            this.set = set
        }

        @Override
        void performCommand(@NotNull Environment env) {
            def addedValue = add(env, set)
            assert set.contains(addedValue)
        }
    }

    class Remove extends SetCommand {

        final AWSet<String> set

        Remove(AWSet<String> set) {
            this.set = set
        }

        @Override
        void performCommand(@NotNull Environment env) {
            def removedValue = remove(env, set)
            if (removedValue != null) {
                assert !set.contains(removedValue)
            }
        }
    }

    class Merge extends SetCommand {

        final Set<List<AWSet<String>>> pairs

        Merge(List<AWSet<String>> sets) {
            this.pairs = sets.subsequences().findAll { it.size() == 2 }
        }

        @Override
        void performCommand(@NotNull Environment env) {
            pairs.each { pair ->
                pair.tap {
                    env.logMessage("Merging sets ${first().id} and ${last().id}")
                    def preMergeFirstSetValues = first().values()
                    def preMergeSecondSetValues = last().values()
                    first().merge(last())
                    last().merge(first())
                    assert first().values().containsAll(preMergeFirstSetValues)
                    assert last().values().containsAll(preMergeSecondSetValues)
                    assert first().causallyEqual(last())
                }
            }
        }
    }

    class AddWins extends SetCommand {

        final Set<List<AWSet<String>>> pairs

        AddWins(List<AWSet<String>> sets) {
            this.pairs = sets.subsequences().findAll { it.size() == 2 }
        }

        @Override
        void performCommand(@NotNull Environment env) {
            pairs.asList().shuffled().first().tap {
                def addedValue = add(env, first(), last())
                remove(env, first(), addedValue)
                new Merge([first(), last()]).performCommand(env)
            }
        }
    }
}

Listing 2 - Property-based test that harnesses the jetCheck library.

Tuning

It is possible to customize parameters of the test by invoking the PropertyChecker#customized method, for example:

PropertyChecker.customized()
            .withIterationCount(500)
            .printGeneratedValues()
            .checkScenarios(commandSupplier)

Here the iteration count is bumped to 500 from the default value of 100 and print all values generated for testing.