#include "src/kernel/activity/MailboxImpl.hpp"
#include "src/kernel/activity/MutexImpl.hpp"
#include "src/mc/Session.hpp"
+#include "src/mc/checker/SimcallInspector.hpp"
#include "src/mc/mc_comm_pattern.hpp"
+#include "src/mc/mc_pattern.hpp"
#include "src/mc/mc_private.hpp"
#include "src/mc/mc_smx.hpp"
#include "src/mc/remote/RemoteSimulation.hpp"
-#include "src/mc/mc_pattern.hpp"
-#include "src/mc/checker/SimcallInspector.hpp"
#include <xbt/asserts.h>
#include <xbt/log.h>
// #include <xbt/dynar.h>
return colors[id % colors.size()];
}
-static char *pointer_to_string(void *pointer)
+static char* pointer_to_string(void* pointer)
{
if (XBT_LOG_ISENABLED(mc_api, xbt_log_priority_verbose))
return bprintf("%p", pointer);
return xbt_strdup("(verbose only)");
}
-static char *buff_size_to_string(size_t buff_size)
+static char* buff_size_to_string(size_t buff_size)
{
if (XBT_LOG_ISENABLED(mc_api, xbt_log_priority_verbose))
return bprintf("%zu", buff_size);
return xbt_strdup("(verbose only)");
}
+inline
+smx_mailbox_t get_mbox(smx_simcall_t const r)
+{
+ switch (r->call_) {
+ case Simcall::COMM_ISEND:
+ return simcall_comm_isend__get__mbox(r);
+ case Simcall::COMM_IRECV:
+ return simcall_comm_irecv__get__mbox(r);
+ default:
+ return nullptr;
+ }
+}
+
+inline simgrid::kernel::activity::CommImpl* get_comm(smx_simcall_t const r)
+{
+ switch (r->call_) {
+ case Simcall::COMM_WAIT:
+ return simcall_comm_wait__getraw__comm(r);
+ case Simcall::COMM_TEST:
+ return simcall_comm_test__getraw__comm(r);
+ default:
+ return nullptr;
+ }
+}
+
+// Does half the job
+inline bool request_depend_asymmetric(smx_simcall_t r1, smx_simcall_t r2)
+{
+ if (r1->call_ == Simcall::COMM_ISEND && r2->call_ == Simcall::COMM_IRECV)
+ return false;
+
+ if (r1->call_ == Simcall::COMM_IRECV && r2->call_ == Simcall::COMM_ISEND)
+ return false;
+
+ // Those are internal requests, we do not need indirection because those objects are copies:
+ const kernel::activity::CommImpl* synchro1 = get_comm(r1);
+ const kernel::activity::CommImpl* synchro2 = get_comm(r2);
+
+ if ((r1->call_ == Simcall::COMM_ISEND || r1->call_ == Simcall::COMM_IRECV) && r2->call_ == Simcall::COMM_WAIT) {
+ const kernel::activity::MailboxImpl* mbox = get_mbox(r1);
+
+ if (mbox != synchro2->mbox_cpy
+ && simcall_comm_wait__get__timeout(r2) <= 0)
+ return false;
+
+ if ((r1->issuer_ != synchro2->src_actor_.get()) && (r1->issuer_ != synchro2->dst_actor_.get()) &&
+ simcall_comm_wait__get__timeout(r2) <= 0)
+ return false;
+
+ if ((r1->call_ == Simcall::COMM_ISEND) && (synchro2->type_ == kernel::activity::CommImpl::Type::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->type_ == kernel::activity::CommImpl::Type::RECEIVE) &&
+ (synchro2->dst_buff_ != simcall_comm_irecv__get__dst_buff(r1)) && simcall_comm_wait__get__timeout(r2) <= 0)
+ return false;
+ }
+
+ /* FIXME: the following rule assumes that the result of the isend/irecv call is not stored in a buffer used in the
+ * test call. */
+#if 0
+ if((r1->call == Simcall::COMM_ISEND || r1->call == Simcall::COMM_IRECV)
+ && r2->call == Simcall::COMM_TEST)
+ return false;
+#endif
+
+ if (r1->call_ == Simcall::COMM_WAIT && (r2->call_ == Simcall::COMM_WAIT || r2->call_ == Simcall::COMM_TEST) &&
+ (synchro1->src_actor_.get() == nullptr || synchro1->dst_actor_.get() == nullptr))
+ return false;
+
+ if (r1->call_ == Simcall::COMM_TEST &&
+ (simcall_comm_test__get__comm(r1) == nullptr || synchro1->src_buff_ == nullptr || synchro1->dst_buff_ == nullptr))
+ return false;
+
+ if (r1->call_ == Simcall::COMM_TEST && r2->call_ == Simcall::COMM_WAIT &&
+ 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->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;
+}
+
/* Search an enabled transition for the given process.
*
* This can be seen as an iterator returning the next transition of the process.
simgrid::mc::ActorState* procstate = &state->actor_states_[actor->get_pid()];
state->transition_.pid_ = -1;
state->transition_.argument_ = -1;
- state->executed_req_.call_ = Simcall::NONE;
+ state->executed_req_.call_ = Simcall::NONE;
if (not simgrid::mc::actor_is_enabled(actor))
return nullptr; // Not executable in the application
return req;
}
-void mc_api::initialize(char** argv)
+void mc_api::initialize(char** argv) const
{
simgrid::mc::session = new simgrid::mc::Session([argv] {
int i = 1;
return mc_model_checker->get_remote_simulation().actors().size();
}
-bool mc_api::comm_addr_equal(const kernel::activity::CommImpl* comm_addr1, const kernel::activity::CommImpl* comm_addr2) const
+bool mc_api::comm_addr_equal(const kernel::activity::CommImpl* comm_addr1,
+ const kernel::activity::CommImpl* comm_addr2) const
{
return remote(comm_addr1) == remote(comm_addr2);
}
kernel::activity::CommImpl* mc_api::get_comm_waitany_raw_addr(smx_simcall_t request, int value) const
{
- auto addr = mc_model_checker->get_remote_simulation().read(remote(simcall_comm_waitany__getraw__comms(request) + value));
+ auto addr =
+ mc_model_checker->get_remote_simulation().read(remote(simcall_comm_waitany__getraw__comms(request) + value));
return static_cast<simgrid::kernel::activity::CommImpl*>(addr);
}
char* remote_name = mc_model_checker->get_remote_simulation().read<char*>(RemotePtr<char*>(
(uint64_t)(synchro->get_mailbox() ? &synchro->get_mailbox()->get_name() : &synchro->mbox_cpy->get_name())));
- auto rdv = mc_model_checker->get_remote_simulation().read_string(RemotePtr<char>(remote_name));
+ auto rdv = mc_model_checker->get_remote_simulation().read_string(RemotePtr<char>(remote_name));
return rdv;
}
Remote<kernel::activity::CommImpl> temp_synchro;
mc_model_checker->get_remote_simulation().read(temp_synchro, remote((simgrid::kernel::activity::CommImpl*)addr));
const kernel::activity::CommImpl* synchro = temp_synchro.get_buffer();
- auto src_proc = mc_model_checker->get_remote_simulation().resolve_actor(mc::remote(synchro->src_actor_.get()))->get_pid();
+ auto src_proc =
+ mc_model_checker->get_remote_simulation().resolve_actor(mc::remote(synchro->src_actor_.get()))->get_pid();
return src_proc;
}
Remote<kernel::activity::CommImpl> temp_synchro;
mc_model_checker->get_remote_simulation().read(temp_synchro, remote((simgrid::kernel::activity::CommImpl*)addr));
const kernel::activity::CommImpl* synchro = temp_synchro.get_buffer();
- auto src_proc = mc_model_checker->get_remote_simulation().resolve_actor(mc::remote(synchro->dst_actor_.get()))->get_pid();
+ auto src_proc =
+ mc_model_checker->get_remote_simulation().resolve_actor(mc::remote(synchro->dst_actor_.get()))->get_pid();
return src_proc;
}
mc_model_checker->get_remote_simulation().read(temp_synchro, remote((simgrid::kernel::activity::CommImpl*)addr));
const kernel::activity::CommImpl* synchro = temp_synchro.get_buffer();
- std::vector<char> buffer {};
+ std::vector<char> buffer{};
if (synchro->src_buff_ != nullptr) {
buffer.resize(synchro->src_buff_size_);
- mc_model_checker->get_remote_simulation().read_bytes(buffer.data(), buffer.size(),
- remote(synchro->src_buff_));
+ mc_model_checker->get_remote_simulation().read_bytes(buffer.data(), buffer.size(), remote(synchro->src_buff_));
}
return buffer;
}
simgrid::mc::Remote<simgrid::kernel::activity::CommImpl> temp_comm;
mc_model_checker->get_remote_simulation().read(temp_comm, remote((kernel::activity::CommImpl*)comm_addr));
const simgrid::kernel::activity::CommImpl* comm = temp_comm.get_buffer();
-
- std::vector<char> buffer {};
+
+ std::vector<char> buffer{};
if (comm->src_buff_ != nullptr) {
buffer.resize(comm->src_buff_size_);
- mc_model_checker->get_remote_simulation().read_bytes(buffer.data(), buffer.size(),
- remote(comm->src_buff_));
+ mc_model_checker->get_remote_simulation().read_bytes(buffer.data(), buffer.size(), remote(comm->src_buff_));
}
return buffer;
}
session->initialize();
}
-ModelChecker* mc_api::get_model_checker() const
-{
- return mc_model_checker;
-}
-
void mc_api::mc_inc_visited_states() const
{
mc_model_checker->visited_states++;
return MC_smx_simcall_get_issuer(req);
}
+long mc_api::simcall_get_actor_id(s_smx_simcall const* req) const
+{
+ return MC_smx_simcall_get_issuer(req)->get_pid();
+}
+
+smx_mailbox_t mc_api::simcall_get_mbox(smx_simcall_t const req) const
+{
+ return get_mbox(req);
+}
+
+simgrid::kernel::activity::CommImpl* mc_api::simcall_get_comm(smx_simcall_t const req) const
+{
+ return get_comm(req);
+}
+
bool mc_api::mc_is_null() const
{
auto is_null = (mc_model_checker == nullptr) ? true : false;
return nullptr;
}
-bool mc_api::request_depend(smx_simcall_t req1, smx_simcall_t req2) const
+bool mc_api::simcall_check_dependency(smx_simcall_t const req1, smx_simcall_t const req2) const
{
- return simgrid::mc::request_depend(req1, req2);
+ if (req1->issuer_ == req2->issuer_)
+ return false;
+
+ /* Wait with timeout transitions are not considered by the independence theorem, thus we consider them as dependent with all other transitions */
+ if ((req1->call_ == Simcall::COMM_WAIT && simcall_comm_wait__get__timeout(req1) > 0) ||
+ (req2->call_ == Simcall::COMM_WAIT && simcall_comm_wait__get__timeout(req2) > 0))
+ return true;
+
+ if (req1->call_ != req2->call_)
+ return request_depend_asymmetric(req1, req2) && request_depend_asymmetric(req2, req1);
+
+ // Those are internal requests, we do not need indirection because those objects are copies:
+ const kernel::activity::CommImpl* synchro1 = get_comm(req1);
+ const kernel::activity::CommImpl* synchro2 = get_comm(req2);
+
+ switch (req1->call_) {
+ case Simcall::COMM_ISEND:
+ return simcall_comm_isend__get__mbox(req1) == simcall_comm_isend__get__mbox(req2);
+ case Simcall::COMM_IRECV:
+ return simcall_comm_irecv__get__mbox(req1) == simcall_comm_irecv__get__mbox(req2);
+ case Simcall::COMM_WAIT:
+ if (synchro1->src_buff_ == synchro2->src_buff_ && synchro1->dst_buff_ == synchro2->dst_buff_)
+ return false;
+ 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;
+ return true;
+ default:
+ return true;
+ }
}
std::string mc_api::request_to_string(smx_simcall_t req, int value, RequestType request_type) const
return req->inspector_->to_string();
bool use_remote_comm = true;
- switch(request_type) {
- case simgrid::mc::RequestType::simix:
- use_remote_comm = true;
- break;
- case simgrid::mc::RequestType::executed:
- case simgrid::mc::RequestType::internal:
- use_remote_comm = false;
- break;
- default:
- THROW_IMPOSSIBLE;
+ switch (request_type) {
+ case simgrid::mc::RequestType::simix:
+ use_remote_comm = true;
+ break;
+ case simgrid::mc::RequestType::executed:
+ case simgrid::mc::RequestType::internal:
+ use_remote_comm = false;
+ break;
+ default:
+ THROW_IMPOSSIBLE;
}
const char* type = nullptr;
- char *args = nullptr;
+ char* args = nullptr;
smx_actor_t issuer = MC_smx_simcall_get_issuer(req);
mc_model_checker->get_remote_simulation().resolve_actor(simgrid::mc::remote(act->src_actor_.get()));
smx_actor_t dst_proc =
mc_model_checker->get_remote_simulation().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,
+ 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) : "", dst_proc ? dst_proc->get_pid() : 0,
dst_proc ? MC_smx_actor_get_host_name(dst_proc) : "",
mc_model_checker->get_remote_simulation().resolve_actor(simgrid::mc::remote(act->src_actor_.get()));
smx_actor_t dst_proc =
mc_model_checker->get_remote_simulation().resolve_actor(simgrid::mc::remote(act->dst_actor_.get()));
- args = bprintf("comm=%s [(%ld)%s (%s) -> (%ld)%s (%s)]", p, src_proc->get_pid(),
+ 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));
}
simgrid::kernel::activity::CommImpl* remote_sync;
remote_sync =
mc_model_checker->get_remote_simulation().read(remote(simcall_comm_waitany__get__comms(req) + value));
- char* p = pointer_to_string(remote_sync);
- args = bprintf("comm=%s (%d of %zu)", p, value + 1, count);
+ char* p = pointer_to_string(remote_sync);
+ args = bprintf("comm=%s (%d of %zu)", p, value + 1, count);
xbt_free(p);
} else
args = bprintf("comm at idx %d", value);
str = simgrid::xbt::string_printf("[(%ld)%s (%s)] %s ", issuer->get_pid(), MC_smx_actor_get_host_name(issuer),
MC_smx_actor_get_name(issuer), type);
xbt_free(args);
- return str;
+ return str;
}
std::string mc_api::request_get_dot_output(smx_simcall_t req, int value) const
THROW_UNIMPLEMENTED;
}
- return xbt::string_printf("label = \"%s\", color = %s, fontcolor = %s", label.c_str(), color, color);
+ return xbt::string_printf("label = \"%s\", color = %s, fontcolor = %s", label.c_str(), color, color);
}
const char* mc_api::simcall_get_name(simgrid::simix::Simcall kind) const
}
#if SIMGRID_HAVE_MC
-void mc_api::automaton_load(const char *file) const
-{
- MC_automaton_load(file);
+void mc_api::automaton_load(const char* file) const
+{
+ MC_automaton_load(file);
}
#endif
-std::vector<int> mc_api::automaton_propositional_symbol_evaluate() const
+std::vector<int> mc_api::automaton_propositional_symbol_evaluate() const
{
unsigned int cursor = 0;
- std::vector<int> values;
+ std::vector<int> values;
xbt_automaton_propositional_symbol_t ps = nullptr;
xbt_dynar_foreach (mc::property_automaton->propositional_symbols, cursor, ps)
values.push_back(xbt_automaton_propositional_symbol_evaluate(ps));
int mc_api::compare_automaton_exp_label(const xbt_automaton_exp_label* l) const
{
- unsigned int cursor = 0;
+ unsigned int cursor = 0;
xbt_automaton_propositional_symbol_t p = nullptr;
xbt_dynar_foreach (simgrid::mc::property_automaton->propositional_symbols, cursor, p) {
if (std::strcmp(xbt_automaton_propositional_symbol_get_name(p), l->u.predicat) == 0)
xbt_automaton_exp_label_t mc_api::get_automaton_transition_label(xbt_dynar_t const& dynar, int index) const
{
- const xbt_automaton_transition* transition =
- xbt_dynar_get_as(dynar, index, xbt_automaton_transition_t);
+ const xbt_automaton_transition* transition = xbt_dynar_get_as(dynar, index, xbt_automaton_transition_t);
return transition->label;
}
xbt_automaton_state_t mc_api::get_automaton_transition_dst(xbt_dynar_t const& dynar, int index) const
{
- const xbt_automaton_transition* transition =
- xbt_dynar_get_as(dynar, index, xbt_automaton_transition_t);
+ const xbt_automaton_transition* transition = xbt_dynar_get_as(dynar, index, xbt_automaton_transition_t);
return transition->dst;
}