#include "src/mc/mc_private.h"
#include "src/mc/mc_record.h"
#include "src/mc/mc_request.h"
-#include "src/mc/mc_safety.h"
#include "src/mc/mc_smx.h"
#include "src/mc/mc_state.h"
#include "src/mc/remote/Client.hpp"
}
static void update_comm_pattern(simgrid::mc::PatternCommunication* comm_pattern,
- simgrid::mc::RemotePtr<simgrid::kernel::activity::Comm> comm_addr)
+ simgrid::mc::RemotePtr<simgrid::kernel::activity::CommImpl> comm_addr)
{
// HACK, type punning
- simgrid::mc::Remote<simgrid::kernel::activity::Comm> temp_comm;
+ simgrid::mc::Remote<simgrid::kernel::activity::CommImpl> temp_comm;
mc_model_checker->process().read(temp_comm, comm_addr);
- simgrid::kernel::activity::Comm* comm = temp_comm.getBuffer();
+ simgrid::kernel::activity::CommImpl* comm = temp_comm.getBuffer();
smx_actor_t src_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->src_proc));
smx_actor_t dst_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->dst_proc));
if (call_type == MC_CALL_TYPE_SEND) {
/* Create comm pattern */
pattern->type = simgrid::mc::PatternCommunicationType::send;
- pattern->comm_addr = simcall_comm_isend__get__result(request);
+ pattern->comm_addr = static_cast<simgrid::kernel::activity::CommImpl*>(simcall_comm_isend__getraw__result(request));
- simgrid::mc::Remote<simgrid::kernel::activity::Comm> temp_synchro;
+ simgrid::mc::Remote<simgrid::kernel::activity::CommImpl> temp_synchro;
mc_model_checker->process().read(temp_synchro,
- remote(static_cast<simgrid::kernel::activity::Comm*>(pattern->comm_addr)));
- simgrid::kernel::activity::Comm* synchro = static_cast<simgrid::kernel::activity::Comm*>(temp_synchro.getBuffer());
+ remote(static_cast<simgrid::kernel::activity::CommImpl*>(pattern->comm_addr)));
+ simgrid::kernel::activity::CommImpl* synchro =
+ static_cast<simgrid::kernel::activity::CommImpl*>(temp_synchro.getBuffer());
char* remote_name = mc_model_checker->process().read<char*>(
(std::uint64_t)(synchro->mbox ? &synchro->mbox->name_ : &synchro->mbox_cpy->name_));
}
} else if (call_type == MC_CALL_TYPE_RECV) {
pattern->type = simgrid::mc::PatternCommunicationType::receive;
- pattern->comm_addr = simcall_comm_irecv__get__result(request);
+ pattern->comm_addr = static_cast<simgrid::kernel::activity::CommImpl*>(simcall_comm_irecv__getraw__result(request));
simgrid::smpi::Request mpi_request;
mc_model_checker->process().read(&mpi_request,
remote((simgrid::smpi::Request*)simcall_comm_irecv__get__data(request)));
pattern->tag = mpi_request.tag();
- simgrid::mc::Remote<simgrid::kernel::activity::Comm> temp_comm;
+ simgrid::mc::Remote<simgrid::kernel::activity::CommImpl> temp_comm;
mc_model_checker->process().read(temp_comm,
- remote(static_cast<simgrid::kernel::activity::Comm*>(pattern->comm_addr)));
- simgrid::kernel::activity::Comm* comm = temp_comm.getBuffer();
+ remote(static_cast<simgrid::kernel::activity::CommImpl*>(pattern->comm_addr)));
+ simgrid::kernel::activity::CommImpl* comm = temp_comm.getBuffer();
char* remote_name;
mc_model_checker->process().read(&remote_name, remote(comm->mbox ? &comm->mbox->name_ : &comm->mbox_cpy->name_));
}
void CommunicationDeterminismChecker::complete_comm_pattern(
- xbt_dynar_t list, simgrid::mc::RemotePtr<simgrid::kernel::activity::Comm> comm_addr, unsigned int issuer,
+ xbt_dynar_t list, simgrid::mc::RemotePtr<simgrid::kernel::activity::CommImpl> comm_addr, unsigned int issuer,
int backtracking)
{
simgrid::mc::PatternCommunication* current_comm_pattern;
/* 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->interleave(actor.copy.getBuffer());
+ initial_state->addInterleavingSet(actor.copy.getBuffer());
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->interleave(actor.copy.getBuffer());
+ next_state->addInterleavingSet(actor.copy.getBuffer());
if (dot_output != nullptr)
fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",