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/mc_state.h"
14 #include "src/mc/mc_comm_pattern.h"
15 #include "src/mc/mc_request.h"
16 #include "src/mc/mc_safety.h"
17 #include "src/mc/mc_private.h"
18 #include "src/mc/mc_record.h"
19 #include "src/mc/mc_smx.h"
20 #include "src/mc/Client.hpp"
21 #include "src/mc/checker/CommunicationDeterminismChecker.hpp"
22 #include "src/mc/mc_exit.h"
23 #include "src/mc/VisitedState.hpp"
24 #include "src/mc/Transition.hpp"
26 using simgrid::mc::remote;
28 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_determinism, mc,
29 "Logging specific to MC communication determinism detection");
31 /********** Global variables **********/
33 xbt_dynar_t initial_communications_pattern;
34 xbt_dynar_t incomplete_communications_pattern;
36 /********** Static functions ***********/
38 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 == simgrid::mc::PatternCommunicationType::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(
96 simgrid::mc::PatternCommunication* comm_pattern,
97 simgrid::mc::RemotePtr<simgrid::kernel::activity::Comm> comm_addr)
100 simgrid::mc::Remote<simgrid::kernel::activity::Comm> temp_comm;
101 mc_model_checker->process().read(temp_comm, comm_addr);
102 simgrid::kernel::activity::Comm* comm = temp_comm.getBuffer();
104 smx_actor_t src_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->src_proc));
105 smx_actor_t dst_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->dst_proc));
106 comm_pattern->src_proc = src_proc->pid;
107 comm_pattern->dst_proc = dst_proc->pid;
108 comm_pattern->src_host = MC_smx_actor_get_host_name(src_proc);
109 comm_pattern->dst_host = MC_smx_actor_get_host_name(dst_proc);
110 if (comm_pattern->data.size() == 0 && comm->src_buff != nullptr) {
112 mc_model_checker->process().read(
113 &buff_size, remote(comm->dst_buff_size));
114 comm_pattern->data.resize(buff_size);
115 mc_model_checker->process().read_bytes(
116 comm_pattern->data.data(), comm_pattern->data.size(),
117 remote(comm->src_buff));
124 void CommunicationDeterminismChecker::deterministic_comm_pattern(
125 int process, simgrid::mc::PatternCommunication* comm, int backtracking)
127 simgrid::mc::PatternCommunicationList* list =
128 xbt_dynar_get_as(initial_communications_pattern, process, simgrid::mc::PatternCommunicationList*);
131 e_mc_comm_pattern_difference_t diff =
132 compare_comm_pattern(list->list[list->index_comm].get(), comm);
134 if (diff != NONE_DIFF) {
135 if (comm->type == simgrid::mc::PatternCommunicationType::send) {
136 this->send_deterministic = 0;
137 if (this->send_diff != nullptr)
138 xbt_free(this->send_diff);
139 this->send_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
141 this->recv_deterministic = 0;
142 if (this->recv_diff != nullptr)
143 xbt_free(this->recv_diff);
144 this->recv_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
146 if(_sg_mc_send_determinism && !this->send_deterministic){
147 XBT_INFO("*********************************************************");
148 XBT_INFO("***** Non-send-deterministic communications pattern *****");
149 XBT_INFO("*********************************************************");
150 XBT_INFO("%s", this->send_diff);
151 xbt_free(this->send_diff);
152 this->send_diff = nullptr;
153 simgrid::mc::session->logState();
154 mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
155 }else if(_sg_mc_comms_determinism
156 && (!this->send_deterministic && !this->recv_deterministic)) {
157 XBT_INFO("****************************************************");
158 XBT_INFO("***** Non-deterministic communications pattern *****");
159 XBT_INFO("****************************************************");
160 XBT_INFO("%s", this->send_diff);
161 XBT_INFO("%s", this->recv_diff);
162 xbt_free(this->send_diff);
163 this->send_diff = nullptr;
164 xbt_free(this->recv_diff);
165 this->recv_diff = nullptr;
166 simgrid::mc::session->logState();
167 mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
173 /********** Non Static functions ***********/
175 void CommunicationDeterminismChecker::get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking)
177 const smx_actor_t issuer = MC_smx_simcall_get_issuer(request);
178 simgrid::mc::PatternCommunicationList* initial_pattern = xbt_dynar_get_as(
179 initial_communications_pattern, issuer->pid, simgrid::mc::PatternCommunicationList*);
180 xbt_dynar_t incomplete_pattern = xbt_dynar_get_as(
181 incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
183 std::unique_ptr<simgrid::mc::PatternCommunication> pattern =
184 std::unique_ptr<simgrid::mc::PatternCommunication>(
185 new simgrid::mc::PatternCommunication());
187 initial_pattern->index_comm + xbt_dynar_length(incomplete_pattern);
189 if (call_type == MC_CALL_TYPE_SEND) {
190 /* Create comm pattern */
191 pattern->type = simgrid::mc::PatternCommunicationType::send;
192 pattern->comm_addr = simcall_comm_isend__get__result(request);
194 simgrid::mc::Remote<simgrid::kernel::activity::Comm> temp_synchro;
195 mc_model_checker->process().read(temp_synchro, remote(
196 static_cast<simgrid::kernel::activity::Comm*>(pattern->comm_addr)));
197 simgrid::kernel::activity::Comm* synchro =
198 static_cast<simgrid::kernel::activity::Comm*>(temp_synchro.getBuffer());
200 char* remote_name = mc_model_checker->process().read<char*>(
201 (std::uint64_t)(synchro->mbox ? &synchro->mbox->name : &synchro->mbox_cpy->name));
202 pattern->rdv = mc_model_checker->process().read_string(remote_name);
203 pattern->src_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(synchro->src_proc))->pid;
204 pattern->src_host = MC_smx_actor_get_host_name(issuer);
206 struct s_smpi_mpi_request mpi_request =
207 mc_model_checker->process().read<s_smpi_mpi_request>(
208 (std::uint64_t) simcall_comm_isend__get__data(request));
209 pattern->tag = mpi_request.tag;
211 if (synchro->src_buff != nullptr){
212 pattern->data.resize(synchro->src_buff_size);
213 mc_model_checker->process().read_bytes(
214 pattern->data.data(), pattern->data.size(),
215 remote(synchro->src_buff));
217 if(mpi_request.detached){
218 if (!this->initial_communications_pattern_done) {
219 /* Store comm pattern */
220 simgrid::mc::PatternCommunicationList* list = xbt_dynar_get_as(
221 initial_communications_pattern, pattern->src_proc,
222 simgrid::mc::PatternCommunicationList*);
223 list->list.push_back(std::move(pattern));
225 /* Evaluate comm determinism */
226 this->deterministic_comm_pattern(pattern->src_proc, pattern.get(), backtracking);
228 initial_communications_pattern, pattern->src_proc, simgrid::mc::PatternCommunicationList*
233 } else if (call_type == MC_CALL_TYPE_RECV) {
234 pattern->type = simgrid::mc::PatternCommunicationType::receive;
235 pattern->comm_addr = simcall_comm_irecv__get__result(request);
237 struct s_smpi_mpi_request mpi_request;
238 mc_model_checker->process().read(
239 &mpi_request, remote((struct s_smpi_mpi_request*)simcall_comm_irecv__get__data(request)));
240 pattern->tag = mpi_request.tag;
242 simgrid::mc::Remote<simgrid::kernel::activity::Comm> temp_comm;
243 mc_model_checker->process().read(temp_comm, remote(
244 static_cast<simgrid::kernel::activity::Comm*>(pattern->comm_addr)));
245 simgrid::kernel::activity::Comm* comm = temp_comm.getBuffer();
248 mc_model_checker->process().read(&remote_name,
249 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_visited == 0
517 || (visited_state = visitedStates_.addVisitedState(
518 expandedStatesCount_, next_state.get(), compare_snapshots)) == nullptr) {
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",
531 state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_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.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num);
542 XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
545 if (!this->initial_communications_pattern_done)
546 this->initial_communications_pattern_done = 1;
548 /* Trash the current state, no longer needed */
549 XBT_DEBUG("Delete state %d at depth %zi",
550 state->num, stack_.size());
553 visited_state = nullptr;
555 /* Check for deadlocks */
556 if (mc_model_checker->checkDeadlock()) {
558 throw new simgrid::mc::DeadlockError();
561 while (!stack_.empty()) {
562 std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
564 if (state->interleaveSize()
565 && stack_.size() < (std::size_t) _sg_mc_max_depth) {
566 /* We found a back-tracking point, let's loop */
567 XBT_DEBUG("Back-tracking to state %d at depth %zi",
568 state->num, stack_.size() + 1);
569 stack_.push_back(std::move(state));
571 this->restoreState();
573 XBT_DEBUG("Back-tracking to state %d at depth %zi done",
574 stack_.back()->num, stack_.size());
578 XBT_DEBUG("Delete state %d at depth %zi",
579 state->num, stack_.size() + 1);
585 simgrid::mc::session->logState();
588 void CommunicationDeterminismChecker::run()
590 XBT_INFO("Check communication determinism");
591 simgrid::mc::session->initialize();
598 Checker* createCommunicationDeterminismChecker(Session& session)
600 return new CommunicationDeterminismChecker(session);