Skip to main content

Program

must::program

Trait Program 

Source 
pub trait Program {
    // Required methods
    fn num_threads(&self) -> usize;
    fn next(&self, traces: &[Vec<Option<Val>>]) -> Vec<ThreadNext>;

    // Provided method
    fn next_thread(&self, tid: Tid, trace: &[Option<Val>]) -> ThreadNext { ... }
}
Expand description

A program as seen by the explorer: a total, deterministic function from per-thread traces to per-thread next events.

Required Methods§

Source

fn num_threads(&self) -> usize

Number of threads N; thread ids are 0..N.

Source

fn next(&self, traces: &[Vec<Option<Val>>]) -> Vec<ThreadNext>

The next event of every thread under traces. The returned vector has length num_threads(); index i is thread i’s ThreadNext. traces must also have length num_threads() - one per-event trace per thread (see the module docs for the exact contract between traces and events).

Provided Methods§

Source

fn next_thread(&self, tid: Tid, trace: &[Option<Val>]) -> ThreadNext

The next event of a single thread from its own trace. next(traces)[tid] is a pure function of traces[tid] (each process only sees the values it receives), so the explorer can recompute just the one thread whose trace grew.

The default recomputes all threads and keeps tid’s answer; it is correct for any contract-abiding program. Implementations with a cheaper per-thread replay (the coroutine runtime) override it.

Dyn Compatibility§

This trait is dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors§