delete maestro_;
delete context_factory_;
- /* Free the remaining data structures */
-#if SIMGRID_HAVE_MC
- xbt_dynar_free(&actors_vector_);
-#endif
/* clear models before freeing handle, network models can use external callback defined in the handle */
models_prio_.clear();
}
// The communication initialization is done ASAP, as we need to get some init parameters from the MC for different
// layers. But instance_ 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(actors_vector_);
+ simgrid::mc::AppSide::initialize();
#endif
if (xbt_initialized == 0) {
boost::intrusive::member_hook<actor::ActorImpl, boost::intrusive::list_member_hook<>,
&actor::ActorImpl::kernel_destroy_list_hook>>
actors_to_destroy_;
-#if SIMGRID_HAVE_MC
- /* MCer cannot read members actor_list_ above in the remote process, so we copy the info it needs in a dynar.
- * FIXME: This is supposed to be a temporary hack.
- * A better solution would be to change the split between MCer and MCed, where the responsibility
- * to compute the list of the enabled transitions goes to the MCed.
- * That way, the MCer would not need to have the list of actors on its side.
- * These info could be published by the MCed to the MCer in a way inspired of vd.so
- */
- xbt_dynar_t actors_vector_ = xbt_dynar_new(sizeof(actor::ActorImpl*), nullptr);
-#endif
static double now_;
static EngineImpl* instance_;
void add_actor(aid_t pid, actor::ActorImpl* actor) { actor_list_[pid] = actor; }
void remove_actor(aid_t pid) { actor_list_.erase(pid); }
-#if SIMGRID_HAVE_MC
- void reset_actor_dynar() { xbt_dynar_reset(actors_vector_); }
- void add_actor_to_dynar(actor::ActorImpl* actor) { xbt_dynar_push_as(actors_vector_, actor::ActorImpl*, actor); }
-#endif
-
const std::map<aid_t, actor::ActorImpl*>& get_actor_list() const { return actor_list_; }
const std::vector<actor::ActorImpl*>& get_actors_to_run() const { return actors_to_run_; }
const std::vector<actor::ActorImpl*>& get_actors_that_ran() const { return actors_that_ran_; }
xbt_assert(size == sizeof(message), "Broken message. Got %d bytes instead of %d.", (int)size, (int)sizeof(message));
memcpy(&message, buffer, sizeof(message));
- get_remote_process().init(message.mmalloc_default_mdp, message.maxpid, message.actors);
+ get_remote_process().init(message.mmalloc_default_mdp, message.maxpid);
break;
}
actor->simcall_handle(0);
}
}
-#if SIMGRID_HAVE_MC
- engine->reset_actor_dynar();
- for (auto const& [_, actor] : engine->get_actor_list()) {
- // Only visible requests remain at this point, and they all have an observer
- actor->simcall_.mc_max_consider_ = actor->simcall_.observer_->get_max_consider();
-
- engine->add_actor_to_dynar(actor);
- }
-#endif
}
/** @brief returns if there this transition can proceed in a finite amount of time
std::unique_ptr<AppSide> AppSide::instance_;
-AppSide* AppSide::initialize(xbt_dynar_t actors_addr)
+AppSide* AppSide::initialize()
{
if (not std::getenv(MC_ENV_SOCKET_FD)) // We are not in MC mode: don't initialize the MC world
return nullptr;
strerror(errno));
s_mc_message_initial_addresses_t message{MessageType::INITIAL_ADDRESSES, mmalloc_get_current_heap(),
- kernel::actor::ActorImpl::get_maxpid_addr(), actors_addr};
+ kernel::actor::ActorImpl::get_maxpid_addr()};
xbt_assert(instance_->channel_.send(message) == 0, "Could not send the initial message with addresses.");
instance_->handle_messages();
// Singleton :/
// TODO, remove the singleton antipattern.
- static AppSide* initialize(xbt_dynar_t actors_addr);
+ static AppSide* initialize();
static AppSide* get() { return instance_.get(); }
};
} // namespace simgrid::mc
RemoteProcess::RemoteProcess(pid_t pid) : AddressSpace(this), pid_(pid), running_(true) {}
-void RemoteProcess::init(xbt_mheap_t mmalloc_default_mdp, unsigned long* maxpid, xbt_dynar_t actors)
+void RemoteProcess::init(xbt_mheap_t mmalloc_default_mdp, unsigned long* maxpid)
{
this->heap_address = remote(mmalloc_default_mdp);
this->maxpid_addr_ = remote(maxpid);
- this->actors_addr_ = remote(actors);
this->memory_map_ = simgrid::xbt::get_memory_map(this->pid_);
this->init_memory_map_info();
std::size_t size;
};
-/** The Application's process memory, seen from the MCer perspective
- *
- * This class is mixing a lot of different responsibilities and is tied
- * to SIMIX. It should probably be split into different classes.
+/** The Application's process memory, seen from the Checker perspective
*
* Responsibilities:
*
* - reading from the process memory (`AddressSpace`);
* - accessing the system state of the process (heap, …);
- * - storing the SIMIX state of the process;
* - privatization;
* - stack unwinding;
* - etc.
public:
explicit RemoteProcess(pid_t pid);
~RemoteProcess() override;
- void init(xbt_mheap_t mmalloc_default_mdp, unsigned long* maxpid, xbt_dynar_t actors);
+ void init(xbt_mheap_t mmalloc_default_mdp, unsigned long* maxpid);
RemoteProcess(RemoteProcess const&) = delete;
RemoteProcess(RemoteProcess&&) = delete;
private:
// Cache the address of the variables we read directly in the memory of remote
RemotePtr<unsigned long> maxpid_addr_;
- RemotePtr<s_xbt_dynar_t> actors_addr_;
public:
unsigned long get_maxpid() const { return this->read(maxpid_addr_); }
simgrid::mc::MessageType type;
xbt_mheap_t mmalloc_default_mdp;
unsigned long* maxpid;
- xbt_dynar_t actors;
};
struct s_mc_message_ignore_heap_t {
REQUIRE(1 << xbt_pagebits == xbt_pagesize);
process = std::make_unique<simgrid::mc::RemoteProcess>(getpid());
- process->init(nullptr, nullptr, nullptr);
+ process->init(nullptr, nullptr);
mc_model_checker = new ::simgrid::mc::ModelChecker(std::move(process), -1);
}
int main()
{
auto* process = new simgrid::mc::RemoteProcess(getpid());
- process->init(nullptr, nullptr, nullptr);
+ process->init(nullptr, nullptr);
simgrid::dwarf::ExpressionContext state;
state.address_space = (simgrid::mc::AddressSpace*) process;
simgrid::mc::Type* type;
simgrid::mc::RemoteProcess process(getpid());
- process.init(nullptr, nullptr, nullptr);
+ process.init(nullptr, nullptr);
test_global_variable(process, process.binary_info.get(), "some_local_variable", &some_local_variable, sizeof(int));
