3 #include "src/mc/Session.hpp"
4 #include "src/mc/mc_comm_pattern.hpp"
5 #include "src/mc/mc_private.hpp"
6 #include "src/mc/mc_record.hpp"
7 #include "src/mc/mc_smx.hpp"
8 #include "src/mc/remote/RemoteSimulation.hpp"
10 #include <xbt/asserts.h>
13 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_api, mc, "Logging specific to MC Fasade APIs ");
18 /* Search an enabled transition for the given process.
20 * This can be seen as an iterator returning the next transition of the process.
22 * We only consider the processes that are both
23 * - marked "to be interleaved" in their ActorState (controlled by the checker algorithm).
24 * - which simcall can currently be executed (like a comm where the other partner is already known)
25 * Once we returned the last enabled transition of a process, it is marked done.
27 * Things can get muddled with the WAITANY and TESTANY simcalls, that are rewritten on the fly to a bunch of WAIT
28 * (resp TEST) transitions using the transition.argument field to remember what was the last returned sub-transition.
30 static inline smx_simcall_t MC_state_choose_request_for_process(simgrid::mc::State* state, smx_actor_t actor)
32 /* reset the outgoing transition */
33 simgrid::mc::ActorState* procstate = &state->actor_states_[actor->get_pid()];
34 state->transition_.pid_ = -1;
35 state->transition_.argument_ = -1;
36 state->executed_req_.call_ = SIMCALL_NONE;
38 if (not simgrid::mc::actor_is_enabled(actor))
39 return nullptr; // Not executable in the application
41 smx_simcall_t req = nullptr;
42 switch (actor->simcall_.call_) {
43 case SIMCALL_COMM_WAITANY:
44 state->transition_.argument_ = -1;
45 while (procstate->times_considered < simcall_comm_waitany__get__count(&actor->simcall_)) {
46 if (simgrid::mc::request_is_enabled_by_idx(&actor->simcall_, procstate->times_considered)) {
47 state->transition_.argument_ = procstate->times_considered;
48 ++procstate->times_considered;
51 ++procstate->times_considered;
54 if (procstate->times_considered >= simcall_comm_waitany__get__count(&actor->simcall_))
55 procstate->set_done();
56 if (state->transition_.argument_ != -1)
57 req = &actor->simcall_;
60 case SIMCALL_COMM_TESTANY: {
61 unsigned start_count = procstate->times_considered;
62 state->transition_.argument_ = -1;
63 while (procstate->times_considered < simcall_comm_testany__get__count(&actor->simcall_)) {
64 if (simgrid::mc::request_is_enabled_by_idx(&actor->simcall_, procstate->times_considered)) {
65 state->transition_.argument_ = procstate->times_considered;
66 ++procstate->times_considered;
69 ++procstate->times_considered;
72 if (procstate->times_considered >= simcall_comm_testany__get__count(&actor->simcall_))
73 procstate->set_done();
75 if (state->transition_.argument_ != -1 || start_count == 0)
76 req = &actor->simcall_;
81 case SIMCALL_COMM_WAIT: {
82 simgrid::mc::RemotePtr<simgrid::kernel::activity::CommImpl> remote_act =
83 remote(simcall_comm_wait__getraw__comm(&actor->simcall_));
84 simgrid::mc::Remote<simgrid::kernel::activity::CommImpl> temp_act;
85 mc_model_checker->get_remote_simulation().read(temp_act, remote_act);
86 const simgrid::kernel::activity::CommImpl* act = temp_act.get_buffer();
87 if (act->src_actor_.get() && act->dst_actor_.get())
88 state->transition_.argument_ = 0; // OK
89 else if (act->src_actor_.get() == nullptr && act->type_ == simgrid::kernel::activity::CommImpl::Type::READY &&
91 state->transition_.argument_ = 0; // OK
93 state->transition_.argument_ = -1; // timeout
94 procstate->set_done();
95 req = &actor->simcall_;
99 case SIMCALL_MC_RANDOM: {
100 int min_value = simcall_mc_random__get__min(&actor->simcall_);
101 state->transition_.argument_ = procstate->times_considered + min_value;
102 procstate->times_considered++;
103 if (state->transition_.argument_ == simcall_mc_random__get__max(&actor->simcall_))
104 procstate->set_done();
105 req = &actor->simcall_;
110 procstate->set_done();
111 state->transition_.argument_ = 0;
112 req = &actor->simcall_;
118 state->transition_.pid_ = actor->get_pid();
119 state->executed_req_ = *req;
120 // Fetch the data of the request and translate it:
121 state->internal_req_ = *req;
123 /* The waitany and testany request are transformed into a wait or test request over the corresponding communication
124 * action so it can be treated later by the dependence function. */
125 switch (req->call_) {
126 case SIMCALL_COMM_WAITANY: {
127 state->internal_req_.call_ = SIMCALL_COMM_WAIT;
128 simgrid::kernel::activity::CommImpl* remote_comm;
129 remote_comm = mc_model_checker->get_remote_simulation().read(
130 remote(simcall_comm_waitany__get__comms(req) + state->transition_.argument_));
131 mc_model_checker->get_remote_simulation().read(state->internal_comm_, remote(remote_comm));
132 simcall_comm_wait__set__comm(&state->internal_req_, state->internal_comm_.get_buffer());
133 simcall_comm_wait__set__timeout(&state->internal_req_, 0);
137 case SIMCALL_COMM_TESTANY:
138 state->internal_req_.call_ = SIMCALL_COMM_TEST;
140 if (state->transition_.argument_ > 0) {
141 simgrid::kernel::activity::CommImpl* remote_comm = mc_model_checker->get_remote_simulation().read(
142 remote(simcall_comm_testany__get__comms(req) + state->transition_.argument_));
143 mc_model_checker->get_remote_simulation().read(state->internal_comm_, remote(remote_comm));
146 simcall_comm_test__set__comm(&state->internal_req_, state->internal_comm_.get_buffer());
147 simcall_comm_test__set__result(&state->internal_req_, state->transition_.argument_);
150 case SIMCALL_COMM_WAIT:
151 mc_model_checker->get_remote_simulation().read_bytes(&state->internal_comm_, sizeof(state->internal_comm_),
152 remote(simcall_comm_wait__getraw__comm(req)));
153 simcall_comm_wait__set__comm(&state->executed_req_, state->internal_comm_.get_buffer());
154 simcall_comm_wait__set__comm(&state->internal_req_, state->internal_comm_.get_buffer());
157 case SIMCALL_COMM_TEST:
158 mc_model_checker->get_remote_simulation().read_bytes(&state->internal_comm_, sizeof(state->internal_comm_),
159 remote(simcall_comm_test__getraw__comm(req)));
160 simcall_comm_test__set__comm(&state->executed_req_, state->internal_comm_.get_buffer());
161 simcall_comm_test__set__comm(&state->internal_req_, state->internal_comm_.get_buffer());
165 /* No translation needed */
172 void mc_api::initialize(char** argv)
174 simgrid::mc::session = new simgrid::mc::Session([argv] {
176 while (argv[i] != nullptr && argv[i][0] == '-')
178 xbt_assert(argv[i] != nullptr,
179 "Unable to find a binary to exec on the command line. Did you only pass config flags?");
180 execvp(argv[i], argv + i);
181 xbt_die("The model-checked process failed to exec(): %s", strerror(errno));
185 std::vector<simgrid::mc::ActorInformation>& mc_api::get_actors() const
187 return mc_model_checker->get_remote_simulation().actors();
190 bool mc_api::actor_is_enabled(aid_t pid) const
192 return session->actor_is_enabled(pid);
195 unsigned long mc_api::get_maxpid() const
197 return MC_smx_get_maxpid();
200 void mc_api::copy_incomplete_comm_pattern(const simgrid::mc::State* state) const
202 MC_state_copy_incomplete_communications_pattern((simgrid::mc::State*)state);
205 void mc_api::copy_index_comm_pattern(const simgrid::mc::State* state) const
207 MC_state_copy_index_communications_pattern((simgrid::mc::State*)state);
210 void mc_api::s_initialize() const
212 session->initialize();
215 ModelChecker* mc_api::get_model_checker() const
217 return mc_model_checker;
220 void mc_api::mc_inc_visited_states() const
222 mc_model_checker->visited_states++;
225 void mc_api::mc_inc_executed_trans() const
227 mc_model_checker->executed_transitions++;
230 unsigned long mc_api::mc_get_visited_states() const
232 return mc_model_checker->visited_states;
235 unsigned long mc_api::mc_get_executed_trans() const
237 return mc_model_checker->executed_transitions;
240 bool mc_api::mc_check_deadlock() const
242 return mc_model_checker->checkDeadlock();
245 void mc_api::mc_show_deadlock() const
250 smx_actor_t mc_api::mc_smx_simcall_get_issuer(s_smx_simcall const* req) const
252 return MC_smx_simcall_get_issuer(req);
255 bool mc_api::mc_is_null() const
257 auto is_null = (mc_model_checker == nullptr) ? true : false;
261 Checker* mc_api::mc_get_checker() const
263 return mc_model_checker->getChecker();
266 RemoteSimulation& mc_api::mc_get_remote_simulation() const
268 return mc_model_checker->get_remote_simulation();
271 void mc_api::handle_simcall(Transition const& transition) const
273 mc_model_checker->handle_simcall(transition);
276 void mc_api::mc_wait_for_requests() const
278 mc_model_checker->wait_for_requests();
281 void mc_api::mc_exit(int status) const
283 mc_model_checker->exit(status);
286 std::string const& mc_api::mc_get_host_name(std::string const& hostname) const
288 return mc_model_checker->get_host_name(hostname);
291 void mc_api::mc_dump_record_path() const
293 simgrid::mc::dumpRecordPath();
296 smx_simcall_t mc_api::mc_state_choose_request(simgrid::mc::State* state) const
298 for (auto& actor : mc_model_checker->get_remote_simulation().actors()) {
299 /* Only consider the actors that were marked as interleaving by the checker algorithm */
300 if (not state->actor_states_[actor.copy.get_buffer()->get_pid()].is_todo())
303 smx_simcall_t res = MC_state_choose_request_for_process(state, actor.copy.get_buffer());
310 bool mc_api::request_depend(smx_simcall_t req1, smx_simcall_t req2) const
312 return simgrid::mc::request_depend(req1, req2);
315 std::string mc_api::request_to_string(smx_simcall_t req, int value, RequestType request_type) const
317 return simgrid::mc::request_to_string(req, value, request_type).c_str();
320 std::string mc_api::request_get_dot_output(smx_simcall_t req, int value) const
322 return simgrid::mc::request_get_dot_output(req, value);
325 const char* mc_api::simix_simcall_name(e_smx_simcall_t kind) const
327 return SIMIX_simcall_name(kind);
330 bool mc_api::snapshot_equal(const Snapshot* s1, const Snapshot* s2) const
332 return simgrid::mc::snapshot_equal(s1, s2);
335 simgrid::mc::Snapshot* mc_api::take_snapshot(int num_state) const
337 auto snapshot = new simgrid::mc::Snapshot(num_state);
341 void mc_api::s_close() const
346 void mc_api::s_restore_initial_state() const
348 session->restore_initial_state();
351 void mc_api::execute(Transition const& transition)
353 session->execute(transition);
356 void mc_api::s_log_state() const
358 session->log_state();
362 } // namespace simgrid