#ifndef SIMGRID_MC_ADDRESS_SPACE_H
#define SIMGRID_MC_ADDRESS_SPACE_H
+#include <cassert>
#include <cstddef>
#include <cstdint>
#include <type_traits>
static constexpr ReadOptions lazy() { return ReadOptions(1); }
};
+/** A value read from another process */
+template<class T>
+class Remote {
+private:
+ char buffer[sizeof(T)];
+public:
+ void* data() { return buffer; }
+ const void* data() const { return buffer; }
+ constexpr std::size_t size() const { return sizeof(T); }
+};
+
/** A given state of a given process (abstract base class)
*
* Currently, this might either be:
this->read_bytes(buffer, sizeof(T), ptr, process_index);
}
+ template<class T> inline
+ void read(Remote<T>& buffer, RemotePtr<T> ptr, int process_index = ProcessIndexAny)
+ {
+ this->read_bytes(buffer.data(), sizeof(T), ptr, process_index);
+ }
+
/** Read a given data structure from the address space */
template<class T> inline
T read(RemotePtr<T> ptr, int process_index = ProcessIndexMissing)
/********** 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::simix::Comm> comm_addr)
{
- s_smx_synchro_t comm;
- mc_model_checker->process().read(&comm, remote(comm_addr));
+ // HACK, type punning
+ simgrid::mc::Remote<simgrid::simix::Comm> temp_comm;
+ mc_model_checker->process().read(temp_comm, comm_addr);
+ simgrid::simix::Comm* comm =
+ static_cast<simgrid::simix::Comm*>(temp_comm.data());
smx_process_t src_proc = mc_model_checker->process().resolveProcess(
- simgrid::mc::remote(comm.comm.src_proc));
+ simgrid::mc::remote(comm->src_proc));
smx_process_t dst_proc = mc_model_checker->process().resolveProcess(
- simgrid::mc::remote(comm.comm.dst_proc));
+ 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) {
+ 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);
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::simix::Comm> temp_synchro;
+ mc_model_checker->process().read(temp_synchro, remote(
+ static_cast<simgrid::simix::Comm*>(pattern->comm_addr)));
+ simgrid::simix::Comm* synchro =
+ static_cast<simgrid::simix::Comm*>(temp_synchro.data());
char* remote_name = mc_model_checker->process().read<char*>(
- (std::uint64_t)(synchro.comm.mbox ? &synchro.comm.mbox->name : &synchro.comm.mbox_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;
+ simgrid::mc::remote(synchro->src_proc))->pid;
pattern->src_host = MC_smx_process_get_host_name(issuer);
struct s_smpi_mpi_request 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::simix::Comm> temp_comm;
+ mc_model_checker->process().read(temp_comm, remote(
+ static_cast<simgrid::simix::Comm*>(pattern->comm_addr)));
+ simgrid::simix::Comm* comm =
+ static_cast<simgrid::simix::Comm*>(temp_comm.data());
char* remote_name;
mc_model_checker->process().read(&remote_name,
- remote(synchro.comm.mbox ? &synchro.comm.mbox->name : &synchro.comm.mbox_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;
+ simgrid::mc::remote(comm->dst_proc))->pid;
pattern->dst_host = MC_smx_process_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::simix::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;
public:
// These are used by functions which should be moved in CommunicationDeterminismChecker:
void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking);
- void complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking);
+ void complete_comm_pattern(
+ xbt_dynar_t list, simgrid::mc::RemotePtr<simgrid::simix::Comm> comm_addr,
+ unsigned int issuer, int backtracking);
private:
/** Stack representing the position in the exploration graph */
std::list<std::unique_ptr<simgrid::mc::State>> stack_;
*/
class Member {
public:
+ typedef int flags_type;
+ static constexpr flags_type INHERITANCE_FLAG = 1;
+ static constexpr flags_type VIRTUAL_POINTER_FLAG = 2;
+
Member() {}
/** Whether this member represent some inherited part of the object */
- bool inheritance = false;
+ flags_type flags = 0;
/** Name of the member (if any) */
std::string name;
unsigned type_id = 0;
simgrid::mc::Type* type = nullptr;
+ bool isInheritance() const
+ {
+ return this->flags & INHERITANCE_FLAG;
+ }
+ bool isVirtualPointer() const
+ {
+ return this->flags & VIRTUAL_POINTER_FLAG;
+ }
+
/** Whether the member is at a fixed offset from the base address */
bool has_offset_location() const
{
#include <cassert>
+#include <algorithm>
+
#include <simgrid_config.h>
#include <xbt/log.h>
#include "src/mc/mc_protocol.h"
#include "src/simix/Synchro.h"
+#include "src/simix/SynchroIo.hpp"
#include "src/simix/SynchroComm.hpp"
+#include "src/simix/SynchroRaw.hpp"
+#include "src/simix/SynchroSleep.hpp"
+#include "src/simix/SynchroExec.hpp"
#if HAVE_MC
#include "src/mc/mc_request.h"
bool request_is_enabled(smx_simcall_t req)
{
unsigned int index = 0;
-#if HAVE_MC
- simgrid::simix::Synchro temp_synchro;
-#endif
+ // TODO, add support for the subtypes?
switch (req->call) {
case SIMCALL_NONE:
#if HAVE_MC
// Fetch from MCed memory:
+ // HACK, type puning
+ simgrid::mc::Remote<simgrid::simix::Comm> temp_comm;
if (mc_model_checker != nullptr) {
- mc_model_checker->process().read(&temp_synchro, remote(act));
- act = &temp_synchro;
+ mc_model_checker->process().read(temp_comm, remote(act));
+ act = static_cast<simgrid::simix::Comm*>(temp_comm.data());
}
#endif
for (index = 0; index < comms->used; ++index) {
#if HAVE_MC
// Fetch act from MCed memory:
+ // HACK, type puning
+ simgrid::mc::Remote<simgrid::simix::Comm> temp_comm;
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;
+ mc_model_checker->process().read(temp_comm, remote(act));
+ act = static_cast<simgrid::simix::Comm*>(temp_comm.data());
}
else
#endif
case MC_CALL_TYPE_WAIT:
case MC_CALL_TYPE_WAITANY:
{
- smx_synchro_t comm_addr = nullptr;
+ simgrid::mc::RemotePtr<simgrid::simix::Comm> comm_addr = nullptr;
if (call_type == MC_CALL_TYPE_WAIT)
- comm_addr = simcall_comm_wait__get__comm(req);
- else
+ comm_addr = remote(static_cast<simgrid::simix::Comm*>(
+ simcall_comm_wait__get__comm(req)));
+ else {
+ simgrid::simix::Comm* addr;
// comm_addr = REMOTE(xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_synchro_t)):
- simgrid::mc::read_element(mc_model_checker->process(), &comm_addr,
+ simgrid::mc::read_element(mc_model_checker->process(), &addr,
remote(simcall_comm_waitany__get__comms(req)), value, sizeof(comm_addr));
+ comm_addr = remote(addr);
+ }
checker->complete_comm_pattern(pattern, comm_addr,
MC_smx_simcall_get_issuer(req)->pid, backtracking);
}
#include <dwarf.h>
#include <elfutils/libdw.h>
+#include <boost/algorithm/string/predicate.hpp>
+
#include <simgrid_config.h>
#include "src/simgrid/util.hpp"
#include <xbt/log.h>
// TODO, we should use another type (because is is not a type but a member)
simgrid::mc::Member member;
- member.inheritance = tag == DW_TAG_inheritance;
+ if (tag == DW_TAG_inheritance)
+ member.flags |= simgrid::mc::Member::INHERITANCE_FLAG;
const char *name = MC_dwarf_attr_integrate_string(&child, DW_AT_name);
if (name)
member.name = name;
+ // Those base names are used by GCC and clang for virtual table pointers
+ // respectively ("__vptr$ClassName", "__vptr.ClassName"):
+ if (boost::algorithm::starts_with(member.name, "__vptr$") ||
+ boost::algorithm::starts_with(member.name, "__vptr."))
+ member.flags |= simgrid::mc::Member::VIRTUAL_POINTER_FLAG;
+ // A cleaner stolution would be to check against the type:
+ // ---
+ // tag: DW_TAG_member
+ // name: "_vptr$Foo"
+ // type:
+ // # Type for a pointer to a vtable
+ // tag: DW_TAG_pointer_type
+ // type:
+ // # Type for a vtable:
+ // tag: DW_TAG_pointer_type
+ // name: "__vtbl_ptr_type"
+ // type:
+ // tag: DW_TAG_subroutine_type
+ // type:
+ // tag: DW_TAG_base_type
+ // name: "int"
+ // ---
+
member.byte_size =
MC_dwarf_attr_integrate_uint(&child, DW_AT_byte_size, 0);
member.type_id = MC_dwarf_at_type(&child);
static char *buff_size_to_string(size_t size);
static inline
-smx_synchro_t MC_get_comm(smx_simcall_t r)
+simgrid::simix::Comm* MC_get_comm(smx_simcall_t r)
{
switch (r->call ) {
case SIMCALL_COMM_WAIT:
- return simcall_comm_wait__get__comm(r);
+ return static_cast<simgrid::simix::Comm*>(simcall_comm_wait__get__comm(r));
case SIMCALL_COMM_TEST:
- return simcall_comm_test__get__comm(r);
+ return static_cast<simgrid::simix::Comm*>(simcall_comm_test__get__comm(r));
default:
return nullptr;
}
// Those are internal requests, we do not need indirection
// because those objects are copies:
- smx_synchro_t synchro1 = MC_get_comm(r1);
- smx_synchro_t synchro2 = MC_get_comm(r2);
+ simgrid::simix::Comm* synchro1 = MC_get_comm(r1);
+ simgrid::simix::Comm* synchro2 = MC_get_comm(r2);
if ((r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV)
&& r2->call == SIMCALL_COMM_WAIT) {
smx_mailbox_t mbox = MC_get_mbox(r1);
- if (mbox != synchro2->comm.mbox_cpy
+ if (mbox != synchro2->mbox_cpy
&& simcall_comm_wait__get__timeout(r2) <= 0)
return false;
- if ((r1->issuer != synchro2->comm.src_proc)
- && (r1->issuer != synchro2->comm.dst_proc)
+ if ((r1->issuer != synchro2->src_proc)
+ && (r1->issuer != synchro2->dst_proc)
&& simcall_comm_wait__get__timeout(r2) <= 0)
return false;
if ((r1->call == SIMCALL_COMM_ISEND)
- && (synchro2->comm.type == SIMIX_COMM_SEND)
- && (synchro2->comm.src_buff !=
+ && (synchro2->type == SIMIX_COMM_SEND)
+ && (synchro2->src_buff !=
simcall_comm_isend__get__src_buff(r1))
&& simcall_comm_wait__get__timeout(r2) <= 0)
return false;
if ((r1->call == SIMCALL_COMM_IRECV)
- && (synchro2->comm.type == SIMIX_COMM_RECEIVE)
- && (synchro2->comm.dst_buff != simcall_comm_irecv__get__dst_buff(r1))
+ && (synchro2->type == SIMIX_COMM_RECEIVE)
+ && (synchro2->dst_buff != simcall_comm_irecv__get__dst_buff(r1))
&& simcall_comm_wait__get__timeout(r2) <= 0)
return false;
}
if (r1->call == SIMCALL_COMM_WAIT
&& (r2->call == SIMCALL_COMM_WAIT || r2->call == SIMCALL_COMM_TEST)
- && (synchro1->comm.src_proc == nullptr || synchro1->comm.dst_proc == nullptr))
+ && (synchro1->src_proc == nullptr || synchro1->dst_proc == nullptr))
return false;
if (r1->call == SIMCALL_COMM_TEST &&
(simcall_comm_test__get__comm(r1) == nullptr
- || synchro1->comm.src_buff == nullptr
- || synchro1->comm.dst_buff == nullptr))
+ || synchro1->src_buff == nullptr
+ || synchro1->dst_buff == nullptr))
return false;
if (r1->call == SIMCALL_COMM_TEST && r2->call == SIMCALL_COMM_WAIT
- && synchro1->comm.src_buff == synchro2->comm.src_buff
- && synchro1->comm.dst_buff == synchro2->comm.dst_buff)
+ && synchro1->src_buff == synchro2->src_buff
+ && synchro1->dst_buff == synchro2->dst_buff)
return false;
if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_TEST
- && synchro1->comm.src_buff != nullptr
- && synchro1->comm.dst_buff != nullptr
- && synchro2->comm.src_buff != nullptr
- && synchro2->comm.dst_buff != nullptr
- && synchro1->comm.dst_buff != synchro2->comm.src_buff
- && synchro1->comm.dst_buff != synchro2->comm.dst_buff
- && synchro2->comm.dst_buff != synchro1->comm.src_buff)
+ && synchro1->src_buff != nullptr
+ && synchro1->dst_buff != nullptr
+ && synchro2->src_buff != nullptr
+ && synchro2->dst_buff != nullptr
+ && synchro1->dst_buff != synchro2->src_buff
+ && synchro1->dst_buff != synchro2->dst_buff
+ && synchro2->dst_buff != synchro1->src_buff)
return false;
return true;
// Those are internal requests, we do not need indirection
// because those objects are copies:
- smx_synchro_t synchro1 = MC_get_comm(r1);
- smx_synchro_t synchro2 = MC_get_comm(r2);
+ simgrid::simix::Comm* synchro1 = MC_get_comm(r1);
+ simgrid::simix::Comm* synchro2 = MC_get_comm(r2);
switch(r1->call) {
case SIMCALL_COMM_ISEND:
- return simcall_comm_isend__get__mbox(r1) == simcall_comm_isend__get__mbox(r2);
+ return simcall_comm_isend__get__mbox(r1)
+ == simcall_comm_isend__get__mbox(r2);
case SIMCALL_COMM_IRECV:
- return simcall_comm_irecv__get__mbox(r1) == simcall_comm_irecv__get__mbox(r2);
+ return simcall_comm_irecv__get__mbox(r1)
+ == simcall_comm_irecv__get__mbox(r2);
case SIMCALL_COMM_WAIT:
- if (synchro1->comm.src_buff == synchro2->comm.src_buff
- && synchro1->comm.dst_buff == synchro2->comm.dst_buff)
+ if (synchro1->src_buff == synchro2->src_buff
+ && synchro1->dst_buff == synchro2->dst_buff)
return false;
- else if (synchro1->comm.src_buff != nullptr
- && synchro1->comm.dst_buff != nullptr
- && synchro2->comm.src_buff != nullptr
- && synchro2->comm.dst_buff != nullptr
- && synchro1->comm.dst_buff != synchro2->comm.src_buff
- && synchro1->comm.dst_buff != synchro2->comm.dst_buff
- && synchro2->comm.dst_buff != synchro1->comm.src_buff)
+ else if (synchro1->src_buff != nullptr
+ && synchro1->dst_buff != nullptr
+ && synchro2->src_buff != nullptr
+ && synchro2->dst_buff != nullptr
+ && synchro1->dst_buff != synchro2->src_buff
+ && synchro1->dst_buff != synchro2->dst_buff
+ && synchro2->dst_buff != synchro1->src_buff)
return false;
else
return true;
}
case SIMCALL_COMM_WAIT: {
- smx_synchro_t remote_act = simcall_comm_wait__get__comm(req);
+ simgrid::simix::Comm* remote_act =
+ static_cast<simgrid::simix::Comm*>(simcall_comm_wait__get__comm(req));
char* p;
if (value == -1) {
type = "WaitTimeout";
type = "Wait";
p = pointer_to_string(remote_act);
- s_smx_synchro_t synchro;
- smx_synchro_t act;
+ simgrid::mc::Remote<simgrid::simix::Comm> temp_synchro;
+ simgrid::simix::Comm* act;
if (use_remote_comm) {
- mc_model_checker->process().read_bytes(&synchro,
- sizeof(synchro), remote(remote_act));
- act = &synchro;
+ mc_model_checker->process().read(temp_synchro, remote(
+ static_cast<simgrid::simix::Comm*>(remote_act)));
+ act = static_cast<simgrid::simix::Comm*>(temp_synchro.data());
} else
act = remote_act;
smx_process_t src_proc = mc_model_checker->process().resolveProcess(
- simgrid::mc::remote(act->comm.src_proc));
+ simgrid::mc::remote(act->src_proc));
smx_process_t dst_proc = mc_model_checker->process().resolveProcess(
- simgrid::mc::remote(act->comm.dst_proc));
+ simgrid::mc::remote(act->dst_proc));
args = bprintf("comm=%s [(%lu)%s (%s)-> (%lu)%s (%s)]", p,
src_proc ? src_proc->pid : 0,
src_proc ? MC_smx_process_get_host_name(src_proc) : "",
}
case SIMCALL_COMM_TEST: {
- smx_synchro_t remote_act = simcall_comm_test__get__comm(req);
- s_smx_synchro_t synchro;
- smx_synchro_t act;
- if (use_remote_comm) {
- mc_model_checker->process().read_bytes(&synchro,
- sizeof(synchro), remote(remote_act));
- act = &synchro;
- } else
- act = remote_act;
+ simgrid::simix::Comm* remote_act = static_cast<simgrid::simix::Comm*>(
+ simcall_comm_test__get__comm(req));
+ simgrid::mc::Remote<simgrid::simix::Comm> temp_synchro;
+ simgrid::simix::Comm* act;
+ if (use_remote_comm) {
+ mc_model_checker->process().read(temp_synchro, remote(
+ static_cast<simgrid::simix::Comm*>(remote_act)));
+ act = static_cast<simgrid::simix::Comm*>(temp_synchro.data());
+ } else
+ act = remote_act;
char* p;
- if (act->comm.src_proc == nullptr || act->comm.dst_proc == nullptr) {
+ if (act->src_proc == nullptr || act->dst_proc == nullptr) {
type = "Test FALSE";
p = pointer_to_string(remote_act);
args = bprintf("comm=%s", p);
p = pointer_to_string(remote_act);
smx_process_t src_proc = mc_model_checker->process().resolveProcess(
- simgrid::mc::remote(act->comm.src_proc));
+ simgrid::mc::remote(act->src_proc));
smx_process_t dst_proc = mc_model_checker->process().resolveProcess(
- simgrid::mc::remote(act->comm.dst_proc));
+ simgrid::mc::remote(act->dst_proc));
args = bprintf("comm=%s [(%lu)%s (%s) -> (%lu)%s (%s)]", p,
src_proc->pid,
MC_smx_process_get_name(src_proc),
return true;
}
- s_smx_synchro_t synchro;
- mc_model_checker->process().read_bytes(
- &synchro, sizeof(synchro), remote(remote_act));
- return synchro.comm.src_proc && synchro.comm.dst_proc;
+ simgrid::mc::Remote<simgrid::simix::Comm> temp_comm;
+ mc_model_checker->process().read(temp_comm, remote(
+ static_cast<simgrid::simix::Comm*>(remote_act)));
+ simgrid::simix::Comm* comm = static_cast<simgrid::simix::Comm*>(temp_comm.data());
+ return comm->src_proc && comm->dst_proc;
}
bool process_is_enabled(smx_process_t process)
label = simgrid::xbt::string_printf("[(%lu)] WaitTimeout", issuer->pid);
} else {
smx_synchro_t remote_act = simcall_comm_wait__get__comm(req);
- s_smx_synchro_t synchro;
- mc_model_checker->process().read_bytes(&synchro,
- sizeof(synchro), remote(remote_act));
+ simgrid::mc::Remote<simgrid::simix::Comm> temp_comm;
+ mc_model_checker->process().read(temp_comm, remote(
+ static_cast<simgrid::simix::Comm*>(remote_act)));
+ simgrid::simix::Comm* comm = static_cast<simgrid::simix::Comm*>(temp_comm.data());
smx_process_t src_proc = mc_model_checker->process().resolveProcess(
- simgrid::mc::remote(synchro.comm.src_proc));
+ simgrid::mc::remote(comm->src_proc));
smx_process_t dst_proc = mc_model_checker->process().resolveProcess(
- simgrid::mc::remote(synchro.comm.dst_proc));
+ simgrid::mc::remote(comm->dst_proc));
if (issuer->host)
label = simgrid::xbt::string_printf("[(%lu)%s] Wait [(%lu)->(%lu)]",
issuer->pid,
case SIMCALL_COMM_TEST: {
smx_synchro_t remote_act = simcall_comm_test__get__comm(req);
- s_smx_synchro_t synchro;
- mc_model_checker->process().read_bytes(&synchro,
- sizeof(synchro), remote(remote_act));
- if (synchro.comm.src_proc == nullptr || synchro.comm.dst_proc == nullptr) {
+ simgrid::mc::Remote<simgrid::simix::Comm> temp_comm;
+ mc_model_checker->process().read(temp_comm, remote(
+ static_cast<simgrid::simix::Comm*>(remote_act)));
+ simgrid::simix::Comm* comm = static_cast<simgrid::simix::Comm*>(temp_comm.data());
+ if (comm->src_proc == nullptr || comm->dst_proc == nullptr) {
if (issuer->host)
label = simgrid::xbt::string_printf("[(%lu)%s] Test FALSE",
issuer->pid,
State::State()
{
- std::memset(&this->internal_comm, 0, sizeof(this->internal_comm));
+ std::memset(this->internal_comm.data(), 0, this->internal_comm.size());
std::memset(&this->internal_req, 0, sizeof(this->internal_req));
std::memset(&this->executed_req, 0, sizeof(this->executed_req));
}
}
case SIMCALL_COMM_WAIT: {
- smx_synchro_t remote_act = simcall_comm_wait__get__comm(&process->simcall);
- s_smx_synchro_t act;
- mc_model_checker->process().read_bytes(
- &act, sizeof(act), remote(remote_act));
- if (act.comm.src_proc && act.comm.dst_proc)
+ simgrid::mc::RemotePtr<simgrid::simix::Comm> remote_act = remote(
+ static_cast<simgrid::simix::Comm*>(simcall_comm_wait__get__comm(&process->simcall)));
+ simgrid::mc::Remote<simgrid::simix::Comm> temp_act;
+ mc_model_checker->process().read(temp_act, remote_act);
+ simgrid::simix::Comm* act = static_cast<simgrid::simix::Comm*>(temp_act.data());
+ if (act->src_proc && act->dst_proc)
state->transition.argument = 0;
- else if (act.comm.src_proc == nullptr && act.comm.type == SIMIX_COMM_READY
- && act.comm.detached == 1)
+ else if (act->src_proc == nullptr && act->type == SIMIX_COMM_READY
+ && act->detached == 1)
state->transition.argument = 0;
else
state->transition.argument = -1;
read_element(mc_model_checker->process(),
&remote_comm, remote(simcall_comm_waitany__get__comms(req)),
state->transition.argument, sizeof(remote_comm));
- mc_model_checker->process().read(&state->internal_comm, remote(remote_comm));
+ mc_model_checker->process().read(state->internal_comm, remote(
+ static_cast<simgrid::simix::Comm*>(remote_comm)));
simcall_comm_wait__set__comm(&state->internal_req, &state->internal_comm);
simcall_comm_wait__set__timeout(&state->internal_req, 0);
break;
read_element(mc_model_checker->process(),
&remote_comm, remote(simcall_comm_testany__get__comms(req)),
state->transition.argument, sizeof(remote_comm));
- mc_model_checker->process().read(&state->internal_comm, remote(remote_comm));
+ mc_model_checker->process().read(state->internal_comm, remote(
+ static_cast<simgrid::simix::Comm*>(remote_comm)));
}
simcall_comm_test__set__comm(&state->internal_req, &state->internal_comm);
#include <simgrid_config.h>
#include "src/simix/smx_private.h"
+#include "src/simix/SynchroIo.hpp"
+#include "src/simix/SynchroComm.hpp"
+#include "src/simix/SynchroRaw.hpp"
+#include "src/simix/SynchroSleep.hpp"
+#include "src/simix/SynchroExec.hpp"
#include "src/mc/mc_snapshot.h"
#include "src/mc/mc_record.h"
#include "src/mc/Transition.hpp"
namespace simgrid {
namespace mc {
+enum class PatternCommunicationType {
+ none = 0,
+ send = 1,
+ receive = 2,
+};
+
struct PatternCommunication {
int num = 0;
smx_synchro_t comm_addr;
- e_smx_comm_type_t type = SIMIX_COMM_SEND;
+ PatternCommunicationType type = PatternCommunicationType::send;
unsigned long src_proc = 0;
unsigned long dst_proc = 0;
const char *src_host = nullptr;
s_smx_simcall_t internal_req;
/* Can be used as a copy of the remote synchro object */
- s_smx_synchro_t internal_comm;
+ simgrid::mc::Remote<simgrid::simix::Comm> internal_comm;
/** Snapshot of system state (if needed) */
std::shared_ptr<simgrid::mc::Snapshot> system_state;
return;
}
- if ((*request)->action != NULL) { // this is not a detached send
+ if ((*request)->action != NULL)
+ // this is not a detached send
simcall_comm_wait((*request)->action, -1.0);
- if((MC_is_active() || MC_record_replay_is_active()) && (*request)->action) {
- simgrid::simix::Comm *comm = dynamic_cast<simgrid::simix::Comm*>( (*request)->action );
-
- comm->dst_data = NULL; // dangling pointer: dst_data is freed with a wait, need to set it to NULL for system state comparison
- }
- }
-
finish_wait(request, status);
if (*request != MPI_REQUEST_NULL && ((*request)->flags & NON_PERSISTENT))
*request = MPI_REQUEST_NULL;