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/odpor/odpor_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   SECTION("Happens-before is transitively-closed")
 116   {
 117     SECTION("Example 1")
 118     {
 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);
 127
 128       Execution execution;
 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));
 133     }
 134
 135     SECTION("Stress testing transitivity of the happens-before relation")
 136     {
 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);
 151
 152       Execution execution;
 153       execution.push_partial_execution(PartialExecution{e0, e1, e2, e3, e4, e5, e6, e7, e8, e9, e10});
 154
 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((!(e_i_before_e_j and e_j_before_e_k) or e_i_before_e_k));
 164           }
 165         }
 166       }
 167     }
 168   }
 169 }
 170
 171 TEST_CASE("simgrid::mc::odpor::Execution: Testing Racing Events and Initials")
 172 {
 173   SECTION("Example 1")
 174   {
 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);
 180
 181     Execution execution;
 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);
 187
 188     // Nothing comes before event 0
 189     REQUIRE(execution.get_racing_events_of(0) == std::unordered_set<Execution::EventHandle>{});
 190
 191     // Events 0 and 1 are independent
 192     REQUIRE(execution.get_racing_events_of(1) == std::unordered_set<Execution::EventHandle>{});
 193
 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});
 196
 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>{});
 199
 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
 202     //
 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});
 206   }
 207
 208   SECTION("Example 2: Events with multiple races")
 209   {
 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);
 214
 215     Execution execution;
 216     execution.push_transition(a1);
 217     execution.push_transition(a2);
 218     execution.push_transition(a3);
 219     execution.push_transition(a4);
 220
 221     // Nothing comes before event 0
 222     REQUIRE(execution.get_racing_events_of(0) == std::unordered_set<Execution::EventHandle>{});
 223
 224     // Events 0 and 1 are independent
 225     REQUIRE(execution.get_racing_events_of(1) == std::unordered_set<Execution::EventHandle>{});
 226
 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>{});
 229
 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});
 232
 233     SECTION("Check initials with respect to event 1")
 234     {
 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});
 241     }
 242
 243     SECTION("Check initials with respect to event 2")
 244     {
 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
 247       // of E' wrt. `v`
 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});
 250     }
 251   }
 252
 253   SECTION("Example 3: Testing 'Lock' Example")
 254   {
 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);
 262
 263     Execution execution;
 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});
 270   }
 271
 272   SECTION("Example 4: Indirect Races")
 273   {
 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);
 284
 285     Execution execution(PartialExecution{e0, e1, e2, e3, e4, e5, e6, e7, e8, e9});
 286
 287     // Nothing comes before event 0
 288     REQUIRE(execution.get_racing_events_of(0) == std::unordered_set<Execution::EventHandle>{});
 289
 290     // Events 0 and 1 are independent
 291     REQUIRE(execution.get_racing_events_of(1) == std::unordered_set<Execution::EventHandle>{});
 292
 293     // Events 1 and 2 are independent
 294     REQUIRE(execution.get_racing_events_of(2) == std::unordered_set<Execution::EventHandle>{});
 295
 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>{});
 298
 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});
 304
 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});
 308
 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});
 311
 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>{});
 315
 316     // Event 8 is independent with everything
 317     REQUIRE(execution.get_racing_events_of(8) == std::unordered_set<Execution::EventHandle>{});
 318
 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});
 322   }
 323
 324   SECTION("Example 5: Stress testing race detection")
 325   {
 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);
 337
 338     Execution execution(PartialExecution{e0, e1, e2, e3, e4, e5, e6, e7, e8, e9, e10});
 339
 340     // Nothing comes before event 0
 341     CHECK(execution.get_racing_events_of(0) == std::unordered_set<Execution::EventHandle>{});
 342
 343     // Events 0 and 1 are independent
 344     CHECK(execution.get_racing_events_of(1) == std::unordered_set<Execution::EventHandle>{});
 345
 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>{});
 348
 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});
 351
 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>{});
 354
 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});
 358
 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});
 363
 364     // Same goes for event 7 as for 6
 365     CHECK(execution.get_racing_events_of(7) == std::unordered_set<Execution::EventHandle>{6});
 366
 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>{});
 369
 370     // Event 6 blocks event 9 from racing with event 6
 371     CHECK(execution.get_racing_events_of(9) == std::unordered_set<Execution::EventHandle>{});
 372
 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>{});
 375   }
 376
 377   SECTION("Example with many races for one event")
 378   {
 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);
 386
 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});
 389   }
 390 }
 391
 392 TEST_CASE("simgrid::mc::odpor::Execution: Independence Tests")
 393 {
 394   SECTION("Complete independence")
 395   {
 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});
 407
 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));
 414
 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));
 420   }
 421
 422   SECTION("Independence is trivial with an empty extension")
 423   {
 424     REQUIRE(Execution().is_independent_with_execution_of(
 425         PartialExecution{}, std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1)));
 426   }
 427
 428   SECTION("Dependencies stopping independence from being possible")
 429   {
 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});
 441
 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));
 445
 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));
 448
 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));
 452
 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));
 457
 458     // This ensures that independence is trivial with an empty partial execution
 459     REQUIRE(execution.is_independent_with_execution_of(PartialExecution{}, a1));
 460   }
 461
 462   SECTION("More interesting dependencies stopping independence")
 463   {
 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});
 471
 472     SECTION("Action run by same actor disqualifies independence")
 473     {
 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};
 479
 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);
 482
 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);
 486
 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);
 490     }
 491   }
 492 }
 493
 494 TEST_CASE("simgrid::mc::odpor::Execution: Initials Test")
 495 {
 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});
 507
 508   SECTION("Initials trivial with empty executions")
 509   {
 510     // There are no initials for an empty extension since
 511     // a requirement is that the actor be contained in the
 512     // extension itself
 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));
 519   }
 520
 521   SECTION("The first actor is always an initial")
 522   {
 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_));
 535   }
 536
 537   SECTION("Example: Disqualified and re-qualified after switching ordering")
 538   {
 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));
 543
 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));
 546   }
 547
 548   SECTION("Example: Large partial executions")
 549   {
 550     // The record trace is `1 3 4 4 3 1 4 2`
 551
 552     // Actor 1 starts the execution
 553     REQUIRE(Execution().is_initial_after_execution_of(PartialExecution{a1, a2, a3, a4, a6, a7, a8, indep}, 1));
 554
 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));
 558
 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));
 561
 562     // Likewise with actor 4
 563     REQUIRE_FALSE(Execution().is_initial_after_execution_of(PartialExecution{a1, a2, a3, a4, a6, a7, a8, indep}, 4));
 564   }
 565
 566   SECTION("Example: Stress tests for initials computation")
 567   {
 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};
 577
 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));
 580
 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));
 584
 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));
 589
 590     // Actor 4 is blocked actor 3's second action `v_7`
 591     REQUIRE_FALSE(Execution().is_initial_after_execution_of(v, 4));
 592   }
 593 }
 594
 595 TEST_CASE("simgrid::mc::odpor::Execution: ODPOR Smallest Sequence Tests")
 596 {
 597   const auto a0 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
 598   const auto a1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 4);
 599   const auto a2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 3);
 600   const auto a3 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
 601   const auto a4 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
 602   const auto a5 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
 603
 604   Execution execution;
 605   execution.push_transition(a0);
 606   execution.push_transition(a1);
 607   execution.push_transition(a2);
 608   execution.push_transition(a3);
 609   execution.push_transition(a4);
 610   execution.push_transition(a5);
 611
 612   SECTION("Equivalent insertions")
 613   {
 614     SECTION("Example: Eliminated through independence")
 615     {
 616       // TODO: Is this even a sensible question to ask if the two sequences
 617       // don't agree upon what each actor executed after `E`?
 618       const auto insertion =
 619           Execution().get_shortest_odpor_sq_subset_insertion(PartialExecution{a1, a2}, PartialExecution{a2, a5});
 620       REQUIRE(insertion.has_value());
 621       REQUIRE(insertion.value() == PartialExecution{});
 622     }
 623
 624     SECTION("Exact match yields empty set")
 625     {
 626       const auto insertion =
 627           Execution().get_shortest_odpor_sq_subset_insertion(PartialExecution{a1, a2}, PartialExecution{a1, a2});
 628       REQUIRE(insertion.has_value());
 629       REQUIRE(insertion.value() == PartialExecution{});
 630     }
 631   }
 632
 633   SECTION("Match against empty executions")
 634   {
 635     SECTION("Empty `v` trivially yields `w`")
 636     {
 637       auto insertion =
 638           Execution().get_shortest_odpor_sq_subset_insertion(PartialExecution{}, PartialExecution{a1, a5, a2});
 639       REQUIRE(insertion.has_value());
 640       REQUIRE(insertion.value() == PartialExecution{a1, a5, a2});
 641
 642       insertion = execution.get_shortest_odpor_sq_subset_insertion(PartialExecution{}, PartialExecution{a1, a5, a2});
 643       REQUIRE(insertion.has_value());
 644       REQUIRE(insertion.value() == PartialExecution{a1, a5, a2});
 645     }
 646
 647     SECTION("Empty `w` yields empty execution")
 648     {
 649       auto insertion =
 650           Execution().get_shortest_odpor_sq_subset_insertion(PartialExecution{a1, a4, a5}, PartialExecution{});
 651       REQUIRE(insertion.has_value());
 652       REQUIRE(insertion.value() == PartialExecution{});
 653
 654       insertion = execution.get_shortest_odpor_sq_subset_insertion(PartialExecution{a1, a5, a2}, PartialExecution{});
 655       REQUIRE(insertion.has_value());
 656       REQUIRE(insertion.value() == PartialExecution{});
 657     }
 658   }
 659 }