It is now in remote::CheckerSide. This makes it symmetric with remote::ClientSide
There is still a lot to do to clean things up:
- the actual communication Checker->App is spread all over the place
- the ModelChecker singleton dupplicates the function of the mc::Session
- plus the other ugly things that I fail to see right now given the ambiant mess
namespace simgrid {
namespace mc {
-ModelChecker::ModelChecker(std::unique_ptr<RemoteClientMemory> process) : process_(std::move(process)) {}
+ModelChecker::ModelChecker(std::unique_ptr<RemoteClientMemory> process, int sockfd)
+ : event_loop_(sockfd), process_(std::move(process))
+{
+}
void ModelChecker::start()
{
- event_loop_.start(process_->get_channel().get_socket(), [](evutil_socket_t sig, short events, void* arg) {
- ((ModelChecker*)arg)->handle_events(sig, events);
- });
+ event_loop_.start(
+ [](evutil_socket_t sig, short events, void* arg) { ((ModelChecker*)arg)->handle_events(sig, events); });
XBT_DEBUG("Waiting for the model-checked process");
int status;
void ModelChecker::resume(RemoteClientMemory& process)
{
- int res = process.get_channel().send(MC_MESSAGE_CONTINUE);
+ int res = event_loop_.get_channel().send(MC_MESSAGE_CONTINUE);
if (res)
throw xbt::errno_error();
process.clear_cache();
{
if (events == EV_READ) {
char buffer[MC_MESSAGE_LENGTH];
- ssize_t size = process_->get_channel().receive(buffer, sizeof(buffer), false);
+ ssize_t size = event_loop_.get_channel().receive(buffer, sizeof(buffer), false);
if (size == -1 && errno != EAGAIN)
throw simgrid::xbt::errno_error();
m.type = MC_MESSAGE_SIMCALL_HANDLE;
m.pid = transition.pid_;
m.value = transition.argument_;
- this->process_->get_channel().send(m);
+ event_loop_.get_channel().send(m);
this->process_->clear_cache();
if (this->process_->running())
event_loop_.dispatch();
bool ModelChecker::checkDeadlock()
{
- int res = this->process().get_channel().send(MC_MESSAGE_DEADLOCK_CHECK);
+ int res = event_loop_.get_channel().send(MC_MESSAGE_DEADLOCK_CHECK);
xbt_assert(res == 0, "Could not check deadlock state");
s_mc_message_int_t message;
- ssize_t s = mc_model_checker->process().get_channel().receive(message);
+ ssize_t s = event_loop_.get_channel().receive(message);
xbt_assert(s != -1, "Could not receive message");
xbt_assert(s == sizeof(message) && message.type == MC_MESSAGE_DEADLOCK_CHECK_REPLY,
"Received unexpected message %s (%i, size=%i) "
public:
ModelChecker(ModelChecker const&) = delete;
ModelChecker& operator=(ModelChecker const&) = delete;
- explicit ModelChecker(std::unique_ptr<RemoteClientMemory> process);
+ explicit ModelChecker(std::unique_ptr<RemoteClientMemory> process, int sockfd);
RemoteClientMemory& process() { return *process_; }
+ Channel& channel() { return event_loop_.get_channel(); }
PageStore& page_store()
{
return page_store_;
xbt_assert(mc_model_checker == nullptr, "Did you manage to start the MC twice in this process?");
- auto process = std::unique_ptr<simgrid::mc::RemoteClientMemory>(new simgrid::mc::RemoteClientMemory(pid, sockets[1]));
- model_checker_.reset(new simgrid::mc::ModelChecker(std::move(process)));
+ auto process = std::unique_ptr<simgrid::mc::RemoteClientMemory>(new simgrid::mc::RemoteClientMemory(pid));
+ model_checker_.reset(new simgrid::mc::ModelChecker(std::move(process), sockets[1]));
mc_model_checker = model_checker_.get();
model_checker_->start();
bool Session::actor_is_enabled(aid_t pid)
{
s_mc_message_actor_enabled_t msg{MC_MESSAGE_ACTOR_ENABLED, pid};
- model_checker_->process().get_channel().send(msg);
+ model_checker_->channel().send(msg);
char buff[MC_MESSAGE_LENGTH];
- ssize_t received = model_checker_->process().get_channel().receive(buff, MC_MESSAGE_LENGTH, true);
+ ssize_t received = model_checker_->channel().receive(buff, MC_MESSAGE_LENGTH, true);
xbt_assert(received == sizeof(s_mc_message_int_t), "Unexpected size in answer to ACTOR_ENABLED");
return ((s_mc_message_int_t*)buff)->value;
}
event_base_free(base_);
}
-void CheckerSide::start(int socket, void (*handler)(int, short, void*))
+void CheckerSide::start(void (*handler)(int, short, void*))
{
base_ = event_base_new();
- socket_event_ = event_new(base_, socket, EV_READ | EV_PERSIST, handler, this);
+ socket_event_ = event_new(base_, get_channel().get_socket(), EV_READ | EV_PERSIST, handler, this);
event_add(socket_event_, NULL);
signal_event_ = event_new(base_, SIGCHLD, EV_SIGNAL | EV_PERSIST, handler, this);
#ifndef SIMGRID_MC_REMOTE_EVENTLOOP_HPP
#define SIMGRID_MC_REMOTE_EVENTLOOP_HPP
+#include "src/mc/remote/Channel.hpp"
+
#include <event2/event.h>
#include <functional>
struct event* socket_event_ = nullptr;
struct event* signal_event_ = nullptr;
+ Channel channel_;
+
public:
+ explicit CheckerSide(int sockfd) : channel_(sockfd) {}
~CheckerSide();
- void start(int socket, void (*handler)(int, short, void*));
+ Channel const& get_channel() const { return channel_; }
+ Channel& get_channel() { return channel_; }
+
+ void start(void (*handler)(int, short, void*));
void dispatch();
void break_loop();
};
// ***** Process
-RemoteClientMemory::RemoteClientMemory(pid_t pid, int sockfd)
- : AddressSpace(this), pid_(pid), channel_(sockfd), running_(true)
-{
-}
+RemoteClientMemory::RemoteClientMemory(pid_t pid) : AddressSpace(this), pid_(pid), running_(true) {}
void RemoteClientMemory::init()
{
#ifndef SIMGRID_MC_PROCESS_H
#define SIMGRID_MC_PROCESS_H
+#include "mc/datatypes.h"
#include "src/mc/AddressSpace.hpp"
#include "src/mc/inspect/ObjectInformation.hpp"
-#include "src/mc/remote/Channel.hpp"
#include "src/mc/remote/RemotePtr.hpp"
#include "src/xbt/mmalloc/mmprivate.h"
static constexpr int cache_simix_processes = 4;
public:
- RemoteClientMemory(pid_t pid, int sockfd);
+ RemoteClientMemory(pid_t pid);
~RemoteClientMemory();
void init();
void clear_cache() { this->cache_flags_ = RemoteClientMemory::cache_none; }
- Channel const& get_channel() const { return channel_; }
- Channel& get_channel() { return channel_; }
-
std::vector<IgnoredRegion> const& ignored_regions() const { return ignored_regions_; }
void ignore_region(std::uint64_t address, std::size_t size);
void refresh_simix();
pid_t pid_ = -1;
- Channel channel_;
bool running_ = false;
std::vector<xbt::VmMap> memory_map_;
RemotePtr<void> maestro_stack_start_;
REQUIRE(xbt_pagesize == getpagesize());
REQUIRE(1 << xbt_pagebits == xbt_pagesize);
- process.reset(new simgrid::mc::RemoteClientMemory(getpid(), -1));
+ process.reset(new simgrid::mc::RemoteClientMemory(getpid()));
process->init();
- mc_model_checker = new ::simgrid::mc::ModelChecker(std::move(process));
+ mc_model_checker = new ::simgrid::mc::ModelChecker(std::move(process), -1);
}
snap_test_helper::prologue_return snap_test_helper::prologue(int n)
int main()
{
- process = new simgrid::mc::RemoteClientMemory(getpid(), -1);
+ process = new simgrid::mc::RemoteClientMemory(getpid());
process->init();
simgrid::dwarf::ExpressionContext state;
const simgrid::mc::Variable* var;
simgrid::mc::Type* type;
- simgrid::mc::RemoteClientMemory process(getpid(), -1);
+ simgrid::mc::RemoteClientMemory process(getpid());
process.init();
test_global_variable(process, process.binary_info.get(), "some_local_variable", &some_local_variable, sizeof(int));