6 releases
0.1.2 | Jan 5, 2019 |
---|---|
0.1.0 | Nov 1, 2018 |
0.0.4 | May 13, 2018 |
#1531 in Data structures
174 downloads per month
Used in 3 crates
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