src/mc/explo/odpor/Execution_test.cpp

   1 /* Copyright (c) 2017-2023. The SimGrid Team. All rights reserved.               */
   2
   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. */
   5
   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"
  10
  11 using namespace simgrid::mc;
  12 using namespace simgrid::mc::odpor;
  13 using namespace simgrid::mc::udpor;
  14
  15 TEST_CASE("simgrid::mc::odpor::Execution: Constructing Executions")
  16 {
  17   Execution execution;
  18   REQUIRE(execution.empty());
  19   REQUIRE(execution.size() == 0);
  20   REQUIRE_FALSE(execution.get_latest_event_handle().has_value());
  21 }
  22
  23 TEST_CASE("simgrid::mc::odpor::Execution: Testing Happens-Before")
  24 {
  25   SECTION("Example 1")
  26   {
  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);
  33
  34     Execution execution;
  35     execution.push_transition(a1);
  36     execution.push_transition(a2);
  37     execution.push_transition(a3);
  38     execution.push_transition(a4);
  39
  40     SECTION("Happens-before is irreflexive")
  41     {
  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));
  46     }
  47
  48     SECTION("Happens-before values for each pair of events")
  49     {
  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));
  56     }
  57
  58     SECTION("Happens-before is a subset of 'occurs-before' ")
  59     {
  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));
  66     }
  67   }
  68
  69   SECTION("Example 2")
  70   {
  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);
  75
  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"
  78     // the another
  79
  80     Execution execution;
  81     execution.push_transition(a1);
  82     execution.push_transition(a2);
  83     execution.push_transition(a3);
  84     execution.push_transition(a4);
  85
  86     SECTION("Happens-before is irreflexive")
  87     {
  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));
  92     }
  93
  94     SECTION("Happens-before values for each pair of events")
  95     {
  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));
 102     }
 103
 104     SECTION("Happens-before is a subset of 'occurs-before'")
 105     {
 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));
 112     }
 113   }
 114 }
 115
 116 TEST_CASE("simgrid::mc::odpor::Execution: Testing Racing Events and Initials")
 117 {
 118   SECTION("Example 1")
 119   {
 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);
 125
 126     Execution execution;
 127     execution.push_transition(a1);
 128     execution.push_transition(a2);
 129     execution.push_transition(a3);
 130     execution.push_transition(a4);
 131     execution.push_transition(a5);
 132
 133     // Nothing comes before event 0
 134     REQUIRE(execution.get_racing_events_of(0) == std::unordered_set<Execution::EventHandle>{});
 135
 136     // Events 0 and 1 are independent
 137     REQUIRE(execution.get_racing_events_of(1) == std::unordered_set<Execution::EventHandle>{});
 138
 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});
 141
 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>{});
 144
 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
 147     //
 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});
 151   }
 152
 153   SECTION("Example 2: Events with multiple races")
 154   {
 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);
 159
 160     Execution execution;
 161     execution.push_transition(a1);
 162     execution.push_transition(a2);
 163     execution.push_transition(a3);
 164     execution.push_transition(a4);
 165
 166     // Nothing comes before event 0
 167     REQUIRE(execution.get_racing_events_of(0) == std::unordered_set<Execution::EventHandle>{});
 168
 169     // Events 0 and 1 are independent
 170     REQUIRE(execution.get_racing_events_of(1) == std::unordered_set<Execution::EventHandle>{});
 171
 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>{});
 174
 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});
 177
 178     SECTION("Check initials with respect to event 1")
 179     {
 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));
 187     }
 188
 189     SECTION("Check initials with respect to event 2")
 190     {
 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
 193       // of E' wrt. `v`
 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));
 197     }
 198   }
 199
 200   SECTION("Example 3: Testing 'Lock' Example")
 201   {
 202     // In this 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);
 208
 209     Execution execution;
 210     execution.push_transition(a1);
 211     execution.push_transition(a2);
 212     execution.push_transition(a3);
 213     execution.push_transition(a4);
 214     execution.push_transition(a5);
 215
 216     REQUIRE(execution.get_racing_events_of(4) == std::unordered_set<Execution::EventHandle>{0});
 217   }
 218
 219   SECTION("Example 4: Indirect Races")
 220   {
 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);
 231
 232     Execution execution;
 233     execution.push_transition(a0);
 234     execution.push_transition(a1);
 235     execution.push_transition(a2);
 236     execution.push_transition(a3);
 237     execution.push_transition(a4);
 238     execution.push_transition(a5);
 239     execution.push_transition(a6);
 240     execution.push_transition(a7);
 241     execution.push_transition(a8);
 242     execution.push_transition(a9);
 243
 244     // Nothing comes before event 0
 245     REQUIRE(execution.get_racing_events_of(0) == std::unordered_set<Execution::EventHandle>{});
 246
 247     // Events 0 and 1 are independent
 248     REQUIRE(execution.get_racing_events_of(1) == std::unordered_set<Execution::EventHandle>{});
 249
 250     // Events 1 and 2 are independent
 251     REQUIRE(execution.get_racing_events_of(2) == std::unordered_set<Execution::EventHandle>{});
 252
 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>{});
 255
 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});
 261
 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});
 265
 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});
 268
 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>{});
 272
 273     // Event 8 is independent with everything
 274     REQUIRE(execution.get_racing_events_of(8) == std::unordered_set<Execution::EventHandle>{});
 275
 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});
 279   }
 280 }
 281
 282 TEST_CASE("simgrid::mc::odpor::Execution: Testing Races and Conditions")
 283 {
 284   const auto a1 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
 285   const auto a2 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
 286   const auto a3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
 287   const auto a4 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
 288   const auto a5 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
 289
 290   Execution execution;
 291   execution.push_transition(a1);
 292   execution.push_transition(a2);
 293   execution.push_transition(a3);
 294   execution.push_transition(a4);
 295   execution.push_transition(a5);
 296 }
 297
 298 TEST_CASE("simgrid::mc::odpor::Execution: Independence Tests")
 299 {
 300   SECTION("Complete independence")
 301   {
 302     // Every transition is independent with every other and run by different actors. Hopefully
 303     // we say that the events are independent with each other...
 304     const auto a0 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
 305     const auto a1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
 306     const auto a2 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
 307     const auto a3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 4);
 308     const auto a4 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 5);
 309     const auto a5 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 6);
 310     const auto a6 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 7);
 311     const auto a7 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 7);
 312     Execution execution;
 313     execution.push_transition(a0);
 314     execution.push_transition(a1);
 315     execution.push_transition(a2);
 316     execution.push_transition(a3);
 317
 318     REQUIRE(execution.is_independent_with_execution_of(PartialExecution{a4, a5}, a6));
 319
 320     // In this case, we notice that `a6` and `a7` are executed by the same actor.
 321     // Hence, a6 cannot be independent with extending the execution with a4.a5.a7.
 322     // Notice that we are treating *a6* as the next step of actor 7 (that is what we
 323     // supplied as an argument)
 324     REQUIRE_FALSE(execution.is_independent_with_execution_of(PartialExecution{a4, a5, a7}, a6));
 325   }
 326
 327   SECTION("Dependencies stopping independence from being possible")
 328   {
 329     const auto a0    = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
 330     const auto a1    = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
 331     const auto a2    = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 3);
 332     const auto a3    = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
 333     const auto a4    = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
 334     const auto a5    = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2);
 335     const auto a6    = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
 336     const auto a7    = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
 337     const auto a8    = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
 338     const auto indep = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
 339     Execution execution;
 340     execution.push_transition(a0);
 341     execution.push_transition(a1);
 342     execution.push_transition(a2);
 343     execution.push_transition(a3);
 344
 345     // We see that although `a4` comes after `a1` with which it is dependent, it
 346     // would come before "a6" in the partial execution `w`, so it would not be independent
 347     REQUIRE_FALSE(execution.is_independent_with_execution_of(PartialExecution{a5, a6, a7}, a4));
 348
 349     // Removing `a6` from the picture, though, gives us the independence we're looking for.
 350     REQUIRE(execution.is_independent_with_execution_of(PartialExecution{a5, a7}, a4));
 351
 352     // BUT, we we ask about a transition which is run by the same actor, even if they would be
 353     // independent otherwise, we again lose independence
 354     REQUIRE_FALSE(execution.is_independent_with_execution_of(PartialExecution{a5, a7, a8}, a4));
 355
 356     // This is a more interesting case:
 357     // `indep` clearly is independent with the rest of the series, even though
 358     // there are dependencies among the other events in the partial execution
 359     REQUIRE(Execution().is_independent_with_execution_of(PartialExecution{a1, a6, a7}, indep));
 360   }
 361 }
 362
 363 TEST_CASE("simgrid::mc::odpor::Execution: ODPOR Smallest Sequence Tests")
 364 {
 365   const auto a0 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
 366   const auto a1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 4);
 367   const auto a2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 3);
 368   const auto a3 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
 369   const auto a4 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
 370   const auto a5 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
 371
 372   SECTION("Equivalent insertions")
 373   {
 374     // TODO: Is this even a sensible question to ask if the two sequences
 375     // don't agree upon what each actor executed after `E`?
 376     const auto insertion =
 377         Execution().get_shortest_odpor_sq_subset_insertion(PartialExecution{a1, a2}, PartialExecution{a2, a5});
 378     REQUIRE(insertion.has_value());
 379     REQUIRE(insertion.value() == PartialExecution{});
 380   }
 381
 382   SECTION("")
 383   {
 384     Execution execution;
 385     execution.push_transition(a0);
 386     execution.push_transition(a1);
 387     execution.push_transition(a2);
 388     execution.push_transition(a3);
 389     execution.push_transition(a4);
 390     execution.push_transition(a5);
 391   }
 392 }