Struct loom::model::Builder

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 location: bool,
    pub log: bool,
    // some fields omitted
}

Configure a model

Fields

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.

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 existance 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.