void ModelChecker::resume(RemoteSimulation& process)
{
- int res = checker_side_.get_channel().send(MC_MESSAGE_CONTINUE);
+ int res = checker_side_.get_channel().send(MessageType::CONTINUE);
if (res)
throw xbt::errno_error();
process.clear_cache();
memcpy(&base_message, buffer, sizeof(base_message));
switch(base_message.type) {
- case MC_MESSAGE_IGNORE_HEAP:
- {
- s_mc_message_ignore_heap_t message;
- xbt_assert(size == sizeof(message), "Broken message");
- memcpy(&message, buffer, sizeof(message));
-
- IgnoredHeapRegion region;
- region.block = message.block;
- region.fragment = message.fragment;
- region.address = message.address;
- region.size = message.size;
- get_remote_simulation().ignore_heap(region);
- break;
+ case MessageType::IGNORE_HEAP: {
+ s_mc_message_ignore_heap_t message;
+ xbt_assert(size == sizeof(message), "Broken message");
+ memcpy(&message, buffer, sizeof(message));
+
+ IgnoredHeapRegion region;
+ region.block = message.block;
+ region.fragment = message.fragment;
+ region.address = message.address;
+ region.size = message.size;
+ get_remote_simulation().ignore_heap(region);
+ break;
}
- case MC_MESSAGE_UNIGNORE_HEAP:
- {
- s_mc_message_ignore_memory_t message;
- xbt_assert(size == sizeof(message), "Broken message");
- memcpy(&message, buffer, sizeof(message));
- get_remote_simulation().unignore_heap((void*)(std::uintptr_t)message.addr, message.size);
- break;
+ case MessageType::UNIGNORE_HEAP: {
+ s_mc_message_ignore_memory_t message;
+ xbt_assert(size == sizeof(message), "Broken message");
+ memcpy(&message, buffer, sizeof(message));
+ get_remote_simulation().unignore_heap((void*)(std::uintptr_t)message.addr, message.size);
+ break;
}
- case MC_MESSAGE_IGNORE_MEMORY:
- {
- s_mc_message_ignore_memory_t message;
- xbt_assert(size == sizeof(message), "Broken message");
- memcpy(&message, buffer, sizeof(message));
- this->get_remote_simulation().ignore_region(message.addr, message.size);
- break;
+ case MessageType::IGNORE_MEMORY: {
+ s_mc_message_ignore_memory_t message;
+ xbt_assert(size == sizeof(message), "Broken message");
+ memcpy(&message, buffer, sizeof(message));
+ this->get_remote_simulation().ignore_region(message.addr, message.size);
+ break;
}
- case MC_MESSAGE_STACK_REGION:
- {
- s_mc_message_stack_region_t message;
- xbt_assert(size == sizeof(message), "Broken message");
- memcpy(&message, buffer, sizeof(message));
- this->get_remote_simulation().stack_areas().push_back(message.stack_region);
- }
- break;
+ case MessageType::STACK_REGION: {
+ s_mc_message_stack_region_t message;
+ xbt_assert(size == sizeof(message), "Broken message");
+ memcpy(&message, buffer, sizeof(message));
+ this->get_remote_simulation().stack_areas().push_back(message.stack_region);
+ } break;
- case MC_MESSAGE_REGISTER_SYMBOL:
- {
- s_mc_message_register_symbol_t message;
- xbt_assert(size == sizeof(message), "Broken message");
- memcpy(&message, buffer, sizeof(message));
- xbt_assert(not message.callback, "Support for client-side function proposition is not implemented.");
- XBT_DEBUG("Received symbol: %s", message.name);
+ case MessageType::REGISTER_SYMBOL: {
+ s_mc_message_register_symbol_t message;
+ xbt_assert(size == sizeof(message), "Broken message");
+ memcpy(&message, buffer, sizeof(message));
+ xbt_assert(not message.callback, "Support for client-side function proposition is not implemented.");
+ XBT_DEBUG("Received symbol: %s", message.name);
- if (property_automaton == nullptr)
- property_automaton = xbt_automaton_new();
+ if (property_automaton == nullptr)
+ property_automaton = xbt_automaton_new();
- const RemoteSimulation* process = &this->get_remote_simulation();
- RemotePtr<int> address = remote((int*)message.data);
- xbt::add_proposition(property_automaton, message.name, [process, address]() { return process->read(address); });
+ const RemoteSimulation* process = &this->get_remote_simulation();
+ RemotePtr<int> address = remote((int*)message.data);
+ xbt::add_proposition(property_automaton, message.name, [process, address]() { return process->read(address); });
- break;
+ break;
}
- case MC_MESSAGE_WAITING:
- return false;
+ case MessageType::WAITING:
+ return false;
- case MC_MESSAGE_ASSERTION_FAILED:
- MC_report_assertion_error();
- this->exit(SIMGRID_MC_EXIT_SAFETY);
+ case MessageType::ASSERTION_FAILED:
+ MC_report_assertion_error();
+ this->exit(SIMGRID_MC_EXIT_SAFETY);
- default:
- xbt_die("Unexpected message from model-checked application");
+ default:
+ xbt_die("Unexpected message from model-checked application");
}
return true;
}
{
s_mc_message_simcall_handle_t m;
memset(&m, 0, sizeof(m));
- m.type = MC_MESSAGE_SIMCALL_HANDLE;
+ m.type = MessageType::SIMCALL_HANDLE;
m.pid = transition.pid_;
m.value = transition.argument_;
checker_side_.get_channel().send(m);
bool ModelChecker::checkDeadlock()
{
- int res = checker_side_.get_channel().send(MC_MESSAGE_DEADLOCK_CHECK);
+ int res = checker_side_.get_channel().send(MessageType::DEADLOCK_CHECK);
xbt_assert(res == 0, "Could not check deadlock state");
s_mc_message_int_t message;
ssize_t s = checker_side_.get_channel().receive(message);
xbt_assert(s != -1, "Could not receive message");
- xbt_assert(s == sizeof(message) && message.type == MC_MESSAGE_DEADLOCK_CHECK_REPLY,
+ xbt_assert(s == sizeof(message) && message.type == MessageType::DEADLOCK_CHECK_REPLY,
"Received unexpected message %s (%i, size=%i) "
- "expected MC_MESSAGE_DEADLOCK_CHECK_REPLY (%i, size=%i)",
- MC_message_type_name(message.type), (int)message.type, (int)s, (int)MC_MESSAGE_DEADLOCK_CHECK_REPLY,
+ "expected MessageType::DEADLOCK_CHECK_REPLY (%i, size=%i)",
+ MC_message_type_name(message.type), (int)message.type, (int)s, (int)MessageType::DEADLOCK_CHECK_REPLY,
(int)sizeof(message));
return message.value != 0;
}
bool Session::actor_is_enabled(aid_t pid) const
{
- s_mc_message_actor_enabled_t msg{MC_MESSAGE_ACTOR_ENABLED, pid};
+ s_mc_message_actor_enabled_t msg{simgrid::mc::MessageType::ACTOR_ENABLED, pid};
model_checker_->channel().send(msg);
std::array<char, MC_MESSAGE_LENGTH> buff;
ssize_t received = model_checker_->channel().receive(buff.data(), buff.size(), true);
}
// Send result:
- s_mc_message_int_t answer{MC_MESSAGE_DEADLOCK_CHECK_REPLY, deadlock};
+ s_mc_message_int_t answer{MessageType::DEADLOCK_CHECK_REPLY, deadlock};
xbt_assert(channel_.send(answer) == 0, "Could not send response");
}
void AppSide::handle_continue(const s_mc_message_t*) const
smx_actor_t process = SIMIX_process_from_PID(message->pid);
xbt_assert(process != nullptr, "Invalid pid %lu", message->pid);
process->simcall_handle(message->value);
- if (channel_.send(MC_MESSAGE_WAITING))
+ if (channel_.send(MessageType::WAITING))
xbt_die("Could not send MESSAGE_WAITING to model-checker");
}
void AppSide::handle_actor_enabled(const s_mc_message_actor_enabled_t* msg) const
{
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};
+ s_mc_message_int_t answer{MessageType::ACTOR_ENABLED_REPLY, res};
channel_.send(answer);
}
const s_mc_message_t* message = (s_mc_message_t*)message_buffer.data();
switch (message->type) {
- case MC_MESSAGE_DEADLOCK_CHECK:
+ case MessageType::DEADLOCK_CHECK:
assert_msg_size("DEADLOCK_CHECK", s_mc_message_t);
handle_deadlock_check(message);
break;
- case MC_MESSAGE_CONTINUE:
+ case MessageType::CONTINUE:
assert_msg_size("MESSAGE_CONTINUE", s_mc_message_t);
handle_continue(message);
return;
- case MC_MESSAGE_SIMCALL_HANDLE:
+ case MessageType::SIMCALL_HANDLE:
assert_msg_size("SIMCALL_HANDLE", s_mc_message_simcall_handle_t);
handle_simcall((s_mc_message_simcall_handle_t*)message_buffer.data());
break;
- case MC_MESSAGE_ACTOR_ENABLED:
+ case MessageType::ACTOR_ENABLED:
assert_msg_size("ACTOR_ENABLED", s_mc_message_actor_enabled_t);
handle_actor_enabled((s_mc_message_actor_enabled_t*)message_buffer.data());
break;
default:
- xbt_die("Received unexpected message %s (%i)", MC_message_type_name(message->type), message->type);
+ xbt_die("Received unexpected message %s (%i)", MC_message_type_name(message->type),
+ static_cast<int>(message->type));
break;
}
}
{
while (true) {
simgrid::mc::wait_for_requests();
- xbt_assert(channel_.send(MC_MESSAGE_WAITING) == 0, "Could not send WAITING message to model-checker");
+ xbt_assert(channel_.send(MessageType::WAITING) == 0, "Could not send WAITING message to model-checker");
this->handle_messages();
}
}
void AppSide::report_assertion_failure() const
{
- if (channel_.send(MC_MESSAGE_ASSERTION_FAILED))
+ if (channel_.send(MessageType::ASSERTION_FAILED))
xbt_die("Could not send assertion to model-checker");
this->handle_messages();
}
void AppSide::ignore_memory(void* addr, std::size_t size) const
{
s_mc_message_ignore_memory_t message;
- message.type = MC_MESSAGE_IGNORE_MEMORY;
+ message.type = MessageType::IGNORE_MEMORY;
message.addr = (std::uintptr_t)addr;
message.size = size;
if (channel_.send(message))
const s_xbt_mheap_t* heap = mmalloc_get_current_heap();
s_mc_message_ignore_heap_t message;
- message.type = MC_MESSAGE_IGNORE_HEAP;
+ message.type = MessageType::IGNORE_HEAP;
message.address = address;
message.size = size;
message.block = ((char*)address - (char*)heap->heapbase) / BLOCKSIZE + 1;
void AppSide::unignore_heap(void* address, std::size_t size) const
{
s_mc_message_ignore_memory_t message;
- message.type = MC_MESSAGE_UNIGNORE_HEAP;
+ message.type = MessageType::UNIGNORE_HEAP;
message.addr = (std::uintptr_t)address;
message.size = size;
if (channel_.send(message))
void AppSide::declare_symbol(const char* name, int* value) const
{
s_mc_message_register_symbol_t message;
- message.type = MC_MESSAGE_REGISTER_SYMBOL;
+ message.type = MessageType::REGISTER_SYMBOL;
if (strlen(name) + 1 > sizeof(message.name))
xbt_die("Symbol is too long");
strncpy(message.name, name, sizeof(message.name));
region.block = ((char*)stack - (char*)heap->heapbase) / BLOCKSIZE + 1;
s_mc_message_stack_region_t message;
- message.type = MC_MESSAGE_STACK_REGION;
+ message.type = MessageType::STACK_REGION;
message.stack_region = region;
if (channel_.send(message))
xbt_die("Could not send STACK_REGION to model-checker");
/** @brief Send a message; returns 0 on success or errno on failure */
int Channel::send(const void* message, size_t size) const
{
- XBT_DEBUG("Send %s", MC_message_type_name(*(e_mc_message_type*)message));
+ XBT_DEBUG("Send %s", MC_message_type_name(*(MessageType*)message));
while (::send(this->socket_, message, size, 0) == -1) {
if (errno != EINTR)
return errno;
{
ssize_t res = recv(this->socket_, message, size, block ? 0 : MSG_DONTWAIT);
if (res != -1)
- XBT_DEBUG("Receive %s", MC_message_type_name(*(e_mc_message_type*)message));
+ XBT_DEBUG("Receive %s", MC_message_type_name(*(MessageType*)message));
return res;
}
}
// Send
int send(const void* message, size_t size) const;
- int send(e_mc_message_type type) const
+ int send(MessageType type) const
{
s_mc_message_t message = {type};
return this->send(&message, sizeof(message));
* under the terms of the license (GNU LGPL) which comes with this package. */
#include "src/mc/remote/mc_protocol.h"
+#include <array>
-const char* MC_message_type_name(e_mc_message_type type)
+const char* MC_message_type_name(simgrid::mc::MessageType type)
{
- switch (type) {
- case MC_MESSAGE_NONE:
- return "NONE";
- case MC_MESSAGE_CONTINUE:
- return "CONTINUE";
- case MC_MESSAGE_IGNORE_HEAP:
- return "IGNORE_HEAP";
- case MC_MESSAGE_UNIGNORE_HEAP:
- return "UNIGNORE_HEAP";
- case MC_MESSAGE_IGNORE_MEMORY:
- return "IGNORE_MEMORY";
- case MC_MESSAGE_STACK_REGION:
- return "STACK_REGION";
- case MC_MESSAGE_REGISTER_SYMBOL:
- return "REGISTER_SYMBOL";
- case MC_MESSAGE_DEADLOCK_CHECK:
- return "DEADLOCK_CHECK";
- case MC_MESSAGE_DEADLOCK_CHECK_REPLY:
- return "DEADLOCK_CHECK_REPLY";
- case MC_MESSAGE_WAITING:
- return "WAITING";
- case MC_MESSAGE_SIMCALL_HANDLE:
- return "SIMCALL_HANDLE";
- case MC_MESSAGE_ASSERTION_FAILED:
- return "ASSERTION_FAILED";
-
- case MC_MESSAGE_ACTOR_ENABLED:
- return "ACTOR_ENABLED";
- case MC_MESSAGE_ACTOR_ENABLED_REPLY:
- return "ACTOR_ENABLED_REPLY";
-
- default:
- return "?";
- }
+ constexpr std::array<const char*, 14> names{{"NONE", "CONTINUE", "IGNORE_HEAP", "UNIGNORE_HEAP", "IGNORE_MEMORY",
+ "STACK_REGION", "REGISTER_SYMBOL", "DEADLOCK_CHECK",
+ "DEADLOCK_CHECK_REPLY", "WAITING", "SIMCALL_HANDLE", "ASSERTION_FAILED",
+ "ACTOR_ENABLED", "ACTOR_ENABLED_REPLY"}};
+ return names[static_cast<int>(type)];
}
#ifndef SIMGRID_MC_PROTOCOL_H
#define SIMGRID_MC_PROTOCOL_H
-#include "mc/datatypes.h"
-#include "simgrid/forward.h"
-#include "stdint.h"
-
-SG_BEGIN_DECL
-
// ***** Environment variables for passing context to the model-checked process
/** Environment variable name used to pass the communication socket.
*/
#define MC_ENV_SOCKET_FD "SIMGRID_MC_SOCKET_FD"
-// ***** Messages
+#ifdef __cplusplus
-enum e_mc_message_type {
- MC_MESSAGE_NONE,
- MC_MESSAGE_CONTINUE,
- MC_MESSAGE_IGNORE_HEAP,
- MC_MESSAGE_UNIGNORE_HEAP,
- MC_MESSAGE_IGNORE_MEMORY,
- MC_MESSAGE_STACK_REGION,
- MC_MESSAGE_REGISTER_SYMBOL,
- MC_MESSAGE_DEADLOCK_CHECK,
- MC_MESSAGE_DEADLOCK_CHECK_REPLY,
- MC_MESSAGE_WAITING,
- MC_MESSAGE_SIMCALL_HANDLE,
- MC_MESSAGE_ASSERTION_FAILED,
- MC_MESSAGE_ACTOR_ENABLED,
- MC_MESSAGE_ACTOR_ENABLED_REPLY
+#include "cstdint"
+#include "mc/datatypes.h"
+#include "simgrid/forward.h" // aid_t
+
+// ***** Messages
+namespace simgrid {
+namespace mc {
+
+enum class MessageType {
+ NONE,
+ CONTINUE,
+ IGNORE_HEAP,
+ UNIGNORE_HEAP,
+ IGNORE_MEMORY,
+ STACK_REGION,
+ REGISTER_SYMBOL,
+ DEADLOCK_CHECK,
+ DEADLOCK_CHECK_REPLY,
+ WAITING,
+ SIMCALL_HANDLE,
+ ASSERTION_FAILED,
+ ACTOR_ENABLED,
+ ACTOR_ENABLED_REPLY
};
+} // namespace mc
+} // namespace simgrid
+
#define MC_MESSAGE_LENGTH 512
/** Basic structure for a MC message
/* Basic structure: all message start with a message type */
struct s_mc_message_t {
- enum e_mc_message_type type;
+ simgrid::mc::MessageType type;
};
struct s_mc_message_int_t {
- enum e_mc_message_type type;
+ simgrid::mc::MessageType type;
uint64_t value;
};
/* Client->Server */
struct s_mc_message_ignore_heap_t {
- enum e_mc_message_type type;
+ simgrid::mc::MessageType type;
int block;
int fragment;
void* address;
};
struct s_mc_message_ignore_memory_t {
- enum e_mc_message_type type;
+ simgrid::mc::MessageType type;
uint64_t addr;
size_t size;
};
struct s_mc_message_stack_region_t {
- enum e_mc_message_type type;
+ simgrid::mc::MessageType type;
s_stack_region_t stack_region;
};
struct s_mc_message_register_symbol_t {
- enum e_mc_message_type type;
+ simgrid::mc::MessageType type;
char name[128];
int (*callback)(void*);
void* data;
/* Server -> client */
struct s_mc_message_simcall_handle_t {
- enum e_mc_message_type type;
+ simgrid::mc::MessageType type;
unsigned long pid;
int value;
};
struct s_mc_message_restore_t {
- enum e_mc_message_type type;
+ simgrid::mc::MessageType type;
int index;
};
struct s_mc_message_actor_enabled_t {
- enum e_mc_message_type type;
+ simgrid::mc::MessageType type;
aid_t aid; // actor ID
};
-XBT_PRIVATE const char* MC_message_type_name(enum e_mc_message_type type);
-
-SG_END_DECL
+XBT_PRIVATE const char* MC_message_type_name(simgrid::mc::MessageType type);
+#endif // __cplusplus
#endif
