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, Channel};
use traceforge::loc::CommunicationModel;
use traceforge::{thread, Config};

type Ip = i32;
const SERVER_IP: Ip = 42;

type ListenSocket = Ip;
type TcpSock<T> = Channel<T>;

#[derive(PartialEq, Eq, Clone, Debug, Hash)]
struct Listen(Ip);

#[derive(PartialEq, Eq, Clone, Debug, Hash)]
struct Accept(Ip);

// A simple TCP example
#[test]
fn tcp_handshake() {
    // TODO: Renew listen messages before accepting?
    let stats = traceforge::verify(Config::builder().build(), || {
        // server
        let _ = thread::spawn(|| {
            // listen_sock = bind(my_ip)
            let sock: ListenSocket = SERVER_IP;

            // listen(listen_sock)
            Builder::new()
                .with_name(Listen(sock))
                .with_comm(CommunicationModel::NoOrder)
                .build()
                .0
                .send_msg(());

            // let sock = accept(listen_sock)
            let sock: TcpSock<_> = Builder::new()
                .with_name(Accept(sock))
                .with_comm(CommunicationModel::NoOrder)
                .build()
                .1
                .recv_msg_block();

            // recv(sock)
            let msg: &str = sock.1.recv_msg_block();
            println!("Server received: {}", msg);

            // send(sock)
            sock.0.send_msg("Hello from server");
        });
        // client
        let _ = thread::spawn(|| {
            // let sock = connect(server_ip)
            let () = Builder::new()
                .with_name(Listen(SERVER_IP))
                .with_comm(CommunicationModel::NoOrder)
                .build()
                .1
                .recv_msg_block();
            let ch1 = Builder::new()
                .with_comm(CommunicationModel::LocalOrder)
                .build();
            let ch2 = Builder::new()
                .with_comm(CommunicationModel::LocalOrder)
                .build();
            let sock = (ch1.0, ch2.1);
            Builder::new()
                .with_name(Accept(SERVER_IP))
                .with_comm(CommunicationModel::NoOrder)
                .build()
                .0
                .send_msg((ch2.0, ch1.1));

            // send(sock)
            sock.0.send_msg("Hello from client");

            // recv(sock)
            let msg: &str = sock.1.recv_msg_block();
            println!("Client received: {}", msg);
        });
    });
    assert_eq!(stats.execs, 1);
}