include src/mc/api/State.hpp
include src/mc/compare.cpp
include src/mc/explo/CommunicationDeterminismChecker.cpp
+include src/mc/explo/DFSExplorer.cpp
+include src/mc/explo/DFSExplorer.hpp
include src/mc/explo/Exploration.hpp
include src/mc/explo/LivenessChecker.cpp
include src/mc/explo/LivenessChecker.hpp
-include src/mc/explo/SafetyChecker.cpp
-include src/mc/explo/SafetyChecker.hpp
include src/mc/explo/UdporChecker.cpp
include src/mc/explo/UdporChecker.hpp
include src/mc/explo/simgrid_mc.cpp
#!/usr/bin/env tesh
$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/s4u-mc-electric-fence ${platfdir}/model_checker_platform.xml
-> [0.000000] [mc_safety/INFO] Start a DFS exploration. Reduction is: dpor.
+> [0.000000] [mc_dfs/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] DFS exploration ended. 15 unique states visited; 5 backtracks (32 transition replays, 13 states visited overall)
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 15 unique states visited; 5 backtracks (32 transition replays, 13 states visited overall)
#!/usr/bin/env tesh
-$ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_safety.thres:verbose --log=root.fmt="[Checker]%e%m%n" -- ${bindir:=.}/s4u-synchro-barrier 1 --log=s4u_test.thres:critical --log=root.fmt="[App%e%e%e%e]%e%m%n"
+$ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt="[Checker]%e%m%n" -- ${bindir:=.}/s4u-synchro-barrier 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.
> [Checker] Execute 1: BARRIER_LOCK(barrier: 0) (stack depth: 1, state: 1, 0 interleaves)
> [Checker] Execute 1: BARRIER_WAIT(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
> [Checker] Backtracking from 1;1;0
> [Checker] DFS exploration ended. 3 unique states visited; 1 backtracks (3 transition replays, 0 states visited overall)
-$ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_safety.thres:verbose --log=root.fmt="[Checker]%e%m%n" -- ${bindir:=.}/s4u-synchro-barrier 2 --log=s4u_test.thres:critical --log=root.fmt="[App%e%e%e%e]%e%m%n"
+$ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt="[Checker]%e%m%n" -- ${bindir:=.}/s4u-synchro-barrier 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.
> [Checker] Execute 1: BARRIER_LOCK(barrier: 0) (stack depth: 1, state: 1, 0 interleaves)
> [Checker] Execute 2: BARRIER_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
> [Checker] Backtracking from 1;2
> [Checker] DFS exploration ended. 5 unique states visited; 2 backtracks (7 transition replays, 1 states visited overall)
-$ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_safety.thres:verbose --log=root.fmt="[Checker]%e%m%n" -- ${bindir:=.}/s4u-synchro-barrier 3 --log=s4u_test.thres:critical --log=root.fmt="[App%e%e%e%e]%e%m%n"
+$ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt="[Checker]%e%m%n" -- ${bindir:=.}/s4u-synchro-barrier 3 --log=s4u_test.thres:critical --log=root.fmt="[App%e%e%e%e]%e%m%n"
> [Checker] Start a DFS exploration. Reduction is: dpor.
> [Checker] Execute 1: BARRIER_LOCK(barrier: 0) (stack depth: 1, state: 1, 0 interleaves)
> [Checker] Execute 2: BARRIER_LOCK(barrier: 0) (stack depth: 2, state: 2, 0 interleaves)
p This file tests the dependencies between MUTEX transitions
-$ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_safety.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"
+$ ${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] Execute 2: MUTEX_LOCK(mutex: 0, owner:2) (stack depth: 1, state: 1, 0 interleaves)
> [Checker] MUTEX_LOCK(mutex: 0, owner:3) (state=8)
> [Checker] DFS exploration ended. 13 unique states visited; 3 backtracks (18 transition replays, 3 states visited overall)
-$ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_safety.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"
+$ ${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] Execute 2: MUTEX_LOCK(mutex: 0, owner:2) (stack depth: 1, state: 1, 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_safety/INFO] Start a DFS exploration. Reduction is: dpor.
+> [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_safety/INFO] DFS exploration ended. 85 unique states visited; 15 backtracks (240 transition replays, 141 states visited overall)
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 85 unique states visited; 15 backtracks (240 transition replays, 141 states visited overall)
#!/usr/bin/env tesh
-$ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_safety.thres:verbose --log=root.fmt="[Checker]%e%m%n" -- ${bindir:=.}/s4u-synchro-semaphore --log=sem_test.thres:critical --log=root.fmt="[App%e%e%e%e]%e%m%n"
+$ ${bindir:=.}/../../../bin/simgrid-mc --log=mc_dfs.thres:verbose --log=root.fmt="[Checker]%e%m%n" -- ${bindir:=.}/s4u-synchro-semaphore --log=sem_test.thres:critical --log=root.fmt="[App%e%e%e%e]%e%m%n"
> [Checker] Start a DFS exploration. Reduction is: dpor.
> [Checker] Execute 1: SEM_LOCK(semaphore: 0) (stack depth: 1, state: 1, 0 interleaves)
> [Checker] Execute 1: SEM_WAIT(semaphore: 0, granted: yes) (stack depth: 2, state: 2, 0 interleaves)
! timeout 60
$ ../../../smpi_script/bin/smpirun -wrapper "${bindir:=.}/../../../bin/simgrid-mc" --log=xbt_cfg.thresh:warning -hostfile ${srcdir:=.}/hostfile_only_send_deterministic -platform ${srcdir:=.}/../../platforms/cluster_backbone.xml --cfg=model-check/communications-determinism:1 --cfg=smpi/buffering:zero --cfg=smpi/host-speed:1Gf ./smpi_only_send_deterministic
-> [0.000000] [mc_safety/INFO] Start a DFS exploration. Reduction is: dpor.
+> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor.
> [0.000000] [mc_comm_determinism/INFO] Check communication determinism
> [0.000000] [mc_comm_determinism/INFO] *******************************************************
> [0.000000] [mc_comm_determinism/INFO] **** Only-send-deterministic communication pattern ****
> [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 ended. 36 unique states visited; 13 backtracks (97 transition replays, 49 states visited overall)
\ No newline at end of file
+> [0.000000] [mc_dfs/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] Start a DFS exploration. Reduction is: dpor.
+> [0.000000] [mc_dfs/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] DFS exploration ended. 7 unique states visited; 2 backtracks (10 transition replays, 2 states visited overall)
+> [0.000000] [mc_dfs/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] Start a DFS exploration. Reduction is: dpor.
+> [0.000000] [mc_dfs/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] [mc_global/INFO] Path = 1;2
-> [0.000000] [mc_safety/INFO] DFS exploration ended. 3 unique states visited; 1 backtracks (3 transition replays, 0 states visited overall)
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 3 unique states visited; 1 backtracks (3 transition replays, 0 states visited overall)
> Execution failed with code 3.
break;
case ExplorationAlgorithm::Safety:
- explo = simgrid::mc::create_safety_checker(session_.get());
+ explo = simgrid::mc::create_dfs_exploration(session_.get());
break;
case ExplorationAlgorithm::Liveness:
* under the terms of the license (GNU LGPL) which comes with this package. */
#include "src/kernel/activity/MailboxImpl.hpp"
-#include "src/mc/explo/SafetyChecker.hpp"
+#include "src/mc/explo/DFSExplorer.hpp"
#include "src/mc/mc_config.hpp"
#include "src/mc/mc_exit.hpp"
#include "src/mc/mc_forward.hpp"
auto extension = new CommDetExtension();
- SafetyChecker::on_exploration_start([extension]() {
+ DFSExplorer::on_exploration_start([extension]() {
XBT_INFO("Check communication determinism");
extension->exploration_start();
});
- SafetyChecker::on_backtracking([extension]() { extension->initial_communications_pattern_done = true; });
- SafetyChecker::on_state_creation([extension](State* state) { state->extension_set(new StateCommDet(extension)); });
+ DFSExplorer::on_backtracking([extension]() { extension->initial_communications_pattern_done = true; });
+ DFSExplorer::on_state_creation([extension](State* state) { state->extension_set(new StateCommDet(extension)); });
- SafetyChecker::on_restore_system_state(
- [extension](State* state) { extension->restore_communications_pattern(state); });
+ DFSExplorer::on_restore_system_state([extension](State* state) { extension->restore_communications_pattern(state); });
- SafetyChecker::on_restore_initial_state([extension]() {
+ DFSExplorer::on_restore_initial_state([extension]() {
const unsigned long maxpid = Api::get().get_maxpid();
assert(maxpid == extension->incomplete_communications_pattern.size());
assert(maxpid == extension->initial_communications_pattern.size());
}
});
- SafetyChecker::on_transition_replay([extension](Transition* t) { extension->handle_comm_pattern(t); });
- SafetyChecker::on_transition_execute([extension](Transition* t) { extension->handle_comm_pattern(t); });
+ DFSExplorer::on_transition_replay([extension](Transition* t) { extension->handle_comm_pattern(t); });
+ DFSExplorer::on_transition_execute([extension](Transition* t) { extension->handle_comm_pattern(t); });
- SafetyChecker::on_log_state([extension]() {
+ DFSExplorer::on_log_state([extension]() {
if (_sg_mc_comms_determinism) {
if (extension->send_deterministic && not extension->recv_deterministic) {
XBT_INFO("*******************************************************");
delete extension;
});
- return new SafetyChecker(session);
+ return new DFSExplorer(session);
}
} // namespace mc
/* This program is free software; you can redistribute it and/or modify it
* under the terms of the license (GNU LGPL) which comes with this package. */
-#include "src/mc/explo/SafetyChecker.hpp"
+#include "src/mc/explo/DFSExplorer.hpp"
#include "src/mc/VisitedState.hpp"
#include "src/mc/mc_config.hpp"
#include "src/mc/mc_exit.hpp"
#include <string>
#include <vector>
-XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc, "Logging specific to MC safety verification ");
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dfs, mc, "DFS exploration algorithm of the model-checker");
namespace simgrid {
namespace mc {
-xbt::signal<void()> SafetyChecker::on_exploration_start_signal;
-xbt::signal<void()> SafetyChecker::on_backtracking_signal;
+xbt::signal<void()> DFSExplorer::on_exploration_start_signal;
+xbt::signal<void()> DFSExplorer::on_backtracking_signal;
-xbt::signal<void(State*)> SafetyChecker::on_state_creation_signal;
+xbt::signal<void(State*)> DFSExplorer::on_state_creation_signal;
-xbt::signal<void(State*)> SafetyChecker::on_restore_system_state_signal;
-xbt::signal<void()> SafetyChecker::on_restore_initial_state_signal;
-xbt::signal<void(Transition*)> SafetyChecker::on_transition_replay_signal;
-xbt::signal<void(Transition*)> SafetyChecker::on_transition_execute_signal;
+xbt::signal<void(State*)> DFSExplorer::on_restore_system_state_signal;
+xbt::signal<void()> DFSExplorer::on_restore_initial_state_signal;
+xbt::signal<void(Transition*)> DFSExplorer::on_transition_replay_signal;
+xbt::signal<void(Transition*)> DFSExplorer::on_transition_execute_signal;
-xbt::signal<void()> SafetyChecker::on_log_state_signal;
+xbt::signal<void()> DFSExplorer::on_log_state_signal;
-void SafetyChecker::check_non_termination(const State* current_state)
+void DFSExplorer::check_non_termination(const State* current_state)
{
for (auto state = stack_.rbegin(); state != stack_.rend(); ++state)
if (Api::get().snapshot_equal((*state)->system_state_.get(), current_state->system_state_.get())) {
}
}
-RecordTrace SafetyChecker::get_record_trace() // override
+RecordTrace DFSExplorer::get_record_trace() // override
{
RecordTrace res;
for (auto const& state : stack_)
return res;
}
-std::vector<std::string> SafetyChecker::get_textual_trace() // override
+std::vector<std::string> DFSExplorer::get_textual_trace() // override
{
std::vector<std::string> trace;
for (auto const& state : stack_)
return trace;
}
-void SafetyChecker::log_state() // override
+void DFSExplorer::log_state() // override
{
on_log_state_signal();
XBT_INFO("DFS exploration ended. %ld unique states visited; %ld backtracks (%lu transition replays, %lu states "
Transition::get_replayed_transitions());
}
-void SafetyChecker::run()
+void DFSExplorer::run()
{
on_exploration_start_signal();
/* This function runs the DFS algorithm the state space.
log_state();
}
-void SafetyChecker::backtrack()
+void DFSExplorer::backtrack()
{
backtrack_count_++;
XBT_VERB("Backtracking from %s", get_record_trace().to_string().c_str());
}
}
-void SafetyChecker::restore_state()
+void DFSExplorer::restore_state()
{
/* If asked to rollback on a state that has a snapshot, restore it */
State* last_state = stack_.back().get();
}
}
-SafetyChecker::SafetyChecker(Session* session) : Exploration(session)
+DFSExplorer::DFSExplorer(Session* session) : Exploration(session)
{
reductionMode_ = reduction_mode;
if (_sg_mc_termination)
get_session().take_initial_snapshot();
- XBT_DEBUG("Starting the safety algorithm");
+ XBT_DEBUG("Starting the DFS exploration");
auto initial_state = std::make_unique<State>();
stack_.push_back(std::move(initial_state));
}
-Exploration* create_safety_checker(Session* session)
+Exploration* create_dfs_exploration(Session* session)
{
- return new SafetyChecker(session);
+ return new DFSExplorer(session);
}
} // namespace mc
-/* Copyright (c) 2008-2022. The SimGrid Team.
- * All rights reserved. */
+/* Copyright (c) 2008-2022. The SimGrid Team. All rights reserved. */
/* This program is free software; you can redistribute it and/or modify it
* under the terms of the license (GNU LGPL) which comes with this package. */
namespace simgrid {
namespace mc {
-class XBT_PRIVATE SafetyChecker : public Exploration {
+class XBT_PRIVATE DFSExplorer : public Exploration {
ReductionMode reductionMode_ = ReductionMode::unset;
long backtrack_count_ = 0;
static xbt::signal<void()> on_log_state_signal;
public:
- explicit SafetyChecker(Session* session);
+ explicit DFSExplorer(Session* session);
void run() override;
RecordTrace get_record_trace() override;
std::vector<std::string> get_textual_trace() override;
// External constructors so that the types (and the types of their content) remain hidden
XBT_PUBLIC Exploration* create_liveness_checker(Session* session);
-XBT_PUBLIC Exploration* create_safety_checker(Session* session);
+XBT_PUBLIC Exploration* create_dfs_exploration(Session* session);
XBT_PUBLIC Exploration* create_communication_determinism_checker(Session* session);
XBT_PUBLIC Exploration* create_udpor_checker(Session* session);
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] Start a DFS exploration. Reduction is: dpor.
+> [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
> 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] DFS exploration ended. 73 unique states visited; 18 backtracks (592 transition replays, 502 states visited overall)
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 73 unique states visited; 18 backtracks (592 transition replays, 502 states visited overall)
set(MC_SRC
src/mc/explo/Exploration.hpp
src/mc/explo/CommunicationDeterminismChecker.cpp
- src/mc/explo/SafetyChecker.cpp
- src/mc/explo/SafetyChecker.hpp
+ src/mc/explo/DFSExplorer.cpp
+ src/mc/explo/DFSExplorer.hpp
src/mc/explo/LivenessChecker.cpp
src/mc/explo/LivenessChecker.hpp
src/mc/explo/UdporChecker.cpp
