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)
> [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)
> [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)
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()
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());
~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. */
(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());
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;
#!/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@) **************************
! 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@) **************************
> [ 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 **
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