Lib.rs

Rust的简单模型检查工具。

旨在减少编写基于模型和线性化测试所需的样板代码。

它可以通过在不同的命令上运行顺序操作，然后尝试找到一个导致相同返回值的顺序来找到实现中的线性化违规，而无需了解其内部工作原理。

重要：该crate通过宏使用proptest。请确保您正在使用与model在Cargo.toml中列出的相同版本的proptest，否则不匹配的API更改将表现为隐藏在宏中的奇怪的编译时错误。

基于模型的测试

#[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);
    }
}

线性化测试

#[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
        }
    }
}