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/WakeupTree.hpp"
9 #include "src/mc/explo/udpor/udpor_tests_private.hpp"
10 #include "src/xbt/utils/iter/LazyPowerset.hpp"
12 using namespace simgrid::mc;
13 using namespace simgrid::mc::odpor;
14 using namespace simgrid::mc::udpor;
16 static void test_tree_iterator(const WakeupTree& tree, const std::vector<PartialExecution>& expected)
18 uint64_t num_nodes_traversed = 0;
19 auto tree_iter = tree.begin();
20 for (auto expected_iter = expected.begin(); expected_iter != expected.end();
21 ++expected_iter, ++tree_iter, ++num_nodes_traversed) {
22 REQUIRE(tree_iter != tree.end());
23 REQUIRE((*tree_iter)->get_sequence() == *expected_iter);
25 REQUIRE(num_nodes_traversed == tree.get_num_nodes());
28 static void test_tree_empty(const WakeupTree& tree)
30 REQUIRE(tree.empty());
31 REQUIRE(tree.get_num_entries() == 0);
32 REQUIRE(tree.get_num_nodes() == 1);
33 REQUIRE_FALSE(tree.get_min_single_process_node().has_value());
34 REQUIRE_FALSE(tree.get_min_single_process_actor().has_value());
35 test_tree_iterator(tree, std::vector<PartialExecution>{PartialExecution{}});
38 TEST_CASE("simgrid::mc::odpor::WakeupTree: Constructing Trees")
40 SECTION("Constructing empty trees")
42 test_tree_empty(WakeupTree());
45 SECTION("Testing subtree creation and manipulation")
47 // Here, we make everything dependent. This will ensure that each unique sequence
48 // inserted into the tree never "eventually looks like"
49 const auto a0 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
50 const auto a1 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
51 const auto a2 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
52 const auto a3 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 4);
53 const auto a4 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 5);
54 const auto a5 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 6);
57 execution.push_transition(a0);
58 execution.push_transition(a1);
59 execution.push_transition(a2);
60 execution.push_transition(a3);
61 execution.push_transition(a4);
62 execution.push_transition(a5);
64 // The tree is as follows:
75 // Recall that new nodes (in this case the one with
76 // action `a2`) are added such that they are "greater than" (under
77 // the tree's `<` relation) all those that exist under the given parent
79 tree.insert(Execution(), {a1, a2, a3, a4});
80 tree.insert(Execution(), {a1, a3, a2, a4});
81 tree.insert(Execution(), {a1, a3, a2, a4, a5});
82 tree.insert(Execution(), {a1, a3, a5});
83 tree.insert(Execution(), {a4, a2, a1, a3});
84 REQUIRE(tree.get_num_nodes() == 13);
85 test_tree_iterator(tree, std::vector<PartialExecution>{
86 PartialExecution{a1, a2, a3, a4}, PartialExecution{a1, a2, a3},
87 PartialExecution{a1, a2}, PartialExecution{a1, a3, a2, a4},
88 PartialExecution{a1, a3, a2}, PartialExecution{a1, a3, a5}, PartialExecution{a1, a3},
89 PartialExecution{a1}, PartialExecution{a4, a2, a1, a3}, PartialExecution{a4, a2, a1},
90 PartialExecution{a4, a2}, PartialExecution{a4}, PartialExecution{}});
92 SECTION("Cloning a tree from the root produces the same tree")
94 // The root node is the last node
95 auto tree_root = tree.begin();
96 std::advance(tree_root, tree.get_num_nodes() - 1);
98 WakeupTree clone = WakeupTree::make_subtree_rooted_at(*tree_root);
99 REQUIRE(clone.empty() == tree.empty());
100 REQUIRE(clone.get_num_entries() == tree.get_num_entries());
101 REQUIRE(clone.get_num_nodes() == tree.get_num_nodes());
103 auto tree_iter = tree.begin();
104 for (auto clone_iter = clone.begin(); clone_iter != clone.end(); ++clone_iter, ++tree_iter) {
105 REQUIRE(tree_iter != tree.end());
106 REQUIRE((*tree_iter)->get_sequence() == (*clone_iter)->get_sequence());
110 SECTION("Cloning a subtree from a leaf gives an empty tree")
112 // Let's pick the first leaf
113 WakeupTree clone = WakeupTree::make_subtree_rooted_at(*tree.begin());
114 REQUIRE(clone.empty());
115 REQUIRE(clone.get_num_entries() == 0);
116 REQUIRE(clone.get_num_nodes() == 1);
119 SECTION("Cloning a subtree from an interior node gives the subtree underneath")
121 // Here, we pick the second-to-last node in the
122 // series, which is the right-most child of the root
123 auto right_most = tree.begin();
124 std::advance(right_most, tree.get_num_nodes() - 2);
126 WakeupTree clone = WakeupTree::make_subtree_rooted_at(*right_most);
127 REQUIRE_FALSE(clone.empty());
128 REQUIRE(clone.get_num_entries() == 3);
129 REQUIRE(clone.get_num_nodes() == 4);
130 // Importantly, note that action `a4` is not included in
131 // any of the executions; for in the subtree `clone` `a4`
133 test_tree_iterator(clone, std::vector<PartialExecution>{PartialExecution{a2, a1, a3}, PartialExecution{a2, a1},
134 PartialExecution{a2}, PartialExecution{}});
137 SECTION("Removing the first single-process subtree")
139 // Prior to removal, the first `a1` was the first single-process node
140 REQUIRE(tree.get_min_single_process_node().has_value());
141 REQUIRE(tree.get_min_single_process_actor().has_value());
142 REQUIRE(tree.get_min_single_process_actor().value() == a1->aid_);
144 tree.remove_min_single_process_subtree();
146 // Now the first `a4` is
147 REQUIRE(tree.get_min_single_process_node().has_value());
148 REQUIRE(tree.get_min_single_process_actor().has_value());
149 REQUIRE(tree.get_min_single_process_actor().value() == a4->aid_);
151 REQUIRE(tree.get_num_nodes() == 5);
152 test_tree_iterator(tree, std::vector<PartialExecution>{PartialExecution{a4, a2, a1, a3},
153 PartialExecution{a4, a2, a1}, PartialExecution{a4, a2},
154 PartialExecution{a4}, PartialExecution{}});
155 tree.remove_min_single_process_subtree();
157 // At this point, we've removed each single-process subtree, so
158 // the tree should be empty
159 REQUIRE(tree.empty());
162 SECTION("Removing the first single-process subtree from an empty tree has no effect")
164 WakeupTree empty_tree;
165 test_tree_empty(empty_tree);
167 empty_tree.remove_min_single_process_subtree();
169 // There should be no effect: the tree should still be empty
170 // and the function should have no effect
171 test_tree_empty(empty_tree);
176 TEST_CASE("simgrid::mc::odpor::WakeupTree: Testing Insertion for Empty Executions")
178 SECTION("Following an execution")
180 // We imagine the following completed execution `E`
181 // consisting of executing actions a0-a3. Execution
182 // `E` is the first such maximal execution explored
183 // by ODPOR, which implies that a) all sleep sets are
184 // empty and b) all wakeup trees (i.e. for each prefix) consist of the root
185 // node with a single leaf containing the action
186 // taken, save for the wakeup tree of the execution itself
189 // We first notice that there's a reversible race between
192 const auto a0 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
193 const auto a1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 4);
194 const auto a2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
195 const auto a3 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
196 const auto a4 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
199 execution.push_transition(a0);
200 execution.push_transition(a1);
201 execution.push_transition(a2);
202 execution.push_transition(a3);
203 execution.push_transition(a4);
205 REQUIRE(execution.get_racing_events_of(2) == std::unordered_set<Execution::EventHandle>{0});
206 REQUIRE(execution.get_racing_events_of(3) == std::unordered_set<Execution::EventHandle>{0});
210 SECTION("Attempting to insert the empty sequence into an empty tree should have no effect")
212 tree.insert(Execution(), {});
213 test_tree_iterator(tree, std::vector<PartialExecution>{PartialExecution{}});
216 // First, we initialize the tree to how it looked prior
217 // to the insertion of the race.
218 tree.insert(Execution(), {a0});
220 // Then, after insertion, we ensure that the node was
221 // indeed added to the tree.
222 tree.insert(Execution(), {a1, a3});
223 test_tree_iterator(tree, std::vector<PartialExecution>{PartialExecution{a0}, PartialExecution{a1, a3},
224 PartialExecution{a1}, PartialExecution{}});
226 SECTION("Attempting to re-insert the same EXACT sequence should have no effect")
228 tree.insert(Execution(), {a1, a3});
229 test_tree_iterator(tree, std::vector<PartialExecution>{PartialExecution{a0}, PartialExecution{a1, a3},
230 PartialExecution{a1}, PartialExecution{}});
233 SECTION("Attempting to re-insert an equivalent sequence should have no effect")
235 // a3 and a1 are interchangeable since `a1` is independent with everything.
236 // Since we found an equivalent sequence that is a leaf, nothing should result..
237 tree.insert(Execution(), {a3, a1});
238 test_tree_iterator(tree, std::vector<PartialExecution>{PartialExecution{a0}, PartialExecution{a1, a3},
239 PartialExecution{a1}, PartialExecution{}});
242 SECTION("Attempting to insert the empty sequence should have no effect")
244 tree.insert(Execution(), {});
245 test_tree_iterator(tree, std::vector<PartialExecution>{PartialExecution{a0}, PartialExecution{a1, a3},
246 PartialExecution{a1}, PartialExecution{}});
249 SECTION("Inserting an extension should create a branch point")
251 // `a1.a2` shares the same `a1` prefix as `a1.a3`. Thus, the tree
252 // should now look as follows:
260 // Recall that new nodes (in this case the one with
261 // action `a2`) are added such that they are "greater than" (under
262 // the tree's `<` relation) all those that exist under the given parent.
263 tree.insert(Execution(), {a1, a4});
264 test_tree_iterator(tree, std::vector<PartialExecution>{PartialExecution{a0}, PartialExecution{a1, a3},
265 PartialExecution{a1, a4}, PartialExecution{a1},
266 PartialExecution{}});
269 SECTION("Inserting an equivalent sequence to a leaf should preserve the tree as-is")
271 // `a1.a2` is equivalent to `a1.a3` since `a2` and `a3` are independent
272 // (`E ⊢ p ◊ w` where `p := proc(a2)` and `w := a3`). Thus, the tree
273 // should now STILL look as follows:
281 // Recall that new nodes (in this case the one with
282 // action `a2`) are added such that they are "greater than" (under
283 // the tree's `<` relation) all those that exist under the given parent.
284 tree.insert(Execution(), {a1, a3});
285 test_tree_iterator(tree, std::vector<PartialExecution>{PartialExecution{a0}, PartialExecution{a1, a3},
286 PartialExecution{a1}, PartialExecution{}});
290 SECTION("Performing Arbitrary Insertions")
292 const auto a0 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
293 const auto a1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 4);
294 const auto a2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 3);
295 const auto a3 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
296 const auto a4 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
297 const auto a5 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
300 SECTION("Attempting to insert the empty sequence into an empty tree should have no effect")
302 tree.insert(Execution(), {});
303 test_tree_iterator(tree, std::vector<PartialExecution>{PartialExecution{}});
306 SECTION("Attempting to re-insert the same sequence multiple times should have no extra effect")
308 tree.insert(Execution(), {a4});
309 tree.insert(Execution(), {a4});
310 tree.insert(Execution(), {a4});
311 REQUIRE(tree.get_num_nodes() == 2);
312 test_tree_iterator(tree, std::vector<PartialExecution>{PartialExecution{a4}, PartialExecution{}});
315 SECTION("Attempting to insert an independent sequence same should have no extra effect")
317 // a4 and a1 are independent actions. Intuitively, then, we need only
318 // search one ordering of the two actions. The wakeup tree handles
319 // this by computing the `~` relation. The relation itself determines
320 // whether the `a1` is an initial of `a3`, which it is not. It then
321 // checks whether `a1` is independent with everything in the sequence
322 // (in this case, consisting only of `a1`) which IS true. Since `a4`
323 // is already a leaf node of the tree, it suffices to only have `a4`
324 // in this tree to guide ODPOR.
325 tree.insert(Execution(), {a4});
326 tree.insert(Execution(), {a1});
327 REQUIRE(tree.get_num_nodes() == 2);
328 test_tree_iterator(tree, std::vector<PartialExecution>{PartialExecution{a4}, PartialExecution{}});
332 "Attempting to insert a progression of executions should have no extra effect when the first process is a leaf")
334 // All progressions starting with `a0` are effectively already accounted
335 // for by inserting `a0` since we `a0` "can always be made to look like"
336 // (viz. the `~` relation) `a0.*` where `*` is some sequence of actions
337 tree.insert(Execution(), {a0});
338 tree.insert(Execution(), {a0, a3});
339 tree.insert(Execution(), {a0, a3, a2});
340 tree.insert(Execution(), {a0, a3, a2, a4});
341 tree.insert(Execution(), {a0, a3, a2, a4});
342 REQUIRE(tree.get_num_nodes() == 2);
343 test_tree_iterator(tree, std::vector<PartialExecution>{PartialExecution{a0}, PartialExecution{}});
346 SECTION("Stress test with multiple branch points: `~_E` with different looking sequences")
348 // After the insertions below, the tree looks like the following:
354 tree.insert(Execution(), {a0});
355 tree.insert(Execution(), {a2, a0});
356 tree.insert(Execution(), {a2, a3});
357 tree.insert(Execution(), {a2, a5});
358 REQUIRE(tree.get_num_nodes() == 6);
359 test_tree_iterator(tree, std::vector<PartialExecution>{PartialExecution{a0}, PartialExecution{a2, a0},
360 PartialExecution{a2, a3}, PartialExecution{a2, a5},
361 PartialExecution{a2}, PartialExecution{}});
362 SECTION("Adding more stress")
364 // In this case, `a2` and `a1` can be interchanged with each other.
365 // Thus `a2.a1 == a1.a2`. Since there is already an interior node
366 // containing `a2`, we attempt to add the what remains (viz. `a1`) to the
367 // series. HOWEVER: we notice that `a2.a5` is "eventually equivalent to"
368 // (that is `~` with) `a1.a2` since `a2` is an initial of the latter and
369 // `a1` and `a5` are independent of each other.
370 tree.insert(Execution(), {a1, a2});
371 REQUIRE(tree.get_num_nodes() == 6);
372 test_tree_iterator(tree, std::vector<PartialExecution>{PartialExecution{a0}, PartialExecution{a2, a0},
373 PartialExecution{a2, a3}, PartialExecution{a2, a5},
374 PartialExecution{a2}, PartialExecution{}});
376 // With a3.a0, we notice that starting a sequence with `a3` is
377 // always different than starting one with either `a0` or
379 // After the insertion, the tree looks like the following:
385 tree.insert(Execution(), {a3, a0});
386 REQUIRE(tree.get_num_nodes() == 8);
387 test_tree_iterator(tree, std::vector<PartialExecution>{PartialExecution{a0}, PartialExecution{a2, a0},
388 PartialExecution{a2, a3}, PartialExecution{a2, a5},
389 PartialExecution{a2}, PartialExecution{a3, a0},
390 PartialExecution{a3}, PartialExecution{}});
395 SECTION("Insertion with more subtle equivalents")
397 const auto cd_1 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
398 const auto i_2 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
399 const auto i_3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
400 const auto d_1 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
401 const auto d_2 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
402 WakeupTree complex_tree;
403 // After the insertions below, the tree looks like the following:
418 // d_1.i_3.d_2 is equivalent to i_3.d_2.d_1
419 complex_tree.insert(Execution(), {cd_1, i_2, d_1, i_3, d_2, d_2});
420 complex_tree.insert(Execution(), {i_2, d_2, cd_1, d_1, i_3, d_2});
421 complex_tree.insert(Execution(), {i_2, d_2, cd_1, i_3, d_2, d_1});
422 REQUIRE(complex_tree.get_num_nodes() == 16);
423 test_tree_iterator(complex_tree, std::vector<PartialExecution>{{cd_1, i_2, d_1, i_3, d_2, d_2},
424 {cd_1, i_2, d_1, i_3, d_2},
425 {cd_1, i_2, d_1, i_3},
429 {i_2, d_2, cd_1, d_1, i_3, d_2},
430 {i_2, d_2, cd_1, d_1, i_3},
431 {i_2, d_2, cd_1, d_1},
432 {i_2, d_2, cd_1, i_3, d_2, d_1},
433 {i_2, d_2, cd_1, i_3, d_2},
434 {i_2, d_2, cd_1, i_3},
439 // Here we note that the sequence that we are attempting to insert, viz.
441 // i_3.i_2.d_2.cd_1.d_2.d_1
443 // is already equivalent to
445 // i_2.d_2.cd_1.i_3.d_2.d_1
446 complex_tree.insert(Execution(), {i_3, i_2, d_2, cd_1, d_2, d_1});
447 REQUIRE(complex_tree.get_num_nodes() == 16);
449 // Here we note that the sequence that we are attempting to insert, viz.
451 // i_2.d_2.cd_1.d_1.i_3
453 // is already equivalent to
455 // i_2.d_2.cd_1.i_3.d_2.d_1
456 complex_tree.insert(Execution(), {i_2, d_2, cd_1, d_1, i_3});
457 REQUIRE(complex_tree.get_num_nodes() == 16);
459 // Here we note that the sequence that we are attempting to insert, viz.
463 // is accounted for by an interior node of the tree. Since there is no
464 // "extra" portions that are different from what is already
465 // contained in the tree, nothing is added and the tree stays the same
466 complex_tree.insert(Execution(), {i_2, d_2, cd_1});
467 REQUIRE(complex_tree.get_num_nodes() == 16);