Enum GlobalDataRaceHandler

pub enum GlobalDataRaceHandler {
    None,
    Genmc(Rc<GenmcCtx>),
    Vclocks(Box<GlobalState>),
}

Variants

None

No data race detection will be done.

Genmc(Rc<GenmcCtx>)

State required to run in GenMC mode. In this mode, the program will be executed repeatedly to explore different concurrent executions. The GenmcCtx must persist across multiple executions, so it is behind an Rc.

The GenmcCtx has several methods with which to inform it about events like atomic memory accesses. In GenMC mode, some functionality is taken over by GenMC:

• Memory Allocation: Allocated addresses need to be consistent across executions, which Miri’s allocator doesn’t guarantee
• Scheduling: To influence which concurrent execution we will explore next, GenMC takes over scheduling
• Atomic operations: GenMC will ensure that we explore all possible values that the memory model allows an atomic operation to see at any specific point of the program.

Vclocks(Box<GlobalState>)

The default data race detector for Miri using vector clocks.

Implementations

impl GlobalDataRaceHandler

fn set_ongoing_action_data_race_free(&self, enable: bool)

Select whether data race checking is disabled. This is solely an implementation detail of allow_data_races_* and must not be used anywhere else!

impl GlobalDataRaceHandler

pub fn is_none(&self) -> bool

pub fn as_vclocks_ref(&self) -> Option<&GlobalState>

pub fn as_vclocks_mut(&mut self) -> Option<&mut GlobalState>

pub fn as_genmc_ref(&self) -> Option<&GenmcCtx>

Trait Implementations

impl VisitProvenance for GlobalDataRaceHandler

fn visit_provenance(&self, visit: &mut VisitWith<'_>)

Layout

Note: Most layout information is completely unstable and may even differ between compilations. The only exception is types with certain repr(...) attributes. Please see the Rust Reference's “Type Layout” chapter for details on type layout guarantees.

Size: 16 bytes

Size for each variant:

• None: 0 bytes
• Genmc: 8 bytes
• Vclocks: 8 bytes