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.getBuffer());
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.getBuffer());
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 = temp_comm.getBuffer();
253 mc_model_checker->process().read(&remote_name,
254 remote(comm->mbox ? &comm->mbox->name : &comm->mbox_cpy->name));
255 pattern->rdv = mc_model_checker->process().read_string(remote_name);
256 pattern->dst_proc = mc_model_checker->process().resolveProcess(
257 simgrid::mc::remote(comm->dst_proc))->pid;
258 pattern->dst_host = MC_smx_process_get_host_name(issuer);
260 xbt_die("Unexpected call_type %i", (int) call_type);
262 XBT_DEBUG("Insert incomplete comm pattern %p for process %lu",
263 pattern.get(), issuer->pid);
265 xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
266 simgrid::mc::PatternCommunication* pattern2 = pattern.release();
267 xbt_dynar_push(dynar, &pattern2);
271 void CommunicationDeterminismChecker::complete_comm_pattern(
272 xbt_dynar_t list, simgrid::mc::RemotePtr<simgrid::simix::Comm> comm_addr,
273 unsigned int issuer, int backtracking)
275 simgrid::mc::PatternCommunication* current_comm_pattern;
276 unsigned int cursor = 0;
277 std::unique_ptr<simgrid::mc::PatternCommunication> comm_pattern;
280 /* Complete comm pattern */
281 xbt_dynar_foreach(xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, current_comm_pattern)
282 if (remote(current_comm_pattern->comm_addr) == comm_addr) {
283 update_comm_pattern(current_comm_pattern, comm_addr);
285 simgrid::mc::PatternCommunication* temp;
287 xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t),
289 comm_pattern = std::unique_ptr<simgrid::mc::PatternCommunication>(temp);
290 XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", issuer, cursor);
295 xbt_die("Corresponding communication not found!");
297 simgrid::mc::PatternCommunicationList* pattern = xbt_dynar_get_as(
298 initial_communications_pattern, issuer, simgrid::mc::PatternCommunicationList*);
300 if (!this->initial_communications_pattern_done)
301 /* Store comm pattern */
302 pattern->list.push_back(std::move(comm_pattern));
304 /* Evaluate comm determinism */
305 this->deterministic_comm_pattern(issuer, comm_pattern.get(), backtracking);
306 pattern->index_comm++;
310 CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session& session)
316 CommunicationDeterminismChecker::~CommunicationDeterminismChecker()
321 RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override
324 for (auto const& state : stack_)
325 res.push_back(state->getTransition());
329 std::vector<std::string> CommunicationDeterminismChecker::getTextualTrace() // override
331 std::vector<std::string> trace;
332 for (auto const& state : stack_) {
333 smx_simcall_t req = &state->executed_req;
335 trace.push_back(simgrid::mc::request_to_string(
336 req, state->transition.argument, simgrid::mc::RequestType::executed));
341 void CommunicationDeterminismChecker::logState() // override
344 if (_sg_mc_comms_determinism &&
345 !this->recv_deterministic &&
346 this->send_deterministic) {
347 XBT_INFO("******************************************************");
348 XBT_INFO("**** Only-send-deterministic communication pattern ****");
349 XBT_INFO("******************************************************");
350 XBT_INFO("%s", this->recv_diff);
351 } else if(_sg_mc_comms_determinism &&
352 !this->send_deterministic &&
353 this->recv_deterministic) {
354 XBT_INFO("******************************************************");
355 XBT_INFO("**** Only-recv-deterministic communication pattern ****");
356 XBT_INFO("******************************************************");
357 XBT_INFO("%s", this->send_diff);
359 XBT_INFO("Expanded states = %lu", expandedStatesCount_);
360 XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
361 XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
362 XBT_INFO("Send-deterministic : %s", !this->send_deterministic ? "No" : "Yes");
363 if (_sg_mc_comms_determinism)
364 XBT_INFO("Recv-deterministic : %s",
365 !this->recv_deterministic ? "No" : "Yes");
368 void CommunicationDeterminismChecker::prepare()
372 const int maxpid = MC_smx_get_maxpid();
374 // Create initial_communications_pattern elements:
375 initial_communications_pattern = simgrid::xbt::newDeleteDynar<simgrid::mc::PatternCommunicationList*>();
376 for (i=0; i < maxpid; i++){
377 simgrid::mc::PatternCommunicationList* process_list_pattern = new simgrid::mc::PatternCommunicationList();
378 xbt_dynar_insert_at(initial_communications_pattern, i, &process_list_pattern);
381 // Create incomplete_communications_pattern elements:
382 incomplete_communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
383 for (i=0; i < maxpid; i++){
384 xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(simgrid::mc::PatternCommunication*), nullptr);
385 xbt_dynar_insert_at(incomplete_communications_pattern, i, &process_pattern);
388 std::unique_ptr<simgrid::mc::State> initial_state =
389 std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
391 XBT_DEBUG("********* Start communication determinism verification *********");
393 /* Get an enabled process and insert it in the interleave set of the initial state */
394 for (auto& p : mc_model_checker->process().simix_processes())
395 if (simgrid::mc::process_is_enabled(p.copy.getBuffer()))
396 initial_state->interleave(p.copy.getBuffer());
398 stack_.push_back(std::move(initial_state));
402 bool all_communications_are_finished()
404 for (size_t current_process = 1; current_process < MC_smx_get_maxpid(); current_process++) {
405 xbt_dynar_t pattern = xbt_dynar_get_as(
406 incomplete_communications_pattern, current_process, xbt_dynar_t);
407 if (!xbt_dynar_is_empty(pattern)) {
408 XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
415 void CommunicationDeterminismChecker::restoreState()
417 /* Intermediate backtracking */
419 simgrid::mc::State* state = stack_.back().get();
420 if (state->system_state) {
421 simgrid::mc::restore_snapshot(state->system_state);
422 MC_restore_communications_pattern(state);
427 /* Restore the initial state */
428 simgrid::mc::session->restoreInitialState();
430 // int n = xbt_dynar_length(incomplete_communications_pattern);
431 unsigned n = MC_smx_get_maxpid();
432 assert(n == xbt_dynar_length(incomplete_communications_pattern));
433 assert(n == xbt_dynar_length(initial_communications_pattern));
434 for (unsigned j=0; j < n ; j++) {
435 xbt_dynar_reset((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, j, xbt_dynar_t));
436 xbt_dynar_get_as(initial_communications_pattern, j, simgrid::mc::PatternCommunicationList*)->index_comm = 0;
439 /* Traverse the stack from the state at position start and re-execute the transitions */
440 for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
441 if (state == stack_.back())
444 int req_num = state->transition.argument;
445 smx_simcall_t saved_req = &state->executed_req;
446 xbt_assert(saved_req);
448 /* because we got a copy of the executed request, we have to fetch the
449 real one, pointed by the request field of the issuer process */
451 const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
452 smx_simcall_t req = &issuer->simcall;
454 /* TODO : handle test and testany simcalls */
455 e_mc_call_type_t call = MC_get_call_type(req);
456 mc_model_checker->handle_simcall(state->transition);
457 MC_handle_comm_pattern(call, req, req_num, nullptr, 1);
458 mc_model_checker->wait_for_requests();
460 /* Update statistics */
461 mc_model_checker->visited_states++;
462 mc_model_checker->executed_transitions++;
466 int CommunicationDeterminismChecker::main(void)
468 std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
469 smx_simcall_t req = nullptr;
471 while (!stack_.empty()) {
473 /* Get current state */
474 simgrid::mc::State* state = stack_.back().get();
476 XBT_DEBUG("**************************************************");
477 XBT_DEBUG("Exploration depth = %zi (state = %d, interleaved processes = %zd)",
478 stack_.size(), state->num,
479 state->interleaveSize());
481 /* Update statistics */
482 mc_model_checker->visited_states++;
484 if (stack_.size() <= (std::size_t) _sg_mc_max_depth
485 && (req = MC_state_get_request(state)) != nullptr
486 && (visited_state == nullptr)) {
488 int req_num = state->transition.argument;
490 XBT_DEBUG("Execute: %s",
491 simgrid::mc::request_to_string(
492 req, req_num, simgrid::mc::RequestType::simix).c_str());
495 if (dot_output != nullptr)
496 req_str = simgrid::mc::request_get_dot_output(req, req_num);
498 mc_model_checker->executed_transitions++;
500 /* TODO : handle test and testany simcalls */
501 e_mc_call_type_t call = MC_CALL_TYPE_NONE;
502 if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
503 call = MC_get_call_type(req);
505 /* Answer the request */
506 mc_model_checker->handle_simcall(state->transition);
507 /* After this call req is no longer useful */
509 if (!this->initial_communications_pattern_done)
510 MC_handle_comm_pattern(call, req, req_num, initial_communications_pattern, 0);
512 MC_handle_comm_pattern(call, req, req_num, nullptr, 0);
514 /* Wait for requests (schedules processes) */
515 mc_model_checker->wait_for_requests();
517 /* Create the new expanded state */
518 std::unique_ptr<simgrid::mc::State> next_state =
519 std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
521 /* If comm determinism verification, we cannot stop the exploration if
522 some communications are not finished (at least, data are transferred).
523 These communications are incomplete and they cannot be analyzed and
524 compared with the initial pattern. */
525 bool compare_snapshots = all_communications_are_finished()
526 && this->initial_communications_pattern_done;
528 if (_sg_mc_visited == 0
529 || (visited_state = visitedStates_.addVisitedState(
530 expandedStatesCount_, next_state.get(), compare_snapshots)) == nullptr) {
532 /* Get enabled processes and insert them in the interleave set of the next state */
533 for (auto& p : mc_model_checker->process().simix_processes())
534 if (simgrid::mc::process_is_enabled(p.copy.getBuffer()))
535 next_state->interleave(p.copy.getBuffer());
537 if (dot_output != nullptr)
538 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
539 state->num, next_state->num, req_str.c_str());
541 } else if (dot_output != nullptr)
542 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
543 state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str.c_str());
545 stack_.push_back(std::move(next_state));
549 if (stack_.size() > (std::size_t) _sg_mc_max_depth)
550 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
551 else if (visited_state != nullptr)
552 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);
554 XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
557 if (!this->initial_communications_pattern_done)
558 this->initial_communications_pattern_done = 1;
560 /* Trash the current state, no longer needed */
561 XBT_DEBUG("Delete state %d at depth %zi",
562 state->num, stack_.size());
565 visited_state = nullptr;
567 /* Check for deadlocks */
568 if (mc_model_checker->checkDeadlock()) {
570 return SIMGRID_MC_EXIT_DEADLOCK;
573 while (!stack_.empty()) {
574 std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
576 if (state->interleaveSize()
577 && stack_.size() < (std::size_t) _sg_mc_max_depth) {
578 /* We found a back-tracking point, let's loop */
579 XBT_DEBUG("Back-tracking to state %d at depth %zi",
580 state->num, stack_.size() + 1);
581 stack_.push_back(std::move(state));
583 this->restoreState();
585 XBT_DEBUG("Back-tracking to state %d at depth %zi done",
586 stack_.back()->num, stack_.size());
590 XBT_DEBUG("Delete state %d at depth %zi",
591 state->num, stack_.size() + 1);
597 simgrid::mc::session->logState();
598 return SIMGRID_MC_EXIT_SUCCESS;
601 int CommunicationDeterminismChecker::run()
603 XBT_INFO("Check communication determinism");
604 simgrid::mc::session->initialize();
608 this->initial_communications_pattern_done = 0;
609 this->recv_deterministic = 1;
610 this->send_deterministic = 1;
611 this->recv_diff = nullptr;
612 this->send_diff = nullptr;
614 int res = this->main();
618 Checker* createCommunicationDeterminismChecker(Session& session)
620 return new CommunicationDeterminismChecker(session);