int Channel::send(const void* message, size_t size) const
{
- XBT_DEBUG("Protocol [%s] send %s",
- MC_mode_name(mc_mode),
+ XBT_DEBUG("Send %s",
MC_message_type_name(*(e_mc_message_type*) message));
-
while (::send(this->socket_, message, size, 0) == -1)
if (errno == EINTR)
continue;
{
int res = recv(this->socket_, message, size, block ? 0 : MSG_DONTWAIT);
if (res != -1)
- XBT_DEBUG("Protocol [%s] received %s",
- MC_mode_name(mc_mode),
+ XBT_DEBUG("Receive %s",
MC_message_type_name(*(e_mc_message_type*) message));
return res;
}
#include <xbt/mmalloc.h>
#include <xbt/swag.h>
+#include <simgrid/modelchecker.h>
+
#include "src/internal_config.h"
#include "src/mc/mc_protocol.h"
if (client_)
return client_.get();
- // Check and set the mode:
- if (mc_mode != MC_MODE_NONE)
- abort();
- mc_mode = MC_MODE_CLIENT;
+ _sg_do_model_check = 1;
// Fetch socket from MC_ENV_SOCKET_FD:
char* fd_env = std::getenv(MC_ENV_SOCKET_FD);
break;
default:
- xbt_die("%s received unexpected message %s (%i)",
- MC_mode_name(mc_mode),
+ xbt_die("Received unexpected message %s (%i)",
MC_message_type_name(message.type),
message.type
);
if (s == -1)
xbt_die("Could not receive message");
if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY)
- xbt_die("%s received unexpected message %s (%i, size=%i) "
+ xbt_die("Received unexpected message %s (%i, size=%i) "
"expected MC_MESSAGE_DEADLOCK_CHECK_REPLY (%i, size=%i)",
- MC_mode_name(mc_mode),
MC_message_type_name(message.type), (int) message.type, (int) s,
(int) MC_MESSAGE_DEADLOCK_CHECK_REPLY, (int) sizeof(message)
);
simgrid::mc::SimixProcessInformation* resolveProcessInfo(
simgrid::mc::RemotePtr<s_smx_process_t> process)
{
- xbt_assert(mc_mode == MC_MODE_SERVER);
+ xbt_assert(mc_model_checker != nullptr);
if (!process)
return nullptr;
this->refresh_simix();
int MC_random(int min, int max)
{
- xbt_assert(mc_mode != MC_MODE_SERVER);
+ xbt_assert(mc_model_checker == nullptr);
/* TODO, if the MC is disabled we do not really need to make a simcall for
* this :) */
return simcall_mc_random(min, max);
void wait_for_requests(void)
{
- assert(mc_mode != MC_MODE_SERVER);
+ xbt_assert(mc_model_checker == nullptr);
smx_process_t process;
smx_simcall_t req;
#if HAVE_MC
// Fetch from MCed memory:
- if (mc_mode == MC_MODE_SERVER) {
+ if (mc_model_checker != nullptr) {
mc_model_checker->process().read(&temp_synchro, remote(act));
act = &temp_synchro;
}
s_xbt_dynar_t comms_buffer;
size_t buffer_size = 0;
- if (mc_mode == MC_MODE_SERVER) {
+ if (mc_model_checker != nullptr) {
// Read dynar:
mc_model_checker->process().read(
&comms_buffer, remote(simcall_comm_waitany__get__comms(req)));
// Read all the dynar buffer:
char buffer[buffer_size];
- if (mc_mode == MC_MODE_SERVER)
+ if (mc_model_checker != nullptr)
mc_model_checker->process().read_bytes(buffer, sizeof(buffer),
remote(comms->data));
#else
for (index = 0; index < comms->used; ++index) {
#if HAVE_MC
// Fetch act from MCed memory:
- if (mc_mode == MC_MODE_SERVER) {
+ if (mc_model_checker != nullptr) {
memcpy(&act, buffer + comms->elmsize * index, sizeof(act));
mc_model_checker->process().read(&temp_synchro, remote(act));
act = &temp_synchro;
smx_mutex_t mutex = simcall_mutex_lock__get__mutex(req);
#if HAVE_MC
s_smx_mutex_t temp_mutex;
- if (mc_mode == MC_MODE_SERVER) {
+ if (mc_model_checker != nullptr) {
mc_model_checker->process().read(&temp_mutex, remote(mutex));
mutex = &temp_mutex;
}
if(mutex->owner == nullptr)
return true;
#if HAVE_MC
- else if (mc_mode == MC_MODE_SERVER) {
+ else if (mc_model_checker != nullptr) {
simgrid::mc::Process& modelchecked = mc_model_checker->process();
// TODO, *(mutex->owner) :/
return modelchecked.resolveProcess(simgrid::mc::remote(mutex->owner))->pid
static inline
void restore_snapshot_fds(simgrid::mc::Snapshot* snapshot)
{
- if (mc_mode == MC_MODE_SERVER)
- xbt_die("FD snapshot not implemented in client/server mode.");
+ xbt_die("FD snapshot not implemented in client/server mode.");
for (auto const& fd : snapshot->current_fds) {
void MC_assert(int prop)
{
+ xbt_assert(mc_model_checker == nullptr);
if (MC_is_active() && !prop)
simgrid::mc::Client::get()->reportAssertionFailure();
}
void MC_cut(void)
{
+ xbt_assert(mc_model_checker == nullptr);
+ if (!MC_is_active())
+ return;
// FIXME, We want to do this in the model-checker:
xbt_die("MC_cut() not implemented");
}
void MC_ignore(void* addr, size_t size)
{
- xbt_assert(mc_mode != MC_MODE_SERVER);
- if (mc_mode != MC_MODE_CLIENT)
+ xbt_assert(mc_model_checker == nullptr);
+ if (!MC_is_active())
return;
simgrid::mc::Client::get()->ignoreMemory(addr, size);
}
void MC_automaton_new_propositional_symbol(const char *id, int(*fct)(void))
{
- xbt_assert(mc_mode != MC_MODE_SERVER);
- if (mc_mode != MC_MODE_CLIENT)
+ xbt_assert(mc_model_checker == nullptr);
+ if (!MC_is_active())
return;
-
xbt_die("Support for client-side function proposition is not implemented: "
- "use MC_automaton_new_propositional_symbol_pointer instead."
- );
+ "use MC_automaton_new_propositional_symbol_pointer instead.");
}
void MC_automaton_new_propositional_symbol_pointer(const char *name, int* value)
{
- xbt_assert(mc_mode != MC_MODE_SERVER);
- if (mc_mode != MC_MODE_CLIENT)
+ xbt_assert(mc_model_checker == nullptr);
+ if (!MC_is_active())
return;
simgrid::mc::Client::get()->declareSymbol(name, value);
}
*/
void MC_register_stack_area(void *stack, smx_process_t process, ucontext_t* context, size_t size)
{
- if (mc_mode != MC_MODE_CLIENT)
+ xbt_assert(mc_model_checker == nullptr);
+ if (!MC_is_active())
return;
simgrid::mc::Client::get()->declareStack(stack, size, process, context);
}
void MC_ignore_global_variable(const char *name)
{
+ xbt_assert(mc_model_checker == nullptr);
+ if (!MC_is_active())
+ return;
// TODO, send a message to the model_checker
xbt_die("Unimplemented");
}
void MC_ignore_heap(void *address, size_t size)
{
- if (mc_mode != MC_MODE_CLIENT)
+ xbt_assert(mc_model_checker == nullptr);
+ if (!MC_is_active())
return;
simgrid::mc::Client::get()->ignoreHeap(address, size);
}
void MC_remove_ignore_heap(void *address, size_t size)
{
- if (mc_mode != MC_MODE_CLIENT)
+ xbt_assert(mc_model_checker == nullptr);
+ if (!MC_is_active())
return;
simgrid::mc::Client::get()->unignoreHeap(address, size);
}
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc, "Logging specific to MC (global)");
-e_mc_mode_t mc_mode;
-
namespace simgrid {
namespace mc {
return "?";
}
}
-
-const char* MC_mode_name(e_mc_mode_t mode)
-{
- switch(mode) {
- case MC_MODE_NONE:
- return "NONE";
- case MC_MODE_CLIENT:
- return "CLIENT";
- case MC_MODE_SERVER:
- return "SERVER";
- default:
- return "?";
- }
-}
/** Environment variable name used to pass the communication socket */
#define MC_ENV_SOCKET_FD "SIMGRID_MC_SOCKET_FD"
-// ***** MC mode
-
-typedef enum {
- MC_MODE_NONE = 0,
- MC_MODE_CLIENT,
- MC_MODE_SERVER
-} e_mc_mode_t;
-
-extern e_mc_mode_t mc_mode;
-
// ***** Messages
typedef enum {
} s_mc_restore_message_t, *mc_restore_message_t;
XBT_PRIVATE const char* MC_message_type_name(e_mc_message_type type);
-XBT_PRIVATE const char* MC_mode_name(e_mc_mode_t mode);
SG_END_DECL()
std::string simgrid::mc::request_to_string(smx_simcall_t req, int value, simgrid::mc::RequestType request_type)
{
- xbt_assert(mc_mode == MC_MODE_SERVER);
+ xbt_assert(mc_model_checker != nullptr);
bool use_remote_comm = true;
switch(request_type) {
*/
smx_process_t MC_smx_simcall_get_issuer(s_smx_simcall_t const* req)
{
- xbt_assert(mc_mode == MC_MODE_SERVER);
+ xbt_assert(mc_model_checker != nullptr);
// This is the address of the smx_process in the MCed process:
auto address = simgrid::mc::remote(req->issuer);
const char* MC_smx_process_get_host_name(smx_process_t p)
{
- if (mc_mode == MC_MODE_CLIENT)
+ if (mc_model_checker == nullptr)
return sg_host_get_name(p->host);
simgrid::mc::Process* process = &mc_model_checker->process();
const char* MC_smx_process_get_name(smx_process_t p)
{
simgrid::mc::Process* process = &mc_model_checker->process();
- if (mc_mode == MC_MODE_CLIENT)
+ if (mc_model_checker == nullptr)
return p->name;
if (!p->name)
return nullptr;
#if HAVE_SMPI
int MC_smpi_process_count(void)
{
- if (mc_mode == MC_MODE_CLIENT)
+ if (mc_model_checker == nullptr)
return smpi_process_count();
int res;
mc_model_checker->process().read_variable("process_count",
// Currently, we need this before sg_config_init:
_sg_do_model_check = 1;
- mc_mode = MC_MODE_SERVER;
// The initialisation function can touch argv.
// We make a copy of argv before modifying it in order to pass the original
void SIMIX_global_init(int *argc, char **argv)
{
#if HAVE_MC
- _sg_do_model_check = getenv(MC_ENV_VARIABLE) != NULL;
+ // The communication initialization is done ASAP.
+ // We need to communicate initialization of the different layers to the model-checker.
+ simgrid::mc::Client::initialize();
#endif
s_smx_process_t proc;
if (xbt_cfg_get_boolean("clean-atexit"))
atexit(SIMIX_clean);
-#if 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();
-#endif
-
if (_sg_cfg_exit_asap)
exit(0);
}