}
}
-bool Session::actor_is_enabled(aid_t pid) const
+void Session::get_actors_status(std::map<aid_t, ActorState>& whereto)
{
- s_mc_message_actor_enabled_t msg;
+ s_mc_message_t msg;
memset(&msg, 0, sizeof msg);
- msg.type = simgrid::mc::MessageType::ACTOR_ENABLED;
- msg.aid = pid;
+ msg.type = simgrid::mc::MessageType::ACTORS_STATUS;
model_checker_->channel().send(msg);
- std::array<char, MC_MESSAGE_LENGTH> buff;
- ssize_t received = model_checker_->channel().receive(buff.data(), buff.size(), true);
- xbt_assert(received == sizeof(s_mc_message_int_t), "Unexpected size in answer to ACTOR_ENABLED");
- return ((s_mc_message_int_t*)buff.data())->value;
+
+ s_mc_message_actors_status_answer_t answer;
+ ssize_t received = model_checker_->channel().receive(answer);
+ xbt_assert(received != -1, "Could not receive message");
+ xbt_assert(received == sizeof(answer) && answer.type == MessageType::ACTORS_STATUS_REPLY,
+ "Received unexpected message %s (%i, size=%i) "
+ "expected MessageType::ACTORS_STATUS_REPLY (%i, size=%i)",
+ to_c_str(answer.type), (int)answer.type, (int)received, (int)MessageType::ACTORS_STATUS_REPLY,
+ (int)sizeof(answer));
+
+ s_mc_message_actors_status_one_t status[answer.count];
+ received = model_checker_->channel().receive(&status, sizeof(status));
+ xbt_assert(static_cast<size_t>(received) == sizeof(status));
+
+ whereto.clear();
+ for (auto const& actor : status)
+ whereto.insert(std::make_pair(actor.aid, ActorState(actor.aid, actor.enabled, actor.max_considered)));
}
void Session::check_deadlock() const
#ifndef SIMGRID_MC_SESSION_HPP
#define SIMGRID_MC_SESSION_HPP
+#include "mc_pattern.hpp"
#include "simgrid/forward.h"
#include "src/mc/ModelChecker.hpp"
#include "src/mc/remote/RemotePtr.hpp"
void log_state() const;
- bool actor_is_enabled(aid_t pid) const;
+ void get_actors_status(std::map<aid_t, ActorState>& whereto);
};
} // namespace simgrid::mc
State::State(Session& session) : num_(++expended_states_)
{
- auto actors = mc_model_checker->get_remote_process().actors();
-
- for (unsigned int i = 0; i < actors.size(); i++) {
- auto remote_actor = actors[i].copy.get_buffer();
- aid_t aid = remote_actor->get_pid();
-
- actors_to_run_.insert(
- std::make_pair(aid, ActorState(aid, session.actor_is_enabled(aid), remote_actor->simcall_.mc_max_consider_)));
- }
+ session.get_actors_status(actors_to_run_);
transition_.reset(new Transition());
/* Stateful model checking */
xbt_assert(channel_.send(answer) == 0, "Could not send response");
}
-void AppSide::handle_actor_enabled(const s_mc_message_actor_enabled_t* msg) const
-{
- bool res = mc::actor_is_enabled(kernel::EngineImpl::get_instance()->get_actor_by_pid(msg->aid));
- s_mc_message_int_t answer{MessageType::ACTOR_ENABLED_REPLY, res};
- xbt_assert(channel_.send(answer) == 0, "Could not send ACTOR_ENABLED_REPLY");
-}
-
void AppSide::handle_finalize(const s_mc_message_int_t* msg) const
{
bool terminate_asap = msg->value;
#endif
}
coverage_checkpoint();
- xbt_assert(channel_.send(MessageType::DEADLOCK_CHECK_REPLY) == 0, // DEADLOCK_CHECK_REPLY, really?
+ xbt_assert(channel_.send(MessageType::DEADLOCK_CHECK_REPLY) ==
+ 0, // DEADLOCK_CHECK_REPLY because I'm too lazy to create another message type with no content (FIXME)
"Could not answer to FINALIZE");
std::fflush(stdout);
if (terminate_asap)
::_Exit(0);
}
+void AppSide::handle_actors_status() const
+{
+ auto const& actor_list = kernel::EngineImpl::get_instance()->get_actor_list();
+ int count = actor_list.size();
+
+ struct s_mc_message_actors_status_answer_t answer {
+ MessageType::ACTORS_STATUS_REPLY, count
+ };
+ s_mc_message_actors_status_one_t status[count];
+ int i = 0;
+ for (auto const& [aid, actor] : actor_list) {
+ status[i].aid = aid;
+ status[i].enabled = mc::actor_is_enabled(actor);
+ status[i].max_considered = actor->simcall_.observer_->get_max_consider();
+ i++;
+ }
+ xbt_assert(channel_.send(answer) == 0, "Could not send ACTORS_STATUS_REPLY msg");
+ xbt_assert(channel_.send(status, sizeof(status)) == 0, "Could not send ACTORS_STATUS_REPLY data");
+}
#define assert_msg_size(_name_, _type_) \
xbt_assert(received_size == sizeof(_type_), "Unexpected size for " _name_ " (%zd != %zu)", received_size, \
handle_simcall_execute((s_mc_message_simcall_execute_t*)message_buffer.data());
break;
- case MessageType::ACTOR_ENABLED:
- assert_msg_size("ACTOR_ENABLED", s_mc_message_actor_enabled_t);
- handle_actor_enabled((s_mc_message_actor_enabled_t*)message_buffer.data());
- break;
-
case MessageType::FINALIZE:
assert_msg_size("FINALIZE", s_mc_message_int_t);
handle_finalize((s_mc_message_int_t*)message_buffer.data());
break;
+ case MessageType::ACTORS_STATUS:
+ assert_msg_size("ACTORS_STATUS", s_mc_message_t);
+ handle_actors_status();
+ break;
+
default:
xbt_die("Received unexpected message %s (%i)", to_c_str(message->type), static_cast<int>(message->type));
break;
private:
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_actor_enabled(const s_mc_message_actor_enabled_t* msg) const;
void handle_finalize(const s_mc_message_int_t* msg) const;
+ void handle_actors_status() const;
public:
Channel const& get_channel() const { return channel_; }
info->remove_local_variable(var_name, frame_name);
}
-/** Load the remote list of actors into the Checker process
- *
- * FIXME: This shall die alltogether and be reimplemented with a networked communication to not suppose anything about
- * the memory layout of the checked App if avoidable.
- *
- * Liveness checking will always require to explore the memory of the App, but safety checking doesn't.
- */
-
-std::vector<simgrid::mc::ActorInformation>& RemoteProcess::actors()
-{
- if (not(this->cache_flags_ & RemoteProcess::cache_simix_processes)) {
- smx_actors_infos.clear();
-
- s_xbt_dynar_t dynar;
- read_bytes(&dynar, sizeof(dynar), actors_addr_);
-
- auto* data = static_cast<simgrid::kernel::actor::ActorImpl**>(::operator new(dynar.elmsize* dynar.used));
- read_bytes(data, dynar.elmsize * dynar.used, simgrid::mc::RemotePtr<void>(dynar.data));
-
- // Load each element of the vector from the MCed process:
- for (unsigned int i = 0; i < dynar.used; ++i) {
- simgrid::mc::ActorInformation info;
-
- info.address = simgrid::mc::RemotePtr<simgrid::kernel::actor::ActorImpl>(data[i]);
- read_bytes(&info.copy, sizeof(info.copy), simgrid::mc::remote(data[i]));
- smx_actors_infos.push_back(std::move(info));
- }
- ::operator delete(data);
-
- this->cache_flags_ |= RemoteProcess::cache_simix_processes;
- }
- return smx_actors_infos;
-}
-
void RemoteProcess::dump_stack() const
{
unw_addr_space_t as = unw_create_addr_space(&_UPT_accessors, BYTE_ORDER);
static constexpr int cache_none = 0;
static constexpr int cache_heap = 1;
static constexpr int cache_malloc = 2;
- static constexpr int cache_simix_processes = 4;
public:
explicit RemoteProcess(pid_t pid);
RemotePtr<s_xbt_dynar_t> actors_addr_;
public:
- std::vector<ActorInformation>& actors();
-
unsigned long get_maxpid() const { return this->read(maxpid_addr_); }
void dump_stack() const;
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, ACTOR_ENABLED, ACTOR_ENABLED_REPLY, FINALIZE);
-
+ SIMCALL_EXECUTE_ANSWER, ASSERTION_FAILED, ACTORS_STATUS, ACTORS_STATUS_REPLY, FINALIZE);
} // namespace simgrid::mc
constexpr unsigned MC_MESSAGE_LENGTH = 512;
int index;
};
-struct s_mc_message_actor_enabled_t {
+struct s_mc_message_actors_status_answer_t {
simgrid::mc::MessageType type;
- aid_t aid; // actor ID
+ int count;
+};
+struct s_mc_message_actors_status_one_t { // an array of `s_mc_message_actors_status_one_t[count]` is sent right after
+ // after a s_mc_message_actors_status_answer_t
+ aid_t aid;
+ bool enabled;
+ int max_considered;
};
#endif // __cplusplus
