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 |