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 #include "src/smpi/smpi_request.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::kernel::activity::Comm> comm_addr)
100 // HACK, type punning
101 simgrid::mc::Remote<simgrid::kernel::activity::Comm> temp_comm;
102 mc_model_checker->process().read(temp_comm, comm_addr);
103 simgrid::kernel::activity::Comm* comm = temp_comm.getBuffer();
105 smx_actor_t src_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->src_proc));
106 smx_actor_t dst_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->dst_proc));
107 comm_pattern->src_proc = src_proc->pid;
108 comm_pattern->dst_proc = dst_proc->pid;
109 comm_pattern->src_host = MC_smx_actor_get_host_name(src_proc);
110 comm_pattern->dst_host = MC_smx_actor_get_host_name(dst_proc);
111 if (comm_pattern->data.size() == 0 && comm->src_buff != nullptr) {
113 mc_model_checker->process().read(
114 &buff_size, remote(comm->dst_buff_size));
115 comm_pattern->data.resize(buff_size);
116 mc_model_checker->process().read_bytes(
117 comm_pattern->data.data(), comm_pattern->data.size(),
118 remote(comm->src_buff));
125 void CommunicationDeterminismChecker::deterministic_comm_pattern(
126 int process, simgrid::mc::PatternCommunication* comm, int backtracking)
128 simgrid::mc::PatternCommunicationList* list =
129 xbt_dynar_get_as(initial_communications_pattern, process, simgrid::mc::PatternCommunicationList*);
132 e_mc_comm_pattern_difference_t diff =
133 compare_comm_pattern(list->list[list->index_comm].get(), comm);
135 if (diff != NONE_DIFF) {
136 if (comm->type == simgrid::mc::PatternCommunicationType::send) {
137 this->send_deterministic = 0;
138 if (this->send_diff != nullptr)
139 xbt_free(this->send_diff);
140 this->send_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
142 this->recv_deterministic = 0;
143 if (this->recv_diff != nullptr)
144 xbt_free(this->recv_diff);
145 this->recv_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
147 if(_sg_mc_send_determinism && !this->send_deterministic){
148 XBT_INFO("*********************************************************");
149 XBT_INFO("***** Non-send-deterministic communications pattern *****");
150 XBT_INFO("*********************************************************");
151 XBT_INFO("%s", this->send_diff);
152 xbt_free(this->send_diff);
153 this->send_diff = nullptr;
154 simgrid::mc::session->logState();
155 mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
156 }else if(_sg_mc_comms_determinism
157 && (!this->send_deterministic && !this->recv_deterministic)) {
158 XBT_INFO("****************************************************");
159 XBT_INFO("***** Non-deterministic communications pattern *****");
160 XBT_INFO("****************************************************");
161 XBT_INFO("%s", this->send_diff);
162 XBT_INFO("%s", this->recv_diff);
163 xbt_free(this->send_diff);
164 this->send_diff = nullptr;
165 xbt_free(this->recv_diff);
166 this->recv_diff = nullptr;
167 simgrid::mc::session->logState();
168 mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
174 /********** Non Static functions ***********/
176 void CommunicationDeterminismChecker::get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking)
178 const smx_actor_t issuer = MC_smx_simcall_get_issuer(request);
179 simgrid::mc::PatternCommunicationList* initial_pattern = xbt_dynar_get_as(
180 initial_communications_pattern, issuer->pid, simgrid::mc::PatternCommunicationList*);
181 xbt_dynar_t incomplete_pattern = xbt_dynar_get_as(
182 incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
184 std::unique_ptr<simgrid::mc::PatternCommunication> pattern =
185 std::unique_ptr<simgrid::mc::PatternCommunication>(
186 new simgrid::mc::PatternCommunication());
188 initial_pattern->index_comm + xbt_dynar_length(incomplete_pattern);
190 if (call_type == MC_CALL_TYPE_SEND) {
191 /* Create comm pattern */
192 pattern->type = simgrid::mc::PatternCommunicationType::send;
193 pattern->comm_addr = simcall_comm_isend__get__result(request);
195 simgrid::mc::Remote<simgrid::kernel::activity::Comm> temp_synchro;
196 mc_model_checker->process().read(temp_synchro, remote(
197 static_cast<simgrid::kernel::activity::Comm*>(pattern->comm_addr)));
198 simgrid::kernel::activity::Comm* synchro =
199 static_cast<simgrid::kernel::activity::Comm*>(temp_synchro.getBuffer());
201 char* remote_name = mc_model_checker->process().read<char*>(
202 (std::uint64_t)(synchro->mbox ? &synchro->mbox->name_ : &synchro->mbox_cpy->name_));
203 pattern->rdv = mc_model_checker->process().read_string(remote_name);
204 pattern->src_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(synchro->src_proc))->pid;
205 pattern->src_host = MC_smx_actor_get_host_name(issuer);
207 simgrid::smpi::Request mpi_request =
208 mc_model_checker->process().read<simgrid::smpi::Request>(
209 (std::uint64_t) simcall_comm_isend__get__data(request));
210 pattern->tag = mpi_request.tag();
212 if (synchro->src_buff != nullptr){
213 pattern->data.resize(synchro->src_buff_size);
214 mc_model_checker->process().read_bytes(
215 pattern->data.data(), pattern->data.size(),
216 remote(synchro->src_buff));
218 if(mpi_request.detached()){
219 if (!this->initial_communications_pattern_done) {
220 /* Store comm pattern */
221 simgrid::mc::PatternCommunicationList* list = xbt_dynar_get_as(
222 initial_communications_pattern, pattern->src_proc,
223 simgrid::mc::PatternCommunicationList*);
224 list->list.push_back(std::move(pattern));
226 /* Evaluate comm determinism */
227 this->deterministic_comm_pattern(pattern->src_proc, pattern.get(), backtracking);
229 initial_communications_pattern, pattern->src_proc, simgrid::mc::PatternCommunicationList*
234 } else if (call_type == MC_CALL_TYPE_RECV) {
235 pattern->type = simgrid::mc::PatternCommunicationType::receive;
236 pattern->comm_addr = simcall_comm_irecv__get__result(request);
238 simgrid::smpi::Request mpi_request;
239 mc_model_checker->process().read(
240 &mpi_request, remote((simgrid::smpi::Request*)simcall_comm_irecv__get__data(request)));
241 pattern->tag = mpi_request.tag();
243 simgrid::mc::Remote<simgrid::kernel::activity::Comm> temp_comm;
244 mc_model_checker->process().read(temp_comm, remote(
245 static_cast<simgrid::kernel::activity::Comm*>(pattern->comm_addr)));
246 simgrid::kernel::activity::Comm* comm = temp_comm.getBuffer();
249 mc_model_checker->process().read(&remote_name, remote(comm->mbox ? &comm->mbox->name_ : &comm->mbox_cpy->name_));
250 pattern->rdv = mc_model_checker->process().read_string(remote_name);
251 pattern->dst_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->dst_proc))->pid;
252 pattern->dst_host = MC_smx_actor_get_host_name(issuer);
254 xbt_die("Unexpected call_type %i", (int) call_type);
256 XBT_DEBUG("Insert incomplete comm pattern %p for process %lu",
257 pattern.get(), issuer->pid);
259 xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
260 simgrid::mc::PatternCommunication* pattern2 = pattern.release();
261 xbt_dynar_push(dynar, &pattern2);
265 void CommunicationDeterminismChecker::complete_comm_pattern(
266 xbt_dynar_t list, simgrid::mc::RemotePtr<simgrid::kernel::activity::Comm> comm_addr,
267 unsigned int issuer, int backtracking)
269 simgrid::mc::PatternCommunication* current_comm_pattern;
270 unsigned int cursor = 0;
271 std::unique_ptr<simgrid::mc::PatternCommunication> comm_pattern;
274 /* Complete comm pattern */
275 xbt_dynar_foreach(xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, current_comm_pattern)
276 if (remote(current_comm_pattern->comm_addr) == comm_addr) {
277 update_comm_pattern(current_comm_pattern, comm_addr);
279 simgrid::mc::PatternCommunication* temp;
281 xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t),
283 comm_pattern = std::unique_ptr<simgrid::mc::PatternCommunication>(temp);
284 XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", issuer, cursor);
289 xbt_die("Corresponding communication not found!");
291 simgrid::mc::PatternCommunicationList* pattern = xbt_dynar_get_as(
292 initial_communications_pattern, issuer, simgrid::mc::PatternCommunicationList*);
294 if (!this->initial_communications_pattern_done)
295 /* Store comm pattern */
296 pattern->list.push_back(std::move(comm_pattern));
298 /* Evaluate comm determinism */
299 this->deterministic_comm_pattern(issuer, comm_pattern.get(), backtracking);
300 pattern->index_comm++;
304 CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session& session)
310 CommunicationDeterminismChecker::~CommunicationDeterminismChecker() = default;
312 RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override
315 for (auto const& state : stack_)
316 res.push_back(state->getTransition());
320 std::vector<std::string> CommunicationDeterminismChecker::getTextualTrace() // override
322 std::vector<std::string> trace;
323 for (auto const& state : stack_) {
324 smx_simcall_t req = &state->executed_req;
326 trace.push_back(simgrid::mc::request_to_string(
327 req, state->transition.argument, simgrid::mc::RequestType::executed));
332 void CommunicationDeterminismChecker::logState() // override
335 if (_sg_mc_comms_determinism &&
336 !this->recv_deterministic &&
337 this->send_deterministic) {
338 XBT_INFO("******************************************************");
339 XBT_INFO("**** Only-send-deterministic communication pattern ****");
340 XBT_INFO("******************************************************");
341 XBT_INFO("%s", this->recv_diff);
342 } else if(_sg_mc_comms_determinism &&
343 !this->send_deterministic &&
344 this->recv_deterministic) {
345 XBT_INFO("******************************************************");
346 XBT_INFO("**** Only-recv-deterministic communication pattern ****");
347 XBT_INFO("******************************************************");
348 XBT_INFO("%s", this->send_diff);
350 XBT_INFO("Expanded states = %lu", expandedStatesCount_);
351 XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
352 XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
353 XBT_INFO("Send-deterministic : %s", !this->send_deterministic ? "No" : "Yes");
354 if (_sg_mc_comms_determinism)
355 XBT_INFO("Recv-deterministic : %s",
356 !this->recv_deterministic ? "No" : "Yes");
359 void CommunicationDeterminismChecker::prepare()
361 const int maxpid = MC_smx_get_maxpid();
363 // Create initial_communications_pattern elements:
364 initial_communications_pattern = simgrid::xbt::newDeleteDynar<simgrid::mc::PatternCommunicationList*>();
365 for (int i = 0; i < maxpid; i++) {
366 simgrid::mc::PatternCommunicationList* process_list_pattern = new simgrid::mc::PatternCommunicationList();
367 xbt_dynar_insert_at(initial_communications_pattern, i, &process_list_pattern);
370 // Create incomplete_communications_pattern elements:
371 incomplete_communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
372 for (int i = 0; i < maxpid; i++) {
373 xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(simgrid::mc::PatternCommunication*), nullptr);
374 xbt_dynar_insert_at(incomplete_communications_pattern, i, &process_pattern);
377 std::unique_ptr<simgrid::mc::State> initial_state =
378 std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
380 XBT_DEBUG("********* Start communication determinism verification *********");
382 /* Get an enabled actor and insert it in the interleave set of the initial state */
383 for (auto& actor : mc_model_checker->process().actors())
384 if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer()))
385 initial_state->interleave(actor.copy.getBuffer());
387 stack_.push_back(std::move(initial_state));
391 bool all_communications_are_finished()
393 for (size_t current_actor = 1; current_actor < MC_smx_get_maxpid(); current_actor++) {
394 xbt_dynar_t pattern = xbt_dynar_get_as(incomplete_communications_pattern, current_actor, xbt_dynar_t);
395 if (!xbt_dynar_is_empty(pattern)) {
396 XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
403 void CommunicationDeterminismChecker::restoreState()
405 /* Intermediate backtracking */
407 simgrid::mc::State* state = stack_.back().get();
408 if (state->system_state) {
409 simgrid::mc::restore_snapshot(state->system_state);
410 MC_restore_communications_pattern(state);
415 /* Restore the initial state */
416 simgrid::mc::session->restoreInitialState();
418 // int n = xbt_dynar_length(incomplete_communications_pattern);
419 unsigned n = MC_smx_get_maxpid();
420 assert(n == xbt_dynar_length(incomplete_communications_pattern));
421 assert(n == xbt_dynar_length(initial_communications_pattern));
422 for (unsigned j=0; j < n ; j++) {
423 xbt_dynar_reset((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, j, xbt_dynar_t));
424 xbt_dynar_get_as(initial_communications_pattern, j, simgrid::mc::PatternCommunicationList*)->index_comm = 0;
427 /* Traverse the stack from the state at position start and re-execute the transitions */
428 for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
429 if (state == stack_.back())
432 int req_num = state->transition.argument;
433 smx_simcall_t saved_req = &state->executed_req;
434 xbt_assert(saved_req);
436 /* because we got a copy of the executed request, we have to fetch the
437 real one, pointed by the request field of the issuer process */
439 const smx_actor_t issuer = MC_smx_simcall_get_issuer(saved_req);
440 smx_simcall_t req = &issuer->simcall;
442 /* TODO : handle test and testany simcalls */
443 e_mc_call_type_t call = MC_get_call_type(req);
444 mc_model_checker->handle_simcall(state->transition);
445 MC_handle_comm_pattern(call, req, req_num, nullptr, 1);
446 mc_model_checker->wait_for_requests();
448 /* Update statistics */
449 mc_model_checker->visited_states++;
450 mc_model_checker->executed_transitions++;
454 void CommunicationDeterminismChecker::main(void)
456 std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
457 smx_simcall_t req = nullptr;
459 while (!stack_.empty()) {
461 /* Get current state */
462 simgrid::mc::State* state = stack_.back().get();
464 XBT_DEBUG("**************************************************");
465 XBT_DEBUG("Exploration depth = %zi (state = %d, interleaved processes = %zd)",
466 stack_.size(), state->num,
467 state->interleaveSize());
469 /* Update statistics */
470 mc_model_checker->visited_states++;
472 if (stack_.size() <= (std::size_t) _sg_mc_max_depth
473 && (req = MC_state_get_request(state)) != nullptr
474 && (visited_state == nullptr)) {
476 int req_num = state->transition.argument;
478 XBT_DEBUG("Execute: %s",
479 simgrid::mc::request_to_string(
480 req, req_num, simgrid::mc::RequestType::simix).c_str());
483 if (dot_output != nullptr)
484 req_str = simgrid::mc::request_get_dot_output(req, req_num);
486 mc_model_checker->executed_transitions++;
488 /* TODO : handle test and testany simcalls */
489 e_mc_call_type_t call = MC_CALL_TYPE_NONE;
490 if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
491 call = MC_get_call_type(req);
493 /* Answer the request */
494 mc_model_checker->handle_simcall(state->transition);
495 /* After this call req is no longer useful */
497 if (!this->initial_communications_pattern_done)
498 MC_handle_comm_pattern(call, req, req_num, initial_communications_pattern, 0);
500 MC_handle_comm_pattern(call, req, req_num, nullptr, 0);
502 /* Wait for requests (schedules processes) */
503 mc_model_checker->wait_for_requests();
505 /* Create the new expanded state */
506 std::unique_ptr<simgrid::mc::State> next_state =
507 std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
509 /* If comm determinism verification, we cannot stop the exploration if
510 some communications are not finished (at least, data are transferred).
511 These communications are incomplete and they cannot be analyzed and
512 compared with the initial pattern. */
513 bool compare_snapshots = all_communications_are_finished()
514 && this->initial_communications_pattern_done;
516 if (_sg_mc_max_visited_states == 0 ||
517 (visited_state = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), compare_snapshots)) ==
520 /* Get enabled actors and insert them in the interleave set of the next state */
521 for (auto& actor : mc_model_checker->process().actors())
522 if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer()))
523 next_state->interleave(actor.copy.getBuffer());
525 if (dot_output != nullptr)
526 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
527 state->num, next_state->num, req_str.c_str());
529 } else if (dot_output != nullptr)
530 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
531 visited_state->original_num == -1 ? visited_state->num : visited_state->original_num, req_str.c_str());
533 stack_.push_back(std::move(next_state));
537 if (stack_.size() > (std::size_t) _sg_mc_max_depth)
538 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
539 else if (visited_state != nullptr)
540 XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.",
541 visited_state->original_num == -1 ? visited_state->num : visited_state->original_num);
543 XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
546 if (!this->initial_communications_pattern_done)
547 this->initial_communications_pattern_done = 1;
549 /* Trash the current state, no longer needed */
550 XBT_DEBUG("Delete state %d at depth %zi",
551 state->num, stack_.size());
554 visited_state = nullptr;
556 /* Check for deadlocks */
557 if (mc_model_checker->checkDeadlock()) {
559 throw new simgrid::mc::DeadlockError();
562 while (!stack_.empty()) {
563 std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
565 if (state->interleaveSize()
566 && stack_.size() < (std::size_t) _sg_mc_max_depth) {
567 /* We found a back-tracking point, let's loop */
568 XBT_DEBUG("Back-tracking to state %d at depth %zi",
569 state->num, stack_.size() + 1);
570 stack_.push_back(std::move(state));
572 this->restoreState();
574 XBT_DEBUG("Back-tracking to state %d at depth %zi done",
575 stack_.back()->num, stack_.size());
579 XBT_DEBUG("Delete state %d at depth %zi",
580 state->num, stack_.size() + 1);
586 simgrid::mc::session->logState();
589 void CommunicationDeterminismChecker::run()
591 XBT_INFO("Check communication determinism");
592 simgrid::mc::session->initialize();
599 Checker* createCommunicationDeterminismChecker(Session& session)
601 return new CommunicationDeterminismChecker(session);