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/udpor/udpor_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.get());
36 execution.push_transition(a2.get());
37 execution.push_transition(a3.get());
38 execution.push_transition(a4.get());
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.get());
82 execution.push_transition(a2.get());
83 execution.push_transition(a3.get());
84 execution.push_transition(a4.get());
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));
116 TEST_CASE("simgrid::mc::odpor::Execution: Testing Racing Events and Initials")
120 const auto a1 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
121 const auto a2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2);
122 const auto a3 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
123 const auto a4 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
124 const auto a5 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
127 execution.push_transition(a1.get());
128 execution.push_transition(a2.get());
129 execution.push_transition(a3.get());
130 execution.push_transition(a4.get());
131 execution.push_transition(a5.get());
133 // Nothing comes before event 0
134 REQUIRE(execution.get_racing_events_of(0) == std::unordered_set<Execution::EventHandle>{});
136 // Events 0 and 1 are independent
137 REQUIRE(execution.get_racing_events_of(1) == std::unordered_set<Execution::EventHandle>{});
139 // 2 and 1 are executed by different actors and happen right after each other
140 REQUIRE(execution.get_racing_events_of(2) == std::unordered_set<Execution::EventHandle>{1});
142 // Although a3 and a4 are dependent, they are executed by the same actor
143 REQUIRE(execution.get_racing_events_of(3) == std::unordered_set<Execution::EventHandle>{});
145 // Event 4 is in a race with neither event 0 nor event 2 since those events
146 // "happen-before" event 3 with which event 4 races
148 // Furthermore, event 1 is run by the same actor and thus also is not in a race.
149 // Hence, only event 3 races with event 4
150 REQUIRE(execution.get_racing_events_of(4) == std::unordered_set<Execution::EventHandle>{3});
153 SECTION("Example 2: Events with multiple races")
155 const auto a1 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
156 const auto a2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2);
157 const auto a3 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
158 const auto a4 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
161 execution.push_transition(a1.get());
162 execution.push_transition(a2.get());
163 execution.push_transition(a3.get());
164 execution.push_transition(a4.get());
166 // Nothing comes before event 0
167 REQUIRE(execution.get_racing_events_of(0) == std::unordered_set<Execution::EventHandle>{});
169 // Events 0 and 1 are independent
170 REQUIRE(execution.get_racing_events_of(1) == std::unordered_set<Execution::EventHandle>{});
172 // Event 2 is independent with event 1 and run by the same actor as event 0
173 REQUIRE(execution.get_racing_events_of(2) == std::unordered_set<Execution::EventHandle>{});
175 // All events are dependent with event 3, but event 0 "happens-before" event 2
176 REQUIRE(execution.get_racing_events_of(3) == std::unordered_set<Execution::EventHandle>{1, 2});
178 SECTION("Check initials with respect to event 1")
180 // First, note that v := notdep(1, execution).p == {e2}.{e3} == {e2, e3}
181 // Since e2 -->_E e3, actor 3 is not an initial for E' := pre(1, execution)
182 // with respect to `v`. e2, however, has nothing happening before it in dom_E(v),
183 // so it is an initial of E' wrt. `v`
184 const auto initial_wrt_event1 = execution.get_first_sdpor_initial_from(1, std::unordered_set<aid_t>{});
185 REQUIRE(initial_wrt_event1.has_value());
186 REQUIRE(initial_wrt_event1.value() == static_cast<aid_t>(1));
189 SECTION("Check initials with respect to event 2")
191 // First, note that v := notdep(1, execution).p == {}.{e3} == {e3}
192 // e3 has nothing happening before it in dom_E(v), so it is an initial
194 const auto initial_wrt_event2 = execution.get_first_sdpor_initial_from(2, std::unordered_set<aid_t>{});
195 REQUIRE(initial_wrt_event2.has_value());
196 REQUIRE(initial_wrt_event2.value() == static_cast<aid_t>(3));
200 SECTION("Example 3: Testing 'Lock' Example")
203 const auto a1 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
204 const auto a2 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
205 const auto a3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
206 const auto a4 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
207 const auto a5 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
210 execution.push_transition(a1.get());
211 execution.push_transition(a2.get());
212 execution.push_transition(a3.get());
213 execution.push_transition(a4.get());
214 execution.push_transition(a5.get());
216 REQUIRE(execution.get_racing_events_of(4) == std::unordered_set<Execution::EventHandle>{0});
219 SECTION("Example 4: Indirect Races")
221 const auto a0 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
222 const auto a1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
223 const auto a2 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
224 const auto a3 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
225 const auto a4 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 6);
226 const auto a5 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
227 const auto a6 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
228 const auto a7 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 3);
229 const auto a8 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 4);
230 const auto a9 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2);
233 execution.push_transition(a0.get());
234 execution.push_transition(a1.get());
235 execution.push_transition(a2.get());
236 execution.push_transition(a3.get());
237 execution.push_transition(a4.get());
238 execution.push_transition(a5.get());
239 execution.push_transition(a6.get());
240 execution.push_transition(a7.get());
241 execution.push_transition(a8.get());
242 execution.push_transition(a9.get());
244 // Nothing comes before event 0
245 REQUIRE(execution.get_racing_events_of(0) == std::unordered_set<Execution::EventHandle>{});
247 // Events 0 and 1 are independent
248 REQUIRE(execution.get_racing_events_of(1) == std::unordered_set<Execution::EventHandle>{});
250 // Events 1 and 2 are independent
251 REQUIRE(execution.get_racing_events_of(2) == std::unordered_set<Execution::EventHandle>{});
253 // Events 1 and 3 are independent; the rest are executed by the same actor
254 REQUIRE(execution.get_racing_events_of(3) == std::unordered_set<Execution::EventHandle>{});
256 // 1. Events 3 and 4 race
257 // 2. Events 2 and 4 do NOT race since 2 --> 3 --> 4
258 // 3. Events 1 and 4 do NOT race since 1 is independent of 4
259 // 4. Events 0 and 4 do NOT race since 0 --> 2 --> 4
260 REQUIRE(execution.get_racing_events_of(4) == std::unordered_set<Execution::EventHandle>{3});
262 // Events 4 and 5 race; and because everyone before 4 (including 3) either
263 // a) happens-before, b) races, or c) does not race with 4, 4 is the race
264 REQUIRE(execution.get_racing_events_of(5) == std::unordered_set<Execution::EventHandle>{4});
266 // The same logic that applied to event 5 applies to event 6
267 REQUIRE(execution.get_racing_events_of(6) == std::unordered_set<Execution::EventHandle>{5});
269 // The same logic applies, except that this time since events 6 and 7 are run
270 // by the same actor, they don'tt actually race with one another
271 REQUIRE(execution.get_racing_events_of(7) == std::unordered_set<Execution::EventHandle>{});
273 // Event 8 is independent with everything
274 REQUIRE(execution.get_racing_events_of(8) == std::unordered_set<Execution::EventHandle>{});
276 // Event 9 is independent with events 7 and 8; event 6, however, is in race with 9.
277 // The same logic above eliminates events before 6
278 REQUIRE(execution.get_racing_events_of(9) == std::unordered_set<Execution::EventHandle>{6});