model 0.1.2

model-based testing for data structures, with linearizability checking
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85

use model::{linearizable, model};

#[test]
fn test_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);
        }
    }
}

#[test]
#[should_panic]
fn test_linearizability_of_bad_impl() {
    use model::Shared;
    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);
            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
            }
        }
    }
}

#[test]
fn test_linearizability_of_good_impl() {
    use model::Shared;
    use std::sync::atomic::{AtomicUsize, Ordering};

    linearizable! {
        Implementation => let i = Shared::new(AtomicUsize::new(0)),
        Add(usize)(v in 0usize..4) -> usize {
            i.fetch_add(v, Ordering::SeqCst)
        },
        Set(usize)(v in 0usize..4) -> () {
            i.store(v, Ordering::SeqCst)
        },
        Cas((usize, usize))((old, new) in (0usize..4, 0usize..4)) -> usize {
            i.compare_and_swap(old, new, Ordering::SeqCst)
        }
    }
}