/********** Static functions ***********/
-static e_mc_comm_pattern_difference_t compare_comm_pattern(simgrid::mc::PatternCommunication* comm1, simgrid::mc::PatternCommunication* comm2) {
+static e_mc_comm_pattern_difference_t compare_comm_pattern(simgrid::mc::PatternCommunication* comm1, simgrid::mc::PatternCommunication* comm2)
+{
if(comm1->type != comm2->type)
return TYPE_DIFF;
if (comm1->rdv != comm2->rdv)
static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int process, simgrid::mc::PatternCommunication* comm, unsigned int cursor) {
char *type, *res;
- if(comm->type == SIMIX_COMM_SEND)
+ if (comm->type == simgrid::mc::PatternCommunicationType::send)
type = bprintf("The send communications pattern of the process %d is different!", process - 1);
else
type = bprintf("The recv communications pattern of the process %d is different!", process - 1);
return res;
}
-static void update_comm_pattern(simgrid::mc::PatternCommunication* comm_pattern, smx_synchro_t comm_addr)
+static void update_comm_pattern(
+ simgrid::mc::PatternCommunication* comm_pattern,
+ simgrid::mc::RemotePtr<simgrid::kernel::activity::Comm> comm_addr)
{
- s_smx_synchro_t comm;
- mc_model_checker->process().read(&comm, remote(comm_addr));
+ // HACK, type punning
+ simgrid::mc::Remote<simgrid::kernel::activity::Comm> temp_comm;
+ mc_model_checker->process().read(temp_comm, comm_addr);
+ simgrid::kernel::activity::Comm* comm = temp_comm.getBuffer();
- smx_process_t src_proc = mc_model_checker->process().resolveProcess(
- simgrid::mc::remote(comm.comm.src_proc));
- smx_process_t dst_proc = mc_model_checker->process().resolveProcess(
- simgrid::mc::remote(comm.comm.dst_proc));
+ 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));
comm_pattern->src_proc = src_proc->pid;
comm_pattern->dst_proc = dst_proc->pid;
- comm_pattern->src_host = MC_smx_process_get_host_name(src_proc);
- comm_pattern->dst_host = MC_smx_process_get_host_name(dst_proc);
- if (comm_pattern->data.size() == 0 && comm.comm.src_buff != nullptr) {
+ comm_pattern->src_host = MC_smx_actor_get_host_name(src_proc);
+ comm_pattern->dst_host = MC_smx_actor_get_host_name(dst_proc);
+ if (comm_pattern->data.size() == 0 && comm->src_buff != nullptr) {
size_t buff_size;
mc_model_checker->process().read(
- &buff_size, remote(comm.comm.dst_buff_size));
+ &buff_size, remote(comm->dst_buff_size));
comm_pattern->data.resize(buff_size);
mc_model_checker->process().read_bytes(
comm_pattern->data.data(), comm_pattern->data.size(),
- remote(comm.comm.src_buff));
+ remote(comm->src_buff));
}
}
namespace simgrid {
namespace mc {
-void CommunicationDeterminismChecker::deterministic_comm_pattern(int process, simgrid::mc::PatternCommunication* comm, int backtracking) {
-
+void CommunicationDeterminismChecker::deterministic_comm_pattern(
+ int process, simgrid::mc::PatternCommunication* comm, int backtracking)
+{
simgrid::mc::PatternCommunicationList* list =
xbt_dynar_get_as(initial_communications_pattern, process, simgrid::mc::PatternCommunicationList*);
compare_comm_pattern(list->list[list->index_comm].get(), comm);
if (diff != NONE_DIFF) {
- if (comm->type == SIMIX_COMM_SEND){
+ if (comm->type == simgrid::mc::PatternCommunicationType::send) {
this->send_deterministic = 0;
if (this->send_diff != nullptr)
xbt_free(this->send_diff);
this->send_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
- }else{
+ } else {
this->recv_deterministic = 0;
if (this->recv_diff != nullptr)
xbt_free(this->recv_diff);
void CommunicationDeterminismChecker::get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking)
{
- const smx_process_t issuer = MC_smx_simcall_get_issuer(request);
+ const smx_actor_t issuer = MC_smx_simcall_get_issuer(request);
simgrid::mc::PatternCommunicationList* initial_pattern = xbt_dynar_get_as(
initial_communications_pattern, issuer->pid, simgrid::mc::PatternCommunicationList*);
xbt_dynar_t incomplete_pattern = xbt_dynar_get_as(
if (call_type == MC_CALL_TYPE_SEND) {
/* Create comm pattern */
- pattern->type = SIMIX_COMM_SEND;
+ pattern->type = simgrid::mc::PatternCommunicationType::send;
pattern->comm_addr = simcall_comm_isend__get__result(request);
- s_smx_synchro_t synchro = mc_model_checker->process().read<s_smx_synchro_t>(
- (std::uint64_t) pattern->comm_addr);
+ simgrid::mc::Remote<simgrid::kernel::activity::Comm> 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());
char* remote_name = mc_model_checker->process().read<char*>(
- (std::uint64_t)(synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name));
+ (std::uint64_t)(synchro->mbox ? &synchro->mbox->name : &synchro->mbox_cpy->name));
pattern->rdv = mc_model_checker->process().read_string(remote_name);
- pattern->src_proc = mc_model_checker->process().resolveProcess(
- simgrid::mc::remote(synchro.comm.src_proc))->pid;
- pattern->src_host = MC_smx_process_get_host_name(issuer);
+ pattern->src_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(synchro->src_proc))->pid;
+ pattern->src_host = MC_smx_actor_get_host_name(issuer);
struct s_smpi_mpi_request mpi_request =
mc_model_checker->process().read<s_smpi_mpi_request>(
(std::uint64_t) simcall_comm_isend__get__data(request));
pattern->tag = mpi_request.tag;
- if(synchro.comm.src_buff != nullptr){
- pattern->data.resize(synchro.comm.src_buff_size);
+ if (synchro->src_buff != nullptr){
+ pattern->data.resize(synchro->src_buff_size);
mc_model_checker->process().read_bytes(
pattern->data.data(), pattern->data.size(),
- remote(synchro.comm.src_buff));
+ remote(synchro->src_buff));
}
if(mpi_request.detached){
if (!this->initial_communications_pattern_done) {
return;
}
} else if (call_type == MC_CALL_TYPE_RECV) {
- pattern->type = SIMIX_COMM_RECEIVE;
+ pattern->type = simgrid::mc::PatternCommunicationType::receive;
pattern->comm_addr = simcall_comm_irecv__get__result(request);
struct s_smpi_mpi_request mpi_request;
&mpi_request, remote((struct s_smpi_mpi_request*)simcall_comm_irecv__get__data(request)));
pattern->tag = mpi_request.tag;
- s_smx_synchro_t synchro;
- mc_model_checker->process().read(&synchro, remote(pattern->comm_addr));
+ simgrid::mc::Remote<simgrid::kernel::activity::Comm> 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();
char* remote_name;
mc_model_checker->process().read(&remote_name,
- remote(synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name));
+ remote(comm->mbox ? &comm->mbox->name : &comm->mbox_cpy->name));
pattern->rdv = mc_model_checker->process().read_string(remote_name);
- pattern->dst_proc = mc_model_checker->process().resolveProcess(
- simgrid::mc::remote(synchro.comm.dst_proc))->pid;
- pattern->dst_host = MC_smx_process_get_host_name(issuer);
+ pattern->dst_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->dst_proc))->pid;
+ pattern->dst_host = MC_smx_actor_get_host_name(issuer);
} else
xbt_die("Unexpected call_type %i", (int) call_type);
}
-void CommunicationDeterminismChecker::complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking)
+void CommunicationDeterminismChecker::complete_comm_pattern(
+ xbt_dynar_t list, simgrid::mc::RemotePtr<simgrid::kernel::activity::Comm> comm_addr,
+ unsigned int issuer, int backtracking)
{
simgrid::mc::PatternCommunication* current_comm_pattern;
unsigned int cursor = 0;
/* Complete comm pattern */
xbt_dynar_foreach(xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, current_comm_pattern)
- if (current_comm_pattern->comm_addr == comm_addr) {
+ if (remote(current_comm_pattern->comm_addr) == comm_addr) {
update_comm_pattern(current_comm_pattern, comm_addr);
completed = 1;
simgrid::mc::PatternCommunication* temp;
}
std::unique_ptr<simgrid::mc::State> initial_state =
- std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
+ std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
XBT_DEBUG("********* Start communication determinism verification *********");
- /* Get an enabled process and insert it in the interleave set of the initial state */
- for (auto& p : mc_model_checker->process().simix_processes())
- if (simgrid::mc::process_is_enabled(&p.copy))
- initial_state->interleave(&p.copy);
+ /* 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());
stack_.push_back(std::move(initial_state));
}
static inline
bool all_communications_are_finished()
{
- for (size_t current_process = 1; current_process < MC_smx_get_maxpid(); current_process++) {
- xbt_dynar_t pattern = xbt_dynar_get_as(
- incomplete_communications_pattern, current_process, xbt_dynar_t);
+ for (size_t current_actor = 1; current_actor < MC_smx_get_maxpid(); current_actor++) {
+ xbt_dynar_t pattern = xbt_dynar_get_as(incomplete_communications_pattern, current_actor, xbt_dynar_t);
if (!xbt_dynar_is_empty(pattern)) {
XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
return false;
/* because we got a copy of the executed request, we have to fetch the
real one, pointed by the request field of the issuer process */
- const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
+ const smx_actor_t issuer = MC_smx_simcall_get_issuer(saved_req);
smx_simcall_t req = &issuer->simcall;
/* TODO : handle test and testany simcalls */
/* Create the new expanded state */
std::unique_ptr<simgrid::mc::State> next_state =
- std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
+ std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
/* If comm determinism verification, we cannot stop the exploration if
- some communications are not finished (at least, data are transfered).
+ some communications are not finished (at least, data are transferred).
These communications are incomplete and they cannot be analyzed and
compared with the initial pattern. */
bool compare_snapshots = all_communications_are_finished()
|| (visited_state = visitedStates_.addVisitedState(
expandedStatesCount_, next_state.get(), compare_snapshots)) == nullptr) {
- /* Get enabled processes and insert them in the interleave set of the next state */
- for (auto& p : mc_model_checker->process().simix_processes())
- if (simgrid::mc::process_is_enabled(&p.copy))
- next_state->interleave(&p.copy);
+ /* 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());
if (dot_output != nullptr)
fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
}
}
-}
\ No newline at end of file
+}
