src/mc/explo/odpor/WakeupTree_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/WakeupTree.hpp"
   9 #include "src/mc/explo/udpor/udpor_tests_private.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::WakeupTree: Testing Insertion")
  16 {
  17   // We imagine the following completed execution `E`
  18   // consisting of executing actions a0-a3. Execution
  19   // `E` cis the first such maximal execution explored
  20   // by ODPOR, which implies that a) all sleep sets are
  21   // empty and b) all wakeup trees (i.e. for each prefix) consist of the root
  22   // node with a single leaf containing the action
  23   // taken, save for the wakeup tree of the execution itself
  24   // which is empty
  25
  26   // We first notice that there's a reversible race between
  27   // events 0 and 3.
  28
  29   const auto a0 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
  30   const auto a1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 4);
  31   const auto a2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
  32   const auto a3 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
  33
  34   Execution execution;
  35   execution.push_transition(a0);
  36   execution.push_transition(a1);
  37   execution.push_transition(a2);
  38   execution.push_transition(a3);
  39
  40   REQUIRE(execution.get_racing_events_of(2) == std::unordered_set<Execution::EventHandle>{0});
  41   REQUIRE(execution.get_racing_events_of(3) == std::unordered_set<Execution::EventHandle>{0});
  42
  43   // First, we initialize the tree to how it looked prior
  44   // to the insertion of the race
  45   WakeupTree tree;
  46   tree.insert(Execution(), {a0});
  47
  48   // Then, after insertion, we ensure that the node was
  49   // indeed added to the tree
  50
  51   tree.insert(Execution(), {a1, a3});
  52
  53   WakeupTreeIterator iter = tree.begin();
  54   REQUIRE((*iter)->get_sequence() == PartialExecution{a0});
  55
  56   ++iter;
  57   REQUIRE(iter != tree.end());
  58   REQUIRE((*iter)->get_sequence() == PartialExecution{a1, a3});
  59
  60   ++iter;
  61   REQUIRE(iter != tree.end());
  62   REQUIRE((*iter)->get_sequence() == PartialExecution{});
  63
  64   ++iter;
  65   REQUIRE(iter == tree.end());
  66
  67   SECTION("Attempting to re-insert the same sequence should have no effect")
  68   {
  69     tree.insert(Execution(), {a1, a3});
  70     iter = tree.begin();
  71
  72     REQUIRE((*iter)->get_sequence() == PartialExecution{a0});
  73
  74     ++iter;
  75     REQUIRE(iter != tree.end());
  76     REQUIRE((*iter)->get_sequence() == PartialExecution{a1, a3});
  77
  78     ++iter;
  79     REQUIRE(iter != tree.end());
  80     REQUIRE((*iter)->get_sequence() == PartialExecution{});
  81
  82     ++iter;
  83     REQUIRE(iter == tree.end());
  84   }
  85
  86   SECTION("Inserting an extension")
  87   {
  88     tree.insert(Execution(), {a1, a2});
  89     iter = tree.begin();
  90     REQUIRE((*iter)->get_sequence() == PartialExecution{a0});
  91
  92     ++iter;
  93     REQUIRE(iter != tree.end());
  94     REQUIRE((*iter)->get_sequence() == PartialExecution{a1, a3});
  95
  96     ++iter;
  97     REQUIRE(iter != tree.end());
  98     REQUIRE((*iter)->get_sequence() == PartialExecution{a1, a2});
  99
 100     ++iter;
 101     REQUIRE(iter != tree.end());
 102     REQUIRE((*iter)->get_sequence() == PartialExecution{});
 103
 104     ++iter;
 105     REQUIRE(iter == tree.end());
 106   }
 107 }