{
// Check deadlock:
bool deadlock = false;
- smx_actor_t process;
+ smx_actor_t actor;
if (xbt_swag_size(simix_global->process_list)) {
deadlock = true;
- xbt_swag_foreach(process, simix_global->process_list)
- if (simgrid::mc::process_is_enabled(process)) {
- deadlock = false;
- break;
+ xbt_swag_foreach(actor, simix_global->process_list) if (simgrid::mc::actor_is_enabled(actor))
+ {
+ deadlock = false;
+ break;
}
}
simgrid::kernel::activity::Comm* comm =
static_cast<simgrid::kernel::activity::Comm*>(temp_comm.getBuffer());
- smx_actor_t src_proc = mc_model_checker->process().resolveProcess(
- simgrid::mc::remote(comm->src_proc));
- smx_actor_t dst_proc = mc_model_checker->process().resolveProcess(
- simgrid::mc::remote(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);
+ 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(
char* remote_name = mc_model_checker->process().read<char*>(
(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->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>(
mc_model_checker->process().read(&remote_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(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);
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.getBuffer()))
- initial_state->interleave(p.copy.getBuffer());
+ /* 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;
|| (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.getBuffer()))
- next_state->interleave(p.copy.getBuffer());
+ /* 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",
process->get_heap()->heaplimit,
process->get_malloc_info());
- this->nb_processes = mc_model_checker->process().simix_processes().size();
+ this->actors_count = mc_model_checker->process().actors().size();
this->automaton_state = automaton_state;
this->num = pair_num;
pair->num, pair->automaton_state, pair->atomic_propositions,
pair->graph_state);
- auto res = boost::range::equal_range(acceptancePairs_,
- new_pair.get(), simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
+ auto res = boost::range::equal_range(acceptancePairs_, new_pair.get(),
+ simgrid::mc::DerefAndCompareByActorsCountAndUsedHeap());
if (pair->search_cycle) for (auto i = res.first; i != res.second; ++i) {
std::shared_ptr<simgrid::mc::VisitedPair> const& pair_test = *i;
pair->num, pair->automaton_state, pair->atomic_propositions,
pair->graph_state);
- auto range = boost::range::equal_range(visitedPairs_,
- visited_pair.get(), simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
+ auto range = boost::range::equal_range(visitedPairs_, visited_pair.get(),
+ simgrid::mc::DerefAndCompareByActorsCountAndUsedHeap());
for (auto i = range.first; i != range.second; ++i) {
VisitedPair* pair_test = i->get();
next_pair->depth = current_pair->depth + 1;
else
next_pair->depth = 1;
- /* Get enabled processes and insert them in the interleave set of the next graph_state */
- for (auto& p : mc_model_checker->process().simix_processes())
- if (simgrid::mc::process_is_enabled(p.copy.getBuffer()))
- next_pair->graph_state->interleave(p.copy.getBuffer());
+ /* 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->interleave(actor.copy.getBuffer());
next_pair->requests = next_pair->graph_state->interleaveSize();
- /* FIXME : get search_cycle value for each acceptant state */
+ /* FIXME : get search_cycle value for each accepting state */
if (next_pair->automaton_state->type == 1 ||
(current_pair && current_pair->search_cycle))
next_pair->search_cycle = true;
xbt_automaton_state_t automaton_state = nullptr;
std::shared_ptr<const std::vector<int>> atomic_propositions;
std::size_t heap_bytes_used = 0;
- int nb_processes = 0;
+ int actors_count = 0;
VisitedPair(
int pair_num, xbt_automaton_state_t automaton_state,
remote(std_heap_var->address),
simgrid::mc::ProcessIndexDisabled);
- this->smx_process_infos.clear();
- this->smx_old_process_infos.clear();
+ this->smx_actors_infos.clear();
+ this->smx_dead_actors_infos.clear();
this->unw_addr_space = simgrid::mc::UnwindContext::createUnwindAddressSpace();
this->unw_underlying_addr_space = simgrid::unw::create_addr_space();
this->unw_underlying_context = simgrid::unw::create_context(
info->remove_local_variable(var_name, frame_name);
}
-std::vector<simgrid::mc::SimixProcessInformation>& Process::simix_processes()
+std::vector<simgrid::mc::ActorInformation>& Process::actors()
{
this->refresh_simix();
- return smx_process_infos;
+ return smx_actors_infos;
}
-std::vector<simgrid::mc::SimixProcessInformation>& Process::old_simix_processes()
+std::vector<simgrid::mc::ActorInformation>& Process::dead_actors()
{
this->refresh_simix();
- return smx_old_process_infos;
+ return smx_dead_actors_infos;
}
void Process::dumpStack()
namespace simgrid {
namespace mc {
-class SimixProcessInformation {
+class ActorInformation {
public:
/** MCed address of the process */
RemotePtr<simgrid::simix::ActorImpl> address = nullptr;
void unignore_heap(void *address, size_t size);
void ignore_local_variable(const char *var_name, const char *frame_name);
- std::vector<simgrid::mc::SimixProcessInformation>& simix_processes();
- std::vector<simgrid::mc::SimixProcessInformation>& old_simix_processes();
+ std::vector<simgrid::mc::ActorInformation>& actors();
+ std::vector<simgrid::mc::ActorInformation>& dead_actors();
- /** Get a local description of a remote SIMIX process */
- simgrid::mc::SimixProcessInformation* resolveProcessInfo(
- simgrid::mc::RemotePtr<simgrid::simix::ActorImpl> process)
+ /** Get a local description of a remote SIMIX actor */
+ simgrid::mc::ActorInformation* resolveActorInfo(simgrid::mc::RemotePtr<simgrid::simix::ActorImpl> actor)
{
xbt_assert(mc_model_checker != nullptr);
- if (!process)
+ if (!actor)
return nullptr;
this->refresh_simix();
- for (auto& process_info : this->smx_process_infos)
- if (process_info.address == process)
- return &process_info;
- for (auto& process_info : this->smx_old_process_infos)
- if (process_info.address == process)
- return &process_info;
+ for (auto& actor_info : this->smx_actors_infos)
+ if (actor_info.address == actor)
+ return &actor_info;
+ for (auto& actor_info : this->smx_dead_actors_infos)
+ if (actor_info.address == actor)
+ return &actor_info;
return nullptr;
}
- /** Get a local copy of the SIMIX process structure */
- simgrid::simix::ActorImpl* resolveProcess(simgrid::mc::RemotePtr<simgrid::simix::ActorImpl> process)
+ /** Get a local copy of the SIMIX actor structure */
+ simgrid::simix::ActorImpl* resolveActor(simgrid::mc::RemotePtr<simgrid::simix::ActorImpl> process)
{
- simgrid::mc::SimixProcessInformation* process_info =
- this->resolveProcessInfo(process);
- if (process_info)
- return process_info->copy.getBuffer();
+ simgrid::mc::ActorInformation* actor_info = this->resolveActorInfo(process);
+ if (actor_info)
+ return actor_info->copy.getBuffer();
else
return nullptr;
}
*
* See mc_smx.c.
*/
- std::vector<SimixProcessInformation> smx_process_infos;
+ std::vector<ActorInformation> smx_actors_infos;
/** Copy of `simix_global->process_to_destroy`
*
* See mc_smx.c.
*/
- std::vector<SimixProcessInformation> smx_old_process_infos;
+ std::vector<ActorInformation> smx_dead_actors_infos;
private:
/** State of the cache (which variables are up to date) */
|| (visitedState_ = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), true)) == nullptr) {
/* Get an enabled process and insert it 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.getBuffer())) {
+ for (auto& p : mc_model_checker->process().actors())
+ if (simgrid::mc::actor_is_enabled(p.copy.getBuffer())) {
next_state->interleave(p.copy.getBuffer());
if (reductionMode_ != simgrid::mc::ReductionMode::none)
break;
XBT_DEBUG("**************************************************");
XBT_DEBUG("Initial state");
- /* 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.getBuffer())) {
- initial_state->interleave(p.copy.getBuffer());
+ /* 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());
if (reductionMode_ != simgrid::mc::ReductionMode::none)
break;
}
process->get_heap()->heaplimit,
process->get_malloc_info());
- this->nb_processes =
- mc_model_checker->process().simix_processes().size();
+ this->actors_count = mc_model_checker->process().actors().size();
this->system_state = simgrid::mc::take_snapshot(state_number);
this->num = state_number;
XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)",
new_state->system_state.get(), new_state->num, graph_state->num);
- auto range = boost::range::equal_range(states_,
- new_state.get(), simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
+ auto range =
+ boost::range::equal_range(states_, new_state.get(), simgrid::mc::DerefAndCompareByActorsCountAndUsedHeap());
if (compare_snpashots)
for (auto i = range.first; i != range.second; ++i) {
struct XBT_PRIVATE VisitedState {
std::shared_ptr<simgrid::mc::Snapshot> system_state = nullptr;
std::size_t heap_bytes_used = 0;
- int nb_processes = 0;
+ int actors_count = 0;
int num = 0;
int other_num = 0; // dot_output for
else if (mc_model_checker != nullptr) {
simgrid::mc::Process& modelchecked = mc_model_checker->process();
// TODO, *(mutex->owner) :/
- return modelchecked.resolveProcess(simgrid::mc::remote(mutex->owner))->pid
- == modelchecked.resolveProcess(simgrid::mc::remote(req->issuer))->pid;
+ return modelchecked.resolveActor(simgrid::mc::remote(mutex->owner))->pid ==
+ modelchecked.resolveActor(simgrid::mc::remote(req->issuer))->pid;
}
#endif
else
std::shared_ptr<simgrid::mc::Snapshot> snapshot = std::make_shared<simgrid::mc::Snapshot>(mc_process, num_state);
- for (auto& p : mc_model_checker->process().simix_processes())
+ for (auto& p : mc_model_checker->process().actors())
snapshot->enabled_processes.insert(p.copy.getBuffer()->pid);
snapshot_handle_ignore(snapshot.get());
class Type;
class Variable;
class Frame;
-class SimixProcessInformation;
+class ActorInformation;
class Session;
class Checker;
namespace simgrid {
namespace mc {
-struct DerefAndCompareByNbProcessesAndUsedHeap {
+struct DerefAndCompareByActorsCountAndUsedHeap {
template<class X, class Y>
bool operator()(X const& a, Y const& b)
{
- return std::make_pair(a->nb_processes, a->heap_bytes_used) <
- std::make_pair(b->nb_processes, b->heap_bytes_used);
+ return std::make_pair(a->actors_count, a->heap_bytes_used) < std::make_pair(b->actors_count, b->heap_bytes_used);
}
};
char* p = pointer_to_string(simcall_comm_isend__get__src_buff(req));
char* bs = buff_size_to_string(simcall_comm_isend__get__src_buff_size(req));
if (issuer->host)
- args =
- bprintf("src=(%lu)%s (%s), buff=%s, size=%s", issuer->pid,
- MC_smx_process_get_host_name(issuer),
- MC_smx_process_get_name(issuer),
- p, bs);
+ args = bprintf("src=(%lu)%s (%s), buff=%s, size=%s", issuer->pid, MC_smx_actor_get_host_name(issuer),
+ MC_smx_actor_get_name(issuer), p, bs);
else
- args =
- bprintf("src=(%lu)%s, buff=%s, size=%s", issuer->pid,
- MC_smx_process_get_name(issuer), p, bs);
+ args = bprintf("src=(%lu)%s, buff=%s, size=%s", issuer->pid, MC_smx_actor_get_name(issuer), p, bs);
xbt_free(bs);
xbt_free(p);
break;
char* p = pointer_to_string(simcall_comm_irecv__get__dst_buff(req));
char* bs = buff_size_to_string(size);
if (issuer->host)
- args =
- bprintf("dst=(%lu)%s (%s), buff=%s, size=%s", issuer->pid,
- MC_smx_process_get_host_name(issuer),
- MC_smx_process_get_name(issuer),
- p, bs);
+ args = bprintf("dst=(%lu)%s (%s), buff=%s, size=%s", issuer->pid, MC_smx_actor_get_host_name(issuer),
+ MC_smx_actor_get_name(issuer), p, bs);
else
- args =
- bprintf("dst=(%lu)%s, buff=%s, size=%s", issuer->pid,
- MC_smx_process_get_name(issuer),
- p, bs);
+ args = bprintf("dst=(%lu)%s, buff=%s, size=%s", issuer->pid, MC_smx_actor_get_name(issuer), p, bs);
xbt_free(bs);
xbt_free(p);
break;
} else
act = remote_act;
- smx_actor_t src_proc = mc_model_checker->process().resolveProcess(
- simgrid::mc::remote(act->src_proc));
- smx_actor_t dst_proc = mc_model_checker->process().resolveProcess(
- 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) : "",
- src_proc ? MC_smx_process_get_name(src_proc) : "",
- dst_proc ? dst_proc->pid : 0,
- dst_proc ? MC_smx_process_get_host_name(dst_proc) : "",
- dst_proc ? MC_smx_process_get_name(dst_proc) : "");
+ smx_actor_t src_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(act->src_proc));
+ smx_actor_t dst_proc = mc_model_checker->process().resolveActor(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_actor_get_host_name(src_proc) : "", src_proc ? MC_smx_actor_get_name(src_proc) : "",
+ dst_proc ? dst_proc->pid : 0, dst_proc ? MC_smx_actor_get_host_name(dst_proc) : "",
+ dst_proc ? MC_smx_actor_get_name(dst_proc) : "");
}
xbt_free(p);
break;
type = "Test TRUE";
p = pointer_to_string(remote_act);
- smx_actor_t src_proc = mc_model_checker->process().resolveProcess(
- simgrid::mc::remote(act->src_proc));
- smx_actor_t dst_proc = mc_model_checker->process().resolveProcess(
- 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),
- MC_smx_process_get_host_name(src_proc),
- dst_proc->pid,
- MC_smx_process_get_name(dst_proc),
- MC_smx_process_get_host_name(dst_proc));
+ smx_actor_t src_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(act->src_proc));
+ smx_actor_t dst_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(act->dst_proc));
+ args = bprintf("comm=%s [(%lu)%s (%s) -> (%lu)%s (%s)]", p, src_proc->pid, MC_smx_actor_get_name(src_proc),
+ MC_smx_actor_get_host_name(src_proc), dst_proc->pid, MC_smx_actor_get_name(dst_proc),
+ MC_smx_actor_get_host_name(dst_proc));
}
xbt_free(p);
break;
mc_model_checker->process().read_bytes(&mutex_sleeping, sizeof(mutex_sleeping),
remote(mutex.getBuffer()->sleeping));
- args = bprintf("locked = %d, owner = %d, sleeping = %d",
- mutex.getBuffer()->locked,
- mutex.getBuffer()->owner != nullptr ? (int) mc_model_checker->process().resolveProcess(
- simgrid::mc::remote(mutex.getBuffer()->owner))->pid : -1,
- mutex_sleeping.count);
+ args =
+ bprintf("locked = %d, owner = %d, sleeping = %d", mutex.getBuffer()->locked,
+ mutex.getBuffer()->owner != nullptr
+ ? (int)mc_model_checker->process().resolveActor(simgrid::mc::remote(mutex.getBuffer()->owner))->pid
+ : -1,
+ mutex_sleeping.count);
break;
}
std::string str;
if (args != nullptr)
- str = simgrid::xbt::string_printf("[(%lu)%s (%s)] %s(%s)", issuer->pid,
- MC_smx_process_get_host_name(issuer),
- MC_smx_process_get_name(issuer),
- type, args);
+ str = simgrid::xbt::string_printf("[(%lu)%s (%s)] %s(%s)", issuer->pid, MC_smx_actor_get_host_name(issuer),
+ MC_smx_actor_get_name(issuer), type, args);
else
- str = simgrid::xbt::string_printf("[(%lu)%s (%s)] %s ", issuer->pid,
- MC_smx_process_get_host_name(issuer),
- MC_smx_process_get_name(issuer),
- type);
+ str = simgrid::xbt::string_printf("[(%lu)%s (%s)] %s ", issuer->pid, MC_smx_actor_get_host_name(issuer),
+ MC_smx_actor_get_name(issuer), type);
xbt_free(args);
return str;
}
return comm->src_proc && comm->dst_proc;
}
-bool process_is_enabled(smx_actor_t process)
+bool actor_is_enabled(smx_actor_t actor)
{
- return simgrid::mc::request_is_enabled(&process->simcall);
+ return simgrid::mc::request_is_enabled(&actor->simcall);
}
static const char* colors[] = {
switch (req->call) {
case SIMCALL_COMM_ISEND:
if (issuer->host)
- label = simgrid::xbt::string_printf("[(%lu)%s] iSend", issuer->pid,
- MC_smx_process_get_host_name(issuer));
+ label = simgrid::xbt::string_printf("[(%lu)%s] iSend", issuer->pid, MC_smx_actor_get_host_name(issuer));
else
label = bprintf("[(%lu)] iSend", issuer->pid);
break;
case SIMCALL_COMM_IRECV:
if (issuer->host)
- label = simgrid::xbt::string_printf("[(%lu)%s] iRecv", issuer->pid,
- MC_smx_process_get_host_name(issuer));
+ label = simgrid::xbt::string_printf("[(%lu)%s] iRecv", issuer->pid, MC_smx_actor_get_host_name(issuer));
else
label = simgrid::xbt::string_printf("[(%lu)] iRecv", issuer->pid);
break;
case SIMCALL_COMM_WAIT: {
if (value == -1) {
if (issuer->host)
- label = simgrid::xbt::string_printf("[(%lu)%s] WaitTimeout", issuer->pid,
- MC_smx_process_get_host_name(issuer));
+ label = simgrid::xbt::string_printf("[(%lu)%s] WaitTimeout", issuer->pid, MC_smx_actor_get_host_name(issuer));
else
label = simgrid::xbt::string_printf("[(%lu)] WaitTimeout", issuer->pid);
} else {
static_cast<simgrid::kernel::activity::Comm*>(remote_act)));
simgrid::kernel::activity::Comm* comm = temp_comm.getBuffer();
- smx_actor_t src_proc = mc_model_checker->process().resolveProcess(
- simgrid::mc::remote(comm->src_proc));
- smx_actor_t dst_proc = mc_model_checker->process().resolveProcess(
- simgrid::mc::remote(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));
if (issuer->host)
- label = simgrid::xbt::string_printf("[(%lu)%s] Wait [(%lu)->(%lu)]",
- issuer->pid,
- MC_smx_process_get_host_name(issuer),
- src_proc ? src_proc->pid : 0,
- dst_proc ? dst_proc->pid : 0);
+ label = simgrid::xbt::string_printf("[(%lu)%s] Wait [(%lu)->(%lu)]", issuer->pid,
+ MC_smx_actor_get_host_name(issuer), src_proc ? src_proc->pid : 0,
+ dst_proc ? dst_proc->pid : 0);
else
label = simgrid::xbt::string_printf("[(%lu)] Wait [(%lu)->(%lu)]",
issuer->pid,
simgrid::kernel::activity::Comm* comm = temp_comm.getBuffer();
if (comm->src_proc == nullptr || comm->dst_proc == nullptr) {
if (issuer->host)
- label = simgrid::xbt::string_printf("[(%lu)%s] Test FALSE",
- issuer->pid,
- MC_smx_process_get_host_name(issuer));
+ label = simgrid::xbt::string_printf("[(%lu)%s] Test FALSE", issuer->pid, MC_smx_actor_get_host_name(issuer));
else
label = bprintf("[(%lu)] Test FALSE", issuer->pid);
} else {
if (issuer->host)
- label = simgrid::xbt::string_printf("[(%lu)%s] Test TRUE", issuer->pid,
- MC_smx_process_get_host_name(issuer));
+ label = simgrid::xbt::string_printf("[(%lu)%s] Test TRUE", issuer->pid, MC_smx_actor_get_host_name(issuer));
else
label = simgrid::xbt::string_printf("[(%lu)] Test TRUE", issuer->pid);
}
unsigned long comms_size = read_length(
mc_model_checker->process(), remote(simcall_comm_waitany__get__comms(req)));
if (issuer->host)
- label = simgrid::xbt::string_printf("[(%lu)%s] WaitAny [%d of %lu]",
- issuer->pid,
- MC_smx_process_get_host_name(issuer), value + 1,
- comms_size);
+ label = simgrid::xbt::string_printf("[(%lu)%s] WaitAny [%d of %lu]", issuer->pid,
+ MC_smx_actor_get_host_name(issuer), value + 1, comms_size);
else
label = simgrid::xbt::string_printf("[(%lu)] WaitAny [%d of %lu]",
issuer->pid, value + 1, comms_size);
case SIMCALL_COMM_TESTANY:
if (value == -1) {
if (issuer->host)
- label = simgrid::xbt::string_printf("[(%lu)%s] TestAny FALSE",
- issuer->pid, MC_smx_process_get_host_name(issuer));
+ label = simgrid::xbt::string_printf("[(%lu)%s] TestAny FALSE", issuer->pid, MC_smx_actor_get_host_name(issuer));
else
label = simgrid::xbt::string_printf("[(%lu)] TestAny FALSE", issuer->pid);
} else {
if (issuer->host)
- label = simgrid::xbt::string_printf("[(%lu)%s] TestAny TRUE [%d of %lu]",
- issuer->pid,
- MC_smx_process_get_host_name(issuer), value + 1,
- simcall_comm_testany__get__count(req));
+ label = simgrid::xbt::string_printf("[(%lu)%s] TestAny TRUE [%d of %lu]", issuer->pid,
+ MC_smx_actor_get_host_name(issuer), value + 1,
+ simcall_comm_testany__get__count(req));
else
label = simgrid::xbt::string_printf("[(%lu)] TestAny TRUE [%d of %lu]",
issuer->pid,
case SIMCALL_MC_RANDOM:
if (issuer->host)
- label = simgrid::xbt::string_printf("[(%lu)%s] MC_RANDOM (%d)",
- issuer->pid, MC_smx_process_get_host_name(issuer), value);
+ label = simgrid::xbt::string_printf("[(%lu)%s] MC_RANDOM (%d)", issuer->pid, MC_smx_actor_get_host_name(issuer),
+ value);
else
label = simgrid::xbt::string_printf("[(%lu)] MC_RANDOM (%d)", issuer->pid, value);
break;
*
* This is true if the request associated with the process is ready.
*/
-XBT_PRIVATE bool process_is_enabled(smx_actor_t process);
+XBT_PRIVATE bool actor_is_enabled(smx_actor_t process);
XBT_PRIVATE std::string request_get_dot_output(smx_simcall_t req, int value);
-/* Copyright (c) 2015. The SimGrid Team.
- * All rights reserved. */
+/* Copyright (c) 2015-2017. The SimGrid Team. All rights reserved. */
/* This program is free software; you can redistribute it and/or modify it
* under the terms of the license (GNU LGPL) which comes with this package. */
using simgrid::mc::remote;
-/** HACK, Statically "upcast" a s_smx_actor_t into a SimixProcessInformation
+/** HACK, Statically "upcast" a s_smx_actor_t into a ActorInformation
*
- * This gets 'processInfo' from '&processInfo->copy'. It upcasts in the
- * sense that we could achieve the same thing by having SimixProcessInformation
+ * This gets 'actorInfo' from '&actorInfo->copy'. It upcasts in the
+ * sense that we could achieve the same thing by having ActorInformation
* inherit from s_smx_actor_t but we don't really want to do that.
*/
-static inline
-simgrid::mc::SimixProcessInformation* process_info_cast(smx_actor_t p)
+static inline simgrid::mc::ActorInformation* actor_info_cast(smx_actor_t actor)
{
- simgrid::mc::SimixProcessInformation temp;
+ simgrid::mc::ActorInformation temp;
std::size_t offset = (char*) temp.copy.getBuffer() - (char*)&temp;
- simgrid::mc::SimixProcessInformation* process_info =
- (simgrid::mc::SimixProcessInformation*) ((char*) p - offset);
+ simgrid::mc::ActorInformation* process_info = (simgrid::mc::ActorInformation*)((char*)actor - offset);
return process_info;
}
* @param target Local vector (to be filled with copies of `s_smx_actor_t`)
* @param remote_swag Address of the process SWAG in the remote list
*/
-static void MC_process_refresh_simix_process_list(
- simgrid::mc::Process* process,
- std::vector<simgrid::mc::SimixProcessInformation>& target,
- simgrid::mc::RemotePtr<s_xbt_swag_t> remote_swag)
+static void MC_process_refresh_simix_process_list(simgrid::mc::Process* process,
+ std::vector<simgrid::mc::ActorInformation>& target,
+ simgrid::mc::RemotePtr<s_xbt_swag_t> remote_swag)
{
target.clear();
int i = 0;
for (smx_actor_t p = (smx_actor_t) swag.head; p; ++i) {
- simgrid::mc::SimixProcessInformation info;
+ simgrid::mc::ActorInformation info;
info.address = p;
info.hostname = nullptr;
process->read_bytes(&info.copy, sizeof(info.copy), remote(p));
Remote<simgrid::simix::Global> simix_global =
this->read<simgrid::simix::Global>(simix_global_p);
- MC_process_refresh_simix_process_list(
- this, this->smx_process_infos,
- remote(simix_global.getBuffer()->process_list));
- MC_process_refresh_simix_process_list(
- this, this->smx_old_process_infos,
- remote(simix_global.getBuffer()->process_to_destroy));
+ MC_process_refresh_simix_process_list(this, this->smx_actors_infos, remote(simix_global.getBuffer()->process_list));
+ MC_process_refresh_simix_process_list(this, this->smx_dead_actors_infos,
+ remote(simix_global.getBuffer()->process_to_destroy));
this->cache_flags_ |= Process::cache_simix_processes;
}
/** Get the issuer of a simcall (`req->issuer`)
*
* In split-process mode, it does the black magic necessary to get an address
- * of a (shallow) copy of the data structure the issuer SIMIX process in the local
+ * of a (shallow) copy of the data structure the issuer SIMIX actor in the local
* address space.
*
* @param process the MCed process
auto address = simgrid::mc::remote(req->issuer);
// Lookup by address:
- for (auto& p : mc_model_checker->process().simix_processes())
- if (p.address == address)
- return p.copy.getBuffer();
- for (auto& p : mc_model_checker->process().old_simix_processes())
- if (p.address == address)
- return p.copy.getBuffer();
+ for (auto& actor : mc_model_checker->process().actors())
+ if (actor.address == address)
+ return actor.copy.getBuffer();
+ for (auto& actor : mc_model_checker->process().dead_actors())
+ if (actor.address == address)
+ return actor.copy.getBuffer();
xbt_die("Issuer not found");
}
-const char* MC_smx_process_get_host_name(smx_actor_t p)
+const char* MC_smx_actor_get_host_name(smx_actor_t actor)
{
if (mc_model_checker == nullptr)
- return p->host->cname();
+ return actor->host->cname();
simgrid::mc::Process* process = &mc_model_checker->process();
const size_t offset = (char*) &foo.host.name() - (char*) &foo.host;
// Read the simgrid::xbt::string in the MCed process:
- simgrid::mc::SimixProcessInformation* info = process_info_cast(p);
- auto remote_string_address = remote(
- (simgrid::xbt::string_data*) ((char*) p->host + offset));
+ simgrid::mc::ActorInformation* info = actor_info_cast(actor);
+ auto remote_string_address = remote((simgrid::xbt::string_data*)((char*)actor->host + offset));
simgrid::xbt::string_data remote_string = process->read(remote_string_address);
char hostname[remote_string.len];
process->read_bytes(hostname, remote_string.len + 1, remote(remote_string.data));
return info->hostname;
}
-const char* MC_smx_process_get_name(smx_actor_t p)
+const char* MC_smx_actor_get_name(smx_actor_t actor)
{
simgrid::mc::Process* process = &mc_model_checker->process();
if (mc_model_checker == nullptr)
- return p->name.c_str();
+ return actor->name.c_str();
- simgrid::mc::SimixProcessInformation* info = process_info_cast(p);
+ simgrid::mc::ActorInformation* info = actor_info_cast(actor);
if (info->name.empty()) {
- simgrid::xbt::string_data string_data = (simgrid::xbt::string_data&)p->name;
+ simgrid::xbt::string_data string_data = (simgrid::xbt::string_data&)actor->name;
info->name = process->read_string(remote(string_data.data), string_data.len);
}
return info->name.c_str();
*/
XBT_PRIVATE smx_actor_t MC_smx_simcall_get_issuer(s_smx_simcall_t const* req);
-XBT_PRIVATE const char* MC_smx_process_get_name(smx_actor_t p);
-XBT_PRIVATE const char* MC_smx_process_get_host_name(smx_actor_t p);
+XBT_PRIVATE const char* MC_smx_actor_get_name(smx_actor_t p);
+XBT_PRIVATE const char* MC_smx_actor_get_host_name(smx_actor_t p);
XBT_PRIVATE int MC_smpi_process_count(void);
if (!procstate->isToInterleave())
return nullptr;
- if (!simgrid::mc::process_is_enabled(process))
+ if (!simgrid::mc::actor_is_enabled(process))
return nullptr;
smx_simcall_t req = nullptr;
smx_simcall_t MC_state_get_request(simgrid::mc::State* state)
{
- for (auto& p : mc_model_checker->process().simix_processes()) {
+ for (auto& p : mc_model_checker->process().actors()) {
smx_simcall_t res = MC_state_get_request_for_process(state, p.copy.getBuffer());
if (res)
return res;