traceforge 0.2.1

TraceForge is a model checker for concurrent and distributed programs written in Rust
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

use traceforge::{channel::Builder, loc::CommunicationModel::*, thread, Config};

// In the presence of concurrent receives and consistency stronger than NoOrder,
// the model is not prefix-closed and one consistent execution is missed.
#[should_panic(expected = "Detected concurrent receives")]
#[test]
fn not_prefix_closed() {
    let stats = traceforge::verify(Config::builder().build(), || {
        let ch1 = Builder::new().with_comm(LocalOrder).build();
        let ch2 = ch1.clone();
        ch1.0.send_msg(1);
        ch1.0.send_msg(2);
        let _t1 = thread::spawn(move || {
            traceforge::assume!(ch1.1.recv_msg() == Some(2));
        });
        let _t2 = thread::spawn(move || {
            traceforge::assume!(ch2.1.recv_msg() == Some(1));
        });
    });
    assert_eq!(stats.execs, 1);
}

// Receive->receive revisits won't work out of the box:
// two receives would have to revisit the first one,
// but once the first revisit, the second cannot.
#[should_panic(expected = "Detected concurrent receives")]
#[test]
fn not_prefix_closed_extra() {
    let stats = traceforge::verify(Config::builder().build(), || {
        let ch1 = Builder::new().with_comm(LocalOrder).build();
        let ch2 = ch1.clone();
        let ch3 = ch1.clone();
        ch1.0.send_msg(1);
        ch1.0.send_msg(2);
        ch1.0.send_msg(3);
        let _t1 = thread::spawn(move || {
            traceforge::assume!(ch1.1.recv_msg() == Some(3));
        });
        let _t2 = thread::spawn(move || {
            ch2.1.recv_msg();
        });
        let _t3 = thread::spawn(move || {
            ch3.1.recv_msg();
        });
    });
    assert!(stats.execs >= 1);
}

// In the presence of blocking concurrent receives, the model is not extensible.
// missing one consistent execution.
#[should_panic(expected = "Detected concurrent receives")]
#[test]
fn not_extensible() {
    let stats = traceforge::verify(Config::builder().build(), || {
        let ch1 = Builder::new().with_comm(NoOrder).build();
        let ch2 = ch1.clone();
        ch1.0.send_msg(1);
        let _t1 = thread::spawn(move || {
            ch1.1.recv_msg_block();
            traceforge::assume!(ch1.1.recv_msg_block() == 2);
        });
        let _t2 = thread::spawn(move || {
            ch2.1.recv_msg_block();
            ch2.0.send_msg(2);
        });
    });
    assert_eq!(stats.execs, 1);
}

// One blocked execution is missed.
#[should_panic(expected = "Detected concurrent receives")]
#[test]
fn not_extensible_2() {
    let stats = traceforge::verify(Config::builder().build(), || {
        let ch1 = Builder::new().with_comm(NoOrder).build();
        let ch2 = ch1.clone();
        ch1.0.send_msg(1);
        let _t2 = thread::spawn(move || ch1.1.recv_msg_block());
        let _t2 = thread::spawn(move || ch2.1.recv_msg_block());
    });
    assert_eq!((stats.execs, stats.block), (0, 2));
}