template <class T> inline void read(Remote<T>& buffer, RemotePtr<T> ptr) const
{
- this->read_bytes(buffer.getBuffer(), sizeof(T), ptr);
+ this->read_bytes(buffer.get_buffer(), sizeof(T), ptr);
}
/** Read a given data structure from the address space
{
((ModelChecker *)arg)->handle_events(fd, events);
};
- socket_event_ = event_new(base_,
- process_->getChannel().getSocket(),
- EV_READ|EV_PERSIST,
- event_callback, this);
+ socket_event_ = event_new(base_, process_->get_channel().get_socket(), EV_READ | EV_PERSIST, event_callback, this);
event_add(socket_event_, NULL);
signal_event_ = event_new(base_,
SIGCHLD,
void ModelChecker::resume(simgrid::mc::RemoteClient& process)
{
- int res = process.getChannel().send(MC_MESSAGE_CONTINUE);
+ int res = process.get_channel().send(MC_MESSAGE_CONTINUE);
if (res)
throw simgrid::xbt::errno_error();
process.clear_cache();
simgrid::mc::dumpRecordPath();
simgrid::mc::session->log_state();
XBT_INFO("Stack trace:");
- mc_model_checker->process().dumpStack();
+ mc_model_checker->process().dump_stack();
}
static void MC_report_assertion_error()
{
if (events == EV_READ) {
char buffer[MC_MESSAGE_LENGTH];
- ssize_t size = process_->getChannel().receive(buffer, sizeof(buffer), false);
+ ssize_t size = process_->get_channel().receive(buffer, sizeof(buffer), false);
if (size == -1 && errno != EAGAIN)
throw simgrid::xbt::errno_error();
if (not handle_message(buffer, size)) {
m.type = MC_MESSAGE_SIMCALL_HANDLE;
m.pid = transition.pid;
m.value = transition.argument;
- this->process_->getChannel().send(m);
+ this->process_->get_channel().send(m);
this->process_->clear_cache();
if (this->process_->running())
event_base_dispatch(base_);
bool ModelChecker::checkDeadlock()
{
int res;
- if ((res = this->process().getChannel().send(MC_MESSAGE_DEADLOCK_CHECK)))
+ if ((res = this->process().get_channel().send(MC_MESSAGE_DEADLOCK_CHECK)))
xbt_die("Could not check deadlock state");
s_mc_message_int_t message;
- ssize_t s = mc_model_checker->process().getChannel().receive(message);
+ ssize_t s = mc_model_checker->process().get_channel().receive(message);
if (s == -1)
xbt_die("Could not receive message");
if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY)
// HACK, type punning
simgrid::mc::Remote<simgrid::kernel::activity::CommImpl> temp_comm;
mc_model_checker->process().read(temp_comm, comm_addr);
- simgrid::kernel::activity::CommImpl* comm = temp_comm.getBuffer();
+ simgrid::kernel::activity::CommImpl* comm = temp_comm.get_buffer();
- smx_actor_t src_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->src_actor_.get()));
- smx_actor_t dst_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->dst_actor_.get()));
+ smx_actor_t src_proc = mc_model_checker->process().resolve_actor(simgrid::mc::remote(comm->src_actor_.get()));
+ smx_actor_t dst_proc = mc_model_checker->process().resolve_actor(simgrid::mc::remote(comm->dst_actor_.get()));
comm_pattern->src_proc = src_proc->get_pid();
comm_pattern->dst_proc = dst_proc->get_pid();
comm_pattern->src_host = MC_smx_actor_get_host_name(src_proc);
mc_model_checker->process().read(temp_synchro,
remote(static_cast<simgrid::kernel::activity::CommImpl*>(pattern->comm_addr)));
simgrid::kernel::activity::CommImpl* synchro =
- static_cast<simgrid::kernel::activity::CommImpl*>(temp_synchro.getBuffer());
+ static_cast<simgrid::kernel::activity::CommImpl*>(temp_synchro.get_buffer());
char* remote_name = mc_model_checker->process().read<char*>(RemotePtr<char*>(
(uint64_t)(synchro->get_mailbox() ? &synchro->get_mailbox()->name_ : &synchro->mbox_cpy->name_)));
pattern->rdv = mc_model_checker->process().read_string(RemotePtr<char>(remote_name));
pattern->src_proc =
- mc_model_checker->process().resolveActor(simgrid::mc::remote(synchro->src_actor_.get()))->get_pid();
+ mc_model_checker->process().resolve_actor(simgrid::mc::remote(synchro->src_actor_.get()))->get_pid();
pattern->src_host = MC_smx_actor_get_host_name(issuer);
#if HAVE_SMPI
simgrid::mc::Remote<simgrid::kernel::activity::CommImpl> temp_comm;
mc_model_checker->process().read(temp_comm,
remote(static_cast<simgrid::kernel::activity::CommImpl*>(pattern->comm_addr)));
- simgrid::kernel::activity::CommImpl* comm = temp_comm.getBuffer();
+ simgrid::kernel::activity::CommImpl* comm = temp_comm.get_buffer();
char* remote_name;
mc_model_checker->process().read(&remote_name,
: &simgrid::xbt::string::to_string_data(comm->mbox_cpy->name_).data));
pattern->rdv = mc_model_checker->process().read_string(RemotePtr<char>(remote_name));
pattern->dst_proc =
- mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->dst_actor_.get()))->get_pid();
+ mc_model_checker->process().resolve_actor(simgrid::mc::remote(comm->dst_actor_.get()))->get_pid();
pattern->dst_host = MC_smx_actor_get_host_name(issuer);
} else
xbt_die("Unexpected call_type %i", (int) call_type);
/* Get an enabled actor and insert it in the interleave set of the initial state */
for (auto& actor : mc_model_checker->process().actors())
- if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer()))
- initial_state->addInterleavingSet(actor.copy.getBuffer());
+ if (simgrid::mc::actor_is_enabled(actor.copy.get_buffer()))
+ initial_state->addInterleavingSet(actor.copy.get_buffer());
stack_.push_back(std::move(initial_state));
}
/* Get enabled actors and insert them in the interleave set of the next state */
for (auto& actor : mc_model_checker->process().actors())
- if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer()))
- next_state->addInterleavingSet(actor.copy.getBuffer());
+ if (simgrid::mc::actor_is_enabled(actor.copy.get_buffer()))
+ next_state->addInterleavingSet(actor.copy.get_buffer());
if (dot_output != nullptr)
fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", cur_state->num, next_state->num, req_str.c_str());
next_pair->depth = 1;
/* Get enabled actors and insert them in the interleave set of the next graph_state */
for (auto& actor : mc_model_checker->process().actors())
- if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer()))
- next_pair->graph_state->addInterleavingSet(actor.copy.getBuffer());
+ if (simgrid::mc::actor_is_enabled(actor.copy.get_buffer()))
+ next_pair->graph_state->addInterleavingSet(actor.copy.get_buffer());
next_pair->requests = next_pair->graph_state->interleaveSize();
/* FIXME : get search_cycle value for each accepting state */
if (next_pair->automaton_state->type == 1 || (current_pair && current_pair->search_cycle))
/* Get an enabled process and insert it in the interleave set of the next state */
for (auto& remoteActor : mc_model_checker->process().actors()) {
- auto actor = remoteActor.copy.getBuffer();
+ auto actor = remoteActor.copy.get_buffer();
if (simgrid::mc::actor_is_enabled(actor)) {
next_state->addInterleavingSet(actor);
if (reductionMode_ == simgrid::mc::ReductionMode::dpor)
/* Get an enabled actor and insert it in the interleave set of the initial state */
for (auto& actor : mc_model_checker->process().actors())
- if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) {
- initial_state->addInterleavingSet(actor.copy.getBuffer());
+ if (simgrid::mc::actor_is_enabled(actor.copy.get_buffer())) {
+ initial_state->addInterleavingSet(actor.copy.get_buffer());
if (reductionMode_ != simgrid::mc::ReductionMode::none)
break;
}
xbt_assert(mc_model_checker == nullptr);
if (not prop) {
if (MC_is_active())
- simgrid::mc::Client::get()->reportAssertionFailure();
+ simgrid::mc::Client::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()->ignoreMemory(addr, size);
+ simgrid::mc::Client::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()->declareSymbol(name, value);
+ simgrid::mc::Client::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()->declareStack(stack, size, actor, context);
+ simgrid::mc::Client::get()->declare_stack(stack, size, actor, 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()->ignoreHeap(address, size);
+ simgrid::mc::Client::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()->unignoreHeap(address, size);
+ simgrid::mc::Client::get()->unignore_heap(address, size);
}
simgrid::mc::processes_time.resize(SIMIX_process_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()->mainLoop();
+ simgrid::mc::Client::get()->main_loop();
}
void MC_show_deadlock()
if (use_remote_comm) {
mc_model_checker->process().read(temp_synchro,
remote(static_cast<simgrid::kernel::activity::CommImpl*>(remote_act)));
- act = temp_synchro.getBuffer();
+ act = temp_synchro.get_buffer();
} else
act = remote_act;
- smx_actor_t src_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(act->src_actor_.get()));
- smx_actor_t dst_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(act->dst_actor_.get()));
+ smx_actor_t src_proc = mc_model_checker->process().resolve_actor(simgrid::mc::remote(act->src_actor_.get()));
+ smx_actor_t dst_proc = mc_model_checker->process().resolve_actor(simgrid::mc::remote(act->dst_actor_.get()));
args =
bprintf("comm=%s [(%ld)%s (%s)-> (%ld)%s (%s)]", p, src_proc ? src_proc->get_pid() : 0,
src_proc ? MC_smx_actor_get_host_name(src_proc) : "", src_proc ? MC_smx_actor_get_name(src_proc) : "",
if (use_remote_comm) {
mc_model_checker->process().read(temp_synchro,
remote(static_cast<simgrid::kernel::activity::CommImpl*>(remote_act)));
- act = temp_synchro.getBuffer();
+ act = temp_synchro.get_buffer();
} else
act = remote_act;
type = "Test TRUE";
p = pointer_to_string(remote_act);
- smx_actor_t src_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(act->src_actor_.get()));
- smx_actor_t dst_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(act->dst_actor_.get()));
+ smx_actor_t src_proc = mc_model_checker->process().resolve_actor(simgrid::mc::remote(act->src_actor_.get()));
+ smx_actor_t dst_proc = mc_model_checker->process().resolve_actor(simgrid::mc::remote(act->dst_actor_.get()));
args = bprintf("comm=%s [(%ld)%s (%s) -> (%ld)%s (%s)]", p, src_proc->get_pid(), MC_smx_actor_get_name(src_proc),
MC_smx_actor_get_host_name(src_proc), dst_proc->get_pid(), MC_smx_actor_get_name(dst_proc),
MC_smx_actor_get_host_name(dst_proc));
type = "Mutex TRYLOCK";
simgrid::mc::Remote<simgrid::kernel::activity::MutexImpl> mutex;
- mc_model_checker->process().read_bytes(mutex.getBuffer(), sizeof(mutex),
- remote(
- req->call == SIMCALL_MUTEX_LOCK
- ? simcall_mutex_lock__get__mutex(req)
- : simcall_mutex_trylock__get__mutex(req)
- ));
+ mc_model_checker->process().read_bytes(mutex.get_buffer(), sizeof(mutex),
+ remote(req->call == SIMCALL_MUTEX_LOCK
+ ? simcall_mutex_lock__get__mutex(req)
+ : simcall_mutex_trylock__get__mutex(req)));
args = bprintf(
- "locked = %d, owner = %d, sleeping = n/a", mutex.getBuffer()->is_locked(),
- mutex.getBuffer()->owner_ != nullptr
- ? (int)mc_model_checker->process().resolveActor(simgrid::mc::remote(mutex.getBuffer()->owner_))->get_pid()
+ "locked = %d, owner = %d, sleeping = n/a", mutex.get_buffer()->is_locked(),
+ mutex.get_buffer()->owner_ != nullptr
+ ? (int)mc_model_checker->process().resolve_actor(simgrid::mc::remote(mutex.get_buffer()->owner_))->get_pid()
: -1);
break;
}
simgrid::mc::Remote<simgrid::kernel::activity::CommImpl> temp_comm;
mc_model_checker->process().read(temp_comm, remote(remote_act));
- simgrid::kernel::activity::CommImpl* comm = temp_comm.getBuffer();
+ simgrid::kernel::activity::CommImpl* comm = temp_comm.get_buffer();
return comm->src_actor_.get() && comm->dst_actor_.get();
}
simgrid::mc::Remote<simgrid::kernel::activity::CommImpl> temp_comm;
mc_model_checker->process().read(temp_comm,
remote(static_cast<simgrid::kernel::activity::CommImpl*>(remote_act)));
- simgrid::kernel::activity::CommImpl* comm = temp_comm.getBuffer();
+ simgrid::kernel::activity::CommImpl* comm = temp_comm.get_buffer();
- smx_actor_t src_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->src_actor_.get()));
- smx_actor_t dst_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->dst_actor_.get()));
+ smx_actor_t src_proc = mc_model_checker->process().resolve_actor(simgrid::mc::remote(comm->src_actor_.get()));
+ smx_actor_t dst_proc = mc_model_checker->process().resolve_actor(simgrid::mc::remote(comm->dst_actor_.get()));
if (issuer->get_host())
label = simgrid::xbt::string_printf("[(%ld)%s] Wait [(%ld)->(%ld)]", issuer->get_pid(),
MC_smx_actor_get_host_name(issuer), src_proc ? src_proc->get_pid() : 0,
simgrid::kernel::activity::ActivityImpl* remote_act = simcall_comm_test__getraw__comm(req);
simgrid::mc::Remote<simgrid::kernel::activity::CommImpl> temp_comm;
mc_model_checker->process().read(temp_comm, remote(static_cast<simgrid::kernel::activity::CommImpl*>(remote_act)));
- simgrid::kernel::activity::CommImpl* comm = temp_comm.getBuffer();
+ simgrid::kernel::activity::CommImpl* comm = temp_comm.get_buffer();
if (comm->src_actor_.get() == nullptr || comm->dst_actor_.get() == nullptr) {
if (issuer->get_host())
label =
static inline simgrid::mc::ActorInformation* actor_info_cast(smx_actor_t actor)
{
simgrid::mc::ActorInformation temp;
- std::size_t offset = (char*) temp.copy.getBuffer() - (char*)&temp;
+ std::size_t offset = (char*)temp.copy.get_buffer() - (char*)&temp;
simgrid::mc::ActorInformation* process_info = (simgrid::mc::ActorInformation*)((char*)actor - offset);
return process_info;
Remote<simgrid::simix::Global> simix_global =
this->read<simgrid::simix::Global>(simix_global_p);
- MC_process_refresh_simix_actor_dynar(this, this->smx_actors_infos, remote(simix_global.getBuffer()->actors_vector));
+ MC_process_refresh_simix_actor_dynar(this, this->smx_actors_infos, remote(simix_global.get_buffer()->actors_vector));
MC_process_refresh_simix_actor_dynar(this, this->smx_dead_actors_infos,
- remote(simix_global.getBuffer()->dead_actors_vector));
+ remote(simix_global.get_buffer()->dead_actors_vector));
this->cache_flags_ |= RemoteClient::cache_simix_processes;
}
// Lookup by address:
for (auto& actor : mc_model_checker->process().actors())
if (actor.address == address)
- return actor.copy.getBuffer();
+ return actor.copy.get_buffer();
for (auto& actor : mc_model_checker->process().dead_actors())
if (actor.address == address)
- return actor.copy.getBuffer();
+ return actor.copy.get_buffer();
xbt_die("Issuer not found");
}
remote(static_cast<simgrid::kernel::activity::CommImpl*>(simcall_comm_wait__getraw__comm(&actor->simcall)));
simgrid::mc::Remote<simgrid::kernel::activity::CommImpl> temp_act;
mc_model_checker->process().read(temp_act, remote_act);
- simgrid::kernel::activity::CommImpl* act = temp_act.getBuffer();
+ simgrid::kernel::activity::CommImpl* act = temp_act.get_buffer();
if (act->src_actor_.get() && act->dst_actor_.get())
state->transition.argument = 0;
else if (act->src_actor_.get() == nullptr && act->type_ == simgrid::kernel::activity::CommImpl::Type::READY &&
remote_comm =
mc_model_checker->process().read(remote(simcall_comm_waitany__get__comms(req) + state->transition.argument));
mc_model_checker->process().read(state->internal_comm, remote(remote_comm));
- simcall_comm_wait__set__comm(&state->internal_req, state->internal_comm.getBuffer());
+ simcall_comm_wait__set__comm(&state->internal_req, state->internal_comm.get_buffer());
simcall_comm_wait__set__timeout(&state->internal_req, 0);
break;
}
mc_model_checker->process().read(state->internal_comm, remote(remote_comm));
}
- simcall_comm_test__set__comm(&state->internal_req, state->internal_comm.getBuffer());
+ simcall_comm_test__set__comm(&state->internal_req, state->internal_comm.get_buffer());
simcall_comm_test__set__result(&state->internal_req, state->transition.argument);
break;
case SIMCALL_COMM_WAIT:
mc_model_checker->process().read_bytes(&state->internal_comm, sizeof(state->internal_comm),
remote(simcall_comm_wait__getraw__comm(req)));
- simcall_comm_wait__set__comm(&state->executed_req, state->internal_comm.getBuffer());
- simcall_comm_wait__set__comm(&state->internal_req, state->internal_comm.getBuffer());
+ simcall_comm_wait__set__comm(&state->executed_req, state->internal_comm.get_buffer());
+ simcall_comm_wait__set__comm(&state->internal_req, state->internal_comm.get_buffer());
break;
case SIMCALL_COMM_TEST:
mc_model_checker->process().read_bytes(&state->internal_comm, sizeof(state->internal_comm),
remote(simcall_comm_test__getraw__comm(req)));
- simcall_comm_test__set__comm(&state->executed_req, state->internal_comm.getBuffer());
- simcall_comm_test__set__comm(&state->internal_req, state->internal_comm.getBuffer());
+ simcall_comm_test__set__comm(&state->executed_req, state->internal_comm.get_buffer());
+ simcall_comm_test__set__comm(&state->internal_req, state->internal_comm.get_buffer());
break;
default:
{
for (auto& actor : mc_model_checker->process().actors()) {
/* Only consider the actors that were marked as interleaving by the checker algorithm */
- if (not state->actorStates[actor.copy.getBuffer()->get_pid()].isTodo())
+ if (not state->actorStates[actor.copy.get_buffer()->get_pid()].isTodo())
continue;
- smx_simcall_t res = MC_state_get_request_for_process(state, actor.copy.getBuffer());
+ smx_simcall_t res = MC_state_get_request_for_process(state, actor.copy.get_buffer());
if (res)
return res;
}
return this->receive(&m, sizeof(M));
}
- int getSocket() const { return socket_; }
+ int get_socket() const { return socket_; }
};
}
}
if (errno != 0 || raise(SIGSTOP) != 0)
xbt_die("Could not wait for the model-checker (errno = %d: %s)", errno, strerror(errno));
- instance_->handleMessages();
+ instance_->handle_messages();
return instance_.get();
}
-void Client::handleDeadlockCheck(s_mc_message_t*)
+void Client::handle_deadlock_check(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::handleContinue(s_mc_message_t*)
+void Client::handle_continue(s_mc_message_t*)
{
/* Nothing to do */
}
-void Client::handleSimcall(s_mc_message_simcall_handle_t* message)
+void Client::handle_simcall(s_mc_message_simcall_handle_t* message)
{
smx_actor_t process = SIMIX_process_from_PID(message->pid);
if (not process)
xbt_die("Could not send MESSAGE_WAITING to model-checker");
}
-void Client::handleActorEnabled(s_mc_message_actor_enabled_t* msg)
+void Client::handle_actor_enabled(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};
channel_.send(answer);
}
-void Client::handleMessages()
+void Client::handle_messages()
{
while (1) {
XBT_DEBUG("Waiting messages from model-checker");
case MC_MESSAGE_DEADLOCK_CHECK:
xbt_assert(received_size == sizeof(s_mc_message_t), "Unexpected size for DEADLOCK_CHECK (%zd != %zu)",
received_size, sizeof(s_mc_message_t));
- handleDeadlockCheck(message);
+ handle_deadlock_check(message);
break;
case MC_MESSAGE_CONTINUE:
xbt_assert(received_size == sizeof(s_mc_message_t), "Unexpected size for MESSAGE_CONTINUE (%zd != %zu)",
received_size, sizeof(s_mc_message_t));
- handleContinue(message);
+ handle_continue(message);
return;
case MC_MESSAGE_SIMCALL_HANDLE:
xbt_assert(received_size == sizeof(s_mc_message_simcall_handle_t),
"Unexpected size for SIMCALL_HANDLE (%zd != %zu)", received_size,
sizeof(s_mc_message_simcall_handle_t));
- handleSimcall((s_mc_message_simcall_handle_t*)message_buffer);
+ handle_simcall((s_mc_message_simcall_handle_t*)message_buffer);
break;
case MC_MESSAGE_ACTOR_ENABLED:
xbt_assert(received_size == sizeof(s_mc_message_actor_enabled_t),
"Unexpected size for ACTOR_ENABLED (%zd != %zu)", received_size,
sizeof(s_mc_message_actor_enabled_t));
- handleActorEnabled((s_mc_message_actor_enabled_t*)message_buffer);
+ handle_actor_enabled((s_mc_message_actor_enabled_t*)message_buffer);
break;
default:
}
}
-void Client::mainLoop()
+void Client::main_loop()
{
while (1) {
simgrid::mc::wait_for_requests();
xbt_assert(channel_.send(MC_MESSAGE_WAITING) == 0, "Could not send WAITING message to model-checker");
- this->handleMessages();
+ this->handle_messages();
}
}
-void Client::reportAssertionFailure()
+void Client::report_assertion_failure()
{
if (channel_.send(MC_MESSAGE_ASSERTION_FAILED))
xbt_die("Could not send assertion to model-checker");
- this->handleMessages();
+ this->handle_messages();
}
-void Client::ignoreMemory(void* addr, std::size_t size)
+void Client::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::ignoreHeap(void* address, std::size_t size)
+void Client::ignore_heap(void* address, std::size_t size)
{
xbt_mheap_t heap = mmalloc_get_current_heap();
xbt_die("Could not send ignored region to MCer");
}
-void Client::unignoreHeap(void* address, std::size_t size)
+void Client::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::declareSymbol(const char* name, int* value)
+void Client::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::declareStack(void* stack, size_t size, smx_actor_t process, ucontext_t* context)
+void Client::declare_stack(void* stack, size_t size, smx_actor_t process, ucontext_t* context)
{
xbt_mheap_t heap = mmalloc_get_current_heap();
public:
Client();
explicit Client(int fd) : channel_(fd) {}
- void handleMessages();
+ void handle_messages();
private:
- void handleDeadlockCheck(s_mc_message_t* msg);
- void handleContinue(s_mc_message_t* msg);
- void handleSimcall(s_mc_message_simcall_handle_t* message);
- void handleActorEnabled(s_mc_message_actor_enabled_t* msg);
+ void handle_deadlock_check(s_mc_message_t* msg);
+ void handle_continue(s_mc_message_t* msg);
+ void handle_simcall(s_mc_message_simcall_handle_t* message);
+ void handle_actor_enabled(s_mc_message_actor_enabled_t* msg);
public:
- Channel const& getChannel() const { return channel_; }
- Channel& getChannel() { return channel_; }
- XBT_ATTRIB_NORETURN void mainLoop();
- void reportAssertionFailure();
- void ignoreMemory(void* addr, std::size_t size);
- void ignoreHeap(void* addr, std::size_t size);
- void unignoreHeap(void* addr, std::size_t size);
- void declareSymbol(const char* name, int* value);
+ Channel const& get_channel() const { return channel_; }
+ Channel& get_channel() { return channel_; }
+ XBT_ATTRIB_NORETURN void main_loop();
+ void report_assertion_failure();
+ void ignore_memory(void* addr, std::size_t size);
+ void ignore_heap(void* addr, std::size_t size);
+ void unignore_heap(void* addr, std::size_t size);
+ void declare_symbol(const char* name, int* value);
#if HAVE_UCONTEXT_H
- void declareStack(void* stack, size_t size, smx_actor_t process, ucontext_t* context);
+ void declare_stack(void* stack, size_t size, smx_actor_t process, ucontext_t* context);
#endif
// Singleton :/
return smx_dead_actors_infos;
}
-void RemoteClient::dumpStack()
+void RemoteClient::dump_stack()
{
unw_addr_space_t as = unw_create_addr_space(&_UPT_accessors, BYTE_ORDER);
if (as == nullptr) {
bool RemoteClient::actor_is_enabled(aid_t pid)
{
s_mc_message_actor_enabled_t msg{MC_MESSAGE_ACTOR_ENABLED, pid};
- process()->getChannel().send(msg);
+ process()->get_channel().send(msg);
char buff[MC_MESSAGE_LENGTH];
- ssize_t received = process()->getChannel().receive(buff, MC_MESSAGE_LENGTH, true);
+ ssize_t received = process()->get_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;
}
template <class T> Remote<T> read_variable(const char* name) const
{
Remote<T> res;
- read_variable(name, res.getBuffer(), sizeof(T));
+ read_variable(name, res.get_buffer(), sizeof(T));
return res;
}
void clear_cache() { this->cache_flags_ = RemoteClient::cache_none; }
- Channel const& getChannel() const { return channel_; }
- Channel& getChannel() { return channel_; }
+ 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);
std::vector<simgrid::mc::ActorInformation>& dead_actors();
/** Get a local description of a remote SIMIX actor */
- simgrid::mc::ActorInformation* resolveActorInfo(simgrid::mc::RemotePtr<simgrid::kernel::actor::ActorImpl> actor)
+ simgrid::mc::ActorInformation* resolve_actor_info(simgrid::mc::RemotePtr<simgrid::kernel::actor::ActorImpl> actor)
{
xbt_assert(mc_model_checker != nullptr);
if (not actor)
}
/** Get a local copy of the SIMIX actor structure */
- simgrid::kernel::actor::ActorImpl* resolveActor(simgrid::mc::RemotePtr<simgrid::kernel::actor::ActorImpl> process)
+ simgrid::kernel::actor::ActorImpl* resolve_actor(simgrid::mc::RemotePtr<simgrid::kernel::actor::ActorImpl> process)
{
- simgrid::mc::ActorInformation* actor_info = this->resolveActorInfo(process);
+ simgrid::mc::ActorInformation* actor_info = this->resolve_actor_info(process);
if (actor_info)
- return actor_info->copy.getBuffer();
+ return actor_info->copy.get_buffer();
else
return nullptr;
}
- void dumpStack();
+ void dump_stack();
private:
void init_memory_map_info();
Remote() = default;
explicit Remote(T const& p) { std::memcpy(&buffer, &p, sizeof buffer); }
- T* getBuffer() { return reinterpret_cast<T*>(&buffer); }
- const T* getBuffer() const { return reinterpret_cast<const T*>(&buffer); }
- std::size_t getBufferSize() const { return sizeof(T); }
+ T* get_buffer() { return reinterpret_cast<T*>(&buffer); }
+ const T* get_buffer() const { return reinterpret_cast<const T*>(&buffer); }
+ std::size_t get_buffer_size() const { return sizeof(T); }
operator T() const
{
static_assert(std::is_trivial<T>::value, "Cannot convert non trivial type");
- return *getBuffer();
+ return *get_buffer();
}
void clear() { std::memset(&buffer, 0, sizeof buffer); }
};
explicit RemotePtr(std::nullptr_t) : address_(0) {}
explicit RemotePtr(std::uint64_t address) : address_(address) {}
explicit RemotePtr(T* address) : address_((std::uintptr_t)address) {}
- explicit RemotePtr(Remote<T*> p) : address_((std::uintptr_t)*p.getBuffer()) {}
+ explicit RemotePtr(Remote<T*> p) : address_((std::uintptr_t)*p.get_buffer()) {}
std::uint64_t address() const { return address_; }
/** Turn into a local pointer
, hash_(0)
{
for (auto const& p : process->actors())
- enabled_processes_.insert(p.copy.getBuffer()->get_pid());
+ enabled_processes_.insert(p.copy.get_buffer()->get_pid());
snapshot_handle_ignore(this);