1 /* Copyright (c) 2008-2015. The SimGrid Team.
2 * All rights reserved. */
4 /* This program is free software; you can redistribute it and/or modify it
5 * under the terms of the license (GNU LGPL) which comes with this package. */
10 #include <xbt/dynar.hpp>
12 #include <xbt/sysdep.h>
14 #include "src/mc/mc_state.h"
15 #include "src/mc/mc_comm_pattern.h"
16 #include "src/mc/mc_request.h"
17 #include "src/mc/mc_safety.h"
18 #include "src/mc/mc_private.h"
19 #include "src/mc/mc_record.h"
20 #include "src/mc/mc_smx.h"
21 #include "src/mc/Client.hpp"
22 #include "src/mc/CommunicationDeterminismChecker.hpp"
23 #include "src/mc/mc_exit.h"
24 #include "src/mc/VisitedState.hpp"
25 #include "src/mc/Transition.hpp"
27 using simgrid::mc::remote;
29 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_determinism, mc,
30 "Logging specific to MC communication determinism detection");
32 /********** Global variables **********/
34 xbt_dynar_t initial_communications_pattern;
35 xbt_dynar_t incomplete_communications_pattern;
37 /********** Static functions ***********/
39 static e_mc_comm_pattern_difference_t compare_comm_pattern(simgrid::mc::PatternCommunication* comm1, simgrid::mc::PatternCommunication* comm2)
41 if(comm1->type != comm2->type)
43 if (comm1->rdv != comm2->rdv)
45 if (comm1->src_proc != comm2->src_proc)
47 if (comm1->dst_proc != comm2->dst_proc)
49 if (comm1->tag != comm2->tag)
51 if (comm1->data.size() != comm2->data.size())
52 return DATA_SIZE_DIFF;
53 if (comm1->data != comm2->data)
58 static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int process, simgrid::mc::PatternCommunication* comm, unsigned int cursor) {
61 if (comm->type == simgrid::mc::PatternCommunicationType::send)
62 type = bprintf("The send communications pattern of the process %d is different!", process - 1);
64 type = bprintf("The recv communications pattern of the process %d is different!", process - 1);
68 res = bprintf("%s Different type for communication #%d", type, cursor);
71 res = bprintf("%s Different rdv for communication #%d", type, cursor);
74 res = bprintf("%s Different tag for communication #%d", type, cursor);
77 res = bprintf("%s Different source for communication #%d", type, cursor);
80 res = bprintf("%s Different destination for communication #%d", type, cursor);
83 res = bprintf("%s\n Different data size for communication #%d", type, cursor);
86 res = bprintf("%s\n Different data for communication #%d", type, cursor);
96 static void update_comm_pattern(
97 simgrid::mc::PatternCommunication* comm_pattern,
98 simgrid::mc::RemotePtr<simgrid::simix::Comm> comm_addr)
100 // HACK, type punning
101 simgrid::mc::Remote<simgrid::simix::Comm> temp_comm;
102 mc_model_checker->process().read(temp_comm, comm_addr);
103 simgrid::simix::Comm* comm =
104 static_cast<simgrid::simix::Comm*>(temp_comm.data());
106 smx_process_t src_proc = mc_model_checker->process().resolveProcess(
107 simgrid::mc::remote(comm->src_proc));
108 smx_process_t dst_proc = mc_model_checker->process().resolveProcess(
109 simgrid::mc::remote(comm->dst_proc));
110 comm_pattern->src_proc = src_proc->pid;
111 comm_pattern->dst_proc = dst_proc->pid;
112 comm_pattern->src_host = MC_smx_process_get_host_name(src_proc);
113 comm_pattern->dst_host = MC_smx_process_get_host_name(dst_proc);
114 if (comm_pattern->data.size() == 0 && comm->src_buff != nullptr) {
116 mc_model_checker->process().read(
117 &buff_size, remote(comm->dst_buff_size));
118 comm_pattern->data.resize(buff_size);
119 mc_model_checker->process().read_bytes(
120 comm_pattern->data.data(), comm_pattern->data.size(),
121 remote(comm->src_buff));
128 void CommunicationDeterminismChecker::deterministic_comm_pattern(
129 int process, simgrid::mc::PatternCommunication* comm, int backtracking)
131 simgrid::mc::PatternCommunicationList* list =
132 xbt_dynar_get_as(initial_communications_pattern, process, simgrid::mc::PatternCommunicationList*);
135 e_mc_comm_pattern_difference_t diff =
136 compare_comm_pattern(list->list[list->index_comm].get(), comm);
138 if (diff != NONE_DIFF) {
139 if (comm->type == simgrid::mc::PatternCommunicationType::send) {
140 this->send_deterministic = 0;
141 if (this->send_diff != nullptr)
142 xbt_free(this->send_diff);
143 this->send_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
145 this->recv_deterministic = 0;
146 if (this->recv_diff != nullptr)
147 xbt_free(this->recv_diff);
148 this->recv_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
150 if(_sg_mc_send_determinism && !this->send_deterministic){
151 XBT_INFO("*********************************************************");
152 XBT_INFO("***** Non-send-deterministic communications pattern *****");
153 XBT_INFO("*********************************************************");
154 XBT_INFO("%s", this->send_diff);
155 xbt_free(this->send_diff);
156 this->send_diff = nullptr;
157 simgrid::mc::session->logState();
158 mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
159 }else if(_sg_mc_comms_determinism
160 && (!this->send_deterministic && !this->recv_deterministic)) {
161 XBT_INFO("****************************************************");
162 XBT_INFO("***** Non-deterministic communications pattern *****");
163 XBT_INFO("****************************************************");
164 XBT_INFO("%s", this->send_diff);
165 XBT_INFO("%s", this->recv_diff);
166 xbt_free(this->send_diff);
167 this->send_diff = nullptr;
168 xbt_free(this->recv_diff);
169 this->recv_diff = nullptr;
170 simgrid::mc::session->logState();
171 mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
177 /********** Non Static functions ***********/
179 void CommunicationDeterminismChecker::get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking)
181 const smx_process_t issuer = MC_smx_simcall_get_issuer(request);
182 simgrid::mc::PatternCommunicationList* initial_pattern = xbt_dynar_get_as(
183 initial_communications_pattern, issuer->pid, simgrid::mc::PatternCommunicationList*);
184 xbt_dynar_t incomplete_pattern = xbt_dynar_get_as(
185 incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
187 std::unique_ptr<simgrid::mc::PatternCommunication> pattern =
188 std::unique_ptr<simgrid::mc::PatternCommunication>(
189 new simgrid::mc::PatternCommunication());
191 initial_pattern->index_comm + xbt_dynar_length(incomplete_pattern);
193 if (call_type == MC_CALL_TYPE_SEND) {
194 /* Create comm pattern */
195 pattern->type = simgrid::mc::PatternCommunicationType::send;
196 pattern->comm_addr = simcall_comm_isend__get__result(request);
198 simgrid::mc::Remote<simgrid::simix::Comm> temp_synchro;
199 mc_model_checker->process().read(temp_synchro, remote(
200 static_cast<simgrid::simix::Comm*>(pattern->comm_addr)));
201 simgrid::simix::Comm* synchro =
202 static_cast<simgrid::simix::Comm*>(temp_synchro.data());
204 char* remote_name = mc_model_checker->process().read<char*>(
205 (std::uint64_t)(synchro->mbox ? &synchro->mbox->name : &synchro->mbox_cpy->name));
206 pattern->rdv = mc_model_checker->process().read_string(remote_name);
207 pattern->src_proc = mc_model_checker->process().resolveProcess(
208 simgrid::mc::remote(synchro->src_proc))->pid;
209 pattern->src_host = MC_smx_process_get_host_name(issuer);
211 struct s_smpi_mpi_request mpi_request =
212 mc_model_checker->process().read<s_smpi_mpi_request>(
213 (std::uint64_t) simcall_comm_isend__get__data(request));
214 pattern->tag = mpi_request.tag;
216 if (synchro->src_buff != nullptr){
217 pattern->data.resize(synchro->src_buff_size);
218 mc_model_checker->process().read_bytes(
219 pattern->data.data(), pattern->data.size(),
220 remote(synchro->src_buff));
222 if(mpi_request.detached){
223 if (!this->initial_communications_pattern_done) {
224 /* Store comm pattern */
225 simgrid::mc::PatternCommunicationList* list = xbt_dynar_get_as(
226 initial_communications_pattern, pattern->src_proc,
227 simgrid::mc::PatternCommunicationList*);
228 list->list.push_back(std::move(pattern));
230 /* Evaluate comm determinism */
231 this->deterministic_comm_pattern(pattern->src_proc, pattern.get(), backtracking);
233 initial_communications_pattern, pattern->src_proc, simgrid::mc::PatternCommunicationList*
238 } else if (call_type == MC_CALL_TYPE_RECV) {
239 pattern->type = simgrid::mc::PatternCommunicationType::receive;
240 pattern->comm_addr = simcall_comm_irecv__get__result(request);
242 struct s_smpi_mpi_request mpi_request;
243 mc_model_checker->process().read(
244 &mpi_request, remote((struct s_smpi_mpi_request*)simcall_comm_irecv__get__data(request)));
245 pattern->tag = mpi_request.tag;
247 simgrid::mc::Remote<simgrid::simix::Comm> temp_comm;
248 mc_model_checker->process().read(temp_comm, remote(
249 static_cast<simgrid::simix::Comm*>(pattern->comm_addr)));
250 simgrid::simix::Comm* comm =
251 static_cast<simgrid::simix::Comm*>(temp_comm.data());
254 mc_model_checker->process().read(&remote_name,
255 remote(comm->mbox ? &comm->mbox->name : &comm->mbox_cpy->name));
256 pattern->rdv = mc_model_checker->process().read_string(remote_name);
257 pattern->dst_proc = mc_model_checker->process().resolveProcess(
258 simgrid::mc::remote(comm->dst_proc))->pid;
259 pattern->dst_host = MC_smx_process_get_host_name(issuer);
261 xbt_die("Unexpected call_type %i", (int) call_type);
263 XBT_DEBUG("Insert incomplete comm pattern %p for process %lu",
264 pattern.get(), issuer->pid);
266 xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
267 simgrid::mc::PatternCommunication* pattern2 = pattern.release();
268 xbt_dynar_push(dynar, &pattern2);
272 void CommunicationDeterminismChecker::complete_comm_pattern(
273 xbt_dynar_t list, simgrid::mc::RemotePtr<simgrid::simix::Comm> comm_addr,
274 unsigned int issuer, int backtracking)
276 simgrid::mc::PatternCommunication* current_comm_pattern;
277 unsigned int cursor = 0;
278 std::unique_ptr<simgrid::mc::PatternCommunication> comm_pattern;
281 /* Complete comm pattern */
282 xbt_dynar_foreach(xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, current_comm_pattern)
283 if (remote(current_comm_pattern->comm_addr) == comm_addr) {
284 update_comm_pattern(current_comm_pattern, comm_addr);
286 simgrid::mc::PatternCommunication* temp;
288 xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t),
290 comm_pattern = std::unique_ptr<simgrid::mc::PatternCommunication>(temp);
291 XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", issuer, cursor);
296 xbt_die("Corresponding communication not found!");
298 simgrid::mc::PatternCommunicationList* pattern = xbt_dynar_get_as(
299 initial_communications_pattern, issuer, simgrid::mc::PatternCommunicationList*);
301 if (!this->initial_communications_pattern_done)
302 /* Store comm pattern */
303 pattern->list.push_back(std::move(comm_pattern));
305 /* Evaluate comm determinism */
306 this->deterministic_comm_pattern(issuer, comm_pattern.get(), backtracking);
307 pattern->index_comm++;
311 CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session& session)
317 CommunicationDeterminismChecker::~CommunicationDeterminismChecker()
322 RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override
325 for (auto const& state : stack_)
326 res.push_back(state->getTransition());
330 std::vector<std::string> CommunicationDeterminismChecker::getTextualTrace() // override
332 std::vector<std::string> trace;
333 for (auto const& state : stack_) {
334 smx_simcall_t req = &state->executed_req;
336 trace.push_back(simgrid::mc::request_to_string(
337 req, state->transition.argument, simgrid::mc::RequestType::executed));
342 void CommunicationDeterminismChecker::logState() // override
345 if (_sg_mc_comms_determinism &&
346 !this->recv_deterministic &&
347 this->send_deterministic) {
348 XBT_INFO("******************************************************");
349 XBT_INFO("**** Only-send-deterministic communication pattern ****");
350 XBT_INFO("******************************************************");
351 XBT_INFO("%s", this->recv_diff);
352 } else if(_sg_mc_comms_determinism &&
353 !this->send_deterministic &&
354 this->recv_deterministic) {
355 XBT_INFO("******************************************************");
356 XBT_INFO("**** Only-recv-deterministic communication pattern ****");
357 XBT_INFO("******************************************************");
358 XBT_INFO("%s", this->send_diff);
360 XBT_INFO("Expanded states = %lu", expandedStatesCount_);
361 XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
362 XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
363 XBT_INFO("Send-deterministic : %s", !this->send_deterministic ? "No" : "Yes");
364 if (_sg_mc_comms_determinism)
365 XBT_INFO("Recv-deterministic : %s",
366 !this->recv_deterministic ? "No" : "Yes");
369 void CommunicationDeterminismChecker::prepare()
373 const int maxpid = MC_smx_get_maxpid();
375 // Create initial_communications_pattern elements:
376 initial_communications_pattern = simgrid::xbt::newDeleteDynar<simgrid::mc::PatternCommunicationList*>();
377 for (i=0; i < maxpid; i++){
378 simgrid::mc::PatternCommunicationList* process_list_pattern = new simgrid::mc::PatternCommunicationList();
379 xbt_dynar_insert_at(initial_communications_pattern, i, &process_list_pattern);
382 // Create incomplete_communications_pattern elements:
383 incomplete_communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
384 for (i=0; i < maxpid; i++){
385 xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(simgrid::mc::PatternCommunication*), nullptr);
386 xbt_dynar_insert_at(incomplete_communications_pattern, i, &process_pattern);
389 std::unique_ptr<simgrid::mc::State> initial_state =
390 std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
392 XBT_DEBUG("********* Start communication determinism verification *********");
394 /* Get an enabled process and insert it in the interleave set of the initial state */
395 for (auto& p : mc_model_checker->process().simix_processes())
396 if (simgrid::mc::process_is_enabled(&p.copy))
397 initial_state->interleave(&p.copy);
399 stack_.push_back(std::move(initial_state));
403 bool all_communications_are_finished()
405 for (size_t current_process = 1; current_process < MC_smx_get_maxpid(); current_process++) {
406 xbt_dynar_t pattern = xbt_dynar_get_as(
407 incomplete_communications_pattern, current_process, xbt_dynar_t);
408 if (!xbt_dynar_is_empty(pattern)) {
409 XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
416 void CommunicationDeterminismChecker::restoreState()
418 /* Intermediate backtracking */
420 simgrid::mc::State* state = stack_.back().get();
421 if (state->system_state) {
422 simgrid::mc::restore_snapshot(state->system_state);
423 MC_restore_communications_pattern(state);
428 /* Restore the initial state */
429 simgrid::mc::session->restoreInitialState();
431 // int n = xbt_dynar_length(incomplete_communications_pattern);
432 unsigned n = MC_smx_get_maxpid();
433 assert(n == xbt_dynar_length(incomplete_communications_pattern));
434 assert(n == xbt_dynar_length(initial_communications_pattern));
435 for (unsigned j=0; j < n ; j++) {
436 xbt_dynar_reset((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, j, xbt_dynar_t));
437 xbt_dynar_get_as(initial_communications_pattern, j, simgrid::mc::PatternCommunicationList*)->index_comm = 0;
440 /* Traverse the stack from the state at position start and re-execute the transitions */
441 for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
442 if (state == stack_.back())
445 int req_num = state->transition.argument;
446 smx_simcall_t saved_req = &state->executed_req;
447 xbt_assert(saved_req);
449 /* because we got a copy of the executed request, we have to fetch the
450 real one, pointed by the request field of the issuer process */
452 const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
453 smx_simcall_t req = &issuer->simcall;
455 /* TODO : handle test and testany simcalls */
456 e_mc_call_type_t call = MC_get_call_type(req);
457 mc_model_checker->handle_simcall(state->transition);
458 MC_handle_comm_pattern(call, req, req_num, nullptr, 1);
459 mc_model_checker->wait_for_requests();
461 /* Update statistics */
462 mc_model_checker->visited_states++;
463 mc_model_checker->executed_transitions++;
467 int CommunicationDeterminismChecker::main(void)
469 std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
470 smx_simcall_t req = nullptr;
472 while (!stack_.empty()) {
474 /* Get current state */
475 simgrid::mc::State* state = stack_.back().get();
477 XBT_DEBUG("**************************************************");
478 XBT_DEBUG("Exploration depth = %zi (state = %d, interleaved processes = %zd)",
479 stack_.size(), state->num,
480 state->interleaveSize());
482 /* Update statistics */
483 mc_model_checker->visited_states++;
485 if (stack_.size() <= (std::size_t) _sg_mc_max_depth
486 && (req = MC_state_get_request(state)) != nullptr
487 && (visited_state == nullptr)) {
489 int req_num = state->transition.argument;
491 XBT_DEBUG("Execute: %s",
492 simgrid::mc::request_to_string(
493 req, req_num, simgrid::mc::RequestType::simix).c_str());
496 if (dot_output != nullptr)
497 req_str = simgrid::mc::request_get_dot_output(req, req_num);
499 mc_model_checker->executed_transitions++;
501 /* TODO : handle test and testany simcalls */
502 e_mc_call_type_t call = MC_CALL_TYPE_NONE;
503 if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
504 call = MC_get_call_type(req);
506 /* Answer the request */
507 mc_model_checker->handle_simcall(state->transition);
508 /* After this call req is no longer useful */
510 if (!this->initial_communications_pattern_done)
511 MC_handle_comm_pattern(call, req, req_num, initial_communications_pattern, 0);
513 MC_handle_comm_pattern(call, req, req_num, nullptr, 0);
515 /* Wait for requests (schedules processes) */
516 mc_model_checker->wait_for_requests();
518 /* Create the new expanded state */
519 std::unique_ptr<simgrid::mc::State> next_state =
520 std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
522 /* If comm determinism verification, we cannot stop the exploration if
523 some communications are not finished (at least, data are transfered).
524 These communications are incomplete and they cannot be analyzed and
525 compared with the initial pattern. */
526 bool compare_snapshots = all_communications_are_finished()
527 && this->initial_communications_pattern_done;
529 if (_sg_mc_visited == 0
530 || (visited_state = visitedStates_.addVisitedState(
531 expandedStatesCount_, next_state.get(), compare_snapshots)) == nullptr) {
533 /* Get enabled processes and insert them in the interleave set of the next state */
534 for (auto& p : mc_model_checker->process().simix_processes())
535 if (simgrid::mc::process_is_enabled(&p.copy))
536 next_state->interleave(&p.copy);
538 if (dot_output != nullptr)
539 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
540 state->num, next_state->num, req_str.c_str());
542 } else if (dot_output != nullptr)
543 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
544 state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str.c_str());
546 stack_.push_back(std::move(next_state));
550 if (stack_.size() > (std::size_t) _sg_mc_max_depth)
551 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
552 else if (visited_state != nullptr)
553 XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num);
555 XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
558 if (!this->initial_communications_pattern_done)
559 this->initial_communications_pattern_done = 1;
561 /* Trash the current state, no longer needed */
562 XBT_DEBUG("Delete state %d at depth %zi",
563 state->num, stack_.size());
566 visited_state = nullptr;
568 /* Check for deadlocks */
569 if (mc_model_checker->checkDeadlock()) {
571 return SIMGRID_MC_EXIT_DEADLOCK;
574 while (!stack_.empty()) {
575 std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
577 if (state->interleaveSize()
578 && stack_.size() < (std::size_t) _sg_mc_max_depth) {
579 /* We found a back-tracking point, let's loop */
580 XBT_DEBUG("Back-tracking to state %d at depth %zi",
581 state->num, stack_.size() + 1);
582 stack_.push_back(std::move(state));
584 this->restoreState();
586 XBT_DEBUG("Back-tracking to state %d at depth %zi done",
587 stack_.back()->num, stack_.size());
591 XBT_DEBUG("Delete state %d at depth %zi",
592 state->num, stack_.size() + 1);
598 simgrid::mc::session->logState();
599 return SIMGRID_MC_EXIT_SUCCESS;
602 int CommunicationDeterminismChecker::run()
604 XBT_INFO("Check communication determinism");
605 simgrid::mc::session->initialize();
609 this->initial_communications_pattern_done = 0;
610 this->recv_deterministic = 1;
611 this->send_deterministic = 1;
612 this->recv_diff = nullptr;
613 this->send_diff = nullptr;
615 int res = this->main();
619 Checker* createCommunicationDeterminismChecker(Session& session)
621 return new CommunicationDeterminismChecker(session);