Expand description
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;