Crate model

simple model-checking tools for rust.

aims to reduce the boiler plate required to write model-based and linearizability tests.

it can find linearizability violations in implementations without having any knowledge of their inner-workings, by running sequential operations on different commands and then trying to find a sequential ordering that results in the same return values.

important: the crate makes use of proptest via macros. ensure that you are using the same version of proptest that model lists in Cargo.toml, otherwise mismatched API change will manifest as strange compile-time errors hidden in macros.

model-based testing:

#[macro_use]
extern crate model;

use std::sync::atomic::{AtomicUsize, Ordering};

model! {
    Model => let m = AtomicUsize::new(0),
    Implementation => let mut i: usize = 0,
    Add(usize)(v in 0usize..4) => {
        let expected = m.fetch_add(v, Ordering::SeqCst) + v;
        i += v;
        assert_eq!(expected, i);
    },
    Set(usize)(v in 0usize..4) => {
        m.store(v, Ordering::SeqCst);
        i = v;
    },
    Eq(usize)(v in 0usize..4) => {
        let expected = m.load(Ordering::SeqCst) == v;
        let actual = i == v;
        assert_eq!(expected, actual);
    },
    Cas((usize, usize))((old, new) in (0usize..4, 0usize..4)) => {
        let expected =
            m.compare_and_swap(old, new, Ordering::SeqCst);
        let actual = if i == old {
            i = new;
            old
        } else {
            i
        };
        assert_eq!(expected, actual);
    }
}

linearizability testing:

#[macro_use]
extern crate model;

use std::sync::atomic::{AtomicUsize, Ordering};

linearizable! {
    Implementation => let i = model::Shared::new(AtomicUsize::new(0)),
    BuggyAdd(usize)(v in 0usize..4) -> usize {
        let current = i.load(Ordering::SeqCst);
        std::thread::yield_now();
        i.store(current + v, Ordering::SeqCst);
        current + v
    },
    Set(usize)(v in 0usize..4) -> () {
        i.store(v, Ordering::SeqCst)
    },
    BuggyCas((usize, usize))((old, new) in (0usize..4, 0usize..4)) -> usize {
        let current = i.load(Ordering::SeqCst);
        std::thread::yield_now();
        if current == old {
            i.store(new, Ordering::SeqCst);
            new
        } else {
            current
        }
    }
}

Re-exports

pub extern crate proptest as pt;

Macros

linearizable
model

Structs

Shared

Functions

default_config
permutohedron_heap