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 }
  21
  22 TEST_CASE("simgrid::mc::odpor::Execution: Testing Happens-Before")
  23 {
  24   SECTION("Example 1")
  25   {
  26     // We check each permutation for happens before
  27     // among the given actions added to the execution
  28     const auto a1 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
  29     const auto a2 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
  30     const auto a3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
  31     const auto a4 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 4);
  32
  33     Execution execution;
  34     execution.push_transition(a1.get());
  35     execution.push_transition(a2.get());
  36     execution.push_transition(a3.get());
  37     execution.push_transition(a4.get());
  38
  39     SECTION("Happens-before is irreflexive")
  40     {
  41       REQUIRE_FALSE(execution.happens_before(0, 0));
  42       REQUIRE_FALSE(execution.happens_before(1, 1));
  43       REQUIRE_FALSE(execution.happens_before(2, 2));
  44       REQUIRE_FALSE(execution.happens_before(3, 3));
  45     }
  46
  47     SECTION("Happens-before values for each pair of events")
  48     {
  49       REQUIRE_FALSE(execution.happens_before(0, 1));
  50       REQUIRE_FALSE(execution.happens_before(0, 2));
  51       REQUIRE(execution.happens_before(0, 3));
  52       REQUIRE_FALSE(execution.happens_before(1, 2));
  53       REQUIRE_FALSE(execution.happens_before(1, 3));
  54       REQUIRE_FALSE(execution.happens_before(2, 3));
  55     }
  56
  57     SECTION("Happens-before is a subset of 'occurs-before' ")
  58     {
  59       REQUIRE_FALSE(execution.happens_before(1, 0));
  60       REQUIRE_FALSE(execution.happens_before(2, 0));
  61       REQUIRE_FALSE(execution.happens_before(3, 0));
  62       REQUIRE_FALSE(execution.happens_before(2, 1));
  63       REQUIRE_FALSE(execution.happens_before(3, 1));
  64       REQUIRE_FALSE(execution.happens_before(3, 2));
  65     }
  66   }
  67
  68   SECTION("Example 2")
  69   {
  70     const auto a1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
  71     const auto a2 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
  72     const auto a3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
  73     const auto a4 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
  74
  75     // Notice that `a5` and `a6` are executed by the same actor; thus, although
  76     // the actor is executing independent actions, each still "happen-before"
  77     // the another
  78
  79     Execution execution;
  80     execution.push_transition(a1.get());
  81     execution.push_transition(a2.get());
  82     execution.push_transition(a3.get());
  83     execution.push_transition(a4.get());
  84
  85     SECTION("Happens-before is irreflexive")
  86     {
  87       REQUIRE_FALSE(execution.happens_before(0, 0));
  88       REQUIRE_FALSE(execution.happens_before(1, 1));
  89       REQUIRE_FALSE(execution.happens_before(2, 2));
  90       REQUIRE_FALSE(execution.happens_before(3, 3));
  91     }
  92
  93     SECTION("Happens-before values for each pair of events")
  94     {
  95       REQUIRE_FALSE(execution.happens_before(0, 1));
  96       REQUIRE_FALSE(execution.happens_before(0, 2));
  97       REQUIRE_FALSE(execution.happens_before(0, 3));
  98       REQUIRE(execution.happens_before(1, 2));
  99       REQUIRE(execution.happens_before(1, 3));
 100       REQUIRE(execution.happens_before(2, 3));
 101     }
 102
 103     SECTION("Happens-before is a subset of 'occurs-before'")
 104     {
 105       REQUIRE_FALSE(execution.happens_before(1, 0));
 106       REQUIRE_FALSE(execution.happens_before(2, 0));
 107       REQUIRE_FALSE(execution.happens_before(3, 0));
 108       REQUIRE_FALSE(execution.happens_before(2, 1));
 109       REQUIRE_FALSE(execution.happens_before(3, 1));
 110       REQUIRE_FALSE(execution.happens_before(3, 2));
 111     }
 112   }
 113 }
 114
 115 TEST_CASE("simgrid::mc::odpor::Execution: Testing Racing Events Initials")
 116 {
 117   SECTION("Example 1")
 118   {
 119     const auto a1 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
 120     const auto a2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2);
 121     const auto a3 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
 122     const auto a4 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
 123     const auto a5 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
 124
 125     Execution execution;
 126     execution.push_transition(a1.get());
 127     execution.push_transition(a2.get());
 128     execution.push_transition(a3.get());
 129     execution.push_transition(a4.get());
 130     execution.push_transition(a5.get());
 131
 132     // Nothing comes before event 0
 133     REQUIRE(execution.get_racing_events_of(0) == std::unordered_set<Execution::EventHandle>{});
 134
 135     // Events 0 and 1 are independent
 136     REQUIRE(execution.get_racing_events_of(1) == std::unordered_set<Execution::EventHandle>{});
 137
 138     // 2 and 1 are executed by different actors and happen right after each other
 139     REQUIRE(execution.get_racing_events_of(2) == std::unordered_set<Execution::EventHandle>{1});
 140
 141     // Although a3 and a4 are dependent, they are executed by the same actor
 142     REQUIRE(execution.get_racing_events_of(3) == std::unordered_set<Execution::EventHandle>{});
 143
 144     // Event 4 is in a race with neither event 0 nor event 2 since those events
 145     // "happen-before" event 3 with which event 4 races
 146     //
 147     // Furthermore, event 1 is run by the same actor and thus also is not in a race.
 148     // Hence, only event 3 races with event 4
 149     REQUIRE(execution.get_racing_events_of(4) == std::unordered_set<Execution::EventHandle>{3});
 150   }
 151
 152   SECTION("Example 2: Events with multiple races")
 153   {
 154     const auto a1 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
 155     const auto a2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2);
 156     const auto a3 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
 157     const auto a4 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
 158
 159     Execution execution;
 160     execution.push_transition(a1.get());
 161     execution.push_transition(a2.get());
 162     execution.push_transition(a3.get());
 163     execution.push_transition(a4.get());
 164
 165     // Nothing comes before event 0
 166     REQUIRE(execution.get_racing_events_of(0) == std::unordered_set<Execution::EventHandle>{});
 167
 168     // Events 0 and 1 are independent
 169     REQUIRE(execution.get_racing_events_of(1) == std::unordered_set<Execution::EventHandle>{});
 170
 171     // Event 2 is independent with event 1 and run by the same actor as event 0
 172     REQUIRE(execution.get_racing_events_of(2) == std::unordered_set<Execution::EventHandle>{});
 173
 174     // All events are dependent with event 3, but event 0 "happens-before" event 2
 175     REQUIRE(execution.get_racing_events_of(3) == std::unordered_set<Execution::EventHandle>{1, 2});
 176   }
 177 }