#include "src/mc/mc_config.hpp"
#include "src/mc/mc_exit.hpp"
#include "src/mc/mc_private.hpp"
-#include "src/mc/remote/RemoteClient.hpp"
+#include "src/mc/remote/RemoteClientMemory.hpp"
#include "xbt/automaton.hpp"
#include "xbt/system_error.hpp"
namespace simgrid {
namespace mc {
-ModelChecker::ModelChecker(std::unique_ptr<RemoteClient> 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::setup_ignore()
{
- RemoteClient& process = this->process();
+ RemoteClientMemory& process = this->process();
for (std::pair<const char*, const char*> const& var :
ignored_local_variables)
process.ignore_local_variable(var.first, var.second);
{
XBT_DEBUG("Shuting down model-checker");
- RemoteClient* process = &this->process();
+ RemoteClientMemory* process = &this->process();
if (process->running()) {
XBT_DEBUG("Killing process");
kill(process->pid(), SIGKILL);
}
}
-void ModelChecker::resume(RemoteClient& process)
+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 (property_automaton == nullptr)
property_automaton = xbt_automaton_new();
- RemoteClient* process = &this->process();
+ RemoteClientMemory* process = &this->process();
RemotePtr<int> address = remote((int*)message.data);
xbt::add_proposition(property_automaton, message.name, [process, address]() { return process->read(address); });
{
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) "