Crate fibril_verifier

source ·
Expand description

Fibril Verifier is a library for model checking Fibril systems.

Example

[dependencies]
fibril = { version = "0", features = ["fibers", "rt", "serde_json"] }
serde = { version = "1", features = ["derive"] }

[dev-dependencies]
fibril_verifier = "0"

use fibril::*;

#[derive(Clone, Debug, PartialEq, serde::Deserialize, serde::Serialize)]
enum Msg { Inc, Double, Value(u64) }

fn server(sdk: Sdk<Msg>) {
    let mut val = 0;
    loop {
        let (src, msg) = sdk.recv();
        match msg {
            Msg::Inc => {
                val += 1;
                sdk.send(src, Msg::Value(val));
            }
            Msg::Double => {
                val *= 2;
                sdk.send(src, Msg::Value(val));
            }
            _ => sdk.exit(),
        }
    }
}

// In the binary, bind the server to a UDP socket.
fn run_server_over_udp() {
    use std::net::Ipv4Addr;
    let mut rt = UdpRuntime::new_with_serde_json()
        .ipv4(Ipv4Addr::LOCALHOST)
        .port_fn(|n| 3000 + n);
    rt.spawn(|| Fiber::new(server));
    rt.join().unwrap();
}

// In the tests, the model checker will attempt to find a "trace" (sequence of steps) that
// causes a panic.
#[cfg(test)]
#[test]
fn may_panic() {
    use fibril_verifier::*;
    let mut verifier = Verifier::new(|cfg| {
        let server = cfg.spawn(Fiber::new(server));
        cfg.spawn(Fiber::new(move |sdk| {
            sdk.send(server, Msg::Inc);
            let (_src, msg) = sdk.recv();
            assert_eq!(msg, Msg::Value(1)); // truth depends on race winner
        }));
        cfg.spawn(Fiber::new(move |sdk| {
            sdk.send(server, Msg::Double);
            let (_src, msg) = sdk.recv();
            assert_eq!(msg, Msg::Value(2)); // truth depends on race winner
        }));
    });
    // TIP: alternatively use verifier.assert_no_panic() to fail the test.
    let (msg, _minimal_trace) = verifier.assert_panic();
    assert!(msg.contains("left == right"));
}

And here is an example of how to interact with the server using netcat.

# send STDOUT to disk for clarity as replies are not newline delimited
$ nc -u 127.0.0.1 3000 > /tmp/replies
"Inc"
"Inc"
"Double"
^C

$ cat /tmp/replies
{"Value":1}{"Value":2}{"Value":4}

Macros

Structs

Enums

Traits