Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Merge an initialization function into the constructor
authorMartin Quinson <martin.quinson@ens-rennes.fr>
Tue, 2 Aug 2022 10:04:56 +0000 (12:04 +0200)
committerMartin Quinson <martin.quinson@ens-rennes.fr>
Tue, 2 Aug 2022 21:29:53 +0000 (23:29 +0200)
examples/cpp/synchro-mutex/s4u-mc-synchro-mutex.tesh
src/mc/api/RemoteApp.cpp
src/mc/api/RemoteApp.hpp
src/mc/explo/DFSExplorer.cpp
src/mc/explo/LivenessChecker.cpp
teshsuite/mc/random-bug/random-bug.tesh
teshsuite/smpi/coll-allreduce-with-leaks/mc-coll-allreduce-with-leaks.tesh

index e7dedc4..5bec63f 100644 (file)
@@ -3,8 +3,8 @@
 p This file tests the dependencies between MUTEX transitions
 
 $ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt="[Checker]%e%m%n" -- ${bindir:=.}/s4u-synchro-mutex --cfg=actors:1 --log=s4u_test.thres:critical --log=root.fmt="[App%e%e%e%e]%e%m%n"
-> [Checker] Start a DFS exploration. Reduction is: dpor.
 > [App    ] Configuration change: Set 'actors' to '1'
+> [Checker] Start a DFS exploration. Reduction is: dpor.
 > [Checker] Execute 1: MUTEX_LOCK(mutex: 0, owner:1) (stack depth: 1, state: 1, 0 interleaves)
 > [Checker] Execute 1: MUTEX_WAIT(mutex: 0, owner:1) (stack depth: 2, state: 2, 0 interleaves)
 > [Checker] Execute 1: MUTEX_UNLOCK(mutex: 0, owner:-1) (stack depth: 3, state: 3, 0 interleaves)
@@ -43,8 +43,8 @@ $ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt
 > [Checker] DFS exploration ended. 13 unique states visited; 3 backtracks (18 transition replays, 3 states visited overall)
 
 $ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt="[Checker]%e%m%n" -- ${bindir:=.}/s4u-synchro-mutex --cfg=actors:2 --log=s4u_test.thres:critical --log=root.fmt="[App%e%e%e%e]%e%m%n"
-> [Checker] Start a DFS exploration. Reduction is: dpor.
 > [App    ] Configuration change: Set 'actors' to '2'
+> [Checker] Start a DFS exploration. Reduction is: dpor.
 > [Checker] Execute 1: MUTEX_LOCK(mutex: 0, owner:1) (stack depth: 1, state: 1, 0 interleaves)
 > [Checker] Execute 1: MUTEX_WAIT(mutex: 0, owner:1) (stack depth: 2, state: 2, 0 interleaves)
 > [Checker] Execute 1: MUTEX_UNLOCK(mutex: 0, owner:-1) (stack depth: 3, state: 3, 0 interleaves)
@@ -221,6 +221,6 @@ $ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt
 > [Checker] DFS exploration ended. 37 unique states visited; 7 backtracks (76 transition replays, 33 states visited overall)
 
 $ ${bindir:=.}/../../../bin/simgrid-mc -- ${bindir:=.}/s4u-synchro-mutex --cfg=actors:3 --log=s4u_test.thres:critical
-> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor.
 > [0.000000] [xbt_cfg/INFO] Configuration change: Set 'actors' to '3'
+> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor.
 > [0.000000] [mc_dfs/INFO] DFS exploration ended. 85 unique states visited; 15 backtracks (240 transition replays, 141 states visited overall)
index 6037b6a..810f527 100644 (file)
@@ -89,6 +89,10 @@ RemoteApp::RemoteApp(const std::function<void()>& code)
 
   mc_model_checker = model_checker_.get();
   model_checker_->start();
+
+  /* Take the initial snapshot */
+  model_checker_->wait_for_requests();
+  initial_snapshot_ = std::make_shared<simgrid::mc::Snapshot>(0);
 }
 
 RemoteApp::~RemoteApp()
@@ -96,14 +100,6 @@ RemoteApp::~RemoteApp()
   this->close();
 }
 
-/** The application must be stopped. */
-void RemoteApp::take_initial_snapshot()
-{
-  xbt_assert(initial_snapshot_ == nullptr);
-  model_checker_->wait_for_requests();
-  initial_snapshot_ = std::make_shared<simgrid::mc::Snapshot>(0);
-}
-
 void RemoteApp::restore_initial_state() const
 {
   this->initial_snapshot_->restore(&model_checker_->get_remote_process());
index a9a9ea3..1b862bc 100644 (file)
@@ -45,7 +45,6 @@ public:
   ~RemoteApp();
   void close();
 
-  void take_initial_snapshot();
   void restore_initial_state() const;
 
   /** Ask to the application to check for a deadlock. If so, do an error message and throw a DeadlockError. */
index 1d429a2..22b4bda 100644 (file)
@@ -281,8 +281,6 @@ DFSExplorer::DFSExplorer(RemoteApp* remote_app) : Exploration(remote_app)
              (reductionMode_ == ReductionMode::none ? "none"
                                                     : (reductionMode_ == ReductionMode::dpor ? "dpor" : "unknown")));
 
-  get_remote_app().take_initial_snapshot();
-
   XBT_DEBUG("Starting the DFS exploration");
 
   auto initial_state = std::make_unique<State>(get_remote_app());
index 3acd33a..3fc4fd2 100644 (file)
@@ -271,7 +271,6 @@ void LivenessChecker::run()
   Api::get().automaton_load(_sg_mc_property_file.get().c_str());
 
   XBT_DEBUG("Starting the liveness algorithm");
-  get_remote_app().take_initial_snapshot();
 
   /* Initialize */
   this->previous_pair_ = 0;
index f73d665..3b6ffa2 100644 (file)
@@ -1,8 +1,8 @@
 #!/usr/bin/env tesh
 ! expect return 1
 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug assert ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --log=xbt_cfg.thresh:warning
-> [  0.000000] (0:maestro@) Start a DFS exploration. Reduction is: dpor.
 > [  0.000000] (0:maestro@) Behavior: assert
+> [  0.000000] (0:maestro@) Start a DFS exploration. Reduction is: dpor.
 > [  0.000000] (0:maestro@) **************************
 > [  0.000000] (0:maestro@) *** PROPERTY NOT VALID ***
 > [  0.000000] (0:maestro@) **************************
@@ -15,8 +15,8 @@ $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug assert ${platfdir
 ! expect return 6
 # because SIMGRID_MC_EXIT_PROGRAM_CRASH = 6
 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug abort ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --log=xbt_cfg.thresh:warning --log=no_loc
-> [  0.000000] (0:maestro@) Start a DFS exploration. Reduction is: dpor.
 > [  0.000000] (0:maestro@) Behavior: abort
+> [  0.000000] (0:maestro@) Start a DFS exploration. Reduction is: dpor.
 > [  0.000000] (0:maestro@) **************************
 > [  0.000000] (0:maestro@) ** CRASH IN THE PROGRAM **
 > [  0.000000] (0:maestro@) **************************
@@ -29,16 +29,16 @@ $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug abort ${platfdir}
 > [  0.000000] (0:maestro@) Stack trace not displayed because you passed --log=no_loc
 
 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug printf ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --log=xbt_cfg.thresh:warning
-> [  0.000000] (0:maestro@) Start a DFS exploration. Reduction is: dpor.
 > [  0.000000] (0:maestro@) Behavior: printf
+> [  0.000000] (0:maestro@) Start a DFS exploration. Reduction is: dpor.
 > [  0.000000] (1:app@Fafard) Error reached
 > [  0.000000] (0:maestro@) DFS exploration ended. 43 unique states visited; 36 backtracks (108 transition replays, 30 states visited overall)
 
 ! expect return 6
 # because SIMGRID_MC_EXIT_PROGRAM_CRASH = 6
 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug segv ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --log=xbt_cfg.thresh:warning --log=no_loc
-> [  0.000000] (0:maestro@) Start a DFS exploration. Reduction is: dpor.
 > [  0.000000] (0:maestro@) Behavior: segv
+> [  0.000000] (0:maestro@) Start a DFS exploration. Reduction is: dpor.
 > Segmentation fault.
 > [  0.000000] (0:maestro@) **************************
 > [  0.000000] (0:maestro@) ** CRASH IN THE PROGRAM **
index 4ffce51..2010817 100644 (file)
@@ -2,11 +2,11 @@
 
 p Test allreduce
 $ $VALGRIND_NO_LEAK_CHECK ${bindir:=.}/../../../smpi_script/bin/smpirun -wrapper "${bindir:=.}/../../../bin/simgrid-mc" -map -hostfile ../hostfile_coll -platform  ${platfdir:=.}/small_platform.xml -np 4 --log=xbt_cfg.thres:critical ${bindir:=.}/coll-allreduce-with-leaks --log=smpi_config.thres:warning --cfg=smpi/display-allocs:yes --cfg=smpi/simulate-computation:no --log=smpi_coll.thres:error --log=smpi_mpi.thres:error --log=smpi_pmpi.thres:error --cfg=smpi/list-leaks:10 --log=no_loc
-> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor.
 > [0.000000] [smpi/INFO] [rank 0] -> Tremblay
 > [0.000000] [smpi/INFO] [rank 1] -> Tremblay
 > [0.000000] [smpi/INFO] [rank 2] -> Tremblay
 > [0.000000] [smpi/INFO] [rank 3] -> Tremblay
+> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor.
 > [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed MPI handles:
 > [0.000000] [smpi_utils/WARNING] To get more information (location of allocations), compile your code with -trace-call-location flag of smpicc/f90
 > [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Comm