! expect return 1
! timeout 20
$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/s4u-mc-bugged1 ${platfdir:=.}/model_checker_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=contexts/stack-size:256
-> [ 0.000000] (0:maestro@) Check a safety property. Reduction is: dpor.
+> [ 0.000000] (0:maestro@) Start a DFS exploration. Reduction is: dpor.
> [ 0.000000] (2:client@HostB) Sent!
> [ 0.000000] (3:client@HostC) Sent!
> [ 0.000000] (1:server@HostA) OK
> [ 0.000000] (0:maestro@) 3: iSend(mbox=0)
> [ 0.000000] (0:maestro@) 1: WaitComm(from 3 to 1, mbox=0, no timeout)
> [ 0.000000] (0:maestro@) Path = 1;2;1;1;2;4;1;1;3;1
-> [ 0.000000] (0:maestro@) 22 unique states visited; 4 backtracks (56 transition replays, 30 states visited overall)
\ No newline at end of file
+> [ 0.000000] (0:maestro@) DFS exploration ended. 22 unique states visited; 4 backtracks (56 transition replays, 30 states visited overall)
\ No newline at end of file
! expect return 1
! timeout 20
$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/s4u-mc-bugged2 ${platfdir:=.}/model_checker_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=contexts/stack-size:256
-> [ 0.000000] (0:maestro@) Check a safety property. Reduction is: dpor.
+> [ 0.000000] (0:maestro@) Start a DFS exploration. Reduction is: dpor.
> [ 0.000000] (1:server@HostA) First pair received: 1 1
> [ 0.000000] (1:server@HostA) Second pair received: 2 2
> [ 0.000000] (1:server@HostA) First pair received: 1 1
> [ 0.000000] (0:maestro@) 3: iSend(mbox=0)
> [ 0.000000] (0:maestro@) 1: WaitComm(from 3 to 1, mbox=0, no timeout)
> [ 0.000000] (0:maestro@) Path = 1;3;1;3;1;3;1
-> [ 0.000000] (0:maestro@) 1006 unique states visited; 350 backtracks (5319 transition replays, 3963 states visited overall)
+> [ 0.000000] (0:maestro@) DFS exploration ended. 1006 unique states visited; 350 backtracks (5319 transition replays, 3963 states visited overall)
#!/usr/bin/env tesh
$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/s4u-mc-electric-fence ${platfdir}/model_checker_platform.xml
-> [0.000000] [mc_safety/INFO] Check a safety property. Reduction is: dpor.
+> [0.000000] [mc_safety/INFO] Start a DFS exploration. Reduction is: dpor.
> [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent!
> [HostA:server:(1) 0.000000] [electric_fence/INFO] OK
> [HostC:client:(3) 0.000000] [electric_fence/INFO] Sent!
> [HostA:server:(1) 0.000000] [electric_fence/INFO] OK
> [HostB:client:(2) 0.000000] [electric_fence/INFO] Sent!
> [HostC:client:(3) 0.000000] [electric_fence/INFO] Sent!
-> [0.000000] [mc_safety/INFO] No property violation found.
-> [0.000000] [mc_safety/INFO] 15 unique states visited; 5 backtracks (32 transition replays, 13 states visited overall)
+> [0.000000] [mc_safety/INFO] DFS exploration ended. 15 unique states visited; 5 backtracks (32 transition replays, 13 states visited overall)
! expect return 1
! timeout 20
$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/s4u-mc-failing-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@) Check a safety property. Reduction is: dpor.
+> [ 0.000000] (0:maestro@) Start a DFS exploration. Reduction is: dpor.
> [ 0.000000] (2:client1@Bourassa) Sent!
> [ 0.000000] (1:server@Boivin) OK
> [ 0.000000] (3:client2@Fafard) Sent!
> [ 0.000000] (0:maestro@) 2: iSend(mbox=0)
> [ 0.000000] (0:maestro@) 1: WaitComm(from 2 to 1, mbox=0, no timeout)
> [ 0.000000] (0:maestro@) Path = 1;3;1;1;2;1
-> [ 0.000000] (0:maestro@) 18 unique states visited; 4 backtracks (36 transition replays, 14 states visited overall)
+> [ 0.000000] (0:maestro@) DFS exploration ended. 18 unique states visited; 4 backtracks (36 transition replays, 14 states visited overall)
> [0.000000] [mc_comm_determinism/INFO] The recv communications pattern of the actor 0 is different! Different source for communication #1
> [0.000000] [mc_comm_determinism/INFO] Send-deterministic : Yes
> [0.000000] [mc_comm_determinism/INFO] Recv-deterministic : No
-> [0.000000] [mc_safety/INFO] DFS exploration successful. 36 unique states visited; 13 backtracks (97 transition replays, 49 states visited overall)
\ No newline at end of file
+> [0.000000] [mc_safety/INFO] DFS exploration ended. 36 unique states visited; 13 backtracks (97 transition replays, 49 states visited overall)
\ No newline at end of file
p Testing the permissive model
! timeout 60
$ ../../../smpi_script/bin/smpirun -quiet -wrapper "${bindir:=.}/../../../bin/simgrid-mc" -np 2 -platform ${platfdir:=.}/cluster_backbone.xml --cfg=smpi/buffering:infty --log=xbt_cfg.thresh:warning ./smpi_sendsend
-> [0.000000] [mc_safety/INFO] Check a safety property. Reduction is: dpor.
+> [0.000000] [mc_safety/INFO] Start a DFS exploration. Reduction is: dpor.
> Sent 0 to rank 1
> Sent 1 to rank 0
> rank 0 recv the data
> rank 1 recv the data
> Sent 0 to rank 1
-> [0.000000] [mc_safety/INFO] No property violation found.
-> [0.000000] [mc_safety/INFO] 7 unique states visited; 2 backtracks (10 transition replays, 2 states visited overall)
+> [0.000000] [mc_safety/INFO] DFS exploration ended. 7 unique states visited; 2 backtracks (10 transition replays, 2 states visited overall)
p Testing the paranoid model
! timeout 60
! expect return 3
$ ../../../smpi_script/bin/smpirun -quiet -wrapper "${bindir:=.}/../../../bin/simgrid-mc" -np 2 -platform ${platfdir:=.}/cluster_backbone.xml --cfg=smpi/buffering:zero --log=xbt_cfg.thresh:warning ./smpi_sendsend
-> [0.000000] [mc_safety/INFO] Check a safety property. Reduction is: dpor.
+> [0.000000] [mc_safety/INFO] Start a DFS exploration. Reduction is: dpor.
> [0.000000] [mc_global/INFO] **************************
> [0.000000] [mc_global/INFO] *** DEADLOCK DETECTED ***
> [0.000000] [mc_global/INFO] **************************
> [0.000000] [mc_global/INFO] 1: iSend(mbox=2)
> [0.000000] [mc_global/INFO] 2: iSend(mbox=0)
> [0.000000] [Api/INFO] Path = 1;2
-> [0.000000] [mc_safety/INFO] 3 unique states visited; 1 backtracks (3 transition replays, 0 states visited overall)
+> [0.000000] [mc_safety/INFO] DFS exploration ended. 3 unique states visited; 1 backtracks (3 transition replays, 0 states visited overall)
> Execution failed with code 3.
void SafetyChecker::log_state() // override
{
on_log_state_signal();
- XBT_INFO("DFS exploration successful. %ld unique states visited; %ld backtracks (%lu transition replays, %lu states "
+ XBT_INFO("DFS exploration ended. %ld unique states visited; %ld backtracks (%lu transition replays, %lu states "
"visited overall)",
State::get_expanded_states(), backtrack_count_, api::get().mc_get_visited_states(),
Transition::get_replayed_transitions());
#!/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@) Check a safety property. Reduction is: dpor.
+> [ 0.000000] (0:maestro@) Start a DFS exploration. Reduction is: dpor.
> [ 0.000000] (0:maestro@) Behavior: assert
> [ 0.000000] (0:maestro@) **************************
> [ 0.000000] (0:maestro@) *** PROPERTY NOT VALID ***
> [ 0.000000] (0:maestro@) 27 unique states visited; 22 backtracks (68 transition replays, 19 states visited overall)
$ ${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@) Check a safety property. Reduction is: dpor.
+> [ 0.000000] (0:maestro@) Start a DFS exploration. Reduction is: dpor.
> [ 0.000000] (0:maestro@) Behavior: printf
> [ 0.000000] (1:app@Fafard) Error reached
> [ 0.000000] (0:maestro@) No property violation found.
#!/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@) Check a safety property. Reduction is: dpor.
+> [ 0.000000] (0:maestro@) Start a DFS exploration. Reduction is: dpor.
> [ 0.000000] (0:maestro@) Behavior: assert
> [ 0.000000] (0:maestro@) **************************
> [ 0.000000] (0:maestro@) *** PROPERTY NOT VALID ***
> [ 0.000000] (0:maestro@) Random([0;5] ~> 3)
> [ 0.000000] (0:maestro@) Random([0;5] ~> 4)
> [ 0.000000] (0:maestro@) Path = 1/3;1/4
-> [ 0.000000] (0:maestro@) 27 unique states visited; 22 backtracks (68 transition replays, 19 states visited overall)
+> [ 0.000000] (0:maestro@) DFS exploration ended. 27 unique states visited; 22 backtracks (68 transition replays, 19 states visited overall)
! 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@) Check a safety property. Reduction is: dpor.
+> [ 0.000000] (0:maestro@) Start a DFS exploration. Reduction is: dpor.
> [ 0.000000] (0:maestro@) Behavior: abort
> [ 0.000000] (0:maestro@) **************************
> [ 0.000000] (0:maestro@) ** CRASH IN THE PROGRAM **
> [ 0.000000] (0:maestro@) Random([0;5] ~> 3)
> [ 0.000000] (0:maestro@) Random([0;5] ~> 4)
> [ 0.000000] (0:maestro@) Path = 1/3;1/4
-> [ 0.000000] (0:maestro@) 27 unique states visited; 22 backtracks (68 transition replays, 19 states visited overall)
+> [ 0.000000] (0:maestro@) DFS exploration ended. 27 unique states visited; 22 backtracks (68 transition replays, 19 states visited overall)
> [ 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@) Check a safety property. Reduction is: dpor.
+> [ 0.000000] (0:maestro@) Start a DFS exploration. Reduction is: dpor.
> [ 0.000000] (0:maestro@) Behavior: printf
> [ 0.000000] (1:app@Fafard) Error reached
-> [ 0.000000] (0:maestro@) No property violation found.
-> [ 0.000000] (0:maestro@) 43 unique states visited; 36 backtracks (108 transition replays, 30 states visited overall)
+> [ 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@) Check a safety property. Reduction is: dpor.
+> [ 0.000000] (0:maestro@) Start a DFS exploration. Reduction is: dpor.
> [ 0.000000] (0:maestro@) Behavior: segv
> Segmentation fault.
> [ 0.000000] (0:maestro@) **************************
> [ 0.000000] (0:maestro@) Random([0;5] ~> 3)
> [ 0.000000] (0:maestro@) Random([0;5] ~> 4)
> [ 0.000000] (0:maestro@) Path = 1/3;1/4
-> [ 0.000000] (0:maestro@) 27 unique states visited; 22 backtracks (68 transition replays, 19 states visited overall)
+> [ 0.000000] (0:maestro@) DFS exploration ended. 27 unique states visited; 22 backtracks (68 transition replays, 19 states visited overall)
> [ 0.000000] (0:maestro@) Stack trace not displayed because you passed --log=no_loc
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_safety/INFO] Check a safety property. Reduction is: dpor.
+> [0.000000] [mc_safety/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
> 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] No property violation found.
-> [0.000000] [mc_safety/INFO] 73 unique states visited; 18 backtracks (592 transition replays, 502 states visited overall)
+> [0.000000] [mc_safety/INFO] DFS exploration ended. 73 unique states visited; 18 backtracks (592 transition replays, 502 states visited overall)