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) {
40 if(comm1->type != comm2->type)
42 if (comm1->rdv != comm2->rdv)
44 if (comm1->src_proc != comm2->src_proc)
46 if (comm1->dst_proc != comm2->dst_proc)
48 if (comm1->tag != comm2->tag)
50 if (comm1->data.size() != comm2->data.size())
51 return DATA_SIZE_DIFF;
52 if (comm1->data != comm2->data)
57 static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int process, simgrid::mc::PatternCommunication* comm, unsigned int cursor) {
60 if(comm->type == SIMIX_COMM_SEND)
61 type = bprintf("The send communications pattern of the process %d is different!", process - 1);
63 type = bprintf("The recv communications pattern of the process %d is different!", process - 1);
67 res = bprintf("%s Different type for communication #%d", type, cursor);
70 res = bprintf("%s Different rdv for communication #%d", type, cursor);
73 res = bprintf("%s Different tag for communication #%d", type, cursor);
76 res = bprintf("%s Different source for communication #%d", type, cursor);
79 res = bprintf("%s Different destination for communication #%d", type, cursor);
82 res = bprintf("%s\n Different data size for communication #%d", type, cursor);
85 res = bprintf("%s\n Different data for communication #%d", type, cursor);
95 static void update_comm_pattern(simgrid::mc::PatternCommunication* comm_pattern, smx_synchro_t comm_addr)
98 mc_model_checker->process().read(&comm, remote(comm_addr));
100 smx_process_t src_proc = mc_model_checker->process().resolveProcess(
101 simgrid::mc::remote(comm.comm.src_proc));
102 smx_process_t dst_proc = mc_model_checker->process().resolveProcess(
103 simgrid::mc::remote(comm.comm.dst_proc));
104 comm_pattern->src_proc = src_proc->pid;
105 comm_pattern->dst_proc = dst_proc->pid;
106 comm_pattern->src_host = MC_smx_process_get_host_name(src_proc);
107 comm_pattern->dst_host = MC_smx_process_get_host_name(dst_proc);
108 if (comm_pattern->data.size() == 0 && comm.comm.src_buff != nullptr) {
110 mc_model_checker->process().read(
111 &buff_size, remote(comm.comm.dst_buff_size));
112 comm_pattern->data.resize(buff_size);
113 mc_model_checker->process().read_bytes(
114 comm_pattern->data.data(), comm_pattern->data.size(),
115 remote(comm.comm.src_buff));
122 void CommunicationDeterminismChecker::deterministic_comm_pattern(int process, simgrid::mc::PatternCommunication* comm, int backtracking) {
124 simgrid::mc::PatternCommunicationList* list =
125 xbt_dynar_get_as(initial_communications_pattern, process, simgrid::mc::PatternCommunicationList*);
128 e_mc_comm_pattern_difference_t diff =
129 compare_comm_pattern(list->list[list->index_comm].get(), comm);
131 if (diff != NONE_DIFF) {
132 if (comm->type == SIMIX_COMM_SEND){
133 this->send_deterministic = 0;
134 if (this->send_diff != nullptr)
135 xbt_free(this->send_diff);
136 this->send_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
138 this->recv_deterministic = 0;
139 if (this->recv_diff != nullptr)
140 xbt_free(this->recv_diff);
141 this->recv_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
143 if(_sg_mc_send_determinism && !this->send_deterministic){
144 XBT_INFO("*********************************************************");
145 XBT_INFO("***** Non-send-deterministic communications pattern *****");
146 XBT_INFO("*********************************************************");
147 XBT_INFO("%s", this->send_diff);
148 xbt_free(this->send_diff);
149 this->send_diff = nullptr;
150 simgrid::mc::session->logState();
151 mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
152 }else if(_sg_mc_comms_determinism
153 && (!this->send_deterministic && !this->recv_deterministic)) {
154 XBT_INFO("****************************************************");
155 XBT_INFO("***** Non-deterministic communications pattern *****");
156 XBT_INFO("****************************************************");
157 XBT_INFO("%s", this->send_diff);
158 XBT_INFO("%s", this->recv_diff);
159 xbt_free(this->send_diff);
160 this->send_diff = nullptr;
161 xbt_free(this->recv_diff);
162 this->recv_diff = nullptr;
163 simgrid::mc::session->logState();
164 mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
170 /********** Non Static functions ***********/
172 void CommunicationDeterminismChecker::get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking)
174 const smx_process_t issuer = MC_smx_simcall_get_issuer(request);
175 simgrid::mc::PatternCommunicationList* initial_pattern = xbt_dynar_get_as(
176 initial_communications_pattern, issuer->pid, simgrid::mc::PatternCommunicationList*);
177 xbt_dynar_t incomplete_pattern = xbt_dynar_get_as(
178 incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
180 std::unique_ptr<simgrid::mc::PatternCommunication> pattern =
181 std::unique_ptr<simgrid::mc::PatternCommunication>(
182 new simgrid::mc::PatternCommunication());
184 initial_pattern->index_comm + xbt_dynar_length(incomplete_pattern);
186 if (call_type == MC_CALL_TYPE_SEND) {
187 /* Create comm pattern */
188 pattern->type = SIMIX_COMM_SEND;
189 pattern->comm_addr = simcall_comm_isend__get__result(request);
191 s_smx_synchro_t synchro = mc_model_checker->process().read<s_smx_synchro_t>(
192 (std::uint64_t) pattern->comm_addr);
194 char* remote_name = mc_model_checker->process().read<char*>(
195 (std::uint64_t)(synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name));
196 pattern->rdv = mc_model_checker->process().read_string(remote_name);
197 pattern->src_proc = mc_model_checker->process().resolveProcess(
198 simgrid::mc::remote(synchro.comm.src_proc))->pid;
199 pattern->src_host = MC_smx_process_get_host_name(issuer);
201 struct s_smpi_mpi_request mpi_request =
202 mc_model_checker->process().read<s_smpi_mpi_request>(
203 (std::uint64_t) simcall_comm_isend__get__data(request));
204 pattern->tag = mpi_request.tag;
206 if(synchro.comm.src_buff != nullptr){
207 pattern->data.resize(synchro.comm.src_buff_size);
208 mc_model_checker->process().read_bytes(
209 pattern->data.data(), pattern->data.size(),
210 remote(synchro.comm.src_buff));
212 if(mpi_request.detached){
213 if (!this->initial_communications_pattern_done) {
214 /* Store comm pattern */
215 simgrid::mc::PatternCommunicationList* list = xbt_dynar_get_as(
216 initial_communications_pattern, pattern->src_proc,
217 simgrid::mc::PatternCommunicationList*);
218 list->list.push_back(std::move(pattern));
220 /* Evaluate comm determinism */
221 this->deterministic_comm_pattern(pattern->src_proc, pattern.get(), backtracking);
223 initial_communications_pattern, pattern->src_proc, simgrid::mc::PatternCommunicationList*
228 } else if (call_type == MC_CALL_TYPE_RECV) {
229 pattern->type = SIMIX_COMM_RECEIVE;
230 pattern->comm_addr = simcall_comm_irecv__get__result(request);
232 struct s_smpi_mpi_request mpi_request;
233 mc_model_checker->process().read(
234 &mpi_request, remote((struct s_smpi_mpi_request*)simcall_comm_irecv__get__data(request)));
235 pattern->tag = mpi_request.tag;
237 s_smx_synchro_t synchro;
238 mc_model_checker->process().read(&synchro, remote(pattern->comm_addr));
241 mc_model_checker->process().read(&remote_name,
242 remote(synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name));
243 pattern->rdv = mc_model_checker->process().read_string(remote_name);
244 pattern->dst_proc = mc_model_checker->process().resolveProcess(
245 simgrid::mc::remote(synchro.comm.dst_proc))->pid;
246 pattern->dst_host = MC_smx_process_get_host_name(issuer);
248 xbt_die("Unexpected call_type %i", (int) call_type);
250 XBT_DEBUG("Insert incomplete comm pattern %p for process %lu",
251 pattern.get(), issuer->pid);
253 xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
254 simgrid::mc::PatternCommunication* pattern2 = pattern.release();
255 xbt_dynar_push(dynar, &pattern2);
259 void CommunicationDeterminismChecker::complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking)
261 simgrid::mc::PatternCommunication* current_comm_pattern;
262 unsigned int cursor = 0;
263 std::unique_ptr<simgrid::mc::PatternCommunication> comm_pattern;
266 /* Complete comm pattern */
267 xbt_dynar_foreach(xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, current_comm_pattern)
268 if (current_comm_pattern->comm_addr == comm_addr) {
269 update_comm_pattern(current_comm_pattern, comm_addr);
271 simgrid::mc::PatternCommunication* temp;
273 xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t),
275 comm_pattern = std::unique_ptr<simgrid::mc::PatternCommunication>(temp);
276 XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", issuer, cursor);
281 xbt_die("Corresponding communication not found!");
283 simgrid::mc::PatternCommunicationList* pattern = xbt_dynar_get_as(
284 initial_communications_pattern, issuer, simgrid::mc::PatternCommunicationList*);
286 if (!this->initial_communications_pattern_done)
287 /* Store comm pattern */
288 pattern->list.push_back(std::move(comm_pattern));
290 /* Evaluate comm determinism */
291 this->deterministic_comm_pattern(issuer, comm_pattern.get(), backtracking);
292 pattern->index_comm++;
296 CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session& session)
302 CommunicationDeterminismChecker::~CommunicationDeterminismChecker()
307 RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override
310 for (auto const& state : stack_)
311 res.push_back(state->getTransition());
315 std::vector<std::string> CommunicationDeterminismChecker::getTextualTrace() // override
317 std::vector<std::string> trace;
318 for (auto const& state : stack_) {
319 smx_simcall_t req = &state->executed_req;
321 trace.push_back(simgrid::mc::request_to_string(
322 req, state->transition.argument, simgrid::mc::RequestType::executed));
327 void CommunicationDeterminismChecker::logState() // override
330 if (_sg_mc_comms_determinism &&
331 !this->recv_deterministic &&
332 this->send_deterministic) {
333 XBT_INFO("******************************************************");
334 XBT_INFO("**** Only-send-deterministic communication pattern ****");
335 XBT_INFO("******************************************************");
336 XBT_INFO("%s", this->recv_diff);
337 } else if(_sg_mc_comms_determinism &&
338 !this->send_deterministic &&
339 this->recv_deterministic) {
340 XBT_INFO("******************************************************");
341 XBT_INFO("**** Only-recv-deterministic communication pattern ****");
342 XBT_INFO("******************************************************");
343 XBT_INFO("%s", this->send_diff);
345 XBT_INFO("Expanded states = %lu", expandedStatesCount_);
346 XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
347 XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
348 XBT_INFO("Send-deterministic : %s", !this->send_deterministic ? "No" : "Yes");
349 if (_sg_mc_comms_determinism)
350 XBT_INFO("Recv-deterministic : %s",
351 !this->recv_deterministic ? "No" : "Yes");
354 void CommunicationDeterminismChecker::prepare()
358 const int maxpid = MC_smx_get_maxpid();
360 // Create initial_communications_pattern elements:
361 initial_communications_pattern = simgrid::xbt::newDeleteDynar<simgrid::mc::PatternCommunicationList*>();
362 for (i=0; i < maxpid; i++){
363 simgrid::mc::PatternCommunicationList* process_list_pattern = new simgrid::mc::PatternCommunicationList();
364 xbt_dynar_insert_at(initial_communications_pattern, i, &process_list_pattern);
367 // Create incomplete_communications_pattern elements:
368 incomplete_communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
369 for (i=0; i < maxpid; i++){
370 xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(simgrid::mc::PatternCommunication*), nullptr);
371 xbt_dynar_insert_at(incomplete_communications_pattern, i, &process_pattern);
374 std::unique_ptr<simgrid::mc::State> initial_state =
375 std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
377 XBT_DEBUG("********* Start communication determinism verification *********");
379 /* Get an enabled process and insert it in the interleave set of the initial state */
380 for (auto& p : mc_model_checker->process().simix_processes())
381 if (simgrid::mc::process_is_enabled(&p.copy))
382 initial_state->interleave(&p.copy);
384 stack_.push_back(std::move(initial_state));
388 bool all_communications_are_finished()
390 for (size_t current_process = 1; current_process < MC_smx_get_maxpid(); current_process++) {
391 xbt_dynar_t pattern = xbt_dynar_get_as(
392 incomplete_communications_pattern, current_process, 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_process_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 int 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>(MC_state_new(++expandedStatesCount_));
507 /* If comm determinism verification, we cannot stop the exploration if
508 some communications are not finished (at least, data are transfered).
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_visited == 0
515 || (visited_state = visitedStates_.addVisitedState(
516 expandedStatesCount_, next_state.get(), compare_snapshots)) == nullptr) {
518 /* Get enabled processes and insert them in the interleave set of the next state */
519 for (auto& p : mc_model_checker->process().simix_processes())
520 if (simgrid::mc::process_is_enabled(&p.copy))
521 next_state->interleave(&p.copy);
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",
529 state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_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.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num);
540 XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
543 if (!this->initial_communications_pattern_done)
544 this->initial_communications_pattern_done = 1;
546 /* Trash the current state, no longer needed */
547 XBT_DEBUG("Delete state %d at depth %zi",
548 state->num, stack_.size());
551 visited_state = nullptr;
553 /* Check for deadlocks */
554 if (mc_model_checker->checkDeadlock()) {
556 return SIMGRID_MC_EXIT_DEADLOCK;
559 while (!stack_.empty()) {
560 std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
562 if (state->interleaveSize()
563 && stack_.size() < (std::size_t) _sg_mc_max_depth) {
564 /* We found a back-tracking point, let's loop */
565 XBT_DEBUG("Back-tracking to state %d at depth %zi",
566 state->num, stack_.size() + 1);
567 stack_.push_back(std::move(state));
569 this->restoreState();
571 XBT_DEBUG("Back-tracking to state %d at depth %zi done",
572 stack_.back()->num, stack_.size());
576 XBT_DEBUG("Delete state %d at depth %zi",
577 state->num, stack_.size() + 1);
583 simgrid::mc::session->logState();
584 return SIMGRID_MC_EXIT_SUCCESS;
587 int CommunicationDeterminismChecker::run()
589 XBT_INFO("Check communication determinism");
590 simgrid::mc::session->initialize();
594 this->initial_communications_pattern_done = 0;
595 this->recv_deterministic = 1;
596 this->send_deterministic = 1;
597 this->recv_diff = nullptr;
598 this->send_diff = nullptr;
600 int res = this->main();
604 Checker* createCommunicationDeterminismChecker(Session& session)
606 return new CommunicationDeterminismChecker(session);