interweave 0.1.1

Stateless model checker for concurrent programs, powered by Optimal DPOR.
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

//! Watch the checker find a reply-misrouting bug in an RPC connection multiplexer.
//!
//! Several callers share one connection (a single MPSC channel). Each reply frame
//! carries the request id it answers, and a single reader demultiplexes them. The
//! reader is *supposed* to route each reply to its caller — but instead of trusting
//! the id carried in the frame, it consults a shared `in_flight` cell that each
//! caller stamps with its own id just before sending. It looks airtight: every frame
//! is tagged, the reader checks the tag, and the FIFO channel preserves order. The
//! trap is that `in_flight` is shared mutable state updated out of band — a second
//! caller can stamp its id over the first's before the reader has correlated the
//! first caller's reply, so the reader hands one caller's result to another call.
//! Correlation state must travel *with* the message, not live in a shared slot.
//!
//! `recv` blocks on an empty connection, so the state space is finite: the reader
//! demuxes exactly as many frames as were sent.
//!
//! ```sh
//! cargo run --example rpc_mux
//! ```

use interweave::{World, explore};

// A reply frame on the shared connection: the request id it answers and the result
// destined for that request's caller (call k's result is k * 10).
#[derive(Debug, Clone, Copy)]
struct Reply {
    id: i32,
    result: i32,
}

fn rpc_mux(world: &mut World) {
    // The id of the call currently believed to be awaiting a reply on the connection.
    let in_flight = world.atomic("in_flight", -1);
    let (conn, reader) = world.channel::<Reply>("conn");

    // Two callers share the one connection. Each marks its call in-flight, then sends
    // the reply frame for its own call — the round-trip is collapsed, there is no
    // separate server task in this minimal model.
    for id in 0..2 {
        let (in_flight, conn) = (in_flight.clone(), conn.clone());
        world.spawn(format!("caller-{id}"), async move {
            in_flight.store(id).await;
            conn.send(Reply {
                id,
                result: id * 10,
            })
            .await;
            Ok(())
        });
    }

    // The reader demultiplexes replies, handing each frame's result to whatever call
    // it thinks is in flight — instead of to the id carried in the frame.
    world.spawn("reader", async move {
        for _ in 0..2 {
            let frame = reader.recv().await;
            let routed_to = in_flight.load().await;
            // The result we deliver must belong to the call we deliver it to.
            if frame.result != routed_to * 10 {
                return Err(format!(
                    "call {routed_to} received call {}'s result ({})",
                    frame.id, frame.result
                )
                .into());
            }
        }
        Ok(())
    });
}

fn main() {
    match explore(&rpc_mux, &mut ()) {
        Ok(()) => println!("every reply reaches its caller (unexpected for this program)"),
        Err(failed) => {
            println!("found a schedule where a reply is misrouted:");
            println!("  {failed}");
        }
    }
}