1 /* Copyright (c) 2008-2017. The SimGrid Team. All rights reserved. */
3 /* This program is free software; you can redistribute it and/or modify it
4 * under the terms of the license (GNU LGPL) which comes with this package. */
9 #include <xbt/dynar.hpp>
11 #include <xbt/sysdep.h>
13 #include "src/mc/Transition.hpp"
14 #include "src/mc/VisitedState.hpp"
15 #include "src/mc/checker/CommunicationDeterminismChecker.hpp"
16 #include "src/mc/mc_exit.h"
17 #include "src/mc/mc_private.h"
18 #include "src/mc/mc_record.h"
19 #include "src/mc/mc_request.h"
20 #include "src/mc/mc_safety.h"
21 #include "src/mc/mc_smx.h"
22 #include "src/mc/mc_state.h"
23 #include "src/mc/remote/Client.hpp"
25 using simgrid::mc::remote;
27 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_determinism, mc,
28 "Logging specific to MC communication determinism detection");
30 /********** Global variables **********/
32 xbt_dynar_t initial_communications_pattern;
33 xbt_dynar_t incomplete_communications_pattern;
35 /********** Static functions ***********/
37 static e_mc_comm_pattern_difference_t compare_comm_pattern(simgrid::mc::PatternCommunication* comm1, simgrid::mc::PatternCommunication* comm2)
39 if(comm1->type != comm2->type)
41 if (comm1->rdv != comm2->rdv)
43 if (comm1->src_proc != comm2->src_proc)
45 if (comm1->dst_proc != comm2->dst_proc)
47 if (comm1->tag != comm2->tag)
49 if (comm1->data.size() != comm2->data.size())
50 return DATA_SIZE_DIFF;
51 if (comm1->data != comm2->data)
56 static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int process, simgrid::mc::PatternCommunication* comm, unsigned int cursor) {
59 if (comm->type == simgrid::mc::PatternCommunicationType::send)
60 type = bprintf("The send communications pattern of the process %d is different!", process - 1);
62 type = bprintf("The recv communications pattern of the process %d is different!", process - 1);
66 res = bprintf("%s Different type for communication #%d", type, cursor);
69 res = bprintf("%s Different rdv for communication #%d", type, cursor);
72 res = bprintf("%s Different tag for communication #%d", type, cursor);
75 res = bprintf("%s Different source for communication #%d", type, cursor);
78 res = bprintf("%s Different destination for communication #%d", type, cursor);
81 res = bprintf("%s\n Different data size for communication #%d", type, cursor);
84 res = bprintf("%s\n Different data for communication #%d", type, cursor);
94 static void update_comm_pattern(
95 simgrid::mc::PatternCommunication* comm_pattern,
96 simgrid::mc::RemotePtr<simgrid::kernel::activity::Comm> comm_addr)
99 simgrid::mc::Remote<simgrid::kernel::activity::Comm> temp_comm;
100 mc_model_checker->process().read(temp_comm, comm_addr);
101 simgrid::kernel::activity::Comm* comm = temp_comm.getBuffer();
103 smx_actor_t src_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->src_proc));
104 smx_actor_t dst_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->dst_proc));
105 comm_pattern->src_proc = src_proc->pid;
106 comm_pattern->dst_proc = dst_proc->pid;
107 comm_pattern->src_host = MC_smx_actor_get_host_name(src_proc);
108 comm_pattern->dst_host = MC_smx_actor_get_host_name(dst_proc);
109 if (comm_pattern->data.size() == 0 && comm->src_buff != nullptr) {
111 mc_model_checker->process().read(
112 &buff_size, remote(comm->dst_buff_size));
113 comm_pattern->data.resize(buff_size);
114 mc_model_checker->process().read_bytes(
115 comm_pattern->data.data(), comm_pattern->data.size(),
116 remote(comm->src_buff));
123 void CommunicationDeterminismChecker::deterministic_comm_pattern(
124 int process, simgrid::mc::PatternCommunication* comm, int backtracking)
126 simgrid::mc::PatternCommunicationList* list =
127 xbt_dynar_get_as(initial_communications_pattern, process, simgrid::mc::PatternCommunicationList*);
130 e_mc_comm_pattern_difference_t diff =
131 compare_comm_pattern(list->list[list->index_comm].get(), comm);
133 if (diff != NONE_DIFF) {
134 if (comm->type == simgrid::mc::PatternCommunicationType::send) {
135 this->send_deterministic = 0;
136 if (this->send_diff != nullptr)
137 xbt_free(this->send_diff);
138 this->send_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
140 this->recv_deterministic = 0;
141 if (this->recv_diff != nullptr)
142 xbt_free(this->recv_diff);
143 this->recv_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
145 if(_sg_mc_send_determinism && !this->send_deterministic){
146 XBT_INFO("*********************************************************");
147 XBT_INFO("***** Non-send-deterministic communications pattern *****");
148 XBT_INFO("*********************************************************");
149 XBT_INFO("%s", this->send_diff);
150 xbt_free(this->send_diff);
151 this->send_diff = nullptr;
152 simgrid::mc::session->logState();
153 mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
154 }else if(_sg_mc_comms_determinism
155 && (!this->send_deterministic && !this->recv_deterministic)) {
156 XBT_INFO("****************************************************");
157 XBT_INFO("***** Non-deterministic communications pattern *****");
158 XBT_INFO("****************************************************");
159 XBT_INFO("%s", this->send_diff);
160 XBT_INFO("%s", this->recv_diff);
161 xbt_free(this->send_diff);
162 this->send_diff = nullptr;
163 xbt_free(this->recv_diff);
164 this->recv_diff = nullptr;
165 simgrid::mc::session->logState();
166 mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
172 /********** Non Static functions ***********/
174 void CommunicationDeterminismChecker::get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking)
176 const smx_actor_t issuer = MC_smx_simcall_get_issuer(request);
177 simgrid::mc::PatternCommunicationList* initial_pattern = xbt_dynar_get_as(
178 initial_communications_pattern, issuer->pid, simgrid::mc::PatternCommunicationList*);
179 xbt_dynar_t incomplete_pattern = xbt_dynar_get_as(
180 incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
182 std::unique_ptr<simgrid::mc::PatternCommunication> pattern =
183 std::unique_ptr<simgrid::mc::PatternCommunication>(
184 new simgrid::mc::PatternCommunication());
186 initial_pattern->index_comm + xbt_dynar_length(incomplete_pattern);
188 if (call_type == MC_CALL_TYPE_SEND) {
189 /* Create comm pattern */
190 pattern->type = simgrid::mc::PatternCommunicationType::send;
191 pattern->comm_addr = simcall_comm_isend__get__result(request);
193 simgrid::mc::Remote<simgrid::kernel::activity::Comm> temp_synchro;
194 mc_model_checker->process().read(temp_synchro, remote(
195 static_cast<simgrid::kernel::activity::Comm*>(pattern->comm_addr)));
196 simgrid::kernel::activity::Comm* synchro =
197 static_cast<simgrid::kernel::activity::Comm*>(temp_synchro.getBuffer());
199 char* remote_name = mc_model_checker->process().read<char*>(
200 (std::uint64_t)(synchro->mbox ? &synchro->mbox->name : &synchro->mbox_cpy->name));
201 pattern->rdv = mc_model_checker->process().read_string(remote_name);
202 pattern->src_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(synchro->src_proc))->pid;
203 pattern->src_host = MC_smx_actor_get_host_name(issuer);
205 struct s_smpi_mpi_request mpi_request =
206 mc_model_checker->process().read<s_smpi_mpi_request>(
207 (std::uint64_t) simcall_comm_isend__get__data(request));
208 pattern->tag = mpi_request.tag;
210 if (synchro->src_buff != nullptr){
211 pattern->data.resize(synchro->src_buff_size);
212 mc_model_checker->process().read_bytes(
213 pattern->data.data(), pattern->data.size(),
214 remote(synchro->src_buff));
216 if(mpi_request.detached){
217 if (!this->initial_communications_pattern_done) {
218 /* Store comm pattern */
219 simgrid::mc::PatternCommunicationList* list = xbt_dynar_get_as(
220 initial_communications_pattern, pattern->src_proc,
221 simgrid::mc::PatternCommunicationList*);
222 list->list.push_back(std::move(pattern));
224 /* Evaluate comm determinism */
225 this->deterministic_comm_pattern(pattern->src_proc, pattern.get(), backtracking);
227 initial_communications_pattern, pattern->src_proc, simgrid::mc::PatternCommunicationList*
232 } else if (call_type == MC_CALL_TYPE_RECV) {
233 pattern->type = simgrid::mc::PatternCommunicationType::receive;
234 pattern->comm_addr = simcall_comm_irecv__get__result(request);
236 struct s_smpi_mpi_request mpi_request;
237 mc_model_checker->process().read(
238 &mpi_request, remote((struct s_smpi_mpi_request*)simcall_comm_irecv__get__data(request)));
239 pattern->tag = mpi_request.tag;
241 simgrid::mc::Remote<simgrid::kernel::activity::Comm> temp_comm;
242 mc_model_checker->process().read(temp_comm, remote(
243 static_cast<simgrid::kernel::activity::Comm*>(pattern->comm_addr)));
244 simgrid::kernel::activity::Comm* comm = temp_comm.getBuffer();
247 mc_model_checker->process().read(&remote_name,
248 remote(comm->mbox ? &comm->mbox->name : &comm->mbox_cpy->name));
249 pattern->rdv = mc_model_checker->process().read_string(remote_name);
250 pattern->dst_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->dst_proc))->pid;
251 pattern->dst_host = MC_smx_actor_get_host_name(issuer);
253 xbt_die("Unexpected call_type %i", (int) call_type);
255 XBT_DEBUG("Insert incomplete comm pattern %p for process %lu",
256 pattern.get(), issuer->pid);
258 xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
259 simgrid::mc::PatternCommunication* pattern2 = pattern.release();
260 xbt_dynar_push(dynar, &pattern2);
264 void CommunicationDeterminismChecker::complete_comm_pattern(
265 xbt_dynar_t list, simgrid::mc::RemotePtr<simgrid::kernel::activity::Comm> comm_addr,
266 unsigned int issuer, int backtracking)
268 simgrid::mc::PatternCommunication* current_comm_pattern;
269 unsigned int cursor = 0;
270 std::unique_ptr<simgrid::mc::PatternCommunication> comm_pattern;
273 /* Complete comm pattern */
274 xbt_dynar_foreach(xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, current_comm_pattern)
275 if (remote(current_comm_pattern->comm_addr) == comm_addr) {
276 update_comm_pattern(current_comm_pattern, comm_addr);
278 simgrid::mc::PatternCommunication* temp;
280 xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t),
282 comm_pattern = std::unique_ptr<simgrid::mc::PatternCommunication>(temp);
283 XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", issuer, cursor);
288 xbt_die("Corresponding communication not found!");
290 simgrid::mc::PatternCommunicationList* pattern = xbt_dynar_get_as(
291 initial_communications_pattern, issuer, simgrid::mc::PatternCommunicationList*);
293 if (!this->initial_communications_pattern_done)
294 /* Store comm pattern */
295 pattern->list.push_back(std::move(comm_pattern));
297 /* Evaluate comm determinism */
298 this->deterministic_comm_pattern(issuer, comm_pattern.get(), backtracking);
299 pattern->index_comm++;
303 CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session& session)
309 CommunicationDeterminismChecker::~CommunicationDeterminismChecker() = default;
311 RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override
314 for (auto const& state : stack_)
315 res.push_back(state->getTransition());
319 std::vector<std::string> CommunicationDeterminismChecker::getTextualTrace() // override
321 std::vector<std::string> trace;
322 for (auto const& state : stack_) {
323 smx_simcall_t req = &state->executed_req;
325 trace.push_back(simgrid::mc::request_to_string(
326 req, state->transition.argument, simgrid::mc::RequestType::executed));
331 void CommunicationDeterminismChecker::logState() // override
334 if (_sg_mc_comms_determinism &&
335 !this->recv_deterministic &&
336 this->send_deterministic) {
337 XBT_INFO("******************************************************");
338 XBT_INFO("**** Only-send-deterministic communication pattern ****");
339 XBT_INFO("******************************************************");
340 XBT_INFO("%s", this->recv_diff);
341 } else if(_sg_mc_comms_determinism &&
342 !this->send_deterministic &&
343 this->recv_deterministic) {
344 XBT_INFO("******************************************************");
345 XBT_INFO("**** Only-recv-deterministic communication pattern ****");
346 XBT_INFO("******************************************************");
347 XBT_INFO("%s", this->send_diff);
349 XBT_INFO("Expanded states = %lu", expandedStatesCount_);
350 XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
351 XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
352 XBT_INFO("Send-deterministic : %s", !this->send_deterministic ? "No" : "Yes");
353 if (_sg_mc_comms_determinism)
354 XBT_INFO("Recv-deterministic : %s",
355 !this->recv_deterministic ? "No" : "Yes");
358 void CommunicationDeterminismChecker::prepare()
360 const int maxpid = MC_smx_get_maxpid();
362 // Create initial_communications_pattern elements:
363 initial_communications_pattern = simgrid::xbt::newDeleteDynar<simgrid::mc::PatternCommunicationList*>();
364 for (int i = 0; i < maxpid; i++) {
365 simgrid::mc::PatternCommunicationList* process_list_pattern = new simgrid::mc::PatternCommunicationList();
366 xbt_dynar_insert_at(initial_communications_pattern, i, &process_list_pattern);
369 // Create incomplete_communications_pattern elements:
370 incomplete_communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
371 for (int i = 0; i < maxpid; i++) {
372 xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(simgrid::mc::PatternCommunication*), nullptr);
373 xbt_dynar_insert_at(incomplete_communications_pattern, i, &process_pattern);
376 std::unique_ptr<simgrid::mc::State> initial_state =
377 std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
379 XBT_DEBUG("********* Start communication determinism verification *********");
381 /* Get an enabled actor and insert it in the interleave set of the initial state */
382 for (auto& actor : mc_model_checker->process().actors())
383 if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer()))
384 initial_state->interleave(actor.copy.getBuffer());
386 stack_.push_back(std::move(initial_state));
390 bool all_communications_are_finished()
392 for (size_t current_actor = 1; current_actor < MC_smx_get_maxpid(); current_actor++) {
393 xbt_dynar_t pattern = xbt_dynar_get_as(incomplete_communications_pattern, current_actor, xbt_dynar_t);
394 if (!xbt_dynar_is_empty(pattern)) {
395 XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
402 void CommunicationDeterminismChecker::restoreState()
404 /* Intermediate backtracking */
406 simgrid::mc::State* state = stack_.back().get();
407 if (state->system_state) {
408 simgrid::mc::restore_snapshot(state->system_state);
409 MC_restore_communications_pattern(state);
414 /* Restore the initial state */
415 simgrid::mc::session->restoreInitialState();
417 // int n = xbt_dynar_length(incomplete_communications_pattern);
418 unsigned n = MC_smx_get_maxpid();
419 assert(n == xbt_dynar_length(incomplete_communications_pattern));
420 assert(n == xbt_dynar_length(initial_communications_pattern));
421 for (unsigned j=0; j < n ; j++) {
422 xbt_dynar_reset((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, j, xbt_dynar_t));
423 xbt_dynar_get_as(initial_communications_pattern, j, simgrid::mc::PatternCommunicationList*)->index_comm = 0;
426 /* Traverse the stack from the state at position start and re-execute the transitions */
427 for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
428 if (state == stack_.back())
431 int req_num = state->transition.argument;
432 smx_simcall_t saved_req = &state->executed_req;
433 xbt_assert(saved_req);
435 /* because we got a copy of the executed request, we have to fetch the
436 real one, pointed by the request field of the issuer process */
438 const smx_actor_t issuer = MC_smx_simcall_get_issuer(saved_req);
439 smx_simcall_t req = &issuer->simcall;
441 /* TODO : handle test and testany simcalls */
442 e_mc_call_type_t call = MC_get_call_type(req);
443 mc_model_checker->handle_simcall(state->transition);
444 MC_handle_comm_pattern(call, req, req_num, nullptr, 1);
445 mc_model_checker->wait_for_requests();
447 /* Update statistics */
448 mc_model_checker->visited_states++;
449 mc_model_checker->executed_transitions++;
453 void CommunicationDeterminismChecker::main(void)
455 std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
456 smx_simcall_t req = nullptr;
458 while (!stack_.empty()) {
460 /* Get current state */
461 simgrid::mc::State* state = stack_.back().get();
463 XBT_DEBUG("**************************************************");
464 XBT_DEBUG("Exploration depth = %zi (state = %d, interleaved processes = %zd)",
465 stack_.size(), state->num,
466 state->interleaveSize());
468 /* Update statistics */
469 mc_model_checker->visited_states++;
471 if (stack_.size() <= (std::size_t) _sg_mc_max_depth
472 && (req = MC_state_get_request(state)) != nullptr
473 && (visited_state == nullptr)) {
475 int req_num = state->transition.argument;
477 XBT_DEBUG("Execute: %s",
478 simgrid::mc::request_to_string(
479 req, req_num, simgrid::mc::RequestType::simix).c_str());
482 if (dot_output != nullptr)
483 req_str = simgrid::mc::request_get_dot_output(req, req_num);
485 mc_model_checker->executed_transitions++;
487 /* TODO : handle test and testany simcalls */
488 e_mc_call_type_t call = MC_CALL_TYPE_NONE;
489 if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
490 call = MC_get_call_type(req);
492 /* Answer the request */
493 mc_model_checker->handle_simcall(state->transition);
494 /* After this call req is no longer useful */
496 if (!this->initial_communications_pattern_done)
497 MC_handle_comm_pattern(call, req, req_num, initial_communications_pattern, 0);
499 MC_handle_comm_pattern(call, req, req_num, nullptr, 0);
501 /* Wait for requests (schedules processes) */
502 mc_model_checker->wait_for_requests();
504 /* Create the new expanded state */
505 std::unique_ptr<simgrid::mc::State> next_state =
506 std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
508 /* If comm determinism verification, we cannot stop the exploration if
509 some communications are not finished (at least, data are transferred).
510 These communications are incomplete and they cannot be analyzed and
511 compared with the initial pattern. */
512 bool compare_snapshots = all_communications_are_finished()
513 && this->initial_communications_pattern_done;
515 if (_sg_mc_max_visited_states == 0 ||
516 (visited_state = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), compare_snapshots)) ==
519 /* Get enabled actors and insert them in the interleave set of the next state */
520 for (auto& actor : mc_model_checker->process().actors())
521 if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer()))
522 next_state->interleave(actor.copy.getBuffer());
524 if (dot_output != nullptr)
525 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
526 state->num, next_state->num, req_str.c_str());
528 } else if (dot_output != nullptr)
529 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
530 visited_state->original_num == -1 ? visited_state->num : visited_state->original_num, req_str.c_str());
532 stack_.push_back(std::move(next_state));
536 if (stack_.size() > (std::size_t) _sg_mc_max_depth)
537 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
538 else if (visited_state != nullptr)
539 XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.",
540 visited_state->original_num == -1 ? visited_state->num : visited_state->original_num);
542 XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
545 if (!this->initial_communications_pattern_done)
546 this->initial_communications_pattern_done = 1;
548 /* Trash the current state, no longer needed */
549 XBT_DEBUG("Delete state %d at depth %zi",
550 state->num, stack_.size());
553 visited_state = nullptr;
555 /* Check for deadlocks */
556 if (mc_model_checker->checkDeadlock()) {
558 throw new simgrid::mc::DeadlockError();
561 while (!stack_.empty()) {
562 std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
564 if (state->interleaveSize()
565 && stack_.size() < (std::size_t) _sg_mc_max_depth) {
566 /* We found a back-tracking point, let's loop */
567 XBT_DEBUG("Back-tracking to state %d at depth %zi",
568 state->num, stack_.size() + 1);
569 stack_.push_back(std::move(state));
571 this->restoreState();
573 XBT_DEBUG("Back-tracking to state %d at depth %zi done",
574 stack_.back()->num, stack_.size());
578 XBT_DEBUG("Delete state %d at depth %zi",
579 state->num, stack_.size() + 1);
585 simgrid::mc::session->logState();
588 void CommunicationDeterminismChecker::run()
590 XBT_INFO("Check communication determinism");
591 simgrid::mc::session->initialize();
598 Checker* createCommunicationDeterminismChecker(Session& session)
600 return new CommunicationDeterminismChecker(session);