#testing #simulation #deterministic #model-checking

model

model-based testing for data structures, with linearizability checking

6 releases

✓ Uses Rust 2018 edition

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

#21 in Testing

Download history 540/week @ 2018-11-08 606/week @ 2018-11-15 412/week @ 2018-11-22 690/week @ 2018-11-29 613/week @ 2018-12-06 618/week @ 2018-12-13 470/week @ 2018-12-20 408/week @ 2018-12-27 538/week @ 2019-01-03 1570/week @ 2019-01-10 1718/week @ 2019-01-17 1607/week @ 2019-01-24 1827/week @ 2019-01-31 1999/week @ 2019-02-07 2608/week @ 2019-02-14

1,727 downloads per month
Used in 2 crates

MIT/Apache

11KB
209 lines


lib.rs:

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

# fn main() {
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};

# fn main() {
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
~25K SLoC