[−][src]Crate model
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; |
Macros
linearizable | |
model |
Structs
Shared |
Functions
default_config | |
permutohedron_heap |