Grcov report - explore

1

//! Validates the parallel and caching exploration drivers against the

2

//! single-threaded [`merc_explore::explore`], which is simple enough to act as

3

//! the naive reference. That baseline is in turn anchored to closed-form state

4

//! and transition counts so it cannot drift silently.

5

6

mod mock_lps;

7

8

use std::collections::BTreeSet;

9

use std::collections::HashMap;

10

11

use merc_explore::CacheLPS;

12

use merc_explore::CachingStrategy;

13

use merc_explore::ExplorationStrategy;

14

use merc_explore::LPS;

15

use merc_explore::Summand;

16

use merc_explore::explore;

17

use merc_explore::explore_parallel;

18

use merc_utilities::Timing;

19

20

use mock_lps::Edge;

21

use mock_lps::Label;

22

use mock_lps::MockLps;

23

use mock_lps::State;

24

25

/// Per-worker accumulator: the dense index -> state-vector map (from `on_state`)

26

/// and the raw `(from_index, label, to_index)` transitions (from `on_transition`).

27

#[derive(Default)]

28

struct Accumulator {

29

    states: HashMap<usize, State>,

30

    edges: Vec<(usize, Label, usize)>,

31

32

33

/// Translates the index-keyed accumulator into state-vector form, so runs are

34

/// compared by concrete state rather than by the dense index numbering the

35

/// drivers assign. Every transition endpoint is a discovered state, so it is

36

/// present in the map once exploration finishes.

37

92

fn resolve(states: HashMap<usize, State>, edges: Vec<(usize, Label, usize)>) -> (BTreeSet<State>, BTreeSet<Edge>) {

38

92

    let resolved_edges = edges

39

92

        .into_iter()

40

3320

        .map(|(from, label, to)| {

41

3320

            let from = states.get(&from).expect("source state was reported").clone();

42

3320

            let to = states.get(&to).expect("target state was reported").clone();

43

3320

            (from, label, to)

44

3320

})

45

92

        .collect();

46

92

    let states = states.into_values().collect();

47

92

    (states, resolved_edges)

48

92

49

50

/// Runs the sequential driver and returns its reachable states and transitions.

51

65

fn run_sequential<P>(lps: &P, strategy: ExplorationStrategy) -> (BTreeSet<State>, BTreeSet<Edge>)

52

65

where

53

65

    P: LPS<Value = usize, Label = Label, StateInfo = State>,

54

55

65

    let mut acc = Accumulator::default();

56

65

    explore(

57

65

        lps,

58

65

        strategy,

59

65

        &Timing::new(),

60

65

        &mut acc,

61

967

        |acc, index, info| {

62

967

            acc.states.insert(index.value(), info.clone());

63

967

            Ok(())

64

967

},

65

2330

        |acc, from, label, to| {

66

2330

            acc.edges.push((from.value(), *label, to.value()));

67

2330

            Ok(())

68

2330

},

69

70

65

    .expect("exploration succeeds");

71

65

    resolve(acc.states, acc.edges)

72

65

73

74

/// Runs the parallel driver and merges the per-worker accumulators.

75

27

fn run_parallel<P>(lps: &P) -> (BTreeSet<State>, BTreeSet<Edge>)

76

27

where

77

27

    P: LPS<Value = usize, Label = Label, StateInfo = State> + Sync,

78

27

    <P::Summand as Summand>::Context: Send,

79

80

27

    let (_initial, locals) = explore_parallel(

81

27

        lps,

82

        Accumulator::default,

83

408

        |acc, index, info| {

84

408

            acc.states.insert(index.value(), info.clone());

85

408

            Ok(())

86

408

},

87

990

        |acc, from, label, to| {

88

990

            acc.edges.push((from.value(), *label, to.value()));

89

990

            Ok(())

90

990

},

91

92

27

    .expect("parallel exploration succeeds");

93

94

27

    let mut states = HashMap::new();

95

27

    let mut edges = Vec::new();

96

108

    for acc in locals {

97

108

        states.extend(acc.states);

98

108

        edges.extend(acc.edges);

99

108

100

27

    resolve(states, edges)

101

27

102

103

/// The fixtures every driver is checked against: plain grids of varying shape,

104

/// a grid carrying a conjunction-guarded diagonal summand, and a degenerate

105

/// grid whose only state is the initial one (all guards false from the start).

106

4

fn fixtures() -> Vec<MockLps> {

107

4

    vec![

108

4

        MockLps::grid(&[0]),

109

4

        MockLps::grid(&[3]),

110

4

        MockLps::grid(&[2, 3]),

111

4

        MockLps::grid(&[2, 2, 2]),

112

4

        MockLps::grid_with_diagonal(&[2, 3]),

113

4

        MockLps::grid_with_diagonal(&[3, 3, 2]),

114

        // Grids whose summands fan out to several successors, with a different

115

        // step bound per coordinate (a `0` step yields a guarded self-loop).

116

4

        MockLps::grid_with_steps(&[3], &[2]),

117

4

        MockLps::grid_with_steps(&[2, 3], &[1, 2]),

118

4

        MockLps::grid_with_steps(&[2, 2, 2], &[0, 1, 2]),

119

120

4

121

122

/// The naive baseline: a single-threaded depth-first exploration. Its reachable

123

/// states and transitions are what the other drivers are compared against.

124

38

fn baseline(lps: &MockLps) -> (BTreeSet<State>, BTreeSet<Edge>) {

125

38

    run_sequential(lps, ExplorationStrategy::Dfs)

126

38

127

128

#[test]

129

1

fn breadth_first_matches_depth_first() {

130

    // The traversal order must not change the discovered state space.

131

9

    for lps in fixtures() {

132

9

        assert_eq!(

133

9

            run_sequential(&lps, ExplorationStrategy::Bfs),

134

9

            baseline(&lps),

135

            "BFS disagreed with DFS"

136

);

137

138

1

139

140

#[test]

141

#[cfg_attr(miri, ignore)] // rayon uses crossbeam-epoch which has Stacked Borrows violations under Miri

142

1

fn parallel_matches_sequential() {

143

9

    for lps in fixtures() {

144

9

        assert_eq!(

145

9

            run_parallel(&lps),

146

9

            baseline(&lps),

147

            "parallel driver disagreed with sequential"

148

);

149

150

1

151

152

#[test]

153

#[cfg_attr(miri, ignore)] // rayon uses crossbeam-epoch which has Stacked Borrows violations under Miri

154

1

fn cached_matches_sequential() {

155

2

    for strategy in [CachingStrategy::Local, CachingStrategy::None] {

156

18

        for lps in fixtures() {

157

18

            let expected = baseline(&lps);

158

18

            let cached = CacheLPS::new(lps, strategy);

159

160

18

            assert_eq!(

161

18

                run_sequential(&cached, ExplorationStrategy::Dfs),

162

                expected,

163

                "cached sequential driver disagreed with sequential (strategy {strategy:?})"

164

);

165

18

            assert_eq!(

166

18

                run_parallel(&cached),

167

                expected,

168

                "cached parallel driver disagreed with sequential (strategy {strategy:?})"

169

);

170

171

172

1

173

174

#[test]

175

1

fn sequential_propagates_callback_error() {

176

    // A transition callback that always fails must surface as an error rather

177

    // than completing the exploration.

178

1

    let lps = MockLps::grid(&[3, 3]);

179

1

    let result = explore(

180

1

        &lps,

181

1

        ExplorationStrategy::Dfs,

182

1

        &Timing::new(),

183

1

        &mut (),

184

1

        |_ctx, _index, _info| Ok(()),

185

1

        |_ctx, _from, _label, _to| Err("boom".into()),

186

);

187

1

    assert!(result.is_err(), "callback error must surface");

188

1

189

190

#[test]

191

#[cfg_attr(miri, ignore)] // rayon uses crossbeam-epoch which has Stacked Borrows violations under Miri

192

1

fn parallel_propagates_callback_error() {

193

    // Exercises the abort path: one worker's failing callback sets `aborted`,

194

    // and every worker stops and reports the error.

195

1

    let lps = MockLps::grid(&[3, 3]);

196

1

    let result = explore_parallel(

197

1

        &lps,

198

        || (),

199

1

        |_local, _index, _info| Ok(()),

200

1

        |_local, _from, _label, _to| Err("boom".into()),

201

);

202

1

    assert!(result.is_err(), "callback error must surface from the parallel driver");

203

1

204

205

#[test]

206

1

fn grid_state_and_transition_counts() {

207

    // Anchor the naive baseline to closed-form counts, so the driver everything

208

    // else is compared against cannot drift undetected.

209

1

    let lps = MockLps::grid(&[2, 3]);

210

1

    let (states, edges) = baseline(&lps);

211

    // States: the full product grid (bound + 1 per axis).

212

1

    assert_eq!(states.len(), 3 * 4);

213

    // Transitions: along axis i, the source ranges over its bound values while

214

    // the others range freely: 2*4 + 3*3 = 17.

215

1

    assert_eq!(edges.len(), 2 * 4 + 3 * 3);

216

1

217

218

#[test]

219

1

fn stepped_grid_state_and_transition_counts() {

220

    // A one-dimensional grid whose only summand fires at the initial state and

221

    // adds any value in `0..=2`, producing three successors (`0`, `1`, `2`).

222

1

    let lps = MockLps::grid_with_steps(&[1], &[2]);

223

1

    let (states, edges) = baseline(&lps);

224

    // Reachable states: the initial `0` plus the two further targets `1` and `2`.

225

1

    assert_eq!(states, BTreeSet::from([vec![0], vec![1], vec![2]]));

226

    // Only state `0` satisfies the guard; it emits one edge per delta value.

227

1

    assert_eq!(

228

        edges,

229

1

        BTreeSet::from([(vec![0], 0, vec![0]), (vec![0], 0, vec![1]), (vec![0], 0, vec![2])])

230

);

231

1