#testing #deterministic #model-checking #simulation

model

model-based testing for data structures, with linearizability checking

6 releases

0.1.2 Jan 5, 2019
0.1.0 Nov 1, 2018
0.0.4 May 13, 2018

⚠️ Issues reported

#1531 in Data structures

Download history 38/week @ 2024-03-11 46/week @ 2024-03-18 38/week @ 2024-03-25 60/week @ 2024-04-01 40/week @ 2024-04-08 39/week @ 2024-04-15 52/week @ 2024-04-22 48/week @ 2024-04-29 44/week @ 2024-05-06 30/week @ 2024-05-13 40/week @ 2024-05-20 48/week @ 2024-05-27 33/week @ 2024-06-03 46/week @ 2024-06-10 51/week @ 2024-06-17 40/week @ 2024-06-24

174 downloads per month
Used in 3 crates

MIT/Apache

12KB
209 lines

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
        }
    }
}

Dependencies

~1.5MB
~31K SLoC