/** @brief Save the current state */
VisitedState::VisitedState(unsigned long state_number, unsigned int actor_count, RemoteApp& remote_app)
- : heap_bytes_used_(remote_app.get_remote_process_memory().get_remote_heap_bytes())
+ : heap_bytes_used_(remote_app.get_remote_process_memory()->get_remote_heap_bytes())
, actor_count_(actor_count)
, num_(state_number)
{
this->system_state_ = std::make_shared<simgrid::mc::Snapshot>(state_number, remote_app.get_page_store(),
- remote_app.get_remote_process_memory());
+ *remote_app.get_remote_process_memory());
}
void VisitedStates::prune()
for (auto i = range_begin; i != range_end; ++i) {
auto& visited_state = *i;
if (visited_state->system_state_->equals_to(*new_state->system_state_.get(),
- remote_app.get_remote_process_memory())) {
+ *remote_app.get_remote_process_memory())) {
// The state has been visited:
std::unique_ptr<simgrid::mc::VisitedState> old_state = std::move(visited_state);
for (auto* arg : args)
app_args_.push_back(arg);
- checker_side_ = std::make_unique<simgrid::mc::CheckerSide>(app_args_);
+ checker_side_ = std::make_unique<simgrid::mc::CheckerSide>(app_args_, need_memory_introspection);
if (need_memory_introspection)
- initial_snapshot_ = std::make_shared<simgrid::mc::Snapshot>(0, page_store_, checker_side_->get_remote_memory());
+ initial_snapshot_ = std::make_shared<simgrid::mc::Snapshot>(0, page_store_, *checker_side_->get_remote_memory());
}
RemoteApp::~RemoteApp()
{
if (initial_snapshot_ == nullptr) { // No memory introspection
shutdown();
- checker_side_.reset(
- nullptr); // We need to destroy the existing CheckerSide before creating the new one, or libevent gets crazy
- checker_side_.reset(new simgrid::mc::CheckerSide(app_args_));
+ // We need to destroy the existing CheckerSide before creating the new one, or libevent gets crazy
+ checker_side_.reset(nullptr);
+ checker_side_.reset(new simgrid::mc::CheckerSide(app_args_, true));
} else
- initial_snapshot_->restore(checker_side_->get_remote_memory());
+ initial_snapshot_->restore(*checker_side_->get_remote_memory());
}
unsigned long RemoteApp::get_maxpid() const
m.times_considered_ = times_considered;
checker_side_->get_channel().send(m);
- get_remote_process_memory().clear_cache();
+ auto* memory = get_remote_process_memory();
+ if (memory != nullptr)
+ memory->clear_cache();
if (checker_side_->running())
checker_side_->dispatch_events(); // The app may send messages while processing the transition
Transition* handle_simcall(aid_t aid, int times_considered, bool new_transition);
/* Get the memory of the remote process */
- RemoteProcessMemory& get_remote_process_memory() { return checker_side_->get_remote_memory(); }
+ RemoteProcessMemory* get_remote_process_memory() { return checker_side_->get_remote_memory(); }
PageStore& get_page_store() { return page_store_; }
};
/* Stateful model checking */
if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination)
system_state_ = std::make_shared<simgrid::mc::Snapshot>(num_, remote_app.get_page_store(),
- remote_app.get_remote_process_memory());
+ *remote_app.get_remote_process_memory());
}
State::State(RemoteApp& remote_app, const State* parent_state)
/* Stateful model checking */
if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination)
system_state_ = std::make_shared<simgrid::mc::Snapshot>(num_, remote_app.get_page_store(),
- remote_app.get_remote_process_memory());
+ *remote_app.get_remote_process_memory());
/* If we want sleep set reduction, copy the sleep set and eventually removes things from it */
if (_sg_mc_sleep_set) {
{
for (auto const& state : stack_) {
if (state->get_system_state()->equals_to(*current_state->get_system_state(),
- get_remote_app().get_remote_process_memory())) {
+ *get_remote_app().get_remote_process_memory())) {
XBT_INFO("Non-progressive cycle: state %ld -> state %ld", state->get_num(), current_state->get_num());
XBT_INFO("******************************************");
XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
/* If asked to rollback on a state that has a snapshot, restore it */
State* last_state = stack_.back().get();
if (const auto* system_state = last_state->get_system_state()) {
- system_state->restore(get_remote_app().get_remote_process_memory());
+ system_state->restore(*get_remote_app().get_remote_process_memory());
on_restore_system_state_signal(last_state, get_remote_app());
return;
}
} // If no backtracing point, then the stack is empty and the exploration is over
}
-DFSExplorer::DFSExplorer(const std::vector<char*>& args, bool with_dpor) : Exploration(args, true)
+//DFSExplorer::DFSExplorer(const std::vector<char*>& args, bool with_dpor) : Exploration(args, _sg_mc_termination) // UNCOMMENT TO ACTIVATE REFORKS
+DFSExplorer::DFSExplorer(const std::vector<char*>& args, bool with_dpor) : Exploration(args, true) // This version does not use reforks as it breaks
{
if (with_dpor)
reduction_mode_ = ReductionMode::dpor;
if (xbt_log_no_loc) {
XBT_INFO("Stack trace not displayed because you passed --log=no_loc");
} else {
- XBT_INFO("Stack trace:");
- get_remote_app().get_remote_process_memory().dump_stack();
+ auto* memory = get_remote_app().get_remote_process_memory();
+ if (memory) {
+ XBT_INFO("Stack trace:");
+ memory->dump_stack();
+ } else {
+ XBT_INFO("Stack trace not shown because there is no memory introspection.");
+ }
}
system_exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
RemoteApp& remote_app)
: num(pair_num), prop_state_(prop_state)
{
- auto& memory = remote_app.get_remote_process_memory();
+ auto* memory = remote_app.get_remote_process_memory();
this->app_state_ = std::move(app_state);
if (not this->app_state_->get_system_state())
- this->app_state_->set_system_state(std::make_shared<Snapshot>(pair_num, remote_app.get_page_store(), memory));
- this->heap_bytes_used = memory.get_remote_heap_bytes();
+ this->app_state_->set_system_state(std::make_shared<Snapshot>(pair_num, remote_app.get_page_store(), *memory));
+ this->heap_bytes_used = memory->get_remote_heap_bytes();
this->actor_count_ = app_state_->get_actor_count();
this->other_num = -1;
this->atomic_propositions = std::move(atomic_propositions);
if (xbt_automaton_state_compare(pair_test->prop_state_, new_pair->prop_state_) != 0 ||
*(pair_test->atomic_propositions) != *(new_pair->atomic_propositions) ||
(not pair_test->app_state_->get_system_state()->equals_to(*new_pair->app_state_->get_system_state(),
- get_remote_app().get_remote_process_memory())))
+ *get_remote_app().get_remote_process_memory())))
continue;
XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num);
exploration_stack_.pop_back();
if (_sg_mc_checkpoint > 0) {
const Pair* pair = exploration_stack_.back().get();
if (const auto* system_state = pair->app_state_->get_system_state()) {
- system_state->restore(get_remote_app().get_remote_process_memory());
+ system_state->restore(*get_remote_app().get_remote_process_memory());
return;
}
}
if (xbt_automaton_state_compare(pair_test->prop_state_, visited_pair->prop_state_) != 0 ||
*(pair_test->atomic_propositions) != *(visited_pair->atomic_propositions) ||
(not pair_test->app_state_->get_system_state()->equals_to(*visited_pair->app_state_->get_system_state(),
- get_remote_app().get_remote_process_memory())))
+ *get_remote_app().get_remote_process_memory())))
continue;
if (pair_test->other_num == -1)
visited_pair->other_num = pair_test->num;
xbt_assert(errno == 0 && raise(SIGSTOP) == 0, "Could not wait for the model-checker (errno = %d: %s)", errno,
strerror(errno));
- s_mc_message_initial_addresses_t message = {};
- message.type = MessageType::INITIAL_ADDRESSES;
- message.mmalloc_default_mdp = mmalloc_get_current_heap();
- xbt_assert(instance_->channel_.send(message) == 0, "Could not send the initial message with addresses.");
-
instance_->handle_messages();
return instance_.get();
}
if (terminate_asap)
::_Exit(0);
}
+void AppSide::handle_initial_addresses() const
+{
+ s_mc_message_initial_addresses_reply_t answer = {};
+ answer.type = MessageType::INITIAL_ADDRESSES_REPLY;
+ answer.mmalloc_default_mdp = mmalloc_get_current_heap();
+ xbt_assert(channel_.send(answer) == 0, "Could not send response with initial addresses.");
+}
void AppSide::handle_actors_status() const
{
auto const& actor_list = kernel::EngineImpl::get_instance()->get_actor_list();
handle_finalize((s_mc_message_int_t*)message_buffer.data());
break;
+ case MessageType::INITIAL_ADDRESSES:
+ assert_msg_size("INITIAL_ADDRESSES", s_mc_message_t);
+ handle_initial_addresses();
+ break;
+
case MessageType::ACTORS_STATUS:
assert_msg_size("ACTORS_STATUS", s_mc_message_t);
handle_actors_status();
void AppSide::ignore_memory(void* addr, std::size_t size) const
{
- if (not MC_is_active())
+ if (not MC_is_active() || not need_memory_info_)
return;
s_mc_message_ignore_memory_t message = {};
void AppSide::ignore_heap(void* address, std::size_t size) const
{
- if (not MC_is_active())
+ if (not MC_is_active() || not need_memory_info_)
return;
const s_xbt_mheap_t* heap = mmalloc_get_current_heap();
void AppSide::unignore_heap(void* address, std::size_t size) const
{
- if (not MC_is_active())
+ if (not MC_is_active() || not need_memory_info_)
return;
s_mc_message_ignore_memory_t message = {};
void AppSide::declare_symbol(const char* name, int* value) const
{
- if (not MC_is_active())
+ if (not MC_is_active() || not need_memory_info_)
return;
s_mc_message_register_symbol_t message = {};
*/
void AppSide::declare_stack(void* stack, size_t size, ucontext_t* context) const
{
- if (not MC_is_active())
+ if (not MC_is_active() || not need_memory_info_)
return;
const s_xbt_mheap_t* heap = mmalloc_get_current_heap();
private:
Channel channel_;
static std::unique_ptr<AppSide> instance_;
+ bool need_memory_info_ = false; /* by default we don't send memory info, unless we got a INITIAL_ADDRESSES */
public:
AppSide();
void handle_deadlock_check(const s_mc_message_t* msg) const;
void handle_simcall_execute(const s_mc_message_simcall_execute_t* message) const;
void handle_finalize(const s_mc_message_int_t* msg) const;
+ void handle_initial_addresses() const;
void handle_actors_status() const;
void handle_actors_maxpid() const;
signal_event_.reset(signal_event);
}
-CheckerSide::CheckerSide(const std::vector<char*>& args) : running_(true)
+CheckerSide::CheckerSide(const std::vector<char*>& args, bool need_memory_introspection) : running_(true)
{
// Create an AF_LOCAL socketpair used for exchanging messages between the model-checker process (ancestor)
// and the application process (child)
wait_application_process(pid_);
wait_for_requests();
+
+ // Request the initial memory on need
+ if (need_memory_introspection) {
+ channel_.send(MessageType::INITIAL_ADDRESSES);
+ s_mc_message_initial_addresses_reply_t answer;
+ ssize_t answer_size = channel_.receive(answer);
+ xbt_assert(answer_size != -1, "Could not receive message");
+ xbt_assert(answer.type == MessageType::INITIAL_ADDRESSES_REPLY,
+ "The received message is not the INITIAL_ADDRESS_REPLY I was expecting but of type %s",
+ to_c_str(answer.type));
+ xbt_assert(answer_size == sizeof answer, "Broken message (size=%zd; expected %zu)", answer_size, sizeof answer);
+
+ /* We now have enough info to create the memory address space */
+ remote_memory_ = std::make_unique<simgrid::mc::RemoteProcessMemory>(pid_, answer.mmalloc_default_mdp);
+ }
}
void CheckerSide::dispatch_events() const
memcpy(&base_message, buffer, sizeof(base_message));
switch (base_message.type) {
- case MessageType::INITIAL_ADDRESSES: {
- s_mc_message_initial_addresses_t message;
- xbt_assert(size == sizeof(message), "Broken message. Got %d bytes instead of %d.", (int)size,
- (int)sizeof(message));
- memcpy(&message, buffer, sizeof(message));
- /* Create the memory address space, now that we have the mandatory information */
- remote_memory_ = std::make_unique<simgrid::mc::RemoteProcessMemory>(pid_, message.mmalloc_default_mdp);
- break;
- }
-
case MessageType::IGNORE_HEAP: {
- s_mc_message_ignore_heap_t message;
- xbt_assert(size == sizeof(message), "Broken message");
- memcpy(&message, buffer, sizeof(message));
-
- IgnoredHeapRegion region;
- region.block = message.block;
- region.fragment = message.fragment;
- region.address = message.address;
- region.size = message.size;
- get_remote_memory().ignore_heap(region);
+ if (remote_memory_ != nullptr) {
+ s_mc_message_ignore_heap_t message;
+ xbt_assert(size == sizeof(message), "Broken message");
+ memcpy(&message, buffer, sizeof(message));
+
+ IgnoredHeapRegion region;
+ region.block = message.block;
+ region.fragment = message.fragment;
+ region.address = message.address;
+ region.size = message.size;
+ get_remote_memory()->ignore_heap(region);
+ } else {
+ XBT_INFO("Ignoring a IGNORE_HEAP message because we don't need to introspect memory.");
+ }
break;
}
case MessageType::UNIGNORE_HEAP: {
- s_mc_message_ignore_memory_t message;
- xbt_assert(size == sizeof(message), "Broken message");
- memcpy(&message, buffer, sizeof(message));
- get_remote_memory().unignore_heap((void*)(std::uintptr_t)message.addr, message.size);
+ if (remote_memory_ != nullptr) {
+ s_mc_message_ignore_memory_t message;
+ xbt_assert(size == sizeof(message), "Broken message");
+ memcpy(&message, buffer, sizeof(message));
+ get_remote_memory()->unignore_heap((void*)(std::uintptr_t)message.addr, message.size);
+ } else {
+ XBT_INFO("Ignoring an UNIGNORE_HEAP message because we don't need to introspect memory.");
+ }
break;
}
case MessageType::IGNORE_MEMORY: {
- s_mc_message_ignore_memory_t message;
- xbt_assert(size == sizeof(message), "Broken message");
- memcpy(&message, buffer, sizeof(message));
- get_remote_memory().ignore_region(message.addr, message.size);
+ if (remote_memory_ != nullptr) {
+ s_mc_message_ignore_memory_t message;
+ xbt_assert(size == sizeof(message), "Broken message");
+ memcpy(&message, buffer, sizeof(message));
+ get_remote_memory()->ignore_region(message.addr, message.size);
+ } else {
+ XBT_INFO("Ignoring an IGNORE_MEMORY message because we don't need to introspect memory.");
+ }
break;
}
case MessageType::STACK_REGION: {
- s_mc_message_stack_region_t message;
- xbt_assert(size == sizeof(message), "Broken message");
- memcpy(&message, buffer, sizeof(message));
- get_remote_memory().stack_areas().push_back(message.stack_region);
- } break;
+ if (remote_memory_ != nullptr) {
+ s_mc_message_stack_region_t message;
+ xbt_assert(size == sizeof(message), "Broken message");
+ memcpy(&message, buffer, sizeof(message));
+ get_remote_memory()->stack_areas().push_back(message.stack_region);
+ } else {
+ XBT_INFO("Ignoring an STACK_REGION message because we don't need to introspect memory.");
+ }
+ break;
+ }
case MessageType::REGISTER_SYMBOL: {
s_mc_message_register_symbol_t message;
xbt_assert(not message.callback, "Support for client-side function proposition is not implemented.");
XBT_DEBUG("Received symbol: %s", message.name.data());
- LivenessChecker::automaton_register_symbol(get_remote_memory(), message.name.data(), remote((int*)message.data));
+ LivenessChecker::automaton_register_symbol(*get_remote_memory(), message.name.data(), remote((int*)message.data));
break;
}
event_del(evt);
event_free(evt);
};
- std::unique_ptr<event, decltype(&event_free)> socket_event_{nullptr, free_event_fun};
- std::unique_ptr<event, decltype(&event_free)> signal_event_{nullptr, free_event_fun};
+ std::unique_ptr<event, decltype(&event_free)> socket_event_{nullptr, &event_free};
+ std::unique_ptr<event, decltype(&event_free)> signal_event_{nullptr, &event_free};
std::unique_ptr<event_base, decltype(&event_base_free)> base_{nullptr, &event_base_free};
std::unique_ptr<RemoteProcessMemory> remote_memory_;
void handle_waitpid();
public:
- explicit CheckerSide(const std::vector<char*>& args);
+ explicit CheckerSide(const std::vector<char*>& args, bool need_memory_introspection);
// No copy:
CheckerSide(CheckerSide const&) = delete;
pid_t get_pid() const { return pid_; }
bool running() const { return running_; }
void terminate() { running_ = false; }
- RemoteProcessMemory& get_remote_memory() { return *remote_memory_.get(); }
+ RemoteProcessMemory* get_remote_memory() { return remote_memory_.get(); }
};
} // namespace simgrid::mc
// ***** Messages
namespace simgrid::mc {
-XBT_DECLARE_ENUM_CLASS(MessageType, NONE, INITIAL_ADDRESSES, CONTINUE, IGNORE_HEAP, UNIGNORE_HEAP, IGNORE_MEMORY,
- STACK_REGION, REGISTER_SYMBOL, DEADLOCK_CHECK, DEADLOCK_CHECK_REPLY, WAITING, SIMCALL_EXECUTE,
- SIMCALL_EXECUTE_ANSWER, ASSERTION_FAILED, ACTORS_STATUS, ACTORS_STATUS_REPLY, ACTORS_MAXPID,
- ACTORS_MAXPID_REPLY, FINALIZE, FINALIZE_REPLY);
+XBT_DECLARE_ENUM_CLASS(MessageType, NONE, INITIAL_ADDRESSES, INITIAL_ADDRESSES_REPLY, CONTINUE, IGNORE_HEAP,
+ UNIGNORE_HEAP, IGNORE_MEMORY, STACK_REGION, REGISTER_SYMBOL, DEADLOCK_CHECK,
+ DEADLOCK_CHECK_REPLY, WAITING, SIMCALL_EXECUTE, SIMCALL_EXECUTE_ANSWER, ASSERTION_FAILED,
+ ACTORS_STATUS, ACTORS_STATUS_REPLY, ACTORS_MAXPID, ACTORS_MAXPID_REPLY, FINALIZE,
+ FINALIZE_REPLY);
} // namespace simgrid::mc
constexpr unsigned MC_MESSAGE_LENGTH = 512;
};
/* Client->Server */
-struct s_mc_message_initial_addresses_t {
- simgrid::mc::MessageType type;
- xbt_mheap_t mmalloc_default_mdp;
-};
-
struct s_mc_message_ignore_heap_t {
simgrid::mc::MessageType type;
int block;
};
/* Server -> client */
+struct s_mc_message_initial_addresses_reply_t {
+ simgrid::mc::MessageType type;
+ xbt_mheap_t mmalloc_default_mdp;
+};
+
struct s_mc_message_simcall_execute_t {
simgrid::mc::MessageType type;
aid_t aid_;
