From 63834b5431ab8aadc3373b34be3a4ea0491fad5d Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Sun, 28 Feb 2021 10:40:40 +0100 Subject: [PATCH] objectification of MC simcall achieved -- many tests still failing * MC_RANDOM is now a regular simcall, made observable by its SimcallInspector - remove it from simcall.in and remove all relevant elements - Other simcalls that are visible from MC (ie, that are generated by simcall.py and are handled in MC with big switch cases) are not modified at all, even if the patch reindent them since this execution path is now in a new conditionnal. * SimcallInspectors are used everywhere where a specific handling was made for MC_RANDOM - In MC_state_choose_request_for_process, we get the next value to be picked by MC_random (or the next comm to be picked by waitany) depending on the amount of times we consider this simcall (ie, on the amount of decision forks we did on that transition while exploring the state space. This operation was not named before, it's now called is_pending() because it returns whether we should do another decision fork from that transition. Maybe is_branching() would be a better name. Or consider() since its parameter is times_considered, and there is one call location where its return value is ignored (when we replay all transitions on the path leading to the state we want to restore). But there is already a mc::ActorState::consider() where the Checker express interest in a given simcall. - The two other generic methods of SimcallInspectors are to_string() to get a textual representation of the transtion (eg to display the backtrace leading to the property violation), and dot_label() to get a label that can be used in dot(1). This is useful to get a visual representation of the state space. - There is a visible() method too, but I guess it's useless: Only visible simcall will be given an inspector. Or it will be more complex, because differing model checking algorithms will be interested in differing sets of simcalls (so visible() should be Checker-dependend). Leave it as is for now. - RandomSimcall is also implementing a get_value() method that allows its implementation. At the end of the day, the connexion between the actor side (out of the kernel) and the model-checker side is made with this code: auto observer = new simgrid::mc::RandomSimcall(SIMIX_process_self(), min, max); return simgrid::kernel::actor::simcall([observer] { return observer->get_value(); }, observer); The RandomSimcall object is really making the link between the two worlds. - When we will convert the other simcalls, something will be needed to handle transition dependency. Since MC_RANDOM is never dependent with anything, this is left unhandled in SimcallInspector for now. One problem at a time. * SimcallInspectors live in the AppSide while these information are needed in the ModelChecker side. So the network protocol was extended to allow the Modelchecker to get this information thru RPC. This is not satisfactory because it probably slows things down, even if it's hard to say for sure because many tests just deadlock with it. When the AppSide is dead, you'd better not ask for a RPC to collect information about the simcalls that lead to the issue. I extended the State::Transition object (that is used to both replay a trace leading to a state I want to restore and to display the backtrace that lead to a violation) to include the textual representation of the transitions, to not do a RPC to the dead application on violation. But when the application abort(), I seem to have a stack corruption on the app side or something. And debugging the verified application is made very difficult by the Dwarf inspector that prevents the verification from starting if the subprocess is not compiled in one segment only (valgrind violates this rule). Plus valgrind has a subprocess itself, probably defeating the checkpoint/restore mechanism. Maybe I should try the Sanitizers. * A better approach (if we fail to fix the curreny design) could be to pre-compute on AppSide all information that can be extracted from the inspectors, and copy it over to the CheckerSide once per scheduling round. That would speed things up, and ensure that there is no RPC after the death of the application. That should be done in place of MC_process_refresh_simix_actor_dynar() that copies some (less useful) information over. --- src/mc/ModelChecker.cpp | 97 ++- src/mc/ModelChecker.hpp | 6 + src/mc/Transition.hpp | 5 +- src/mc/api.cpp | 586 +++++++++--------- .../CommunicationDeterminismChecker.cpp | 6 +- src/mc/checker/LivenessChecker.cpp | 6 +- src/mc/checker/SafetyChecker.cpp | 16 +- src/mc/checker/SimcallInspector.hpp | 39 +- src/mc/mc_base.cpp | 20 +- src/mc/mc_record.cpp | 10 +- src/mc/remote/AppSide.cpp | 59 ++ src/mc/remote/mc_protocol.h | 36 +- src/simix/libsmx.cpp | 9 +- src/simix/popping_accessors.hpp | 38 -- src/simix/popping_bodies.cpp | 7 - src/simix/popping_enum.hpp | 3 +- src/simix/popping_generated.cpp | 11 +- src/simix/simcalls.in | 2 +- src/simix/simcalls.py | 9 +- teshsuite/mc/random-bug/random-bug.cpp | 1 + tools/cmake/DefinePackages.cmake | 1 + 21 files changed, 566 insertions(+), 401 deletions(-) diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp index f7859f4495..84e6a8dedc 100644 --- a/src/mc/ModelChecker.cpp +++ b/src/mc/ModelChecker.cpp @@ -309,12 +309,107 @@ void ModelChecker::handle_simcall(Transition const& transition) memset(&m, 0, sizeof(m)); m.type = MessageType::SIMCALL_HANDLE; m.pid = transition.pid_; - m.value = transition.argument_; + m.value = transition.times_considered_; checker_side_.get_channel().send(m); this->remote_simulation_->clear_cache(); if (this->remote_simulation_->running()) checker_side_.dispatch(); } +bool ModelChecker::simcall_is_pending(int aid, int times_considered) +{ + s_mc_message_simcall_is_pending_t m; + memset(&m, 0, sizeof(m)); + m.type = MessageType::SIMCALL_IS_PENDING; + m.aid = aid; + m.time_considered = times_considered; + checker_side_.get_channel().send(m); + + s_mc_message_simcall_is_pending_answer_t answer; + ssize_t s = checker_side_.get_channel().receive(answer); + xbt_assert(s != -1, "Could not receive message"); + xbt_assert(s == sizeof(answer) && answer.type == MessageType::SIMCALL_IS_PENDING_ANSWER, + "Received unexpected message %s (%i, size=%i) " + "expected MessageType::SIMCALL_IS_PENDING_ANSWER (%i, size=%i)", + to_c_str(answer.type), (int)answer.type, (int)s, (int)MessageType::SIMCALL_IS_PENDING_ANSWER, + (int)sizeof(answer)); + + XBT_DEBUG("is_pending(%d, %d) is returning %s", aid, times_considered, answer.value ? "true" : "false"); + + this->remote_simulation_->clear_cache(); + return answer.value; +} +bool ModelChecker::simcall_is_visible(int aid) +{ + xbt_assert(mc_model_checker != nullptr, "This should be called from the checker side"); + + s_mc_message_simcall_is_visible_t m; + memset(&m, 0, sizeof(m)); + m.type = MessageType::SIMCALL_IS_VISIBLE; + m.aid = aid; + checker_side_.get_channel().send(m); + + s_mc_message_simcall_is_visible_answer_t answer; + ssize_t s = checker_side_.get_channel().receive(answer); + xbt_assert(s != -1, "Could not receive message"); + xbt_assert(s == sizeof(answer) && answer.type == MessageType::SIMCALL_IS_VISIBLE_ANSWER, + "Received unexpected message %s (%i, size=%i) " + "expected MessageType::SIMCALL_IS_VISIBLE_ANSWER (%i, size=%i)", + to_c_str(answer.type), (int)answer.type, (int)s, (int)MessageType::SIMCALL_IS_VISIBLE_ANSWER, + (int)sizeof(answer)); + + XBT_DEBUG("is_visible(%d) is returning %s", aid, answer.value ? "true" : "false"); + + this->remote_simulation_->clear_cache(); + return answer.value; +} +std::string ModelChecker::simcall_to_string(int aid, int times_considered) +{ + xbt_assert(mc_model_checker != nullptr, "This should be called from the checker side"); + + s_mc_message_simcall_to_string_t m; + memset(&m, 0, sizeof(m)); + m.type = MessageType::SIMCALL_TO_STRING; + m.aid = aid; + m.time_considered = times_considered; + checker_side_.get_channel().send(m); + + s_mc_message_simcall_to_string_answer_t answer; + ssize_t s = checker_side_.get_channel().receive(answer); + xbt_assert(s != -1, "Could not receive message"); + xbt_assert(s == sizeof(answer) && answer.type == MessageType::SIMCALL_TO_STRING_ANSWER, + "Received unexpected message %s (%i, size=%i) " + "expected MessageType::SIMCALL_TO_STRING_ANSWER (%i, size=%i)", + to_c_str(answer.type), (int)answer.type, (int)s, (int)MessageType::SIMCALL_TO_STRING_ANSWER, + (int)sizeof(answer)); + + XBT_DEBUG("to_string(%d) is returning %s", aid, answer.value); + + return std::string(answer.value); +} +std::string ModelChecker::simcall_dot_label(int aid, int times_considered) +{ + xbt_assert(mc_model_checker != nullptr, "This should be called from the checker side"); + + s_mc_message_simcall_to_string_t m; + memset(&m, 0, sizeof(m)); + m.type = MessageType::SIMCALL_DOT_LABEL; + m.aid = aid; + m.time_considered = times_considered; + checker_side_.get_channel().send(m); + + s_mc_message_simcall_to_string_answer_t answer; + ssize_t s = checker_side_.get_channel().receive(answer); + xbt_assert(s != -1, "Could not receive message"); + xbt_assert(s == sizeof(answer) && answer.type == MessageType::SIMCALL_TO_STRING_ANSWER, + "Received unexpected message %s (%i, size=%i) " + "expected MessageType::SIMCALL_TO_STRING_ANSWER (%i, size=%i)", + to_c_str(answer.type), (int)answer.type, (int)s, (int)MessageType::SIMCALL_TO_STRING_ANSWER, + (int)sizeof(answer)); + + XBT_DEBUG("dot_label(%d) is returning %s", aid, answer.value); + + return std::string(answer.value); +} bool ModelChecker::checkDeadlock() { diff --git a/src/mc/ModelChecker.hpp b/src/mc/ModelChecker.hpp index cacf530f9b..434609c4c4 100644 --- a/src/mc/ModelChecker.hpp +++ b/src/mc/ModelChecker.hpp @@ -51,6 +51,12 @@ public: void wait_for_requests(); void handle_simcall(Transition const& transition); + /* Interactions with the simcall observer */ + bool simcall_is_pending(int aid, int times_considered); + bool simcall_is_visible(int aid); + std::string simcall_to_string(int aid, int times_considered); + std::string simcall_dot_label(int aid, int times_considered); + XBT_ATTRIB_NORETURN void exit(int status); bool checkDeadlock(); diff --git a/src/mc/Transition.hpp b/src/mc/Transition.hpp index 2527d8c7be..6b616cdfe4 100644 --- a/src/mc/Transition.hpp +++ b/src/mc/Transition.hpp @@ -30,7 +30,10 @@ public: * * * random can produce different values. */ - int argument_ = 0; + int times_considered_ = 0; + + /* Textual representation of the transition, to display backtraces */ + char textual[200]; }; } // namespace mc diff --git a/src/mc/api.cpp b/src/mc/api.cpp index c510c3746d..2ced4afb0e 100644 --- a/src/mc/api.cpp +++ b/src/mc/api.cpp @@ -66,86 +66,86 @@ static inline smx_simcall_t MC_state_choose_request_for_process(simgrid::mc::Sta /* reset the outgoing transition */ simgrid::mc::ActorState* procstate = &state->actor_states_[actor->get_pid()]; state->transition_.pid_ = -1; - state->transition_.argument_ = -1; + state->transition_.times_considered_ = -1; + state->transition_.textual[0] = '\0'; state->executed_req_.call_ = Simcall::NONE; if (not simgrid::mc::actor_is_enabled(actor)) return nullptr; // Not executable in the application smx_simcall_t req = nullptr; - switch (actor->simcall_.call_) { - case Simcall::COMM_WAITANY: - state->transition_.argument_ = -1; - while (procstate->times_considered < simcall_comm_waitany__get__count(&actor->simcall_)) { - if (simgrid::mc::request_is_enabled_by_idx(&actor->simcall_, procstate->times_considered)) { - state->transition_.argument_ = procstate->times_considered; + if (actor->simcall_.inspector_ != nullptr) { + bool pending = mc_model_checker->simcall_is_pending(actor->get_pid(), procstate->times_considered); + + ++procstate->times_considered; + state->transition_.times_considered_ = procstate->times_considered; + if (not pending) + procstate->set_done(); + req = &actor->simcall_; + } else + switch (actor->simcall_.call_) { + case Simcall::COMM_WAITANY: + state->transition_.times_considered_ = -1; + while (procstate->times_considered < simcall_comm_waitany__get__count(&actor->simcall_)) { + if (simgrid::mc::request_is_enabled_by_idx(&actor->simcall_, procstate->times_considered)) { + state->transition_.times_considered_ = procstate->times_considered; + ++procstate->times_considered; + break; + } ++procstate->times_considered; - break; } - ++procstate->times_considered; - } - if (procstate->times_considered >= simcall_comm_waitany__get__count(&actor->simcall_)) - procstate->set_done(); - if (state->transition_.argument_ != -1) - req = &actor->simcall_; - break; + if (procstate->times_considered >= simcall_comm_waitany__get__count(&actor->simcall_)) + procstate->set_done(); + if (state->transition_.times_considered_ != -1) + req = &actor->simcall_; + break; - case Simcall::COMM_TESTANY: { - unsigned start_count = procstate->times_considered; - state->transition_.argument_ = -1; - while (procstate->times_considered < simcall_comm_testany__get__count(&actor->simcall_)) { - if (simgrid::mc::request_is_enabled_by_idx(&actor->simcall_, procstate->times_considered)) { - state->transition_.argument_ = procstate->times_considered; + case Simcall::COMM_TESTANY: { + unsigned start_count = procstate->times_considered; + state->transition_.times_considered_ = -1; + while (procstate->times_considered < simcall_comm_testany__get__count(&actor->simcall_)) { + if (simgrid::mc::request_is_enabled_by_idx(&actor->simcall_, procstate->times_considered)) { + state->transition_.times_considered_ = procstate->times_considered; + ++procstate->times_considered; + break; + } ++procstate->times_considered; - break; } - ++procstate->times_considered; - } - if (procstate->times_considered >= simcall_comm_testany__get__count(&actor->simcall_)) - procstate->set_done(); + if (procstate->times_considered >= simcall_comm_testany__get__count(&actor->simcall_)) + procstate->set_done(); - if (state->transition_.argument_ != -1 || start_count == 0) - req = &actor->simcall_; + if (state->transition_.times_considered_ != -1 || start_count == 0) + req = &actor->simcall_; - break; - } + break; + } - case Simcall::COMM_WAIT: { - simgrid::mc::RemotePtr remote_act = - remote(simcall_comm_wait__getraw__comm(&actor->simcall_)); - simgrid::mc::Remote temp_act; - mc_model_checker->get_remote_simulation().read(temp_act, remote_act); - const simgrid::kernel::activity::CommImpl* act = temp_act.get_buffer(); - if (act->src_actor_.get() && act->dst_actor_.get()) - state->transition_.argument_ = 0; // OK - else if (act->src_actor_.get() == nullptr && act->state_ == simgrid::kernel::activity::State::READY && - act->detached()) - state->transition_.argument_ = 0; // OK - else - state->transition_.argument_ = -1; // timeout - procstate->set_done(); - req = &actor->simcall_; - break; - } + case Simcall::COMM_WAIT: { + simgrid::mc::RemotePtr remote_act = + remote(simcall_comm_wait__getraw__comm(&actor->simcall_)); + simgrid::mc::Remote temp_act; + mc_model_checker->get_remote_simulation().read(temp_act, remote_act); + const simgrid::kernel::activity::CommImpl* act = temp_act.get_buffer(); + if (act->src_actor_.get() && act->dst_actor_.get()) + state->transition_.times_considered_ = 0; // OK + else if (act->src_actor_.get() == nullptr && act->state_ == simgrid::kernel::activity::State::READY && + act->detached()) + state->transition_.times_considered_ = 0; // OK + else + state->transition_.times_considered_ = -1; // timeout + procstate->set_done(); + req = &actor->simcall_; + break; + } - case Simcall::MC_RANDOM: { - int min_value = simcall_mc_random__get__min(&actor->simcall_); - state->transition_.argument_ = procstate->times_considered + min_value; - procstate->times_considered++; - if (state->transition_.argument_ == simcall_mc_random__get__max(&actor->simcall_)) + default: procstate->set_done(); - req = &actor->simcall_; - break; + state->transition_.times_considered_ = 0; + req = &actor->simcall_; + break; } - - default: - procstate->set_done(); - state->transition_.argument_ = 0; - req = &actor->simcall_; - break; - } if (not req) return nullptr; @@ -161,7 +161,7 @@ static inline smx_simcall_t MC_state_choose_request_for_process(simgrid::mc::Sta state->internal_req_.call_ = Simcall::COMM_WAIT; simgrid::kernel::activity::CommImpl* remote_comm; remote_comm = mc_model_checker->get_remote_simulation().read( - remote(simcall_comm_waitany__get__comms(req) + state->transition_.argument_)); + remote(simcall_comm_waitany__get__comms(req) + state->transition_.times_considered_)); mc_model_checker->get_remote_simulation().read(state->internal_comm_, remote(remote_comm)); simcall_comm_wait__set__comm(&state->internal_req_, state->internal_comm_.get_buffer()); simcall_comm_wait__set__timeout(&state->internal_req_, 0); @@ -171,14 +171,14 @@ static inline smx_simcall_t MC_state_choose_request_for_process(simgrid::mc::Sta case Simcall::COMM_TESTANY: state->internal_req_.call_ = Simcall::COMM_TEST; - if (state->transition_.argument_ > 0) { + if (state->transition_.times_considered_ > 0) { simgrid::kernel::activity::CommImpl* remote_comm = mc_model_checker->get_remote_simulation().read( - remote(simcall_comm_testany__get__comms(req) + state->transition_.argument_)); + remote(simcall_comm_testany__get__comms(req) + state->transition_.times_considered_)); mc_model_checker->get_remote_simulation().read(state->internal_comm_, remote(remote_comm)); } simcall_comm_test__set__comm(&state->internal_req_, state->internal_comm_.get_buffer()); - simcall_comm_test__set__result(&state->internal_req_, state->transition_.argument_); + simcall_comm_test__set__result(&state->internal_req_, state->transition_.times_considered_); break; case Simcall::COMM_WAIT: @@ -707,9 +707,6 @@ std::string Api::request_to_string(smx_simcall_t req, int value, RequestType req { xbt_assert(mc_model_checker != nullptr, "Must be called from MCer"); - if (req->inspector_ != nullptr) - return req->inspector_->to_string(); - bool use_remote_comm = true; switch (request_type) { case simgrid::mc::RequestType::simix: @@ -728,51 +725,78 @@ std::string Api::request_to_string(smx_simcall_t req, int value, RequestType req smx_actor_t issuer = simcall_get_issuer(req); - switch (req->call_) { - case Simcall::COMM_ISEND: { - type = "iSend"; - 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->get_host()) - args = bprintf("src=(%ld)%s (%s), buff=%s, size=%s", issuer->get_pid(), actor_get_host_name(issuer), - actor_get_name(issuer), p, bs); - else - args = bprintf("src=(%ld)%s, buff=%s, size=%s", issuer->get_pid(), actor_get_name(issuer), p, bs); - xbt_free(bs); - xbt_free(p); - break; - } + if (issuer->simcall_.inspector_ != nullptr) { + return mc_model_checker->simcall_to_string(issuer->get_pid(), value); - case Simcall::COMM_IRECV: { - size_t* remote_size = simcall_comm_irecv__get__dst_buff_size(req); - size_t size = 0; - if (remote_size) - mc_model_checker->get_remote_simulation().read_bytes(&size, sizeof(size), remote(remote_size)); - - type = "iRecv"; - char* p = pointer_to_string(simcall_comm_irecv__get__dst_buff(req)); - char* bs = buff_size_to_string(size); - if (issuer->get_host()) - args = bprintf("dst=(%ld)%s (%s), buff=%s, size=%s", issuer->get_pid(), actor_get_host_name(issuer), - actor_get_name(issuer), p, bs); - else - args = bprintf("dst=(%ld)%s, buff=%s, size=%s", issuer->get_pid(), actor_get_name(issuer), p, bs); - xbt_free(bs); - xbt_free(p); - break; - } + } else + switch (req->call_) { + case Simcall::COMM_ISEND: { + type = "iSend"; + 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->get_host()) + args = bprintf("src=(%ld)%s (%s), buff=%s, size=%s", issuer->get_pid(), actor_get_host_name(issuer), + actor_get_name(issuer), p, bs); + else + args = bprintf("src=(%ld)%s, buff=%s, size=%s", issuer->get_pid(), actor_get_name(issuer), p, bs); + xbt_free(bs); + xbt_free(p); + break; + } - case Simcall::COMM_WAIT: { - simgrid::kernel::activity::CommImpl* remote_act = simcall_comm_wait__getraw__comm(req); - char* p; - if (value == -1) { - type = "WaitTimeout"; - p = pointer_to_string(remote_act); - args = bprintf("comm=%s", p); - } else { - type = "Wait"; - p = pointer_to_string(remote_act); + case Simcall::COMM_IRECV: { + size_t* remote_size = simcall_comm_irecv__get__dst_buff_size(req); + size_t size = 0; + if (remote_size) + mc_model_checker->get_remote_simulation().read_bytes(&size, sizeof(size), remote(remote_size)); + + type = "iRecv"; + char* p = pointer_to_string(simcall_comm_irecv__get__dst_buff(req)); + char* bs = buff_size_to_string(size); + if (issuer->get_host()) + args = bprintf("dst=(%ld)%s (%s), buff=%s, size=%s", issuer->get_pid(), actor_get_host_name(issuer), + actor_get_name(issuer), p, bs); + else + args = bprintf("dst=(%ld)%s, buff=%s, size=%s", issuer->get_pid(), actor_get_name(issuer), p, bs); + xbt_free(bs); + xbt_free(p); + break; + } + case Simcall::COMM_WAIT: { + simgrid::kernel::activity::CommImpl* remote_act = simcall_comm_wait__getraw__comm(req); + char* p; + if (value == -1) { + type = "WaitTimeout"; + p = pointer_to_string(remote_act); + args = bprintf("comm=%s", p); + } else { + type = "Wait"; + p = pointer_to_string(remote_act); + + simgrid::mc::Remote temp_synchro; + const simgrid::kernel::activity::CommImpl* act; + if (use_remote_comm) { + mc_model_checker->get_remote_simulation().read(temp_synchro, remote(remote_act)); + act = temp_synchro.get_buffer(); + } else + act = remote_act; + + smx_actor_t src_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 ? src_proc->get_pid() : 0, + src_proc ? actor_get_host_name(src_proc) : "", src_proc ? actor_get_name(src_proc) : "", + dst_proc ? dst_proc->get_pid() : 0, dst_proc ? actor_get_host_name(dst_proc) : "", + dst_proc ? actor_get_name(dst_proc) : ""); + } + xbt_free(p); + break; + } + + case Simcall::COMM_TEST: { + simgrid::kernel::activity::CommImpl* remote_act = simcall_comm_test__getraw__comm(req); simgrid::mc::Remote temp_synchro; const simgrid::kernel::activity::CommImpl* act; if (use_remote_comm) { @@ -781,108 +805,79 @@ std::string Api::request_to_string(smx_simcall_t req, int value, RequestType req } else act = remote_act; - smx_actor_t src_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 ? src_proc->get_pid() : 0, - src_proc ? actor_get_host_name(src_proc) : "", - src_proc ? actor_get_name(src_proc) : "", dst_proc ? dst_proc->get_pid() : 0, - dst_proc ? actor_get_host_name(dst_proc) : "", - dst_proc ? actor_get_name(dst_proc) : ""); + char* p; + if (act->src_actor_.get() == nullptr || act->dst_actor_.get() == nullptr) { + type = "Test FALSE"; + p = pointer_to_string(remote_act); + args = bprintf("comm=%s", p); + } else { + type = "Test TRUE"; + p = pointer_to_string(remote_act); + + smx_actor_t src_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(), actor_get_name(src_proc), + actor_get_host_name(src_proc), dst_proc->get_pid(), actor_get_name(dst_proc), + actor_get_host_name(dst_proc)); + } + xbt_free(p); + break; } - xbt_free(p); - break; - } - case Simcall::COMM_TEST: { - simgrid::kernel::activity::CommImpl* remote_act = simcall_comm_test__getraw__comm(req); - simgrid::mc::Remote temp_synchro; - const simgrid::kernel::activity::CommImpl* act; - if (use_remote_comm) { - mc_model_checker->get_remote_simulation().read(temp_synchro, remote(remote_act)); - act = temp_synchro.get_buffer(); - } else - act = remote_act; - - char* p; - if (act->src_actor_.get() == nullptr || act->dst_actor_.get() == nullptr) { - type = "Test FALSE"; - p = pointer_to_string(remote_act); - args = bprintf("comm=%s", p); - } else { - type = "Test TRUE"; - p = pointer_to_string(remote_act); - - smx_actor_t src_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(), - actor_get_name(src_proc), actor_get_host_name(src_proc), dst_proc->get_pid(), - actor_get_name(dst_proc), actor_get_host_name(dst_proc)); + case Simcall::COMM_WAITANY: { + type = "WaitAny"; + size_t count = simcall_comm_waitany__get__count(req); + if (count > 0) { + 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); + xbt_free(p); + } else + args = bprintf("comm at idx %d", value); + break; } - xbt_free(p); - break; - } - case Simcall::COMM_WAITANY: { - type = "WaitAny"; - size_t count = simcall_comm_waitany__get__count(req); - if (count > 0) { - 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); - xbt_free(p); - } else - args = bprintf("comm at idx %d", value); - break; - } + case Simcall::COMM_TESTANY: + if (value == -1) { + type = "TestAny FALSE"; + args = xbt_strdup("-"); + } else { + type = "TestAny"; + args = bprintf("(%d of %zu)", value + 1, simcall_comm_testany__get__count(req)); + } + break; - case Simcall::COMM_TESTANY: - if (value == -1) { - type = "TestAny FALSE"; - args = xbt_strdup("-"); - } else { - type = "TestAny"; - args = bprintf("(%d of %zu)", value + 1, simcall_comm_testany__get__count(req)); + case Simcall::MUTEX_TRYLOCK: + case Simcall::MUTEX_LOCK: { + if (req->call_ == Simcall::MUTEX_LOCK) + type = "Mutex LOCK"; + else + type = "Mutex TRYLOCK"; + + simgrid::mc::Remote mutex; + mc_model_checker->get_remote_simulation().read_bytes(mutex.get_buffer(), sizeof(mutex), + remote(req->call_ == Simcall::MUTEX_LOCK + ? simcall_mutex_lock__get__mutex(req) + : simcall_mutex_trylock__get__mutex(req))); + args = bprintf("locked = %d, owner = %d, sleeping = n/a", mutex.get_buffer()->is_locked(), + mutex.get_buffer()->get_owner() != nullptr + ? (int)mc_model_checker->get_remote_simulation() + .resolve_actor(simgrid::mc::remote(mutex.get_buffer()->get_owner())) + ->get_pid() + : -1); + break; } - break; - case Simcall::MUTEX_TRYLOCK: - case Simcall::MUTEX_LOCK: { - if (req->call_ == Simcall::MUTEX_LOCK) - type = "Mutex LOCK"; - else - type = "Mutex TRYLOCK"; - - simgrid::mc::Remote mutex; - mc_model_checker->get_remote_simulation().read_bytes(mutex.get_buffer(), sizeof(mutex), - remote(req->call_ == Simcall::MUTEX_LOCK - ? simcall_mutex_lock__get__mutex(req) - : simcall_mutex_trylock__get__mutex(req))); - args = bprintf("locked = %d, owner = %d, sleeping = n/a", mutex.get_buffer()->is_locked(), - mutex.get_buffer()->get_owner() != nullptr - ? (int)mc_model_checker->get_remote_simulation() - .resolve_actor(simgrid::mc::remote(mutex.get_buffer()->get_owner())) - ->get_pid() - : -1); - break; + default: + type = SIMIX_simcall_name(req->call_); + args = bprintf("??"); + break; } - case Simcall::MC_RANDOM: - type = "MC_RANDOM"; - args = bprintf("%d", value); - break; - - default: - type = SIMIX_simcall_name(req->call_); - args = bprintf("??"); - break; - } - std::string str; if (args != nullptr) str = simgrid::xbt::string_printf("[(%ld)%s (%s)] %s(%s)", issuer->get_pid(), actor_get_host_name(issuer), @@ -899,120 +894,109 @@ std::string Api::request_get_dot_output(smx_simcall_t req, int value) const const smx_actor_t issuer = simcall_get_issuer(req); const char* color = get_color(issuer->get_pid() - 1); - if (req->inspector_ != nullptr) - return simgrid::xbt::string_printf("label = \"%s\", color = %s, fontcolor = %s", - req->inspector_->dot_label().c_str(), color, color); - std::string label; - switch (req->call_) { - case Simcall::COMM_ISEND: - if (issuer->get_host()) - label = xbt::string_printf("[(%ld)%s] iSend", issuer->get_pid(), actor_get_host_name(issuer)); - else - label = bprintf("[(%ld)] iSend", issuer->get_pid()); - break; - - case Simcall::COMM_IRECV: - if (issuer->get_host()) - label = xbt::string_printf("[(%ld)%s] iRecv", issuer->get_pid(), actor_get_host_name(issuer)); - else - label = xbt::string_printf("[(%ld)] iRecv", issuer->get_pid()); - break; - - case Simcall::COMM_WAIT: - if (value == -1) { + if (req->inspector_ != nullptr) { + label = mc_model_checker->simcall_dot_label(issuer->get_pid(), value); + } else + switch (req->call_) { + case Simcall::COMM_ISEND: if (issuer->get_host()) - label = xbt::string_printf("[(%ld)%s] WaitTimeout", issuer->get_pid(), actor_get_host_name(issuer)); + label = xbt::string_printf("[(%ld)%s] iSend", issuer->get_pid(), actor_get_host_name(issuer)); else - label = xbt::string_printf("[(%ld)] WaitTimeout", issuer->get_pid()); - } else { - kernel::activity::ActivityImpl* remote_act = simcall_comm_wait__getraw__comm(req); - Remote temp_comm; - mc_model_checker->get_remote_simulation().read(temp_comm, - remote(static_cast(remote_act))); - const kernel::activity::CommImpl* comm = temp_comm.get_buffer(); + label = bprintf("[(%ld)] iSend", issuer->get_pid()); + break; - const kernel::actor::ActorImpl* src_proc = - mc_model_checker->get_remote_simulation().resolve_actor(mc::remote(comm->src_actor_.get())); - const kernel::actor::ActorImpl* dst_proc = - mc_model_checker->get_remote_simulation().resolve_actor(mc::remote(comm->dst_actor_.get())); + case Simcall::COMM_IRECV: if (issuer->get_host()) - label = - xbt::string_printf("[(%ld)%s] Wait [(%ld)->(%ld)]", issuer->get_pid(), actor_get_host_name(issuer), - src_proc ? src_proc->get_pid() : 0, dst_proc ? dst_proc->get_pid() : 0); + label = xbt::string_printf("[(%ld)%s] iRecv", issuer->get_pid(), actor_get_host_name(issuer)); else - label = xbt::string_printf("[(%ld)] Wait [(%ld)->(%ld)]", issuer->get_pid(), - src_proc ? src_proc->get_pid() : 0, dst_proc ? dst_proc->get_pid() : 0); - } - break; + label = xbt::string_printf("[(%ld)] iRecv", issuer->get_pid()); + break; - case Simcall::COMM_TEST: { - kernel::activity::ActivityImpl* remote_act = simcall_comm_test__getraw__comm(req); - Remote temp_comm; - mc_model_checker->get_remote_simulation().read(temp_comm, - remote(static_cast(remote_act))); - const kernel::activity::CommImpl* comm = temp_comm.get_buffer(); - if (comm->src_actor_.get() == nullptr || comm->dst_actor_.get() == nullptr) { - if (issuer->get_host()) - label = xbt::string_printf("[(%ld)%s] Test FALSE", issuer->get_pid(), actor_get_host_name(issuer)); - else - label = bprintf("[(%ld)] Test FALSE", issuer->get_pid()); - } else { - if (issuer->get_host()) - label = xbt::string_printf("[(%ld)%s] Test TRUE", issuer->get_pid(), actor_get_host_name(issuer)); - else - label = xbt::string_printf("[(%ld)] Test TRUE", issuer->get_pid()); - } - break; - } + case Simcall::COMM_WAIT: + if (value == -1) { + if (issuer->get_host()) + label = xbt::string_printf("[(%ld)%s] WaitTimeout", issuer->get_pid(), actor_get_host_name(issuer)); + else + label = xbt::string_printf("[(%ld)] WaitTimeout", issuer->get_pid()); + } else { + kernel::activity::ActivityImpl* remote_act = simcall_comm_wait__getraw__comm(req); + Remote temp_comm; + mc_model_checker->get_remote_simulation().read(temp_comm, + remote(static_cast(remote_act))); + const kernel::activity::CommImpl* comm = temp_comm.get_buffer(); + + const kernel::actor::ActorImpl* src_proc = + mc_model_checker->get_remote_simulation().resolve_actor(mc::remote(comm->src_actor_.get())); + const kernel::actor::ActorImpl* dst_proc = + mc_model_checker->get_remote_simulation().resolve_actor(mc::remote(comm->dst_actor_.get())); + if (issuer->get_host()) + label = xbt::string_printf("[(%ld)%s] Wait [(%ld)->(%ld)]", issuer->get_pid(), actor_get_host_name(issuer), + src_proc ? src_proc->get_pid() : 0, dst_proc ? dst_proc->get_pid() : 0); + else + label = xbt::string_printf("[(%ld)] Wait [(%ld)->(%ld)]", issuer->get_pid(), + src_proc ? src_proc->get_pid() : 0, dst_proc ? dst_proc->get_pid() : 0); + } + break; - case Simcall::COMM_WAITANY: { - size_t comms_size = simcall_comm_waitany__get__count(req); - if (issuer->get_host()) - label = xbt::string_printf("[(%ld)%s] WaitAny [%d of %zu]", issuer->get_pid(), - actor_get_host_name(issuer), value + 1, comms_size); - else - label = xbt::string_printf("[(%ld)] WaitAny [%d of %zu]", issuer->get_pid(), value + 1, comms_size); - break; - } + case Simcall::COMM_TEST: { + kernel::activity::ActivityImpl* remote_act = simcall_comm_test__getraw__comm(req); + Remote temp_comm; + mc_model_checker->get_remote_simulation().read(temp_comm, + remote(static_cast(remote_act))); + const kernel::activity::CommImpl* comm = temp_comm.get_buffer(); + if (comm->src_actor_.get() == nullptr || comm->dst_actor_.get() == nullptr) { + if (issuer->get_host()) + label = xbt::string_printf("[(%ld)%s] Test FALSE", issuer->get_pid(), actor_get_host_name(issuer)); + else + label = bprintf("[(%ld)] Test FALSE", issuer->get_pid()); + } else { + if (issuer->get_host()) + label = xbt::string_printf("[(%ld)%s] Test TRUE", issuer->get_pid(), actor_get_host_name(issuer)); + else + label = xbt::string_printf("[(%ld)] Test TRUE", issuer->get_pid()); + } + break; + } - case Simcall::COMM_TESTANY: - if (value == -1) { - if (issuer->get_host()) - label = xbt::string_printf("[(%ld)%s] TestAny FALSE", issuer->get_pid(), actor_get_host_name(issuer)); - else - label = xbt::string_printf("[(%ld)] TestAny FALSE", issuer->get_pid()); - } else { + case Simcall::COMM_WAITANY: { + size_t comms_size = simcall_comm_waitany__get__count(req); if (issuer->get_host()) - label = - xbt::string_printf("[(%ld)%s] TestAny TRUE [%d of %lu]", issuer->get_pid(), - actor_get_host_name(issuer), value + 1, simcall_comm_testany__get__count(req)); + label = xbt::string_printf("[(%ld)%s] WaitAny [%d of %zu]", issuer->get_pid(), actor_get_host_name(issuer), + value + 1, comms_size); else - label = xbt::string_printf("[(%ld)] TestAny TRUE [%d of %lu]", issuer->get_pid(), value + 1, - simcall_comm_testany__get__count(req)); + label = xbt::string_printf("[(%ld)] WaitAny [%d of %zu]", issuer->get_pid(), value + 1, comms_size); + break; } - break; - case Simcall::MUTEX_TRYLOCK: - label = xbt::string_printf("[(%ld)] Mutex TRYLOCK", issuer->get_pid()); - break; + case Simcall::COMM_TESTANY: + if (value == -1) { + if (issuer->get_host()) + label = xbt::string_printf("[(%ld)%s] TestAny FALSE", issuer->get_pid(), actor_get_host_name(issuer)); + else + label = xbt::string_printf("[(%ld)] TestAny FALSE", issuer->get_pid()); + } else { + if (issuer->get_host()) + label = xbt::string_printf("[(%ld)%s] TestAny TRUE [%d of %lu]", issuer->get_pid(), + actor_get_host_name(issuer), value + 1, simcall_comm_testany__get__count(req)); + else + label = xbt::string_printf("[(%ld)] TestAny TRUE [%d of %lu]", issuer->get_pid(), value + 1, + simcall_comm_testany__get__count(req)); + } + break; - case Simcall::MUTEX_LOCK: - label = xbt::string_printf("[(%ld)] Mutex LOCK", issuer->get_pid()); - break; + case Simcall::MUTEX_TRYLOCK: + label = xbt::string_printf("[(%ld)] Mutex TRYLOCK", issuer->get_pid()); + break; - case Simcall::MC_RANDOM: - if (issuer->get_host()) - label = xbt::string_printf("[(%ld)%s] MC_RANDOM (%d)", issuer->get_pid(), actor_get_host_name(issuer), - value); - else - label = xbt::string_printf("[(%ld)] MC_RANDOM (%d)", issuer->get_pid(), value); - break; + case Simcall::MUTEX_LOCK: + label = xbt::string_printf("[(%ld)] Mutex LOCK", issuer->get_pid()); + break; - default: - THROW_UNIMPLEMENTED; - } + default: + THROW_UNIMPLEMENTED; + } return xbt::string_printf("label = \"%s\", color = %s, fontcolor = %s", label.c_str(), color, color); } @@ -1070,6 +1054,8 @@ void Api::restore_initial_state() const void Api::execute(Transition const& transition) const { session->execute(transition); + auto textual = mc_model_checker->simcall_to_string(transition.pid_, transition.times_considered_); + strcpy((char*)transition.textual, textual.c_str()); } #if SIMGRID_HAVE_MC diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp index 8b443690dc..eb2d66638e 100644 --- a/src/mc/checker/CommunicationDeterminismChecker.cpp +++ b/src/mc/checker/CommunicationDeterminismChecker.cpp @@ -276,7 +276,7 @@ std::vector CommunicationDeterminismChecker::get_textual_trace() // std::vector trace; for (auto const& state : stack_) { smx_simcall_t req = &state->executed_req_; - trace.push_back(api::get().request_to_string(req, state->transition_.argument_, RequestType::executed)); + trace.push_back(api::get().request_to_string(req, state->transition_.times_considered_, RequestType::executed)); } return trace; } @@ -364,7 +364,7 @@ void CommunicationDeterminismChecker::restoreState() if (state == stack_.back()) break; - int req_num = state->transition_.argument_; + int req_num = state->transition_.times_considered_; const s_smx_simcall* saved_req = &state->executed_req_; xbt_assert(saved_req); @@ -433,7 +433,7 @@ void CommunicationDeterminismChecker::real_run() req = nullptr; if (req != nullptr && visited_state == nullptr) { - int req_num = cur_state->transition_.argument_; + int req_num = cur_state->transition_.times_considered_; XBT_DEBUG("Execute: %s", api::get().request_to_string(req, req_num, RequestType::simix).c_str()); diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp index 1a026d4a1e..3f2030e6ec 100644 --- a/src/mc/checker/LivenessChecker.cpp +++ b/src/mc/checker/LivenessChecker.cpp @@ -129,7 +129,7 @@ void LivenessChecker::replay() std::shared_ptr state = pair->graph_state; if (pair->exploration_started) { - int req_num = state->transition_.argument_; + int req_num = state->transition_.times_considered_; const s_smx_simcall* saved_req = &state->executed_req_; smx_simcall_t req = nullptr; @@ -239,7 +239,7 @@ std::vector LivenessChecker::get_textual_trace() // override { std::vector trace; for (std::shared_ptr const& pair : exploration_stack_) { - int req_num = pair->graph_state->transition_.argument_; + int req_num = pair->graph_state->transition_.times_considered_; smx_simcall_t req = &pair->graph_state->executed_req_; if (req->call_ != simix::Simcall::NONE) trace.push_back(api::get().request_to_string(req, req_num, RequestType::executed)); @@ -360,7 +360,7 @@ void LivenessChecker::run() } smx_simcall_t req = api::get().mc_state_choose_request(current_pair->graph_state.get()); - int req_num = current_pair->graph_state->transition_.argument_; + int req_num = current_pair->graph_state->transition_.times_considered_; if (dot_output != nullptr) { if (this->previous_pair_ != 0 && this->previous_pair_ != current_pair->num) { diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp index f74ab5f82d..049d3fb67c 100644 --- a/src/mc/checker/SafetyChecker.cpp +++ b/src/mc/checker/SafetyChecker.cpp @@ -62,11 +62,8 @@ RecordTrace SafetyChecker::get_record_trace() // override std::vector SafetyChecker::get_textual_trace() // override { std::vector trace; - for (auto const& state : stack_) { - int value = state->transition_.argument_; - smx_simcall_t req = &state->executed_req_; - trace.push_back(api::get().request_to_string(req, value, RequestType::executed)); - } + for (auto const& state : stack_) + trace.push_back(state->transition_.textual); return trace; } @@ -124,11 +121,12 @@ void SafetyChecker::run() // If there are processes to interleave and the maximum depth has not been // reached then perform one step of the exploration algorithm. - XBT_DEBUG("Execute: %s", api::get().request_to_string(req, state->transition_.argument_, RequestType::simix).c_str()); + XBT_DEBUG("Execute: %s", + api::get().request_to_string(req, state->transition_.times_considered_, RequestType::simix).c_str()); std::string req_str; if (dot_output != nullptr) - req_str = api::get().request_get_dot_output(req, state->transition_.argument_); + req_str = api::get().request_get_dot_output(req, state->transition_.times_considered_); api::get().mc_inc_executed_trans(); @@ -203,11 +201,11 @@ void SafetyChecker::backtrack() if (api::get().simcall_check_dependency(req, &prev_state->internal_req_)) { if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) { XBT_DEBUG("Dependent Transitions:"); - int value = prev_state->transition_.argument_; + int value = prev_state->transition_.times_considered_; smx_simcall_t prev_req = &prev_state->executed_req_; XBT_DEBUG("%s (state=%d)", api::get().request_to_string(prev_req, value, RequestType::internal).c_str(), prev_state->num_); - value = state->transition_.argument_; + value = state->transition_.times_considered_; prev_req = &state->executed_req_; XBT_DEBUG("%s (state=%d)", api::get().request_to_string(prev_req, value, RequestType::executed).c_str(), state->num_); diff --git a/src/mc/checker/SimcallInspector.hpp b/src/mc/checker/SimcallInspector.hpp index 3759a7fa2d..b00b85c411 100644 --- a/src/mc/checker/SimcallInspector.hpp +++ b/src/mc/checker/SimcallInspector.hpp @@ -6,13 +6,19 @@ #ifndef SIMGRID_MC_SIMCALL_INSPECTOR_HPP #define SIMGRID_MC_SIMCALL_INSPECTOR_HPP +#include "simgrid/forward.h" + #include namespace simgrid { namespace mc { class SimcallInspector { + kernel::actor::ActorImpl* issuer_; + public: + SimcallInspector(kernel::actor::ActorImpl* issuer) : issuer_(issuer) {} + kernel::actor::ActorImpl* get_issuer() { return issuer_; } /** Whether this transition can currently be taken without blocking. * * For example, a mutex_lock is not enabled when the mutex is not free. @@ -20,20 +26,45 @@ public: */ virtual bool is_enabled() { return true; } - /** Prepare the simcall to be executed + /** Check whether the simcall will still be firable on this execution path + * + * Return true if the simcall can be fired another time, and false if it gave all its content already. + * + * This is not to be mixed with is_enabled(). Even if is_pending() returns true, + * is_enabled() may return false at a given point but will eventually return true further + * on that execution path. + * + * If is_pending() returns false the first time, it means that the execution path is not branching + * on that transition. Only one execution path goes out of that simcall. * - * Do the choices that the platform would have done in non-MC settings. + * is_pending() is to decide whether we should branch a new execution path with this transition while + * is_enabled() is about continuing the current execution path with that transition or saving it for later. + * + * This function should also do the choices that the platform would have done in non-MC settings. * For example if it's a waitany, pick the communication that should finish first. * If it's a random(), choose the next value to explore. */ - virtual void arm() {} + virtual bool is_pending(int times_considered) { return false; } /** Some simcalls may only be observable under some circumstances. * Most simcalls are not visible from the MC because they don't have an inspector at all. */ virtual bool is_visible() { return true; } - virtual std::string to_string() = 0; + virtual std::string to_string(int times_considered); virtual std::string dot_label() = 0; }; + +class RandomSimcall : public SimcallInspector { + int min_; + int max_; + int next_value_ = 0; + +public: + RandomSimcall(smx_actor_t actor, int min, int max) : SimcallInspector(actor), min_(min), max_(max) {} + bool is_pending(int times_considered) override; + std::string to_string(int times_considered) override; + std::string dot_label() override; + int get_value(); +}; } // namespace mc } // namespace simgrid diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp index 8274ec2b0c..cf5ef31400 100644 --- a/src/mc/mc_base.cpp +++ b/src/mc/mc_base.cpp @@ -156,23 +156,15 @@ bool request_is_visible(const s_smx_simcall* req) #if SIMGRID_HAVE_MC xbt_assert(mc_model_checker == nullptr, "This should be called from the client side"); #endif + if (req->inspector_ != nullptr) + return req->inspector_->is_visible(); using simix::Simcall; - return (req->inspector_ != nullptr && req->inspector_->is_visible()) || req->call_ == Simcall::COMM_ISEND || - req->call_ == Simcall::COMM_IRECV || req->call_ == Simcall::COMM_WAIT || req->call_ == Simcall::COMM_WAITANY || - req->call_ == Simcall::COMM_TEST || req->call_ == Simcall::COMM_TESTANY || req->call_ == Simcall::MC_RANDOM || - req->call_ == Simcall::MUTEX_LOCK || req->call_ == Simcall::MUTEX_TRYLOCK || - req->call_ == Simcall::MUTEX_UNLOCK; + return req->call_ == Simcall::COMM_ISEND || req->call_ == Simcall::COMM_IRECV || req->call_ == Simcall::COMM_WAIT || + req->call_ == Simcall::COMM_WAITANY || req->call_ == Simcall::COMM_TEST || + req->call_ == Simcall::COMM_TESTANY || req->call_ == Simcall::MUTEX_LOCK || + req->call_ == Simcall::MUTEX_TRYLOCK || req->call_ == Simcall::MUTEX_UNLOCK; } } } - -int simcall_HANDLER_mc_random(smx_simcall_t simcall, int min, int max) -{ - if (not MC_is_active() && not MC_record_replay_is_active()) { - static simgrid::xbt::random::XbtRandom prng; - return prng.uniform_int(min, max); - } - return simcall->mc_value_; -} diff --git a/src/mc/mc_record.cpp b/src/mc/mc_record.cpp index b326b20cc9..38321e4a89 100644 --- a/src/mc/mc_record.cpp +++ b/src/mc/mc_record.cpp @@ -28,7 +28,7 @@ void replay(RecordTrace const& trace) simgrid::mc::wait_for_requests(); for (simgrid::mc::Transition const& transition : trace) { - XBT_DEBUG("Executing %i$%i", transition.pid_, transition.argument_); + XBT_DEBUG("Executing %i$%i", transition.pid_, transition.times_considered_); // Choose a request: kernel::actor::ActorImpl* actor = kernel::actor::ActorImpl::by_PID(transition.pid_); @@ -41,7 +41,7 @@ void replay(RecordTrace const& trace) xbt_die("Unexpected simcall."); // Execute the request: - simcall->issuer_->simcall_handle(transition.argument_); + simcall->issuer_->simcall_handle(transition.times_considered_); simgrid::mc::wait_for_requests(); } } @@ -64,7 +64,7 @@ RecordTrace parseRecordTrace(const char* data) const char* current = data; while (*current) { simgrid::mc::Transition item; - int count = sscanf(current, "%d/%d", &item.pid_, &item.argument_); + int count = sscanf(current, "%d/%d", &item.pid_, &item.times_considered_); if(count != 2 && count != 1) throw std::invalid_argument("Could not parse record path"); @@ -90,8 +90,8 @@ std::string traceToString(simgrid::mc::RecordTrace const& trace) if (i != trace.begin()) stream << ';'; stream << i->pid_; - if (i->argument_) - stream << '/' << i->argument_; + if (i->times_considered_) + stream << '/' << i->times_considered_; } return stream.str(); } diff --git a/src/mc/remote/AppSide.cpp b/src/mc/remote/AppSide.cpp index 3cd49b2f57..665da7dab6 100644 --- a/src/mc/remote/AppSide.cpp +++ b/src/mc/remote/AppSide.cpp @@ -6,6 +6,7 @@ #include "src/mc/remote/AppSide.hpp" #include "src/internal_config.h" #include "src/kernel/actor/ActorImpl.hpp" +#include "src/mc/checker/SimcallInspector.hpp" #include #include @@ -135,6 +136,64 @@ void AppSide::handle_messages() const handle_simcall((s_mc_message_simcall_handle_t*)message_buffer.data()); break; + case MessageType::SIMCALL_IS_PENDING: { + assert_msg_size("SIMCALL_IS_PENDING", s_mc_message_simcall_is_pending_t); + auto msg_simcall = (s_mc_message_simcall_is_pending_t*)message_buffer.data(); + kernel::actor::ActorImpl* actor = kernel::actor::ActorImpl::by_PID(msg_simcall->aid); + xbt_assert(actor != nullptr, "Invalid pid %d", msg_simcall->aid); + xbt_assert(actor->simcall_.inspector_, "The transition of %s has no inspector", actor->get_cname()); + bool value = actor->simcall_.inspector_->is_pending(msg_simcall->time_considered); + + // Send result: + s_mc_message_simcall_is_pending_answer_t answer{MessageType::SIMCALL_IS_PENDING_ANSWER, value}; + xbt_assert(channel_.send(answer) == 0, "Could not send response"); + break; + } + + case MessageType::SIMCALL_IS_VISIBLE: { + assert_msg_size("SIMCALL_IS_VISIBLE", s_mc_message_simcall_is_visible_t); + auto msg_simcall = (s_mc_message_simcall_is_visible_t*)message_buffer.data(); + kernel::actor::ActorImpl* actor = kernel::actor::ActorImpl::by_PID(msg_simcall->aid); + xbt_assert(actor != nullptr, "Invalid pid %d", msg_simcall->aid); + xbt_assert(actor->simcall_.inspector_, "The transition of %s has no inspector", actor->get_cname()); + bool value = actor->simcall_.inspector_->is_visible(); + + // Send result: + s_mc_message_simcall_is_visible_answer_t answer{MessageType::SIMCALL_IS_VISIBLE_ANSWER, value}; + xbt_assert(channel_.send(answer) == 0, "Could not send response"); + break; + } + + case MessageType::SIMCALL_TO_STRING: { + assert_msg_size("SIMCALL_TO_STRING", s_mc_message_simcall_to_string_t); + auto msg_simcall = (s_mc_message_simcall_to_string_t*)message_buffer.data(); + kernel::actor::ActorImpl* actor = kernel::actor::ActorImpl::by_PID(msg_simcall->aid); + xbt_assert(actor != nullptr, "Invalid pid %d", msg_simcall->aid); + xbt_assert(actor->simcall_.inspector_, "The transition of %s has no inspector", actor->get_cname()); + std::string value = actor->simcall_.inspector_->to_string(msg_simcall->time_considered); + + // Send result: + s_mc_message_simcall_to_string_answer_t answer{MessageType::SIMCALL_TO_STRING_ANSWER, 0}; + strcat(answer.value, value.c_str()); + xbt_assert(channel_.send(answer) == 0, "Could not send response"); + break; + } + + case MessageType::SIMCALL_DOT_LABEL: { + assert_msg_size("SIMCALL_DOT_LABEL", s_mc_message_simcall_to_string_t); + auto msg_simcall = (s_mc_message_simcall_to_string_t*)message_buffer.data(); + kernel::actor::ActorImpl* actor = kernel::actor::ActorImpl::by_PID(msg_simcall->aid); + xbt_assert(actor != nullptr, "Invalid pid %d", msg_simcall->aid); + xbt_assert(actor->simcall_.inspector_, "The transition of %s has no inspector", actor->get_cname()); + std::string value = actor->simcall_.inspector_->dot_label(); + + // Send result: + s_mc_message_simcall_to_string_answer_t answer{MessageType::SIMCALL_TO_STRING_ANSWER, 0}; + strcat(answer.value, value.c_str()); + xbt_assert(channel_.send(answer) == 0, "Could not send response"); + break; + } + case MessageType::ACTOR_ENABLED: assert_msg_size("ACTOR_ENABLED", s_mc_message_actor_enabled_t); handle_actor_enabled((s_mc_message_actor_enabled_t*)message_buffer.data()); diff --git a/src/mc/remote/mc_protocol.h b/src/mc/remote/mc_protocol.h index 54ec711ffa..17f7f86d76 100644 --- a/src/mc/remote/mc_protocol.h +++ b/src/mc/remote/mc_protocol.h @@ -27,8 +27,10 @@ namespace simgrid { namespace mc { XBT_DECLARE_ENUM_CLASS(MessageType, NONE, CONTINUE, IGNORE_HEAP, UNIGNORE_HEAP, IGNORE_MEMORY, STACK_REGION, - REGISTER_SYMBOL, DEADLOCK_CHECK, DEADLOCK_CHECK_REPLY, WAITING, SIMCALL_HANDLE, ASSERTION_FAILED, - ACTOR_ENABLED, ACTOR_ENABLED_REPLY); + REGISTER_SYMBOL, DEADLOCK_CHECK, DEADLOCK_CHECK_REPLY, WAITING, SIMCALL_HANDLE, + SIMCALL_IS_PENDING, SIMCALL_IS_PENDING_ANSWER, SIMCALL_IS_VISIBLE, SIMCALL_IS_VISIBLE_ANSWER, + SIMCALL_TO_STRING, SIMCALL_TO_STRING_ANSWER, SIMCALL_DOT_LABEL, ASSERTION_FAILED, ACTOR_ENABLED, + ACTOR_ENABLED_REPLY); } // namespace mc } // namespace simgrid @@ -99,5 +101,35 @@ struct s_mc_message_actor_enabled_t { aid_t aid; // actor ID }; +/* RPC */ +struct s_mc_message_simcall_is_pending_t { // MessageType::SIMCALL_IS_PENDING + simgrid::mc::MessageType type; + int aid; + int time_considered; +}; +struct s_mc_message_simcall_is_pending_answer_t { // MessageType::SIMCALL_IS_PENDING_ANSWER + simgrid::mc::MessageType type; + bool value; +}; + +struct s_mc_message_simcall_is_visible_t { // MessageType::SIMCALL_IS_VISIBLE + simgrid::mc::MessageType type; + int aid; +}; +struct s_mc_message_simcall_is_visible_answer_t { // MessageType::SIMCALL_IS_VISIBLE_ANSWER + simgrid::mc::MessageType type; + bool value; +}; + +struct s_mc_message_simcall_to_string_t { // MessageType::SIMCALL_TO_STRING or MessageType::SIMCALL_DOT_LABEL + simgrid::mc::MessageType type; + int aid; + int time_considered; +}; +struct s_mc_message_simcall_to_string_answer_t { // MessageType::SIMCALL_TO_STRING_ANSWER + simgrid::mc::MessageType type; + char value[1024]; +}; + #endif // __cplusplus #endif diff --git a/src/simix/libsmx.cpp b/src/simix/libsmx.cpp index f17c2e515a..9e05fbf4f1 100644 --- a/src/simix/libsmx.cpp +++ b/src/simix/libsmx.cpp @@ -18,8 +18,10 @@ #include "src/kernel/activity/IoImpl.hpp" #include "src/kernel/activity/MailboxImpl.hpp" #include "src/kernel/activity/MutexImpl.hpp" +#include "src/mc/checker/SimcallInspector.hpp" #include "src/mc/mc_replay.hpp" #include "src/plugins/vm/VirtualMachineImpl.hpp" +#include "xbt/random.hpp" #include "popping_bodies.cpp" @@ -362,7 +364,12 @@ void simcall_run_blocking(std::function const& code, simgrid::mc::Simcal } int simcall_mc_random(int min, int max) { - return simcall_BODY_mc_random(min, max); + if (not MC_is_active() && not MC_record_replay_is_active()) { // no need to do a simcall in this case + static simgrid::xbt::random::XbtRandom prng; + return prng.uniform_int(min, max); + } + auto observer = new simgrid::mc::RandomSimcall(SIMIX_process_self(), min, max); + return simgrid::kernel::actor::simcall([observer] { return observer->get_value(); }, observer); } /* ************************************************************************** */ diff --git a/src/simix/popping_accessors.hpp b/src/simix/popping_accessors.hpp index 557581519e..21b3b1a6ab 100644 --- a/src/simix/popping_accessors.hpp +++ b/src/simix/popping_accessors.hpp @@ -859,43 +859,6 @@ static inline void simcall_sem_acquire_timeout__set__result(smx_simcall_t simcal simgrid::simix::marshal(simcall->result_, result); } -static inline int simcall_mc_random__get__min(smx_simcall_t simcall) -{ - return simgrid::simix::unmarshal(simcall->args_[0]); -} -static inline int simcall_mc_random__getraw__min(smx_simcall_t simcall) -{ - return simgrid::simix::unmarshal_raw(simcall->args_[0]); -} -static inline void simcall_mc_random__set__min(smx_simcall_t simcall, int arg) -{ - simgrid::simix::marshal(simcall->args_[0], arg); -} -static inline int simcall_mc_random__get__max(smx_simcall_t simcall) -{ - return simgrid::simix::unmarshal(simcall->args_[1]); -} -static inline int simcall_mc_random__getraw__max(smx_simcall_t simcall) -{ - return simgrid::simix::unmarshal_raw(simcall->args_[1]); -} -static inline void simcall_mc_random__set__max(smx_simcall_t simcall, int arg) -{ - simgrid::simix::marshal(simcall->args_[1], arg); -} -static inline int simcall_mc_random__get__result(smx_simcall_t simcall) -{ - return simgrid::simix::unmarshal(simcall->result_); -} -static inline int simcall_mc_random__getraw__result(smx_simcall_t simcall) -{ - return simgrid::simix::unmarshal_raw(simcall->result_); -} -static inline void simcall_mc_random__set__result(smx_simcall_t simcall, int result) -{ - simgrid::simix::marshal(simcall->result_, result); -} - static inline std::function const* simcall_run_kernel__get__code(smx_simcall_t simcall) { return simgrid::simix::unmarshal const*>(simcall->args_[0]); @@ -940,4 +903,3 @@ XBT_PRIVATE void simcall_HANDLER_cond_wait(smx_simcall_t simcall, smx_cond_t con XBT_PRIVATE void simcall_HANDLER_cond_wait_timeout(smx_simcall_t simcall, smx_cond_t cond, smx_mutex_t mutex, double timeout); XBT_PRIVATE void simcall_HANDLER_sem_acquire(smx_simcall_t simcall, smx_sem_t sem); XBT_PRIVATE void simcall_HANDLER_sem_acquire_timeout(smx_simcall_t simcall, smx_sem_t sem, double timeout); -XBT_PRIVATE int simcall_HANDLER_mc_random(smx_simcall_t simcall, int min, int max); diff --git a/src/simix/popping_bodies.cpp b/src/simix/popping_bodies.cpp index 1aa41085f9..f74df5a063 100644 --- a/src/simix/popping_bodies.cpp +++ b/src/simix/popping_bodies.cpp @@ -153,13 +153,6 @@ inline static int simcall_BODY_sem_acquire_timeout(smx_sem_t sem, double timeout return simcall(Simcall::SEM_ACQUIRE_TIMEOUT, sem, timeout); } -inline static int simcall_BODY_mc_random(int min, int max) -{ - if (false) /* Go to that function to follow the code flow through the simcall barrier */ - simcall_HANDLER_mc_random(&SIMIX_process_self()->simcall_, min, max); - return simcall(Simcall::MC_RANDOM, min, max); -} - inline static void simcall_BODY_run_kernel(std::function const* code) { if (false) /* Go to that function to follow the code flow through the simcall barrier */ diff --git a/src/simix/popping_enum.hpp b/src/simix/popping_enum.hpp index 15c9ca82d8..b03db5ad7e 100644 --- a/src/simix/popping_enum.hpp +++ b/src/simix/popping_enum.hpp @@ -37,11 +37,10 @@ enum class Simcall { COND_WAIT_TIMEOUT, SEM_ACQUIRE, SEM_ACQUIRE_TIMEOUT, - MC_RANDOM, RUN_KERNEL, RUN_BLOCKING, }; -constexpr int NUM_SIMCALLS = 20; +constexpr int NUM_SIMCALLS = 19; } // namespace simix } // namespace simgrid diff --git a/src/simix/popping_generated.cpp b/src/simix/popping_generated.cpp index 0c4e43190d..4cfc088ad0 100644 --- a/src/simix/popping_generated.cpp +++ b/src/simix/popping_generated.cpp @@ -21,6 +21,7 @@ #include "src/mc/mc_forward.hpp" #endif #include "src/kernel/activity/ConditionVariableImpl.hpp" +#include "src/mc/checker/SimcallInspector.hpp" XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(simix_popping); @@ -44,7 +45,6 @@ constexpr std::array simcall_names{{ "Simcall::COND_WAIT_TIMEOUT", "Simcall::SEM_ACQUIRE", "Simcall::SEM_ACQUIRE_TIMEOUT", - "Simcall::MC_RANDOM", "Simcall::RUN_KERNEL", "Simcall::RUN_BLOCKING", }}; @@ -55,8 +55,10 @@ constexpr std::array simcall_names{{ * This function is generated from src/simix/simcalls.in */ void simgrid::kernel::actor::ActorImpl::simcall_handle(int value) { - XBT_DEBUG("Handling simcall %p: %s", &simcall_, SIMIX_simcall_name(simcall_.call_)); + XBT_DEBUG("Handling simcall %p %d: %s", &simcall_, value, SIMIX_simcall_name(simcall_.call_)); SIMCALL_SET_MC_VALUE(simcall_, value); + if (simcall_.inspector_ != nullptr) + simcall_.inspector_->is_pending(value); if (context_->wannadie()) return; switch (simcall_.call_) { @@ -128,11 +130,6 @@ void simgrid::kernel::actor::ActorImpl::simcall_handle(int value) { simcall_HANDLER_sem_acquire_timeout(&simcall_, simgrid::simix::unmarshal(simcall_.args_[0]), simgrid::simix::unmarshal(simcall_.args_[1])); break; - case Simcall::MC_RANDOM: - simgrid::simix::marshal(simcall_.result_, simcall_HANDLER_mc_random(&simcall_, simgrid::simix::unmarshal(simcall_.args_[0]), simgrid::simix::unmarshal(simcall_.args_[1]))); - simcall_answer(); - break; - case Simcall::RUN_KERNEL: SIMIX_run_kernel(simgrid::simix::unmarshal const*>(simcall_.args_[0])); simcall_answer(); diff --git a/src/simix/simcalls.in b/src/simix/simcalls.in index 9791e174bb..3213a56662 100644 --- a/src/simix/simcalls.in +++ b/src/simix/simcalls.in @@ -56,7 +56,7 @@ int cond_wait_timeout(smx_cond_t cond, smx_mutex_t mutex, double timeout) void sem_acquire(smx_sem_t sem) [[block]]; int sem_acquire_timeout(smx_sem_t sem, double timeout) [[block]]; -int mc_random(int min, int max); +#int mc_random(int min, int max); void run_kernel(std::function const* code) [[nohandler]]; void run_blocking(std::function const* code) [[block,nohandler]]; diff --git a/src/simix/simcalls.py b/src/simix/simcalls.py index aed91390ab..d933dc2731 100755 --- a/src/simix/simcalls.py +++ b/src/simix/simcalls.py @@ -68,7 +68,7 @@ class Simcall(object): print ('{') print (' // Your code handling the simcall') print ('}') - return False +# return False else: if self.name in self.simcalls_pre: print ( @@ -325,6 +325,7 @@ if __name__ == '__main__': fd.write('#include "src/mc/mc_forward.hpp"\n') fd.write('#endif\n') fd.write('#include "src/kernel/activity/ConditionVariableImpl.hpp"\n') + fd.write('#include "src/mc/checker/SimcallInspector.hpp"\n') fd.write('\n') fd.write('XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(simix_popping);\n\n') @@ -351,8 +352,10 @@ if __name__ == '__main__': fd.write( ' XBT_DEBUG("Handling simcall %p: %s", &simcall_, SIMIX_simcall_name(simcall_.call_));\n') fd.write(' SIMCALL_SET_MC_VALUE(simcall_, value);\n') - fd.write( - ' if (context_->wannadie())\n') + fd.write(' if (simcall_.inspector_ != nullptr)\n') + fd.write(' simcall_.inspector_->is_pending(value);\n') + + fd.write(' if (context_->wannadie())\n') fd.write(' return;\n') fd.write(' switch (simcall_.call_) {\n') diff --git a/teshsuite/mc/random-bug/random-bug.cpp b/teshsuite/mc/random-bug/random-bug.cpp index 167f621a46..b7579b5579 100644 --- a/teshsuite/mc/random-bug/random-bug.cpp +++ b/teshsuite/mc/random-bug/random-bug.cpp @@ -19,6 +19,7 @@ static void app() { int x = MC_random(0, 5); int y = MC_random(0, 5); + // XBT_INFO("got %d %d",x,y); if (behavior == Behavior::ASSERT) { MC_assert(x != 3 || y != 4); diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake index c597b0f23e..580e18e7a3 100644 --- a/tools/cmake/DefinePackages.cmake +++ b/tools/cmake/DefinePackages.cmake @@ -588,6 +588,7 @@ set(MC_SRC src/mc/checker/CommunicationDeterminismChecker.hpp src/mc/checker/SafetyChecker.cpp src/mc/checker/SafetyChecker.hpp + src/mc/checker/SimcallInspector.cpp src/mc/checker/SimcallInspector.hpp src/mc/checker/LivenessChecker.cpp src/mc/checker/LivenessChecker.hpp -- 2.20.1