static double next() { return simix_timers().empty() ? -1.0 : simix_timers().top().first; }
};
+// In MC mode, the application sends these pointers to the MC
+void* simix_global_get_actors_addr();
+void* simix_global_get_dead_actors_addr();
+
} // namespace simix
} // namespace simgrid
{
return maxpid;
}
+void* get_maxpid_addr()
+{
+ return &maxpid;
+}
ActorImpl* ActorImpl::by_PID(aid_t PID)
{
auto item = simix_global->process_list.find(PID);
XBT_PUBLIC void create_maestro(const std::function<void()>& code);
XBT_PUBLIC unsigned long get_maxpid();
+XBT_PUBLIC void* get_maxpid_addr(); // In MC mode, the application sends this pointers to the MC
+
} // namespace actor
} // namespace kernel
} // namespace simgrid
if (res < 0 || not WIFSTOPPED(status) || WSTOPSIG(status) != SIGSTOP)
xbt_die("Could not wait model-checked process");
- remote_process_->init();
-
if (not _sg_mc_dot_output_file.get().empty())
MC_init_dot_output();
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 %zd bytes instead of %zd.", size, sizeof(message));
+ memcpy(&message, buffer, sizeof(message));
+
+ get_remote_process().init(message.mmalloc_default_mdp, message.maxpid, message.actors, message.dead_actors);
+ break;
+ }
+
case MessageType::IGNORE_HEAP: {
s_mc_message_ignore_heap_t message;
xbt_assert(size == sizeof(message), "Broken message");
#include "src/kernel/actor/ActorImpl.hpp"
#include "src/mc/checker/SimcallObserver.hpp"
#include "src/mc/remote/RemoteProcess.hpp"
+#include "src/xbt_modinter.h" /* mmalloc_preinit to get the default mmalloc arena address */
#include <simgrid/modelchecker.h>
#include <cerrno>
if (errno != 0 || raise(SIGSTOP) != 0)
xbt_die("Could not wait for the model-checker (errno = %d: %s)", errno, strerror(errno));
+ s_mc_message_initial_addresses_t message{
+ MessageType::INITIAL_ADDRESSES, mmalloc_preinit(), simgrid::kernel::actor::get_maxpid_addr(),
+ simgrid::simix::simix_global_get_actors_addr(), simgrid::simix::simix_global_get_dead_actors_addr()};
+ xbt_assert(instance_->channel_.send(message) == 0, "Could not send the initial message with addresses.");
+
instance_->handle_messages();
return instance_.get();
}
RemoteProcess::RemoteProcess(pid_t pid) : AddressSpace(this), pid_(pid), running_(true) {}
-void RemoteProcess::init()
+void RemoteProcess::init(void* mmalloc_default_mdp, void* maxpid, void* actors, void* dead_actors)
{
+ this->heap_address = mmalloc_default_mdp;
+ this->maxpid_addr_ = maxpid;
+ this->actors_addr_ = actors;
+ this->dead_actors_addr_ = dead_actors;
+
this->memory_map_ = simgrid::xbt::get_memory_map(this->pid_);
this->init_memory_map_info();
xbt_assert(fd >= 0, "Could not open file for process virtual address space");
this->memory_file = fd;
- // Read std_heap (is a struct mdesc*):
- const simgrid::mc::Variable* std_heap_var = this->find_variable("__mmalloc_default_mdp");
- xbt_assert(std_heap_var, "No heap information in the target process");
- xbt_assert(std_heap_var->address, "No constant address for this variable");
- this->read_bytes(&this->heap_address, sizeof(mdesc*), remote(std_heap_var->address));
-
this->smx_actors_infos.clear();
this->smx_dead_actors_infos.clear();
this->unw_addr_space = simgrid::mc::UnwindContext::createUnwindAddressSpace();
unsigned long RemoteProcess::get_maxpid() const
{
- static void* maxpid_addr = nullptr;
- if (maxpid_addr == nullptr) {
- const Variable* maxpid_var = find_variable("simgrid::kernel::actor::maxpid");
- if (maxpid_var == nullptr)
- maxpid_var = find_variable("maxpid"); // GCC sometimes eats the namespaces
- maxpid_addr = maxpid_var->address;
- }
unsigned long maxpid;
- this->read_bytes(&maxpid, sizeof(unsigned long), remote(maxpid_addr));
-
+ this->read_bytes(&maxpid, sizeof(unsigned long), remote(maxpid_addr_));
return maxpid;
}
void RemoteProcess::get_actor_vectors(RemotePtr<s_xbt_dynar_t>& actors, RemotePtr<s_xbt_dynar_t>& dead_actors)
{
- static_assert(std::is_same<std::unique_ptr<simgrid::simix::Global>, decltype(simix_global)>::value,
- "Unexpected type for simix_global");
- static_assert(sizeof(simix_global) == sizeof(simgrid::simix::Global*), "Bad size for simix_global");
-
- static RemotePtr<s_xbt_dynar_t> actors_;
- static RemotePtr<s_xbt_dynar_t> dead_actors_;
- static bool inited = false;
- if (not inited) {
- RemotePtr<simgrid::simix::Global> simix_global_p{this->read_variable<simgrid::simix::Global*>("simix_global")};
- Remote<simgrid::simix::Global> simix_global = this->read<simgrid::simix::Global>(simix_global_p);
-
- actors_ = remote(simix_global.get_buffer()->actors_vector);
- dead_actors_ = remote(simix_global.get_buffer()->dead_actors_vector);
- }
- actors = actors_;
- dead_actors = dead_actors_;
+ actors = remote(static_cast<s_xbt_dynar_t*>(actors_addr_));
+ dead_actors = remote(static_cast<s_xbt_dynar_t*>(dead_actors_addr_));
}
} // namespace mc
} // namespace simgrid
public:
explicit RemoteProcess(pid_t pid);
~RemoteProcess() override;
- void init();
+ void init(void* mmalloc_default_mdp, void* maxpid, void* actors, void* dead_actors);
RemoteProcess(RemoteProcess const&) = delete;
RemoteProcess(RemoteProcess&&) = delete;
/* ***************** */
/* SIMIX-related API */
/* ***************** */
+private:
+ // Cache the address of the variables we read directly in the memory of remote
+ void* maxpid_addr_;
+ void* actors_addr_;
+ void* dead_actors_addr_;
+public:
std::vector<ActorInformation>& actors();
std::vector<ActorInformation>& dead_actors();
namespace simgrid {
namespace mc {
-XBT_DECLARE_ENUM_CLASS(MessageType, NONE, CONTINUE, IGNORE_HEAP, UNIGNORE_HEAP, IGNORE_MEMORY, STACK_REGION,
- REGISTER_SYMBOL, DEADLOCK_CHECK, DEADLOCK_CHECK_REPLY, WAITING, SIMCALL_HANDLE,
+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_HANDLE,
SIMCALL_IS_VISIBLE, SIMCALL_IS_VISIBLE_ANSWER, SIMCALL_TO_STRING, SIMCALL_TO_STRING_ANSWER,
SIMCALL_DOT_LABEL, ASSERTION_FAILED, ACTOR_ENABLED, ACTOR_ENABLED_REPLY);
};
/* Client->Server */
+struct s_mc_message_initial_addresses_t {
+ simgrid::mc::MessageType type;
+ void* mmalloc_default_mdp;
+ void* maxpid;
+ void* actors;
+ void* dead_actors;
+};
+
struct s_mc_message_ignore_heap_t {
simgrid::mc::MessageType type;
int block;
REQUIRE(1 << xbt_pagebits == xbt_pagesize);
process = std::make_unique<simgrid::mc::RemoteProcess>(getpid());
- process->init();
+ process->init(nullptr, nullptr, nullptr, nullptr);
mc_model_checker = new ::simgrid::mc::ModelChecker(std::move(process), -1);
}
namespace simgrid {
namespace simix {
config::Flag<bool> cfg_verbose_exit{"debug/verbose-exit", "Display the actor status at exit", true};
+
+void* simix_global_get_actors_addr()
+{
+#if SIMGRID_HAVE_MC
+ return simix_global->actors_vector;
+#else
+ xbt_die("This function is intended to be used when compiling with MC");
+#endif
+}
+void* simix_global_get_dead_actors_addr()
+{
+#if SIMGRID_HAVE_MC
+ return simix_global->dead_actors_vector;
+#else
+ xbt_die("This function is intended to be used when compiling with MC");
+#endif
+}
+
} // namespace simix
} // namespace simgrid
maestro_code = std::bind(code, data);
}
-/**
- * @ingroup SIMIX_API
- * @brief Initialize SIMIX internal data.
- */
void SIMIX_global_init(int* argc, char** argv)
{
+ if (simix_global == nullptr) {
+ simix_global = std::make_unique<simgrid::simix::Global>();
+
#if SIMGRID_HAVE_MC
- // The communication initialization is done ASAP.
- // We need to communicate initialization of the different layers to the model-checker.
- simgrid::mc::AppSide::initialize();
+ // The communication initialization is done ASAP, as we need to get some init parameters from the MC for different layers.
+ // But simix_global needs to be created, as we send the address of some of its fields to the MC that wants to read them directly.
+ simgrid::mc::AppSide::initialize();
#endif
- if (simix_global == nullptr) {
surf_init(argc, argv); /* Initialize SURF structures */
- simix_global = std::make_unique<simgrid::simix::Global>();
simix_global->maestro_ = nullptr;
SIMIX_context_mod_init();
int main()
{
auto* process = new simgrid::mc::RemoteProcess(getpid());
- process->init();
+ process->init(nullptr, nullptr, nullptr, nullptr);
simgrid::dwarf::ExpressionContext state;
state.address_space = (simgrid::mc::AddressSpace*) process;
simgrid::mc::Type* type;
simgrid::mc::RemoteProcess process(getpid());
- process.init();
+ process.init(nullptr, nullptr, nullptr, nullptr);
test_global_variable(process, process.binary_info.get(), "some_local_variable", &some_local_variable, sizeof(int));
