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