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   const auto incremental_exC_recv = ExtensionSetCalculator::partially_extend(Configuration(), &U, comm_recv);
 224   // Assert that event `b` has been added
 225   UnfoldingEvent e_recv(EventSet(), comm_recv);
 226   REQUIRE(incremental_exC_recv.size() == 1);
 227   REQUIRE(incremental_exC_recv.contains_equivalent_to(&e_recv));
 228   REQUIRE(U.size() == 2);
 229   // --- ex({⊥}) ---
 230
 231   // 2. UDPOR will then attempt to expand ex({⊥, a}) or ex({⊥, b}). Both have
 232   // parallel effects and should simply return events already added to ex(C)
 233   //
 234   // NOTE: Note that only once actor is enabled in both cases, meaning that
 235   // we need only consider one incremental expansion for each
 236
 237   const auto* e_a = *incremental_exC_send.begin();
 238   const auto* e_b = *incremental_exC_recv.begin();
 239
 240   // --- ex({⊥, a}) ---
 241   const auto incremental_exC_recv2 = ExtensionSetCalculator::partially_extend(Configuration({e_a}), &U, comm_recv);
 242   // Assert that no event has been added and that
 243   // e_b is contained in the extension set
 244   REQUIRE(incremental_exC_recv2.size() == 1);
 245   REQUIRE(incremental_exC_recv2.contains(e_b));
 246
 247   // Here, `e_a` shouldn't be added again
 248   REQUIRE(U.size() == 2);
 249   // --- ex({⊥, a}) ---
 250
 251   // --- ex({⊥, b}) ---
 252   const auto incremental_exC_send2 = ExtensionSetCalculator::partially_extend(Configuration({e_b}), &U, comm_send);
 253   // Assert that no event has been added and that
 254   // e_a is contained in the extension set
 255   REQUIRE(incremental_exC_send2.size() == 1);
 256   REQUIRE(incremental_exC_send2.contains(e_a));
 257
 258   // Here, `e_b` shouldn't be added again
 259   REQUIRE(U.size() == 2);
 260   // --- ex({⊥, b}) ---
 261
 262   // 3. Expanding from ex({⊥, a, b}) brings in both `CommWait` events since they
 263   // become enabled as soon as the communication has been paired
 264
 265   // --- ex({⊥, a, b}) ---
 266   const auto incremental_exC_wait_actor_1 =
 267       ExtensionSetCalculator::partially_extend(Configuration({e_a, e_b}), &U, comm_wait_1);
 268   // Assert that events `c` has been added
 269   UnfoldingEvent e_wait_1(EventSet({e_a, e_b}), comm_wait_1);
 270   REQUIRE(incremental_exC_wait_actor_1.size() == 1);
 271   REQUIRE(incremental_exC_wait_actor_1.contains_equivalent_to(&e_wait_1));
 272   REQUIRE(U.size() == 3);
 273
 274   const auto incremental_exC_wait_actor_2 =
 275       ExtensionSetCalculator::partially_extend(Configuration({e_a, e_b}), &U, comm_wait_2);
 276   // Assert that events `d` has been added
 277   UnfoldingEvent e_wait_2(EventSet({e_a, e_b}), comm_wait_2);
 278   REQUIRE(incremental_exC_wait_actor_2.size() == 1);
 279   REQUIRE(incremental_exC_wait_actor_2.contains_equivalent_to(&e_wait_2));
 280   REQUIRE(U.size() == 4);
 281   // --- ex({⊥, a, b}) ---
 282
 283   // 4. Expanding from either wait action should simply yield the other event
 284   // with a wait action associated with it.
 285   // This is analogous to the scenario before with send and receive
 286   // ex({⊥, a, b, c}) or ex({⊥, a, b, d})
 287
 288   const auto* e_c = *incremental_exC_wait_actor_1.begin();
 289   const auto* e_d = *incremental_exC_wait_actor_2.begin();
 290
 291   // --- ex({⊥, a, b, d}) ---
 292   const auto incremental_exC_wait_actor_1_2 =
 293       ExtensionSetCalculator::partially_extend(Configuration({e_a, e_b, e_d}), &U, comm_wait_1);
 294   // Assert that no event has been added and that
 295   // `e_c` is contained in the extension set
 296   REQUIRE(incremental_exC_wait_actor_1_2.size() == 1);
 297   REQUIRE(incremental_exC_wait_actor_1_2.contains(e_c));
 298   REQUIRE(U.size() == 4);
 299   // --- ex({⊥, a, b, d}) ---
 300
 301   // --- ex({⊥, a, b, c}) ---
 302   const auto incremental_exC_wait_actor_2_2 =
 303       ExtensionSetCalculator::partially_extend(Configuration({e_a, e_b, e_c}), &U, comm_wait_2);
 304   // Assert that no event has been added and that
 305   // `e_d` is contained in the extension set
 306   REQUIRE(incremental_exC_wait_actor_2_2.size() == 1);
 307   REQUIRE(incremental_exC_wait_actor_2_2.contains(e_d));
 308   REQUIRE(U.size() == 4);
 309   // --- ex({⊥, a, b, c}) ---
 310 }