src/mc/explo/udpor/ExtensionSet_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/udpor/Configuration.hpp"
   8 #include "src/mc/explo/udpor/ExtensionSetCalculator.hpp"
   9 #include "src/mc/explo/udpor/History.hpp"
  10 #include "src/mc/explo/udpor/Unfolding.hpp"
  11
  12 using namespace simgrid::mc;
  13 using namespace simgrid::mc::udpor;
  14
  15 TEST_CASE("simgrid::mc::udpor: Testing Computation with AsyncSend/AsyncReceive Only")
  16 {
  17   // This test checks that the unfolding constructed for the very
  18   // simple program described below is extended correctly. Each
  19   // step of UDPOR is observed to ensure that computations are carried
  20   // out correctly. The program described is simply:
  21   //
  22   //      1                 2
  23   // AsyncSend(m)      AsyncRecv(m)
  24   //
  25   // The unfolding of the simple program is as follows:
  26   //
  27   //                         ⊥
  28   //                  /            /
  29   //       (a) 1: AsyncSend(m)  (b) 2: AsyncRecv(m)
  30
  31   const int times_considered = 0;
  32   const int tag              = 0;
  33   const unsigned mbox        = 0;
  34   const uintptr_t comm       = 0;
  35
  36   Unfolding U;
  37
  38   SECTION("Computing ex({⊥}) with 1: AsyncSend")
  39   {
  40     // Consider the extension with `1: AsyncSend(m)`
  41     Configuration C;
  42     aid_t issuer = 1;
  43
  44     const auto async_send      = std::make_shared<CommSendTransition>(issuer, times_considered, comm, mbox, tag);
  45     const auto incremental_exC = ExtensionSetCalculator::partially_extend(C, &U, async_send);
  46
  47     // Check that the events have been added to `U`
  48     REQUIRE(U.size() == 1);
  49
  50     // Make assertions about the contents of ex(C)
  51     UnfoldingEvent e(EventSet(), async_send);
  52     REQUIRE(incremental_exC.contains_equivalent_to(&e));
  53   }
  54
  55   SECTION("Computing ex({⊥}) with 2: AsyncRecv")
  56   {
  57     // Consider the extension with `2: AsyncRecv(m)`
  58     Configuration C;
  59     aid_t issuer = 2;
  60
  61     const auto async_recv      = std::make_shared<CommRecvTransition>(issuer, times_considered, comm, mbox, tag);
  62     const auto incremental_exC = ExtensionSetCalculator::partially_extend(C, &U, async_recv);
  63
  64     // Check that the events have been added to `U`
  65     REQUIRE(U.size() == 1);
  66
  67     // Make assertions about the contents of ex(C)
  68     UnfoldingEvent e(EventSet(), async_recv);
  69     REQUIRE(incremental_exC.contains_equivalent_to(&e));
  70   }
  71
  72   SECTION("Computing ex({⊥}) fully")
  73   {
  74     // Consider the extension with `1: AsyncSend(m)`
  75     Configuration C;
  76
  77     const auto async_send           = std::make_shared<CommSendTransition>(1, times_considered, comm, mbox, tag);
  78     const auto incremental_exC_send = ExtensionSetCalculator::partially_extend(C, &U, async_send);
  79
  80     // Check that the events have been added to `U`
  81     REQUIRE(U.size() == 1);
  82
  83     // Make assertions about the contents of ex(C)
  84     UnfoldingEvent e_send(EventSet(), async_send);
  85     REQUIRE(incremental_exC_send.contains_equivalent_to(&e_send));
  86
  87     // Consider the extension with `2: AsyncRecv(m)`
  88     const auto async_recv           = std::make_shared<CommRecvTransition>(2, times_considered, comm, mbox, tag);
  89     const auto incremental_exC_recv = ExtensionSetCalculator::partially_extend(C, &U, async_recv);
  90
  91     // Check that the events have been added to `U`
  92     REQUIRE(U.size() == 2);
  93
  94     // Make assertions about the contents of ex(C)
  95     UnfoldingEvent e_recv(EventSet(), async_recv);
  96     REQUIRE(incremental_exC_recv.contains_equivalent_to(&e_recv));
  97   }
  98
  99   SECTION("Computing the full sequence of extensions")
 100   {
 101     Configuration C;
 102
 103     // Consider the extension with `1: AsyncSend(m)`
 104     const auto async_send           = std::make_shared<CommSendTransition>(1, times_considered, comm, mbox, tag);
 105     const auto incremental_exC_send = ExtensionSetCalculator::partially_extend(C, &U, async_send);
 106
 107     // Check that event `a` has been added to `U`
 108     REQUIRE(U.size() == 1);
 109     UnfoldingEvent e_send(EventSet(), async_send);
 110     REQUIRE(incremental_exC_send.contains_equivalent_to(&e_send));
 111
 112     // Consider the extension with `2: AsyncRecv(m)`
 113     const auto async_recv           = std::make_shared<CommRecvTransition>(2, times_considered, comm, mbox, tag);
 114     const auto incremental_exC_recv = ExtensionSetCalculator::partially_extend(C, &U, async_recv);
 115
 116     // Check that event `b` has been added to `U`
 117     REQUIRE(U.size() == 2);
 118     UnfoldingEvent e_recv(EventSet(), async_recv);
 119     REQUIRE(incremental_exC_recv.contains_equivalent_to(&e_recv));
 120
 121     // At this point, UDPOR will pick one of the two events equivalent to
 122     // `e_recv` and e`_send`
 123
 124     // Suppose it picks the event labeled `a` in the graph above first
 125     // (ultimately, UDPOR will choose to search both directions since
 126     // {⊥, b} will be an alternative to {⊥, a})
 127
 128     const auto* e_a = *incremental_exC_send.begin();
 129     const auto* e_b = *incremental_exC_recv.begin();
 130
 131     SECTION("Pick `a` first (ex({⊥, a}))")
 132     {
 133       // After picking `a`, we need only consider the extensions
 134       // possible with `2: AsyncRecv(m)` since actor 1 no longer
 135       // has any actions to run
 136       Configuration C_with_send{e_a};
 137       const auto incremental_exC_with_send = ExtensionSetCalculator::partially_extend(C_with_send, &U, async_recv);
 138
 139       // Check that event `b` has not been duplicated
 140       REQUIRE(U.size() == 2);
 141
 142       // Indeed, in this case we assert that the SAME identity has been
 143       // supplied by the unfolding (it should note that `ex({⊥, a})`
 144       // and `ex({⊥})` have an overlapping event `b`)
 145       REQUIRE(incremental_exC_with_send.contains(e_b));
 146     }
 147
 148     SECTION("Pick `b` first (ex({⊥, b}))")
 149     {
 150       // After picking `b`, we need only consider the extensions
 151       // possible with `1: AsyncSend(m)` since actor 2 no longer
 152       // has any actions to run
 153       Configuration C_with_recv{e_b};
 154       const auto incremental_exC_with_recv = ExtensionSetCalculator::partially_extend(C_with_recv, &U, async_send);
 155
 156       // Check that event `a` has not been duplicated
 157       REQUIRE(U.size() == 2);
 158
 159       // Indeed, in this case we assert that the SAME identity has been
 160       // supplied by the unfolding (it should note that `ex({⊥, b})`
 161       // and `ex({⊥})` have an overlapping event `a`)
 162       REQUIRE(incremental_exC_with_recv.contains(e_a));
 163     }
 164   }
 165 }
 166
 167 TEST_CASE("simgrid::mc::udpor: Testing Waits, Receives, and Sends")
 168 {
 169   // We're going to follow UDPOR down one path of computation
 170   // in a relatively simple program (although the unfolding quickly
 171   // becomes quite complex)
 172   //
 173   //      1                 2
 174   // AsyncSend(m)      AsyncRecv(m)
 175   // Wait(m)           Wait(m)
 176   //
 177   // The unfolding of the simple program is as follows:
 178   //                         ⊥
 179   //                  /            /
 180   //       (a) 1: AsyncSend(m)  (b) 2: AsyncRecv(m)
 181   //                |   \        /        |
 182   //                |      \  /          |
 183   //               |      /   \          |
 184   //               |    /      \         |
 185   //       (c) 1: Wait(m)       (d) 2: Wait(m)
 186   const int times_considered = 0;
 187   const int tag              = 0;
 188   const unsigned mbox        = 0;
 189   const uintptr_t comm       = 0x800;
 190   const bool timeout         = false;
 191
 192   Unfolding U;
 193   const auto comm_send   = std::make_shared<CommSendTransition>(1, times_considered, comm, mbox, tag);
 194   const auto comm_recv   = std::make_shared<CommRecvTransition>(2, times_considered, comm, mbox, tag);
 195   const auto comm_wait_1 = std::make_shared<CommWaitTransition>(1, times_considered, timeout, comm, 1, 2, mbox);
 196   const auto comm_wait_2 = std::make_shared<CommWaitTransition>(2, times_considered, timeout, comm, 1, 2, mbox);
 197
 198   // 1. UDPOR will attempt to expand first ex({⊥})
 199
 200   // --- ex({⊥}) ---
 201   const auto incremental_exC_send = ExtensionSetCalculator::partially_extend(Configuration(), &U, comm_send);
 202   // Assert that event `a` has been added
 203   UnfoldingEvent e_send(EventSet(), comm_send);
 204   REQUIRE(incremental_exC_send.size() == 1);
 205   REQUIRE(incremental_exC_send.contains_equivalent_to(&e_send));
 206   REQUIRE(U.size() == 1);
 207
 208   const auto incremental_exC_recv = ExtensionSetCalculator::partially_extend(Configuration(), &U, comm_recv);
 209   // Assert that event `b` has been added
 210   UnfoldingEvent e_recv(EventSet(), comm_recv);
 211   REQUIRE(incremental_exC_recv.size() == 1);
 212   REQUIRE(incremental_exC_recv.contains_equivalent_to(&e_recv));
 213   REQUIRE(U.size() == 2);
 214   // --- ex({⊥}) ---
 215
 216   // 2. UDPOR will then attempt to expand ex({⊥, a}) or ex({⊥, b}). Both have
 217   // parallel effects and should simply return events already added to ex(C)
 218   //
 219   // NOTE: Note that only once actor is enabled in both cases, meaning that
 220   // we need only consider one incremental expansion for each
 221
 222   const auto* e_a = *incremental_exC_send.begin();
 223   const auto* e_b = *incremental_exC_recv.begin();
 224
 225   // --- ex({⊥, a}) ---
 226   const auto incremental_exC_recv2 = ExtensionSetCalculator::partially_extend(Configuration({e_a}), &U, comm_recv);
 227   // Assert that no event has been added and that
 228   // e_b is contained in the extension set
 229   REQUIRE(incremental_exC_recv2.size() == 1);
 230   REQUIRE(incremental_exC_recv2.contains(e_b));
 231
 232   // Here, `e_a` shouldn't be added again
 233   REQUIRE(U.size() == 2);
 234   // --- ex({⊥, a}) ---
 235
 236   // --- ex({⊥, b}) ---
 237   const auto incremental_exC_send2 = ExtensionSetCalculator::partially_extend(Configuration({e_b}), &U, comm_send);
 238   // Assert that no event has been added and that
 239   // e_a is contained in the extension set
 240   REQUIRE(incremental_exC_send2.size() == 1);
 241   REQUIRE(incremental_exC_send2.contains(e_a));
 242
 243   // Here, `e_b` shouldn't be added again
 244   REQUIRE(U.size() == 2);
 245   // --- ex({⊥, b}) ---
 246
 247   // 3. Expanding from ex({⊥, a, b}) brings in both `CommWait` events since they
 248   // become enabled as soon as the communication has been paired
 249
 250   // --- ex({⊥, a, b}) ---
 251   const auto incremental_exC_wait_actor_1 =
 252       ExtensionSetCalculator::partially_extend(Configuration({e_a, e_b}), &U, comm_wait_1);
 253   // Assert that events `c` has been added
 254   UnfoldingEvent e_wait_1(EventSet({e_a, e_b}), comm_wait_1);
 255   REQUIRE(incremental_exC_wait_actor_1.size() == 1);
 256   REQUIRE(incremental_exC_wait_actor_1.contains_equivalent_to(&e_wait_1));
 257   REQUIRE(U.size() == 3);
 258
 259   const auto incremental_exC_wait_actor_2 =
 260       ExtensionSetCalculator::partially_extend(Configuration({e_a, e_b}), &U, comm_wait_2);
 261   // Assert that events `d` has been added
 262   UnfoldingEvent e_wait_2(EventSet({e_a, e_b}), comm_wait_2);
 263   REQUIRE(incremental_exC_wait_actor_2.size() == 1);
 264   REQUIRE(incremental_exC_wait_actor_2.contains_equivalent_to(&e_wait_2));
 265   REQUIRE(U.size() == 4);
 266   // --- ex({⊥, a, b}) ---
 267
 268   // 4. Expanding from either wait action should simply yield the other event
 269   // with a wait action associated with it.
 270   // This is analogous to the scenario before with send and receive
 271   // ex({⊥, a, b, c}) or ex({⊥, a, b, d})
 272
 273   const auto* e_c = *incremental_exC_wait_actor_1.begin();
 274   const auto* e_d = *incremental_exC_wait_actor_2.begin();
 275
 276   // --- ex({⊥, a, b, d}) ---
 277   const auto incremental_exC_wait_actor_1_2 =
 278       ExtensionSetCalculator::partially_extend(Configuration({e_a, e_b, e_d}), &U, comm_wait_1);
 279   // Assert that no event has been added and that
 280   // `e_c` is contained in the extension set
 281   REQUIRE(incremental_exC_wait_actor_1_2.size() == 1);
 282   REQUIRE(incremental_exC_wait_actor_1_2.contains(e_c));
 283   REQUIRE(U.size() == 4);
 284   // --- ex({⊥, a, b, d}) ---
 285
 286   // --- ex({⊥, a, b, c}) ---
 287   const auto incremental_exC_wait_actor_2_2 =
 288       ExtensionSetCalculator::partially_extend(Configuration({e_a, e_b, e_c}), &U, comm_wait_2);
 289   // Assert that no event has been added and that
 290   // `e_d` is contained in the extension set
 291   REQUIRE(incremental_exC_wait_actor_2_2.size() == 1);
 292   REQUIRE(incremental_exC_wait_actor_2_2.contains(e_d));
 293   REQUIRE(U.size() == 4);
 294   // --- ex({⊥, a, b, c}) ---
 295 }