miri/concurrency/
data_race_handler.rs

1use std::rc::Rc;
2
3use super::{data_race, weak_memory};
4use crate::concurrency::GenmcCtx;
5use crate::{VisitProvenance, VisitWith};
6
7pub enum GlobalDataRaceHandler {
8    /// No data race detection will be done.
9    None,
10    /// State required to run in GenMC mode.
11    /// In this mode, the program will be executed repeatedly to explore different concurrent executions.
12    /// The `GenmcCtx` must persist across multiple executions, so it is behind an `Rc`.
13    ///
14    /// The `GenmcCtx` has several methods with which to inform it about events like atomic memory accesses.
15    /// In GenMC mode, some functionality is taken over by GenMC:
16    /// - Memory Allocation:    Allocated addresses need to be consistent across executions, which Miri's allocator doesn't guarantee
17    /// - Scheduling:           To influence which concurrent execution we will explore next, GenMC takes over scheduling
18    /// - Atomic operations:    GenMC will ensure that we explore all possible values that the memory model allows
19    ///   an atomic operation to see at any specific point of the program.
20    Genmc(Rc<GenmcCtx>),
21    /// The default data race detector for Miri using vector clocks.
22    Vclocks(Box<data_race::GlobalState>),
23}
24
25#[derive(Debug)]
26pub enum AllocDataRaceHandler {
27    None,
28    Genmc,
29    /// Data race detection via the use of vector clocks.
30    /// Weak memory emulation via the use of store buffers (if enabled).
31    Vclocks(data_race::AllocState, Option<weak_memory::AllocState>),
32}
33
34impl GlobalDataRaceHandler {
35    pub fn is_none(&self) -> bool {
36        matches!(self, GlobalDataRaceHandler::None)
37    }
38
39    pub fn as_vclocks_ref(&self) -> Option<&data_race::GlobalState> {
40        if let Self::Vclocks(data_race) = self { Some(data_race) } else { None }
41    }
42
43    pub fn as_vclocks_mut(&mut self) -> Option<&mut data_race::GlobalState> {
44        if let Self::Vclocks(data_race) = self { Some(data_race) } else { None }
45    }
46
47    pub fn as_genmc_ref(&self) -> Option<&GenmcCtx> {
48        if let Self::Genmc(genmc_ctx) = self { Some(genmc_ctx) } else { None }
49    }
50}
51
52impl AllocDataRaceHandler {
53    pub fn as_vclocks_ref(&self) -> Option<&data_race::AllocState> {
54        if let Self::Vclocks(data_race, _weak_memory) = self { Some(data_race) } else { None }
55    }
56
57    pub fn as_vclocks_mut(&mut self) -> Option<&mut data_race::AllocState> {
58        if let Self::Vclocks(data_race, _weak_memory) = self { Some(data_race) } else { None }
59    }
60
61    pub fn as_weak_memory_ref(&self) -> Option<&weak_memory::AllocState> {
62        if let Self::Vclocks(_data_race, weak_memory) = self { weak_memory.as_ref() } else { None }
63    }
64
65    pub fn as_weak_memory_mut(&mut self) -> Option<&mut weak_memory::AllocState> {
66        if let Self::Vclocks(_data_race, weak_memory) = self { weak_memory.as_mut() } else { None }
67    }
68}
69
70impl VisitProvenance for GlobalDataRaceHandler {
71    fn visit_provenance(&self, visit: &mut VisitWith<'_>) {
72        match self {
73            GlobalDataRaceHandler::None => {}
74            GlobalDataRaceHandler::Vclocks(data_race) => data_race.visit_provenance(visit),
75            GlobalDataRaceHandler::Genmc(genmc_ctx) => genmc_ctx.visit_provenance(visit),
76        }
77    }
78}
79
80impl VisitProvenance for AllocDataRaceHandler {
81    fn visit_provenance(&self, visit: &mut VisitWith<'_>) {
82        match self {
83            AllocDataRaceHandler::None => {}
84            AllocDataRaceHandler::Genmc => {}
85            AllocDataRaceHandler::Vclocks(data_race, weak_memory) => {
86                data_race.visit_provenance(visit);
87                weak_memory.visit_provenance(visit);
88            }
89        }
90    }
91}
miri/concurrency/data_race_handler.rs

miri/concurrency/
data_race_handler.rs
