- get_max_consider() returns how many times this simcall should be considered.
- prepare() does what needs to be done for the simcall to be fired in user space
This removes the RPC from MC to App to get this information:
- The value of get_max_consider() is copied in the simcall structure
when the AppSide prepares to wait for new instructions from the MC.
- prepare() was already called by handle_simcall() on AppSide, to
obey trace replays.
Less RPC is faster and less eror prone.
s_mc_message_simcall_handle_t m;
memset(&m, 0, sizeof(m));
m.type = MessageType::SIMCALL_HANDLE;
- m.pid = transition.pid_;
- m.value = transition.times_considered_;
+ m.pid_ = transition.pid_;
+ m.times_considered_ = 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");
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);
smx_simcall_t req = nullptr;
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->times_considered++;
+ if (actor->simcall_.mc_max_consider_ <= procstate->times_considered)
procstate->set_done();
req = &actor->simcall_;
} else
*/
virtual bool is_enabled() { return true; }
- /** Check whether the simcall will still be firable on this execution path
+ /** Returns the amount of time that this transition can be used.
*
- * 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 it's 1 (as with send/wait), there is no need to fork the state space exploration on this point.
+ * If it's more than one (as with mc_random or waitany), we need to consider this transition several times to start
+ * differing branches
+ */
+ virtual int get_max_consider() { return 1; }
+
+ /** Prepares the simcall to be used.
*
- * 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.
+ * For most simcalls, this does nothing. Once enabled, there is nothing to do to prepare a send().
*
- * 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.
+ * It is useful only for the simcalls that can be used several times, such as waitany() or random().
+ * For them, prepare() selects the right outcome for the time being considered.
*
- * 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.
+ * The first time a simcall is considered, times_considered is 0, not 1.
*/
- virtual bool is_pending(int times_considered) { return false; }
+ virtual void prepare(int times_considered) {}
/** 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. */
public:
RandomSimcall(smx_actor_t actor, int min, int max) : SimcallInspector(actor), min_(min), max_(max) {}
- bool is_pending(int times_considered) override;
+ int get_max_consider() override;
+ void prepare(int times_considered) override;
std::string to_string(int times_considered) override;
std::string dot_label() override;
int get_value();
#if SIMGRID_HAVE_MC
xbt_dynar_reset(simix_global->actors_vector);
for (std::pair<const aid_t, smx_actor_t> const& kv : simix_global->process_list) {
- xbt_dynar_push_as(simix_global->actors_vector, smx_actor_t, kv.second);
+ auto actor = kv.second;
+ if (actor->simcall_.inspector_ != nullptr)
+ actor->simcall_.mc_max_consider_ = actor->simcall_.inspector_->get_max_consider();
+ xbt_dynar_push_as(simix_global->actors_vector, smx_actor_t, actor);
}
#endif
}
}
void AppSide::handle_simcall(const s_mc_message_simcall_handle_t* message) const
{
- kernel::actor::ActorImpl* process = kernel::actor::ActorImpl::by_PID(message->pid);
- xbt_assert(process != nullptr, "Invalid pid %lu", message->pid);
- process->simcall_handle(message->value);
+ kernel::actor::ActorImpl* process = kernel::actor::ActorImpl::by_PID(message->pid_);
+ xbt_assert(process != nullptr, "Invalid pid %lu", message->pid_);
+ process->simcall_handle(message->times_considered_);
if (channel_.send(MessageType::WAITING))
xbt_die("Could not send MESSAGE_WAITING to model-checker");
}
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();
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,
- 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);
+ 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
/* Server -> client */
struct s_mc_message_simcall_handle_t {
simgrid::mc::MessageType type;
- unsigned long pid;
- int value;
+ unsigned long pid_;
+ int times_considered_;
};
struct s_mc_message_restore_t {
};
/* 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;
*
* This function is generated from src/simix/simcalls.in
*/
-void simgrid::kernel::actor::ActorImpl::simcall_handle(int value) {
- XBT_DEBUG("Handling simcall %p %d: %s", &simcall_, value, SIMIX_simcall_name(simcall_.call_));
- SIMCALL_SET_MC_VALUE(simcall_, value);
+void simgrid::kernel::actor::ActorImpl::simcall_handle(int times_considered_)
+{
+ XBT_DEBUG("Handling simcall %p: %s", &simcall_, SIMIX_simcall_name(simcall_.call_));
+ SIMCALL_SET_MC_VALUE(simcall_, times_considered_);
if (simcall_.inspector_ != nullptr)
- simcall_.inspector_->is_pending(value);
+ simcall_.inspector_->prepare(times_considered_);
if (context_->wannadie())
return;
switch (simcall_.call_) {
smx_actor_t issuer_ = nullptr;
smx_timer_t timeout_cb_ = nullptr; // Callback to timeouts
simgrid::mc::SimcallInspector* inspector_ = nullptr; // makes that simcall observable by the MC
+ unsigned int mc_max_consider_ = 0; // How many times this simcall should be used. If >1, this will be a fork.
int mc_value_ = 0;
std::array<u_smx_scalar, 11> args_ = {};
u_smx_scalar result_ = {};
fd.write(' * This function is generated from src/simix/simcalls.in\n')
fd.write(' */\n')
fd.write(
- 'void simgrid::kernel::actor::ActorImpl::simcall_handle(int value) {\n')
+ 'void simgrid::kernel::actor::ActorImpl::simcall_handle(int times_considered_) {\n')
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(' SIMCALL_SET_MC_VALUE(simcall_, times_considered_);\n')
fd.write(' if (simcall_.inspector_ != nullptr)\n')
- fd.write(' simcall_.inspector_->is_pending(value);\n')
+ fd.write(' simcall_.inspector_->is_pending(times_considered_);\n')
fd.write(' if (context_->wannadie())\n')
fd.write(' return;\n')
