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

use traceforge::{sync::mpsc::*, *};
// this file shows some example usage of the Must's `sync::mpsc` library

#[test]
fn single_producer() {
    let f = || {
        let (tx, rx) = channel(100);
        let _t = thread::spawn(move || {
            traceforge::future::block_on(async {
                let _ = tx.send(10).await;
                let _ = tx.send(20).await;
                let _ = tx.send(30).await;
            })
        });
        // adding the following line would bring down the finished execution to 1 and blocked execution to 0, why?
        // t.join().unwrap();
        assert(rx.try_recv().unwrap() == 10);
        assert(rx.try_recv().unwrap() == 20);
        assert(rx.try_recv().unwrap() == 30);
    };

    let stats = verify(
        Config::builder().with_keep_going_after_error(false).build(),
        f,
    );
    println!("Stats = {}, {}", stats.execs, stats.block);
}

#[test]
fn multiple_producer() {
    let f = || {
        // increase n would significantly increase the number of finished executions
        // for exmplae, there's 5040 finished executions when n is 5
        // the program even hangs when n is 10
        let n = 5;

        let (tx, rx) = channel(100);
        for i in 0..n {
            let tx = tx.clone();
            thread::spawn(move || {
                traceforge::future::block_on(async {
                    let _ = tx.send(i).await;
                })
            });
        }

        for _ in 0..n {
            let j = rx.try_recv().unwrap();
            assert(0 <= j && j < 10);
        }
    };

    let stats = verify(
        Config::builder().with_keep_going_after_error(false).build(),
        f,
    );
    println!("Stats = {}, {}", stats.execs, stats.block);
}