Crate model [] [src]

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.

model-based testing:

#[macro_use]
extern crate model;
#[macro_use]
extern crate proptest;

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;
#[macro_use]
extern crate proptest;

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

linearizable! {
    Implementation => let i = Shared::new(AtomicUsize::new(0)),
    BuggyAdd(usize)(v in 0usize..4) -> usize {
        let current = i.load(Ordering::SeqCst);
        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);
        thread::yield_now();
        if current == old {
            i.store(new, Ordering::SeqCst);
            new
        } else {
            current
        }
    }
}

Macros

linearizable
model

Structs

Shared

Functions

deterministic_set_seed
permutohedron_heap
thread_rng