[mc] Enable finalize_app() in SafetyChecker.

Update mc-coll-allreduce-with-leaks.tesh accordingly.

diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp
index 892f173..36423ba 100644 (file)
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -110,9 +110,11 @@ void SafetyChecker::run()
     // req is now the transition of the process that was selected to be executed
 
     if (req == nullptr) {
-      XBT_DEBUG("There are no more processes to interleave. (depth %zu)", stack_.size() + 1);
+      XBT_DEBUG("There remains %zu actors, but no more processes to interleave. (depth %zu)",
+                mc_model_checker->get_remote_process().actors().size(), stack_.size() + 1);
 
-//      mc_model_checker->finalize_app();
+      if (mc_model_checker->get_remote_process().actors().empty())
+        mc_model_checker->finalize_app();
       this->backtrack();
       continue;
     }

diff --git a/teshsuite/smpi/coll-allreduce-with-leaks/mc-coll-allreduce-with-leaks.tesh b/teshsuite/smpi/coll-allreduce-with-leaks/mc-coll-allreduce-with-leaks.tesh
index 5890b63..004ebee 100644 (file)
--- a/teshsuite/smpi/coll-allreduce-with-leaks/mc-coll-allreduce-with-leaks.tesh
+++ b/teshsuite/smpi/coll-allreduce-with-leaks/mc-coll-allreduce-with-leaks.tesh
@@ -7,6 +7,20 @@ $ $VALGRIND_NO_LEAK_CHECK ${bindir:=.}/../../../smpi_script/bin/smpirun -wrapper
 > [rank 1] -> Tremblay
 > [rank 2] -> Tremblay
 > [rank 3] -> Tremblay
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 7 unfreed MPI handles : display types and addresses (n max) with --cfg=smpi/list-leaks:n.
+> Running smpirun with -wrapper "valgrind --leak-check=full" can provide more information
+> [0.000000] [smpi_utils/INFO] Memory Usage: Simulated application allocated 128 bytes during its lifetime through malloc/calloc calls.
+> Largest allocation at once from a single process was 16 bytes, at sysdep.h:59. It was called 8 times during the whole simulation.
+> If this is too much, consider sharing allocations for computation buffers.
+> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary)
+>
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 7 unfreed MPI handles : display types and addresses (n max) with --cfg=smpi/list-leaks:n.
+> Running smpirun with -wrapper "valgrind --leak-check=full" can provide more information
+> [0.000000] [smpi_utils/INFO] Memory Usage: Simulated application allocated 128 bytes during its lifetime through malloc/calloc calls.
+> Largest allocation at once from a single process was 16 bytes, at sysdep.h:59. It was called 8 times during the whole simulation.
+> If this is too much, consider sharing allocations for computation buffers.
+> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary)
+>
 > [0.000000] [mc_safety/INFO] Check a safety property. Reduction is: dpor.
 > [0.000000] [mc_safety/INFO] Executed transitions = 484
 > [0.000000] [mc_safety/INFO] Expanded states = 63