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.

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index f7859f4..84e6a8d 100644 (file)
--- 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 cacf530..434609c 100644 (file)
--- 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 2527d8c..6b616cd 100644 (file)
--- 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 c510c37..2ced4af 100644 (file)
--- 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<simgrid::kernel::activity::CommImpl> remote_act =
-          remote(simcall_comm_wait__getraw__comm(&actor->simcall_));
-      simgrid::mc::Remote<simgrid::kernel::activity::CommImpl> 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<simgrid::kernel::activity::CommImpl> remote_act =
+            remote(simcall_comm_wait__getraw__comm(&actor->simcall_));
+        simgrid::mc::Remote<simgrid::kernel::activity::CommImpl> 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<simgrid::kernel::activity::CommImpl> 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<simgrid::kernel::activity::CommImpl> 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<simgrid::kernel::activity::CommImpl> 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<simgrid::kernel::activity::MutexImpl> 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<simgrid::kernel::activity::MutexImpl> 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<kernel::activity::CommImpl> temp_comm;
-        mc_model_checker->get_remote_simulation().read(temp_comm,
-                                                       remote(static_cast<kernel::activity::CommImpl*>(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<simgrid::kernel::activity::CommImpl> temp_comm;
-      mc_model_checker->get_remote_simulation().read(temp_comm,
-                                                     remote(static_cast<kernel::activity::CommImpl*>(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<kernel::activity::CommImpl> temp_comm;
+          mc_model_checker->get_remote_simulation().read(temp_comm,
+                                                         remote(static_cast<kernel::activity::CommImpl*>(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<simgrid::kernel::activity::CommImpl> temp_comm;
+        mc_model_checker->get_remote_simulation().read(temp_comm,
+                                                       remote(static_cast<kernel::activity::CommImpl*>(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 8b44369..eb2d666 100644 (file)
--- a/src/mc/checker/CommunicationDeterminismChecker.cpp
+++ b/src/mc/checker/CommunicationDeterminismChecker.cpp
@@ -276,7 +276,7 @@ std::vector<std::string> CommunicationDeterminismChecker::get_textual_trace() //
   std::vector<std::string> 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 1a026d4..3f2030e 100644 (file)
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -129,7 +129,7 @@ void LivenessChecker::replay()
     std::shared_ptr<State> 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<std::string> LivenessChecker::get_textual_trace() // override
 {
   std::vector<std::string> trace;
   for (std::shared_ptr<Pair> 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 f74ab5f..049d3fb 100644 (file)
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -62,11 +62,8 @@ RecordTrace SafetyChecker::get_record_trace() // override
 std::vector<std::string> SafetyChecker::get_textual_trace() // override
 {
   std::vector<std::string> 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 3759a7f..b00b85c 100644 (file)
--- 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 <string>
 
 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 8274ec2..cf5ef31 100644 (file)
--- 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 b326b20..38321e4 100644 (file)
--- 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 3cd49b2..665da7d 100644 (file)
--- 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 <simgrid/modelchecker.h>
 
 #include <cerrno>
@@ -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 54ec711..17f7f86 100644 (file)
--- 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 f17c2e5..9e05fbf 100644 (file)
--- 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<void()> 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 5575815..21b3b1a 100644 (file)
--- 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<int>(simcall->result_, result);
 }
 
-static inline int simcall_mc_random__get__min(smx_simcall_t simcall)
-{
-  return simgrid::simix::unmarshal<int>(simcall->args_[0]);
-}
-static inline int simcall_mc_random__getraw__min(smx_simcall_t simcall)
-{
-  return simgrid::simix::unmarshal_raw<int>(simcall->args_[0]);
-}
-static inline void simcall_mc_random__set__min(smx_simcall_t simcall, int arg)
-{
-  simgrid::simix::marshal<int>(simcall->args_[0], arg);
-}
-static inline int simcall_mc_random__get__max(smx_simcall_t simcall)
-{
-  return simgrid::simix::unmarshal<int>(simcall->args_[1]);
-}
-static inline int simcall_mc_random__getraw__max(smx_simcall_t simcall)
-{
-  return simgrid::simix::unmarshal_raw<int>(simcall->args_[1]);
-}
-static inline void simcall_mc_random__set__max(smx_simcall_t simcall, int arg)
-{
-  simgrid::simix::marshal<int>(simcall->args_[1], arg);
-}
-static inline int simcall_mc_random__get__result(smx_simcall_t simcall)
-{
-  return simgrid::simix::unmarshal<int>(simcall->result_);
-}
-static inline int simcall_mc_random__getraw__result(smx_simcall_t simcall)
-{
-  return simgrid::simix::unmarshal_raw<int>(simcall->result_);
-}
-static inline void simcall_mc_random__set__result(smx_simcall_t simcall, int result)
-{
-  simgrid::simix::marshal<int>(simcall->result_, result);
-}
-
 static inline std::function<void()> const* simcall_run_kernel__get__code(smx_simcall_t simcall)
 {
   return simgrid::simix::unmarshal<std::function<void()> 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 1aa4108..f74df5a 100644 (file)
--- 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<int, smx_sem_t, double>(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<int, int, int>(Simcall::MC_RANDOM, min, max);
-}
-
 inline static void simcall_BODY_run_kernel(std::function<void()> 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 15c9ca8..b03db5a 100644 (file)
--- 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 0c4e431..4cfc088 100644 (file)
--- 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<const char*, simgrid::simix::NUM_SIMCALLS> 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<const char*, simgrid::simix::NUM_SIMCALLS> 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<smx_sem_t>(simcall_.args_[0]), simgrid::simix::unmarshal<double>(simcall_.args_[1]));
       break;
 
-    case Simcall::MC_RANDOM:
-      simgrid::simix::marshal<int>(simcall_.result_, simcall_HANDLER_mc_random(&simcall_, simgrid::simix::unmarshal<int>(simcall_.args_[0]), simgrid::simix::unmarshal<int>(simcall_.args_[1])));
-      simcall_answer();
-      break;
-
     case Simcall::RUN_KERNEL:
       SIMIX_run_kernel(simgrid::simix::unmarshal<std::function<void()> const*>(simcall_.args_[0]));
       simcall_answer();

diff --git a/src/simix/simcalls.in b/src/simix/simcalls.in
index 9791e17..3213a56 100644 (file)
--- 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<void()> const* code) [[nohandler]];
 void       run_blocking(std::function<void()> const* code) [[block,nohandler]];

diff --git a/src/simix/simcalls.py b/src/simix/simcalls.py
index aed9139..d933dc2 100755 (executable)
--- 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 167f621..b7579b5 100644 (file)
--- 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 c597b0f..580e18e 100644 (file)
--- 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