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 simgrid::smpi::Request mpi_request =
206 mc_model_checker->process().read<simgrid::smpi::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 simgrid::smpi::Request mpi_request;
237 mc_model_checker->process().read(
238 &mpi_request, remote((simgrid::smpi::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, remote(comm->mbox ? &comm->mbox->name_ : &comm->mbox_cpy->name_));
248 pattern->rdv = mc_model_checker->process().read_string(remote_name);
249 pattern->dst_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->dst_proc))->pid;
250 pattern->dst_host = MC_smx_actor_get_host_name(issuer);
252 xbt_die("Unexpected call_type %i", (int) call_type);
254 XBT_DEBUG("Insert incomplete comm pattern %p for process %lu",
255 pattern.get(), issuer->pid);
257 xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
258 simgrid::mc::PatternCommunication* pattern2 = pattern.release();
259 xbt_dynar_push(dynar, &pattern2);
263 void CommunicationDeterminismChecker::complete_comm_pattern(
264 xbt_dynar_t list, simgrid::mc::RemotePtr<simgrid::kernel::activity::Comm> comm_addr,
265 unsigned int issuer, int backtracking)
267 simgrid::mc::PatternCommunication* current_comm_pattern;
268 unsigned int cursor = 0;
269 std::unique_ptr<simgrid::mc::PatternCommunication> comm_pattern;
272 /* Complete comm pattern */
273 xbt_dynar_foreach(xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, current_comm_pattern)
274 if (remote(current_comm_pattern->comm_addr) == comm_addr) {
275 update_comm_pattern(current_comm_pattern, comm_addr);
277 simgrid::mc::PatternCommunication* temp;
279 xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t),
281 comm_pattern = std::unique_ptr<simgrid::mc::PatternCommunication>(temp);
282 XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", issuer, cursor);
287 xbt_die("Corresponding communication not found!");
289 simgrid::mc::PatternCommunicationList* pattern = xbt_dynar_get_as(
290 initial_communications_pattern, issuer, simgrid::mc::PatternCommunicationList*);
292 if (!this->initial_communications_pattern_done)
293 /* Store comm pattern */
294 pattern->list.push_back(std::move(comm_pattern));
296 /* Evaluate comm determinism */
297 this->deterministic_comm_pattern(issuer, comm_pattern.get(), backtracking);
298 pattern->index_comm++;
302 CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session& session)
308 CommunicationDeterminismChecker::~CommunicationDeterminismChecker() = default;
310 RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override
313 for (auto const& state : stack_)
314 res.push_back(state->getTransition());
318 std::vector<std::string> CommunicationDeterminismChecker::getTextualTrace() // override
320 std::vector<std::string> trace;
321 for (auto const& state : stack_) {
322 smx_simcall_t req = &state->executed_req;
324 trace.push_back(simgrid::mc::request_to_string(
325 req, state->transition.argument, simgrid::mc::RequestType::executed));
330 void CommunicationDeterminismChecker::logState() // override
333 if (_sg_mc_comms_determinism &&
334 !this->recv_deterministic &&
335 this->send_deterministic) {
336 XBT_INFO("******************************************************");
337 XBT_INFO("**** Only-send-deterministic communication pattern ****");
338 XBT_INFO("******************************************************");
339 XBT_INFO("%s", this->recv_diff);
340 } else if(_sg_mc_comms_determinism &&
341 !this->send_deterministic &&
342 this->recv_deterministic) {
343 XBT_INFO("******************************************************");
344 XBT_INFO("**** Only-recv-deterministic communication pattern ****");
345 XBT_INFO("******************************************************");
346 XBT_INFO("%s", this->send_diff);
348 XBT_INFO("Expanded states = %lu", expandedStatesCount_);
349 XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
350 XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
351 XBT_INFO("Send-deterministic : %s", !this->send_deterministic ? "No" : "Yes");
352 if (_sg_mc_comms_determinism)
353 XBT_INFO("Recv-deterministic : %s",
354 !this->recv_deterministic ? "No" : "Yes");
357 void CommunicationDeterminismChecker::prepare()
359 const int maxpid = MC_smx_get_maxpid();
361 // Create initial_communications_pattern elements:
362 initial_communications_pattern = simgrid::xbt::newDeleteDynar<simgrid::mc::PatternCommunicationList*>();
363 for (int i = 0; i < maxpid; i++) {
364 simgrid::mc::PatternCommunicationList* process_list_pattern = new simgrid::mc::PatternCommunicationList();
365 xbt_dynar_insert_at(initial_communications_pattern, i, &process_list_pattern);
368 // Create incomplete_communications_pattern elements:
369 incomplete_communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
370 for (int i = 0; i < maxpid; i++) {
371 xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(simgrid::mc::PatternCommunication*), nullptr);
372 xbt_dynar_insert_at(incomplete_communications_pattern, i, &process_pattern);
375 std::unique_ptr<simgrid::mc::State> initial_state =
376 std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
378 XBT_DEBUG("********* Start communication determinism verification *********");
380 /* Get an enabled actor and insert it in the interleave set of the initial state */
381 for (auto& actor : mc_model_checker->process().actors())
382 if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer()))
383 initial_state->interleave(actor.copy.getBuffer());
385 stack_.push_back(std::move(initial_state));
389 bool all_communications_are_finished()
391 for (size_t current_actor = 1; current_actor < MC_smx_get_maxpid(); current_actor++) {
392 xbt_dynar_t pattern = xbt_dynar_get_as(incomplete_communications_pattern, current_actor, xbt_dynar_t);
393 if (!xbt_dynar_is_empty(pattern)) {
394 XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
401 void CommunicationDeterminismChecker::restoreState()
403 /* Intermediate backtracking */
405 simgrid::mc::State* state = stack_.back().get();
406 if (state->system_state) {
407 simgrid::mc::restore_snapshot(state->system_state);
408 MC_restore_communications_pattern(state);
413 /* Restore the initial state */
414 simgrid::mc::session->restoreInitialState();
416 // int n = xbt_dynar_length(incomplete_communications_pattern);
417 unsigned n = MC_smx_get_maxpid();
418 assert(n == xbt_dynar_length(incomplete_communications_pattern));
419 assert(n == xbt_dynar_length(initial_communications_pattern));
420 for (unsigned j=0; j < n ; j++) {
421 xbt_dynar_reset((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, j, xbt_dynar_t));
422 xbt_dynar_get_as(initial_communications_pattern, j, simgrid::mc::PatternCommunicationList*)->index_comm = 0;
425 /* Traverse the stack from the state at position start and re-execute the transitions */
426 for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
427 if (state == stack_.back())
430 int req_num = state->transition.argument;
431 smx_simcall_t saved_req = &state->executed_req;
432 xbt_assert(saved_req);
434 /* because we got a copy of the executed request, we have to fetch the
435 real one, pointed by the request field of the issuer process */
437 const smx_actor_t issuer = MC_smx_simcall_get_issuer(saved_req);
438 smx_simcall_t req = &issuer->simcall;
440 /* TODO : handle test and testany simcalls */
441 e_mc_call_type_t call = MC_get_call_type(req);
442 mc_model_checker->handle_simcall(state->transition);
443 MC_handle_comm_pattern(call, req, req_num, nullptr, 1);
444 mc_model_checker->wait_for_requests();
446 /* Update statistics */
447 mc_model_checker->visited_states++;
448 mc_model_checker->executed_transitions++;
452 void CommunicationDeterminismChecker::main(void)
454 std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
455 smx_simcall_t req = nullptr;
457 while (!stack_.empty()) {
459 /* Get current state */
460 simgrid::mc::State* state = stack_.back().get();
462 XBT_DEBUG("**************************************************");
463 XBT_DEBUG("Exploration depth = %zi (state = %d, interleaved processes = %zd)",
464 stack_.size(), state->num,
465 state->interleaveSize());
467 /* Update statistics */
468 mc_model_checker->visited_states++;
470 if (stack_.size() <= (std::size_t) _sg_mc_max_depth
471 && (req = MC_state_get_request(state)) != nullptr
472 && (visited_state == nullptr)) {
474 int req_num = state->transition.argument;
476 XBT_DEBUG("Execute: %s",
477 simgrid::mc::request_to_string(
478 req, req_num, simgrid::mc::RequestType::simix).c_str());
481 if (dot_output != nullptr)
482 req_str = simgrid::mc::request_get_dot_output(req, req_num);
484 mc_model_checker->executed_transitions++;
486 /* TODO : handle test and testany simcalls */
487 e_mc_call_type_t call = MC_CALL_TYPE_NONE;
488 if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
489 call = MC_get_call_type(req);
491 /* Answer the request */
492 mc_model_checker->handle_simcall(state->transition);
493 /* After this call req is no longer useful */
495 if (!this->initial_communications_pattern_done)
496 MC_handle_comm_pattern(call, req, req_num, initial_communications_pattern, 0);
498 MC_handle_comm_pattern(call, req, req_num, nullptr, 0);
500 /* Wait for requests (schedules processes) */
501 mc_model_checker->wait_for_requests();
503 /* Create the new expanded state */
504 std::unique_ptr<simgrid::mc::State> next_state =
505 std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
507 /* If comm determinism verification, we cannot stop the exploration if
508 some communications are not finished (at least, data are transferred).
509 These communications are incomplete and they cannot be analyzed and
510 compared with the initial pattern. */
511 bool compare_snapshots = all_communications_are_finished()
512 && this->initial_communications_pattern_done;
514 if (_sg_mc_max_visited_states == 0 ||
515 (visited_state = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), compare_snapshots)) ==
518 /* Get enabled actors and insert them in the interleave set of the next state */
519 for (auto& actor : mc_model_checker->process().actors())
520 if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer()))
521 next_state->interleave(actor.copy.getBuffer());
523 if (dot_output != nullptr)
524 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
525 state->num, next_state->num, req_str.c_str());
527 } else if (dot_output != nullptr)
528 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
529 visited_state->original_num == -1 ? visited_state->num : visited_state->original_num, req_str.c_str());
531 stack_.push_back(std::move(next_state));
535 if (stack_.size() > (std::size_t) _sg_mc_max_depth)
536 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
537 else if (visited_state != nullptr)
538 XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.",
539 visited_state->original_num == -1 ? visited_state->num : visited_state->original_num);
541 XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
544 if (!this->initial_communications_pattern_done)
545 this->initial_communications_pattern_done = 1;
547 /* Trash the current state, no longer needed */
548 XBT_DEBUG("Delete state %d at depth %zi",
549 state->num, stack_.size());
552 visited_state = nullptr;
554 /* Check for deadlocks */
555 if (mc_model_checker->checkDeadlock()) {
557 throw new simgrid::mc::DeadlockError();
560 while (!stack_.empty()) {
561 std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
563 if (state->interleaveSize()
564 && stack_.size() < (std::size_t) _sg_mc_max_depth) {
565 /* We found a back-tracking point, let's loop */
566 XBT_DEBUG("Back-tracking to state %d at depth %zi",
567 state->num, stack_.size() + 1);
568 stack_.push_back(std::move(state));
570 this->restoreState();
572 XBT_DEBUG("Back-tracking to state %d at depth %zi done",
573 stack_.back()->num, stack_.size());
577 XBT_DEBUG("Delete state %d at depth %zi",
578 state->num, stack_.size() + 1);
584 simgrid::mc::session->logState();
587 void CommunicationDeterminismChecker::run()
589 XBT_INFO("Check communication determinism");
590 simgrid::mc::session->initialize();
597 Checker* createCommunicationDeterminismChecker(Session& session)
599 return new CommunicationDeterminismChecker(session);