#include "src/kernel/activity/SleepImpl.hpp"
#include "src/kernel/activity/SynchroRaw.hpp"
#include "src/mc/mc_replay.hpp"
-#include "src/mc/remote/Client.hpp"
+#include "src/mc/remote/AppSide.hpp"
#include "src/simix/smx_private.hpp"
#include "src/surf/HostImpl.hpp"
#include "src/surf/cpu_interface.hpp"
#include "src/mc/mc_private.hpp"
#include "src/mc/mc_record.hpp"
#include "src/mc/mc_replay.hpp"
-#include "src/mc/remote/Client.hpp"
+#include "src/mc/remote/AppSide.hpp"
#include "xbt/asserts.h"
/** @file mc_client_api.cpp
xbt_assert(mc_model_checker == nullptr);
if (not prop) {
if (MC_is_active())
- simgrid::mc::Client::get()->report_assertion_failure();
+ simgrid::mc::AppSide::get()->report_assertion_failure();
if (MC_record_replay_is_active())
xbt_die("MC assertion failed");
}
xbt_assert(mc_model_checker == nullptr);
if (not MC_is_active())
return;
- simgrid::mc::Client::get()->ignore_memory(addr, size);
+ simgrid::mc::AppSide::get()->ignore_memory(addr, size);
}
void MC_automaton_new_propositional_symbol(const char* /*id*/, int (*/*fct*/)())
xbt_assert(mc_model_checker == nullptr);
if (not MC_is_active())
return;
- simgrid::mc::Client::get()->declare_symbol(name, value);
+ simgrid::mc::AppSide::get()->declare_symbol(name, value);
}
/** @brief Register a stack in the model checker
xbt_assert(mc_model_checker == nullptr);
if (not MC_is_active())
return;
- simgrid::mc::Client::get()->declare_stack(stack, size, context);
+ simgrid::mc::AppSide::get()->declare_stack(stack, size, context);
}
void MC_ignore_global_variable(const char* /*name*/)
xbt_assert(mc_model_checker == nullptr);
if (not MC_is_active())
return;
- simgrid::mc::Client::get()->ignore_heap(address, size);
+ simgrid::mc::AppSide::get()->ignore_heap(address, size);
}
void MC_unignore_heap(void* address, size_t size)
xbt_assert(mc_model_checker == nullptr);
if (not MC_is_active())
return;
- simgrid::mc::Client::get()->unignore_heap(address, size);
+ simgrid::mc::AppSide::get()->unignore_heap(address, size);
}
#include "src/mc/mc_request.hpp"
#include "src/mc/mc_safety.hpp"
#include "src/mc/mc_smx.hpp"
-#include "src/mc/remote/Client.hpp"
+#include "src/mc/remote/AppSide.hpp"
#include "src/mc/sosp/Snapshot.hpp"
#include "xbt/backtrace.hpp"
simgrid::mc::processes_time.resize(simgrid::kernel::actor::get_maxpid());
MC_ignore_heap(simgrid::mc::processes_time.data(),
simgrid::mc::processes_time.size() * sizeof(simgrid::mc::processes_time[0]));
- simgrid::mc::Client::get()->main_loop();
+ simgrid::mc::AppSide::get()->main_loop();
}
void MC_show_deadlock()
/* This program is free software; you can redistribute it and/or modify it
* under the terms of the license (GNU LGPL) which comes with this package. */
-#include "src/mc/remote/Client.hpp"
+#include "src/mc/remote/AppSide.hpp"
#include "src/internal_config.h"
#include <simgrid/modelchecker.h>
namespace simgrid {
namespace mc {
-std::unique_ptr<Client> Client::instance_;
+std::unique_ptr<AppSide> AppSide::instance_;
-Client* Client::initialize()
+AppSide* AppSide::initialize()
{
- // We are not in MC mode:
- // TODO, handle this more gracefully.
- if (not std::getenv(MC_ENV_SOCKET_FD))
+ if (not std::getenv(MC_ENV_SOCKET_FD)) // We are not in MC mode: don't initialize the MC world
return nullptr;
// Do not break if we are called multiple times:
xbt_assert(type == SOCK_SEQPACKET, "Unexpected socket type %i", type);
XBT_DEBUG("Model-checked application found expected socket type");
- instance_.reset(new simgrid::mc::Client(fd));
+ instance_.reset(new simgrid::mc::AppSide(fd));
// Wait for the model-checker:
errno = 0;
return instance_.get();
}
-void Client::handle_deadlock_check(const s_mc_message_t*)
+void AppSide::handle_deadlock_check(const s_mc_message_t*)
{
bool deadlock = false;
if (not simix_global->process_list.empty()) {
s_mc_message_int_t answer{MC_MESSAGE_DEADLOCK_CHECK_REPLY, deadlock};
xbt_assert(channel_.send(answer) == 0, "Could not send response");
}
-void Client::handle_continue(const s_mc_message_t*)
+void AppSide::handle_continue(const s_mc_message_t*)
{
/* Nothing to do */
}
-void Client::handle_simcall(const s_mc_message_simcall_handle_t* message)
+void AppSide::handle_simcall(const s_mc_message_simcall_handle_t* message)
{
smx_actor_t process = SIMIX_process_from_PID(message->pid);
xbt_assert(process != nullptr, "Invalid pid %lu", message->pid);
xbt_die("Could not send MESSAGE_WAITING to model-checker");
}
-void Client::handle_actor_enabled(const s_mc_message_actor_enabled_t* msg)
+void AppSide::handle_actor_enabled(const s_mc_message_actor_enabled_t* msg)
{
bool res = simgrid::mc::actor_is_enabled(SIMIX_process_from_PID(msg->aid));
s_mc_message_int_t answer{MC_MESSAGE_ACTOR_ENABLED_REPLY, res};
xbt_assert(received_size == sizeof(_type_), "Unexpected size for " _name_ " (%zd != %zu)", received_size, \
sizeof(_type_))
-void Client::handle_messages()
+void AppSide::handle_messages()
{
while (1) {
XBT_DEBUG("Waiting messages from model-checker");
}
}
-void Client::main_loop()
+void AppSide::main_loop()
{
while (1) {
simgrid::mc::wait_for_requests();
}
}
-void Client::report_assertion_failure()
+void AppSide::report_assertion_failure()
{
if (channel_.send(MC_MESSAGE_ASSERTION_FAILED))
xbt_die("Could not send assertion to model-checker");
this->handle_messages();
}
-void Client::ignore_memory(void* addr, std::size_t size)
+void AppSide::ignore_memory(void* addr, std::size_t size)
{
s_mc_message_ignore_memory_t message;
message.type = MC_MESSAGE_IGNORE_MEMORY;
xbt_die("Could not send IGNORE_MEMORY mesage to model-checker");
}
-void Client::ignore_heap(void* address, std::size_t size)
+void AppSide::ignore_heap(void* address, std::size_t size)
{
const s_xbt_mheap_t* heap = mmalloc_get_current_heap();
xbt_die("Could not send ignored region to MCer");
}
-void Client::unignore_heap(void* address, std::size_t size)
+void AppSide::unignore_heap(void* address, std::size_t size)
{
s_mc_message_ignore_memory_t message;
message.type = MC_MESSAGE_UNIGNORE_HEAP;
xbt_die("Could not send IGNORE_HEAP message to model-checker");
}
-void Client::declare_symbol(const char* name, int* value)
+void AppSide::declare_symbol(const char* name, int* value)
{
s_mc_message_register_symbol_t message;
message.type = MC_MESSAGE_REGISTER_SYMBOL;
xbt_die("Could send REGISTER_SYMBOL message to model-checker");
}
-void Client::declare_stack(void* stack, size_t size, ucontext_t* context)
+void AppSide::declare_stack(void* stack, size_t size, ucontext_t* context)
{
const s_xbt_mheap_t* heap = mmalloc_get_current_heap();
+/* mc::remote::AppSide: the Application-side of the channel */
+
/* Copyright (c) 2015-2020. The SimGrid Team. All rights reserved. */
/* This program is free software; you can redistribute it and/or modify it
*
* Send messages to the model-checker and handles message from it.
*/
-class XBT_PUBLIC Client {
+class XBT_PUBLIC AppSide {
private:
Channel channel_;
- static std::unique_ptr<Client> instance_;
+ static std::unique_ptr<AppSide> instance_;
public:
- Client();
- explicit Client(int fd) : channel_(fd) {}
+ AppSide();
+ explicit AppSide(int fd) : channel_(fd) {}
void handle_messages();
private:
// Singleton :/
// TODO, remove the singleton antipattern.
- static Client* initialize();
- static Client* get() { return instance_.get(); }
+ static AppSide* initialize();
+ static AppSide* get() { return instance_.get(); }
};
} // namespace mc
} // namespace simgrid
+/* mc::RemoteClient: representative of the Client memory on the MC side */
+
/* Copyright (c) 2008-2020. The SimGrid Team. All rights reserved. */
/* This program is free software; you can redistribute it and/or modify it
#include "src/surf/xml/platf.hpp"
#if SIMGRID_HAVE_MC
-#include "src/mc/remote/Client.hpp"
+#include "src/mc/remote/AppSide.hpp"
#endif
#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::Client::initialize();
+ simgrid::mc::AppSide::initialize();
#endif
if (simix_global == nullptr) {
src/mc/remote/Channel.cpp
src/mc/remote/Channel.hpp
- src/mc/remote/Client.cpp
- src/mc/remote/Client.hpp
+ src/mc/remote/AppSide.cpp
+ src/mc/remote/AppSide.hpp
src/mc/remote/EventLoop.cpp
src/mc/remote/EventLoop.hpp
src/mc/remote/RemoteClient.hpp
