1 /* Copyright (c) 2017-2023. The SimGrid Team. All rights reserved. */
3 /* This program is free software; you can redistribute it and/or modify it
4 * under the terms of the license (GNU LGPL) which comes with this package. */
6 #include "src/3rd-party/catch.hpp"
7 #include "src/mc/explo/odpor/Execution.hpp"
8 #include "src/mc/explo/odpor/odpor_tests_private.hpp"
9 #include "src/mc/transition/TransitionComm.hpp"
11 using namespace simgrid::mc;
12 using namespace simgrid::mc::odpor;
13 using namespace simgrid::mc::udpor;
15 TEST_CASE("simgrid::mc::odpor::Execution: Constructing Executions")
18 REQUIRE(execution.empty());
19 REQUIRE(execution.size() == 0);
20 REQUIRE_FALSE(execution.get_latest_event_handle().has_value());
23 TEST_CASE("simgrid::mc::odpor::Execution: Testing Happens-Before")
27 // We check each permutation for happens before
28 // among the given actions added to the execution
29 const auto a1 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
30 const auto a2 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
31 const auto a3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
32 const auto a4 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 4);
35 execution.push_transition(a1);
36 execution.push_transition(a2);
37 execution.push_transition(a3);
38 execution.push_transition(a4);
40 SECTION("Happens-before is irreflexive")
42 REQUIRE_FALSE(execution.happens_before(0, 0));
43 REQUIRE_FALSE(execution.happens_before(1, 1));
44 REQUIRE_FALSE(execution.happens_before(2, 2));
45 REQUIRE_FALSE(execution.happens_before(3, 3));
48 SECTION("Happens-before values for each pair of events")
50 REQUIRE_FALSE(execution.happens_before(0, 1));
51 REQUIRE_FALSE(execution.happens_before(0, 2));
52 REQUIRE(execution.happens_before(0, 3));
53 REQUIRE_FALSE(execution.happens_before(1, 2));
54 REQUIRE_FALSE(execution.happens_before(1, 3));
55 REQUIRE_FALSE(execution.happens_before(2, 3));
58 SECTION("Happens-before is a subset of 'occurs-before' ")
60 REQUIRE_FALSE(execution.happens_before(1, 0));
61 REQUIRE_FALSE(execution.happens_before(2, 0));
62 REQUIRE_FALSE(execution.happens_before(3, 0));
63 REQUIRE_FALSE(execution.happens_before(2, 1));
64 REQUIRE_FALSE(execution.happens_before(3, 1));
65 REQUIRE_FALSE(execution.happens_before(3, 2));
71 const auto a1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
72 const auto a2 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
73 const auto a3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
74 const auto a4 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
76 // Notice that `a5` and `a6` are executed by the same actor; thus, although
77 // the actor is executing independent actions, each still "happen-before"
81 execution.push_transition(a1);
82 execution.push_transition(a2);
83 execution.push_transition(a3);
84 execution.push_transition(a4);
86 SECTION("Happens-before is irreflexive")
88 REQUIRE_FALSE(execution.happens_before(0, 0));
89 REQUIRE_FALSE(execution.happens_before(1, 1));
90 REQUIRE_FALSE(execution.happens_before(2, 2));
91 REQUIRE_FALSE(execution.happens_before(3, 3));
94 SECTION("Happens-before values for each pair of events")
96 REQUIRE_FALSE(execution.happens_before(0, 1));
97 REQUIRE_FALSE(execution.happens_before(0, 2));
98 REQUIRE_FALSE(execution.happens_before(0, 3));
99 REQUIRE(execution.happens_before(1, 2));
100 REQUIRE(execution.happens_before(1, 3));
101 REQUIRE(execution.happens_before(2, 3));
104 SECTION("Happens-before is a subset of 'occurs-before'")
106 REQUIRE_FALSE(execution.happens_before(1, 0));
107 REQUIRE_FALSE(execution.happens_before(2, 0));
108 REQUIRE_FALSE(execution.happens_before(3, 0));
109 REQUIRE_FALSE(execution.happens_before(2, 1));
110 REQUIRE_FALSE(execution.happens_before(3, 1));
111 REQUIRE_FALSE(execution.happens_before(3, 2));
115 SECTION("Happens-before is transitively-closed")
119 // Given a reversible race between events `e1` and `e3` in a simulation,
120 // we assert that `e5` would be eliminated from being contained in
121 // the sequence `notdep(e1, E)`
122 const auto e0 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
123 const auto e1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
124 const auto e2 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
125 const auto e3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
126 const auto e4 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
129 execution.push_partial_execution(PartialExecution{e0, e1, e2, e3, e4});
130 REQUIRE(execution.happens_before(0, 2));
131 REQUIRE(execution.happens_before(2, 4));
132 REQUIRE(execution.happens_before(0, 4));
135 SECTION("Stress testing transitivity of the happens-before relation")
137 // This test verifies that for each triple of events
138 // in the execution, for a modestly intersting one,
139 // that transitivity holds
140 const auto e0 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
141 const auto e1 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
142 const auto e2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
143 const auto e3 = std::make_shared<DependentIfSameValueAction>(Transition::Type::UNKNOWN, 2, -10);
144 const auto e4 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
145 const auto e5 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 0);
146 const auto e6 = std::make_shared<DependentIfSameValueAction>(Transition::Type::UNKNOWN, 2, -5);
147 const auto e7 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
148 const auto e8 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 0);
149 const auto e9 = std::make_shared<DependentIfSameValueAction>(Transition::Type::UNKNOWN, 2, -10);
150 const auto e10 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
153 execution.push_partial_execution(PartialExecution{e0, e1, e2, e3, e4, e5, e6, e7, e8, e9, e10});
155 const auto max_handle = execution.get_latest_event_handle();
156 for (Execution::EventHandle e_i = 0; e_i < max_handle; ++e_i) {
157 for (Execution::EventHandle e_j = 0; e_j < max_handle; ++e_j) {
158 for (Execution::EventHandle e_k = 0; e_k < max_handle; ++e_k) {
159 const bool e_i_before_e_j = execution.happens_before(e_i, e_j);
160 const bool e_j_before_e_k = execution.happens_before(e_j, e_k);
161 const bool e_i_before_e_k = execution.happens_before(e_i, e_k);
162 // Logical equivalent of `e_i_before_e_j ^ e_j_before_e_k --> e_i_before_e_k`
163 REQUIRE((not(e_i_before_e_j && e_j_before_e_k) || e_i_before_e_k));
171 TEST_CASE("simgrid::mc::odpor::Execution: Testing Racing Events and Initials")
175 const auto a1 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
176 const auto a2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2);
177 const auto a3 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
178 const auto a4 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
179 const auto a5 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
182 execution.push_transition(a1);
183 execution.push_transition(a2);
184 execution.push_transition(a3);
185 execution.push_transition(a4);
186 execution.push_transition(a5);
188 // Nothing comes before event 0
189 REQUIRE(execution.get_racing_events_of(0) == std::unordered_set<Execution::EventHandle>{});
191 // Events 0 and 1 are independent
192 REQUIRE(execution.get_racing_events_of(1) == std::unordered_set<Execution::EventHandle>{});
194 // 2 and 1 are executed by different actors and happen right after each other
195 REQUIRE(execution.get_racing_events_of(2) == std::unordered_set<Execution::EventHandle>{1});
197 // Although a3 and a4 are dependent, they are executed by the same actor
198 REQUIRE(execution.get_racing_events_of(3) == std::unordered_set<Execution::EventHandle>{});
200 // Event 4 is in a race with neither event 0 nor event 2 since those events
201 // "happen-before" event 3 with which event 4 races
203 // Furthermore, event 1 is run by the same actor and thus also is not in a race.
204 // Hence, only event 3 races with event 4
205 REQUIRE(execution.get_racing_events_of(4) == std::unordered_set<Execution::EventHandle>{3});
208 SECTION("Example 2: Events with multiple races")
210 const auto a1 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
211 const auto a2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2);
212 const auto a3 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
213 const auto a4 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
216 execution.push_transition(a1);
217 execution.push_transition(a2);
218 execution.push_transition(a3);
219 execution.push_transition(a4);
221 // Nothing comes before event 0
222 REQUIRE(execution.get_racing_events_of(0) == std::unordered_set<Execution::EventHandle>{});
224 // Events 0 and 1 are independent
225 REQUIRE(execution.get_racing_events_of(1) == std::unordered_set<Execution::EventHandle>{});
227 // Event 2 is independent with event 1 and run by the same actor as event 0
228 REQUIRE(execution.get_racing_events_of(2) == std::unordered_set<Execution::EventHandle>{});
230 // All events are dependent with event 3, but event 0 "happens-before" event 2
231 REQUIRE(execution.get_racing_events_of(3) == std::unordered_set<Execution::EventHandle>{1, 2});
233 SECTION("Check initials with respect to event 1")
235 // First, note that v := notdep(1, execution).p == {e2}.{e3} == {e2, e3}
236 // Since e2 -->_E e3, actor 3 is not an initial for E' := pre(1, execution)
237 // with respect to `v`. e2, however, has nothing happening before it in dom_E(v),
238 // so it is an initial of E' wrt. `v`
239 const auto initial_wrt_event1 = execution.get_missing_source_set_actors_from(1, std::unordered_set<aid_t>{});
240 REQUIRE(initial_wrt_event1 == std::unordered_set<aid_t>{1});
243 SECTION("Check initials with respect to event 2")
245 // First, note that v := notdep(1, execution).p == {}.{e3} == {e3}
246 // e3 has nothing happening before it in dom_E(v), so it is an initial
248 const auto initial_wrt_event2 = execution.get_missing_source_set_actors_from(2, std::unordered_set<aid_t>{});
249 REQUIRE(initial_wrt_event2 == std::unordered_set<aid_t>{3});
253 SECTION("Example 3: Testing 'Lock' Example")
255 // In this example, `e0` and `e1` are lock actions that
256 // are in a race. We assert that
257 const auto e0 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
258 const auto e1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
259 const auto e2 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
260 const auto e3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
261 const auto e4 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
264 execution.push_transition(e0);
265 execution.push_transition(e1);
266 execution.push_transition(e2);
267 execution.push_transition(e3);
268 execution.push_transition(e4);
269 REQUIRE(execution.get_racing_events_of(4) == std::unordered_set<Execution::EventHandle>{0});
272 SECTION("Example 4: Indirect Races")
274 const auto e0 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
275 const auto e1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
276 const auto e2 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
277 const auto e3 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
278 const auto e4 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 6);
279 const auto e5 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
280 const auto e6 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
281 const auto e7 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 3);
282 const auto e8 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 4);
283 const auto e9 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2);
285 Execution execution(PartialExecution{e0, e1, e2, e3, e4, e5, e6, e7, e8, e9});
287 // Nothing comes before event 0
288 REQUIRE(execution.get_racing_events_of(0) == std::unordered_set<Execution::EventHandle>{});
290 // Events 0 and 1 are independent
291 REQUIRE(execution.get_racing_events_of(1) == std::unordered_set<Execution::EventHandle>{});
293 // Events 1 and 2 are independent
294 REQUIRE(execution.get_racing_events_of(2) == std::unordered_set<Execution::EventHandle>{});
296 // Events 1 and 3 are independent; the rest are executed by the same actor
297 REQUIRE(execution.get_racing_events_of(3) == std::unordered_set<Execution::EventHandle>{});
299 // 1. Events 3 and 4 race
300 // 2. Events 2 and 4 do NOT race since 2 --> 3 --> 4
301 // 3. Events 1 and 4 do NOT race since 1 is independent of 4
302 // 4. Events 0 and 4 do NOT race since 0 --> 2 --> 4
303 REQUIRE(execution.get_racing_events_of(4) == std::unordered_set<Execution::EventHandle>{3});
305 // Events 4 and 5 race; and because everyone before 4 (including 3) either
306 // a) happens-before, b) races, or c) does not race with 4, 4 is the race
307 REQUIRE(execution.get_racing_events_of(5) == std::unordered_set<Execution::EventHandle>{4});
309 // The same logic that applied to event 5 applies to event 6
310 REQUIRE(execution.get_racing_events_of(6) == std::unordered_set<Execution::EventHandle>{5});
312 // The same logic applies, except that this time since events 6 and 7 are run
313 // by the same actor, they don'tt actually race with one another
314 REQUIRE(execution.get_racing_events_of(7) == std::unordered_set<Execution::EventHandle>{});
316 // Event 8 is independent with everything
317 REQUIRE(execution.get_racing_events_of(8) == std::unordered_set<Execution::EventHandle>{});
319 // Event 9 is independent with events 7 and 8; event 6, however, is in race with 9.
320 // The same logic above eliminates events before 6
321 REQUIRE(execution.get_racing_events_of(9) == std::unordered_set<Execution::EventHandle>{6});
324 SECTION("Example 5: Stress testing race detection")
326 const auto e0 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
327 const auto e1 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
328 const auto e2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
329 const auto e3 = std::make_shared<DependentIfSameValueAction>(Transition::Type::UNKNOWN, 2, -10);
330 const auto e4 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
331 const auto e5 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 0);
332 const auto e6 = std::make_shared<DependentIfSameValueAction>(Transition::Type::UNKNOWN, 2, -5);
333 const auto e7 = std::make_shared<DependentIfSameValueAction>(Transition::Type::UNKNOWN, 1, -5);
334 const auto e8 = std::make_shared<DependentIfSameValueAction>(Transition::Type::UNKNOWN, 0, 4);
335 const auto e9 = std::make_shared<DependentIfSameValueAction>(Transition::Type::UNKNOWN, 2, -10);
336 const auto e10 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
338 Execution execution(PartialExecution{e0, e1, e2, e3, e4, e5, e6, e7, e8, e9, e10});
340 // Nothing comes before event 0
341 CHECK(execution.get_racing_events_of(0) == std::unordered_set<Execution::EventHandle>{});
343 // Events 0 and 1 are independent
344 CHECK(execution.get_racing_events_of(1) == std::unordered_set<Execution::EventHandle>{});
346 // Events 1 and 2 are executed by the same actor, even though they are dependent
347 CHECK(execution.get_racing_events_of(2) == std::unordered_set<Execution::EventHandle>{});
349 // Events 2 and 3 are independent while events 1 and 2 are dependent
350 CHECK(execution.get_racing_events_of(3) == std::unordered_set<Execution::EventHandle>{1});
352 // Event 4 is independent with everything so it can never be in a race
353 CHECK(execution.get_racing_events_of(4) == std::unordered_set<Execution::EventHandle>{});
355 // Event 5 is independent with event 4. Since events 2 and 3 are dependent with event 5,
356 // but are independent of each other, both events are in a race with event 5
357 CHECK(execution.get_racing_events_of(5) == std::unordered_set<Execution::EventHandle>{2, 3});
359 // Events 5 and 6 are dependent. Everyone before 5 who's dependent with 5
360 // cannot be in a race with 6; everyone before 5 who's independent with 5
361 // could not race with 6
362 CHECK(execution.get_racing_events_of(6) == std::unordered_set<Execution::EventHandle>{5});
364 // Same goes for event 7 as for 6
365 CHECK(execution.get_racing_events_of(7) == std::unordered_set<Execution::EventHandle>{6});
367 // Events 5 and 8 are both run by the same actor; events in-between are independent
368 CHECK(execution.get_racing_events_of(8) == std::unordered_set<Execution::EventHandle>{});
370 // Event 6 blocks event 9 from racing with event 6
371 CHECK(execution.get_racing_events_of(9) == std::unordered_set<Execution::EventHandle>{});
373 // Event 10 is independent with everything so it can never be in a race
374 CHECK(execution.get_racing_events_of(10) == std::unordered_set<Execution::EventHandle>{});
377 SECTION("Example with many races for one event")
379 const auto e0 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
380 const auto e1 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2);
381 const auto e2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 3);
382 const auto e3 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
383 const auto e4 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 5);
384 const auto e5 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 6);
385 const auto e6 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 7);
387 Execution execution(PartialExecution{e0, e1, e2, e3, e4, e5, e6});
388 REQUIRE(execution.get_racing_events_of(6) == std::unordered_set<Execution::EventHandle>{0, 1, 2, 3, 4, 5});
392 TEST_CASE("simgrid::mc::odpor::Execution: Independence Tests")
394 SECTION("Complete independence")
396 // Every transition is independent with every other and run by different actors. Hopefully
397 // we say that the events are independent with each other...
398 const auto a0 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
399 const auto a1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
400 const auto a2 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
401 const auto a3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 4);
402 const auto a4 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 5);
403 const auto a5 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 6);
404 const auto a6 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 7);
405 const auto a7 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 7);
406 Execution execution(PartialExecution{a0, a1, a2, a3});
408 REQUIRE(execution.is_independent_with_execution_of(PartialExecution{a4, a5}, a6));
409 REQUIRE(execution.is_independent_with_execution_of(PartialExecution{a6, a5}, a1));
410 REQUIRE(execution.is_independent_with_execution_of(PartialExecution{a6, a1}, a0));
411 REQUIRE(Execution().is_independent_with_execution_of(PartialExecution{a7, a7, a1}, a3));
412 REQUIRE(Execution().is_independent_with_execution_of(PartialExecution{a4, a0, a1}, a3));
413 REQUIRE(Execution().is_independent_with_execution_of(PartialExecution{a0, a7, a1}, a2));
415 // In this case, we notice that `a6` and `a7` are executed by the same actor.
416 // Hence, a6 cannot be independent with extending the execution with a4.a5.a7.
417 // Notice that we are treating *a6* as the next step of actor 7 (that is what we
418 // supplied as an argument)
419 REQUIRE_FALSE(execution.is_independent_with_execution_of(PartialExecution{a4, a5, a7}, a6));
422 SECTION("Independence is trivial with an empty extension")
424 REQUIRE(Execution().is_independent_with_execution_of(
425 PartialExecution{}, std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1)));
428 SECTION("Dependencies stopping independence from being possible")
430 const auto a0 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
431 const auto a1 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
432 const auto a2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 3);
433 const auto a3 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
434 const auto a4 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
435 const auto a5 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2);
436 const auto a6 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
437 const auto a7 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
438 const auto a8 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
439 const auto indep = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
440 Execution execution(PartialExecution{a0, a1, a2, a3});
442 // We see that although `a4` comes after `a1` with which it is dependent, it
443 // would come before "a6" in the partial execution `w`, so it would not be independent
444 REQUIRE_FALSE(execution.is_independent_with_execution_of(PartialExecution{a5, a6, a7}, a4));
446 // Removing `a6` from the picture, though, gives us the independence we're looking for.
447 REQUIRE(execution.is_independent_with_execution_of(PartialExecution{a5, a7}, a4));
449 // BUT, we we ask about a transition which is run by the same actor, even if they would be
450 // independent otherwise, we again lose independence
451 REQUIRE_FALSE(execution.is_independent_with_execution_of(PartialExecution{a5, a7, a8}, a4));
453 // This is a more interesting case:
454 // `indep` clearly is independent with the rest of the series, even though
455 // there are dependencies among the other events in the partial execution
456 REQUIRE(Execution().is_independent_with_execution_of(PartialExecution{a1, a6, a7}, indep));
458 // This ensures that independence is trivial with an empty partial execution
459 REQUIRE(execution.is_independent_with_execution_of(PartialExecution{}, a1));
462 SECTION("More interesting dependencies stopping independence")
464 const auto e0 = std::make_shared<DependentIfSameValueAction>(Transition::Type::UNKNOWN, 1, 5);
465 const auto e1 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
466 const auto e2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
467 const auto e3 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2);
468 const auto e4 = std::make_shared<DependentIfSameValueAction>(Transition::Type::UNKNOWN, 3, 5);
469 const auto e5 = std::make_shared<DependentIfSameValueAction>(Transition::Type::UNKNOWN, 4, 4);
470 Execution execution(PartialExecution{e0, e1, e2, e3, e4, e5});
472 SECTION("Action run by same actor disqualifies independence")
474 const auto w_1 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
475 const auto w_2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
476 const auto w_3 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
477 const auto w_4 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 4);
478 const auto w = PartialExecution{w_1, w_2, w_3};
480 const auto actor4_action = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 4);
481 const auto actor4_action2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
483 // Action `actor4_action` is independent with everything EXCEPT the last transition
484 // which is executed by the same actor
485 execution.is_independent_with_execution_of(w, actor4_action);
487 // Action `actor4_action2` is independent with everything
488 // EXCEPT the last transition which is executed by the same actor
489 execution.is_independent_with_execution_of(w, actor4_action);
494 TEST_CASE("simgrid::mc::odpor::Execution: Initials Test")
496 const auto a0 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
497 const auto a1 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
498 const auto a2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 3);
499 const auto a3 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
500 const auto a4 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
501 const auto a5 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2);
502 const auto a6 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
503 const auto a7 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
504 const auto a8 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
505 const auto indep = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
506 Execution execution(PartialExecution{a0, a1, a2, a3});
508 SECTION("Initials trivial with empty executions")
510 // There are no initials for an empty extension since
511 // a requirement is that the actor be contained in the
513 REQUIRE_FALSE(execution.is_initial_after_execution_of(PartialExecution{}, 0));
514 REQUIRE_FALSE(execution.is_initial_after_execution_of(PartialExecution{}, 1));
515 REQUIRE_FALSE(execution.is_initial_after_execution_of(PartialExecution{}, 2));
516 REQUIRE_FALSE(Execution().is_initial_after_execution_of(PartialExecution{}, 0));
517 REQUIRE_FALSE(Execution().is_initial_after_execution_of(PartialExecution{}, 1));
518 REQUIRE_FALSE(Execution().is_initial_after_execution_of(PartialExecution{}, 2));
521 SECTION("The first actor is always an initial")
523 // Even in the case that the action is dependent with every
524 // other, if it is the first action to occur as part of the
525 // extension of the execution sequence, by definition it is
526 // an initial (recall that initials intuitively tell you which
527 // actions can be run starting from an execution `E`; if we claim
528 // to witness `E.w`, then clearly at least the first step of `w` is an initial)
529 REQUIRE(execution.is_initial_after_execution_of(PartialExecution{a3}, a3->aid_));
530 REQUIRE(execution.is_initial_after_execution_of(PartialExecution{a2, a3, a6}, a2->aid_));
531 REQUIRE(execution.is_initial_after_execution_of(PartialExecution{a6, a1, a0}, a6->aid_));
532 REQUIRE(Execution().is_initial_after_execution_of(PartialExecution{a0, a1, a2, a3}, a0->aid_));
533 REQUIRE(Execution().is_initial_after_execution_of(PartialExecution{a5, a2, a8, a7, a6, a0}, a5->aid_));
534 REQUIRE(Execution().is_initial_after_execution_of(PartialExecution{a8, a7, a1}, a8->aid_));
537 SECTION("Example: Disqualified and re-qualified after switching ordering")
539 // Even though actor `2` executes an independent
540 // transition later on, it is blocked since its first transition
541 // is dependent with actor 1's transition
542 REQUIRE_FALSE(Execution().is_initial_after_execution_of(PartialExecution{a1, a5, indep}, 2));
544 // However, if actor 2 executes its independent action first, it DOES become an initial
545 REQUIRE(Execution().is_initial_after_execution_of(PartialExecution{a1, indep, a5}, 2));
548 SECTION("Example: Large partial executions")
550 // The record trace is `1 3 4 4 3 1 4 2`
552 // Actor 1 starts the execution
553 REQUIRE(Execution().is_initial_after_execution_of(PartialExecution{a1, a2, a3, a4, a6, a7, a8, indep}, 1));
555 // Actor 2 all the way at the end is independent with everybody: despite
556 // the tangle that comes before it, we can more it to the front with no issue
557 REQUIRE(Execution().is_initial_after_execution_of(PartialExecution{a1, a2, a3, a4, a6, a7, a8, indep}, 2));
559 // Actor 3 is eliminated since `a1` is dependent with `a2`
560 REQUIRE_FALSE(Execution().is_initial_after_execution_of(PartialExecution{a1, a2, a3, a4, a6, a7, a8, indep}, 3));
562 // Likewise with actor 4
563 REQUIRE_FALSE(Execution().is_initial_after_execution_of(PartialExecution{a1, a2, a3, a4, a6, a7, a8, indep}, 4));
566 SECTION("Example: Stress tests for initials computation")
568 const auto v_1 = std::make_shared<DependentIfSameValueAction>(Transition::Type::UNKNOWN, 1, 3);
569 const auto v_2 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
570 const auto v_3 = std::make_shared<DependentIfSameValueAction>(Transition::Type::UNKNOWN, 2, 3);
571 const auto v_4 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
572 const auto v_5 = std::make_shared<DependentIfSameValueAction>(Transition::Type::UNKNOWN, 3, 8);
573 const auto v_6 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
574 const auto v_7 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
575 const auto v_8 = std::make_shared<DependentIfSameValueAction>(Transition::Type::UNKNOWN, 4, 3);
576 const auto v = PartialExecution{v_1, v_2, v_3, v_4};
578 // Actor 1 being the first actor in the expansion, it is clearly an initial
579 REQUIRE(Execution().is_initial_after_execution_of(v, 1));
581 // Actor 2 can't be switched before actor 1 without creating an trace
582 // that leads to a different state than that of `E.v := ().v := v`
583 REQUIRE_FALSE(Execution().is_initial_after_execution_of(v, 2));
585 // The first action of Actor 3 is independent with what comes before it, so it can
586 // be moved forward. Note that this is the case even though it later executes and action
587 // that's dependent with most everyone else
588 REQUIRE(Execution().is_initial_after_execution_of(v, 3));
590 // Actor 4 is blocked actor 3's second action `v_7`
591 REQUIRE_FALSE(Execution().is_initial_after_execution_of(v, 4));
595 TEST_CASE("simgrid::mc::odpor::Execution: SDPOR Backtracking Simulation")
597 // This test case assumes that each detected race is detected to also
598 // be reversible. For each reversible
599 const auto e0 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
600 const auto e1 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
601 const auto e2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 3);
602 const auto e3 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
603 const auto e4 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
604 const auto e5 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2);
605 const auto e6 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
606 const auto e7 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
610 execution.push_transition(e0);
611 REQUIRE(execution.get_racing_events_of(0) == std::unordered_set<Execution::EventHandle>{});
613 execution.push_transition(e1);
614 REQUIRE(execution.get_racing_events_of(1) == std::unordered_set<Execution::EventHandle>{});
616 // Actor 3, since it starts the extension from event 1, clearly is an initial from there
617 execution.push_transition(e2);
618 REQUIRE(execution.get_racing_events_of(2) == std::unordered_set<Execution::EventHandle>{1});
619 CHECK(execution.get_missing_source_set_actors_from(1, std::unordered_set<aid_t>{}) == std::unordered_set<aid_t>{3});
620 CHECK(execution.get_missing_source_set_actors_from(1, std::unordered_set<aid_t>{4, 5}) ==
621 std::unordered_set<aid_t>{3});
622 CHECK(execution.get_missing_source_set_actors_from(1, std::unordered_set<aid_t>{3}) == std::unordered_set<aid_t>{});
624 // e1 and e3 are in an reversible race. Actor 4 is not hindered from being moved to
625 // the front since e2 is independent with e3; hence, it is an initial
626 execution.push_transition(e3);
627 REQUIRE(execution.get_racing_events_of(3) == std::unordered_set<Execution::EventHandle>{1});
628 CHECK(execution.get_missing_source_set_actors_from(1, std::unordered_set<aid_t>{}) == std::unordered_set<aid_t>{4});
629 CHECK(execution.get_missing_source_set_actors_from(1, std::unordered_set<aid_t>{3, 5}) ==
630 std::unordered_set<aid_t>{4});
631 CHECK(execution.get_missing_source_set_actors_from(1, std::unordered_set<aid_t>{4}) == std::unordered_set<aid_t>{});
633 // e4 is not in a race since e3 is run by the same actor and occurs before e4
634 execution.push_transition(e4);
635 REQUIRE(execution.get_racing_events_of(4) == std::unordered_set<Execution::EventHandle>{});
637 // e5 is independent with everything between e1 and e5, and `proc(e5) == 2`
638 execution.push_transition(e5);
639 REQUIRE(execution.get_racing_events_of(5) == std::unordered_set<Execution::EventHandle>{1});
640 CHECK(execution.get_missing_source_set_actors_from(1, std::unordered_set<aid_t>{}) == std::unordered_set<aid_t>{2});
641 CHECK(execution.get_missing_source_set_actors_from(1, std::unordered_set<aid_t>{4, 5}) ==
642 std::unordered_set<aid_t>{2});
643 CHECK(execution.get_missing_source_set_actors_from(1, std::unordered_set<aid_t>{2}) == std::unordered_set<aid_t>{});
645 // Event 6 has two races: one with event 4 and one with event 5. In the latter race, actor 3 follows
646 // immediately after and so is evidently a source set actor; in the former race, only actor 2 can
647 // be brought to the front of the queue
648 execution.push_transition(e6);
649 REQUIRE(execution.get_racing_events_of(6) == std::unordered_set<Execution::EventHandle>{4, 5});
650 CHECK(execution.get_missing_source_set_actors_from(4, std::unordered_set<aid_t>{}) == std::unordered_set<aid_t>{2});
651 CHECK(execution.get_missing_source_set_actors_from(4, std::unordered_set<aid_t>{6, 7}) ==
652 std::unordered_set<aid_t>{2});
653 CHECK(execution.get_missing_source_set_actors_from(4, std::unordered_set<aid_t>{2}) == std::unordered_set<aid_t>{});
654 CHECK(execution.get_missing_source_set_actors_from(5, std::unordered_set<aid_t>{}) == std::unordered_set<aid_t>{3});
655 CHECK(execution.get_missing_source_set_actors_from(5, std::unordered_set<aid_t>{6, 7}) ==
656 std::unordered_set<aid_t>{3});
657 CHECK(execution.get_missing_source_set_actors_from(5, std::unordered_set<aid_t>{3}) == std::unordered_set<aid_t>{});
659 // Finally, event e7 races with e6 and `proc(e7) = 1` is brought forward
660 execution.push_transition(e7);
661 REQUIRE(execution.get_racing_events_of(7) == std::unordered_set<Execution::EventHandle>{6});
662 CHECK(execution.get_missing_source_set_actors_from(1, std::unordered_set<aid_t>{}) == std::unordered_set<aid_t>{1});
663 CHECK(execution.get_missing_source_set_actors_from(1, std::unordered_set<aid_t>{4, 5}) ==
664 std::unordered_set<aid_t>{1});
665 CHECK(execution.get_missing_source_set_actors_from(1, std::unordered_set<aid_t>{1}) == std::unordered_set<aid_t>{});
668 TEST_CASE("simgrid::mc::odpor::Execution: ODPOR Smallest Sequence Tests")
670 const auto a0 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
671 const auto a1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 4);
672 const auto a2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 3);
673 const auto a3 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
674 const auto a4 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
675 const auto a5 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
678 execution.push_transition(a0);
679 execution.push_transition(a1);
680 execution.push_transition(a2);
681 execution.push_transition(a3);
682 execution.push_transition(a4);
683 execution.push_transition(a5);
685 SECTION("Equivalent insertions")
687 SECTION("Example: Eliminated through independence")
689 // TODO: Is this even a sensible question to ask if the two sequences
690 // don't agree upon what each actor executed after `E`?
691 const auto insertion =
692 Execution().get_shortest_odpor_sq_subset_insertion(PartialExecution{a1, a2}, PartialExecution{a2, a5});
693 REQUIRE(insertion.has_value());
694 REQUIRE(insertion.value() == PartialExecution{});
697 SECTION("Exact match yields empty set")
699 const auto insertion =
700 Execution().get_shortest_odpor_sq_subset_insertion(PartialExecution{a1, a2}, PartialExecution{a1, a2});
701 REQUIRE(insertion.has_value());
702 REQUIRE(insertion.value() == PartialExecution{});
706 SECTION("Match against empty executions")
708 SECTION("Empty `v` trivially yields `w`")
711 Execution().get_shortest_odpor_sq_subset_insertion(PartialExecution{}, PartialExecution{a1, a5, a2});
712 REQUIRE(insertion.has_value());
713 REQUIRE(insertion.value() == PartialExecution{a1, a5, a2});
715 insertion = execution.get_shortest_odpor_sq_subset_insertion(PartialExecution{}, PartialExecution{a1, a5, a2});
716 REQUIRE(insertion.has_value());
717 REQUIRE(insertion.value() == PartialExecution{a1, a5, a2});
720 SECTION("Empty `w` yields empty execution")
723 Execution().get_shortest_odpor_sq_subset_insertion(PartialExecution{a1, a4, a5}, PartialExecution{});
724 REQUIRE(insertion.has_value());
725 REQUIRE(insertion.value() == PartialExecution{});
727 insertion = execution.get_shortest_odpor_sq_subset_insertion(PartialExecution{a1, a5, a2}, PartialExecution{});
728 REQUIRE(insertion.has_value());
729 REQUIRE(insertion.value() == PartialExecution{});