Struct loom::model::Builder

#[non_exhaustive]
pub struct Builder {
    pub max_threads: usize,
    pub max_branches: usize,
    pub max_permutations: Option<usize>,
    pub max_duration: Option<Duration>,
    pub preemption_bound: Option<usize>,
    pub checkpoint_file: Option<PathBuf>,
    pub checkpoint_interval: usize,
    pub expect_explicit_explore: bool,
    pub location: bool,
    pub log: bool,
}

Configure a model

Fields (Non-exhaustive)

Non-exhaustive structs could have additional fields added in future. Therefore, non-exhaustive structs cannot be constructed in external crates using the traditional Struct { .. } syntax; cannot be matched against without a wildcard ..; and struct update syntax will not work.

max_threads: usize

Max number of threads to check as part of the execution.

This should be set as low as possible and must be less than MAX_THREADS.

max_branches: usize

Maximum number of thread switches per permutation.

Defaults to LOOM_MAX_BRANCHES environment variable.

max_permutations: Option<usize>

Maximum number of permutations to explore.

Defaults to LOOM_MAX_PERMUTATIONS environment variable.

max_duration: Option<Duration>

Maximum amount of time to spend on checking

Defaults to LOOM_MAX_DURATION environment variable.

preemption_bound: Option<usize>

Maximum number of thread preemptions to explore

Defaults to LOOM_MAX_PREEMPTIONS environment variable.

checkpoint_file: Option<PathBuf>

When doing an exhaustive check, uses the file to store and load the check progress

Defaults to LOOM_CHECKPOINT_FILE environment variable.

checkpoint_interval: usize

How often to write the checkpoint file

Defaults to LOOM_CHECKPOINT_INTERVAL environment variable.

expect_explicit_explore: bool

When true loom won’t start state exploration until explore_state is called.

location: bool

When true, locations are captured on each loom operation.

Note that is is very expensive. It is recommended to first isolate a failing iteration using LOOM_CHECKPOINT_FILE, then enable location tracking.

Defaults to LOOM_LOCATION environment variable.

log: bool

Log execution output to stdout.

Defaults to existence of LOOM_LOG environment variable.

Implementations

impl Builder

pub fn new() -> Builder

Create a new Builder instance with default values.

pub fn checkpoint_file(&mut self, file: &str) -> &mut Self

Set the checkpoint file.

pub fn check<F>(&self, f: F)

where F: Fn() + Sync + Send + 'static,

Check the provided model.

Trait Implementations

impl Debug for Builder

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for Builder

fn default() -> Self

Returns the “default value” for a type.