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"
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(mc_comm_pattern_t comm1, mc_comm_pattern_t comm2) {
39 if(comm1->type != comm2->type)
41 if (comm1->rdv != comm2->rdv)
43 if (comm1->src_proc != comm2->src_proc)
45 if (comm1->dst_proc != comm2->dst_proc)
47 if (comm1->tag != comm2->tag)
49 if (comm1->data.size() != comm2->data.size())
50 return DATA_SIZE_DIFF;
51 if (comm1->data != comm2->data)
56 static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int process, mc_comm_pattern_t comm, unsigned int cursor) {
59 if(comm->type == SIMIX_COMM_SEND)
60 type = bprintf("The send communications pattern of the process %d is different!", process - 1);
62 type = bprintf("The recv communications pattern of the process %d is different!", process - 1);
66 res = bprintf("%s Different type for communication #%d", type, cursor);
69 res = bprintf("%s Different rdv for communication #%d", type, cursor);
72 res = bprintf("%s Different tag for communication #%d", type, cursor);
75 res = bprintf("%s Different source for communication #%d", type, cursor);
78 res = bprintf("%s Different destination for communication #%d", type, cursor);
81 res = bprintf("%s\n Different data size for communication #%d", type, cursor);
84 res = bprintf("%s\n Different data for communication #%d", type, cursor);
94 static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t comm_addr)
97 mc_model_checker->process().read(&comm, remote(comm_addr));
99 smx_process_t src_proc = MC_smx_resolve_process(comm.comm.src_proc);
100 smx_process_t dst_proc = MC_smx_resolve_process(comm.comm.dst_proc);
101 comm_pattern->src_proc = src_proc->pid;
102 comm_pattern->dst_proc = dst_proc->pid;
103 comm_pattern->src_host = MC_smx_process_get_host_name(src_proc);
104 comm_pattern->dst_host = MC_smx_process_get_host_name(dst_proc);
105 if (comm_pattern->data.size() == 0 && comm.comm.src_buff != nullptr) {
107 mc_model_checker->process().read(
108 &buff_size, remote(comm.comm.dst_buff_size));
109 comm_pattern->data.resize(buff_size);
110 mc_model_checker->process().read_bytes(
111 comm_pattern->data.data(), comm_pattern->data.size(),
112 remote(comm.comm.src_buff));
116 static void deterministic_comm_pattern(int process, mc_comm_pattern_t comm, int backtracking) {
118 mc_list_comm_pattern_t list =
119 xbt_dynar_get_as(initial_communications_pattern, process, mc_list_comm_pattern_t);
122 mc_comm_pattern_t initial_comm =
123 xbt_dynar_get_as(list->list, list->index_comm, mc_comm_pattern_t);
124 e_mc_comm_pattern_difference_t diff =
125 compare_comm_pattern(initial_comm, comm);
127 if (diff != NONE_DIFF) {
128 if (comm->type == SIMIX_COMM_SEND){
129 simgrid::mc::initial_global_state->send_deterministic = 0;
130 if(simgrid::mc::initial_global_state->send_diff != nullptr)
131 xbt_free(simgrid::mc::initial_global_state->send_diff);
132 simgrid::mc::initial_global_state->send_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
134 simgrid::mc::initial_global_state->recv_deterministic = 0;
135 if(simgrid::mc::initial_global_state->recv_diff != nullptr)
136 xbt_free(simgrid::mc::initial_global_state->recv_diff);
137 simgrid::mc::initial_global_state->recv_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
139 if(_sg_mc_send_determinism && !simgrid::mc::initial_global_state->send_deterministic){
140 XBT_INFO("*********************************************************");
141 XBT_INFO("***** Non-send-deterministic communications pattern *****");
142 XBT_INFO("*********************************************************");
143 XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff);
144 xbt_free(simgrid::mc::initial_global_state->send_diff);
145 simgrid::mc::initial_global_state->send_diff = nullptr;
146 MC_print_statistics(mc_stats);
147 mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
148 }else if(_sg_mc_comms_determinism
149 && (!simgrid::mc::initial_global_state->send_deterministic
150 && !simgrid::mc::initial_global_state->recv_deterministic)) {
151 XBT_INFO("****************************************************");
152 XBT_INFO("***** Non-deterministic communications pattern *****");
153 XBT_INFO("****************************************************");
154 XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff);
155 XBT_INFO("%s", simgrid::mc::initial_global_state->recv_diff);
156 xbt_free(simgrid::mc::initial_global_state->send_diff);
157 simgrid::mc::initial_global_state->send_diff = nullptr;
158 xbt_free(simgrid::mc::initial_global_state->recv_diff);
159 simgrid::mc::initial_global_state->recv_diff = nullptr;
160 MC_print_statistics(mc_stats);
161 mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
166 MC_comm_pattern_free(comm);
170 /********** Non Static functions ***********/
172 void MC_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 mc_list_comm_pattern_t initial_pattern = xbt_dynar_get_as(
176 initial_communications_pattern, issuer->pid, mc_list_comm_pattern_t);
177 xbt_dynar_t incomplete_pattern = xbt_dynar_get_as(
178 incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
180 mc_comm_pattern_t pattern = new s_mc_comm_pattern_t();
182 initial_pattern->index_comm + xbt_dynar_length(incomplete_pattern);
184 if (call_type == MC_CALL_TYPE_SEND) {
185 /* Create comm pattern */
186 pattern->type = SIMIX_COMM_SEND;
187 pattern->comm_addr = simcall_comm_isend__get__result(request);
189 s_smx_synchro_t synchro = mc_model_checker->process().read<s_smx_synchro_t>(
190 (std::uint64_t) pattern->comm_addr);
192 char* remote_name = mc_model_checker->process().read<char*>(
193 (std::uint64_t)(synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name));
194 pattern->rdv = mc_model_checker->process().read_string(remote_name);
195 pattern->src_proc = MC_smx_resolve_process(synchro.comm.src_proc)->pid;
196 pattern->src_host = MC_smx_process_get_host_name(issuer);
198 struct s_smpi_mpi_request mpi_request =
199 mc_model_checker->process().read<s_smpi_mpi_request>(
200 (std::uint64_t) simcall_comm_isend__get__data(request));
201 pattern->tag = mpi_request.tag;
203 if(synchro.comm.src_buff != nullptr){
204 pattern->data.resize(synchro.comm.src_buff_size);
205 mc_model_checker->process().read_bytes(
206 pattern->data.data(), pattern->data.size(),
207 remote(synchro.comm.src_buff));
209 if(mpi_request.detached){
210 if (!simgrid::mc::initial_global_state->initial_communications_pattern_done) {
211 /* Store comm pattern */
214 initial_communications_pattern, pattern->src_proc, mc_list_comm_pattern_t
218 /* Evaluate comm determinism */
219 deterministic_comm_pattern(pattern->src_proc, pattern, backtracking);
221 initial_communications_pattern, pattern->src_proc, mc_list_comm_pattern_t
226 } else if (call_type == MC_CALL_TYPE_RECV) {
227 pattern->type = SIMIX_COMM_RECEIVE;
228 pattern->comm_addr = simcall_comm_irecv__get__result(request);
230 struct s_smpi_mpi_request mpi_request;
231 mc_model_checker->process().read(
232 &mpi_request, remote((struct s_smpi_mpi_request*)simcall_comm_irecv__get__data(request)));
233 pattern->tag = mpi_request.tag;
235 s_smx_synchro_t synchro;
236 mc_model_checker->process().read(&synchro, remote(pattern->comm_addr));
239 mc_model_checker->process().read(&remote_name,
240 remote(synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name));
241 pattern->rdv = mc_model_checker->process().read_string(remote_name);
242 pattern->dst_proc = MC_smx_resolve_process(synchro.comm.dst_proc)->pid;
243 pattern->dst_host = MC_smx_process_get_host_name(issuer);
245 xbt_die("Unexpected call_type %i", (int) call_type);
248 xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t),
251 XBT_DEBUG("Insert incomplete comm pattern %p for process %lu", pattern, issuer->pid);
254 void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking) {
255 mc_comm_pattern_t current_comm_pattern;
256 unsigned int cursor = 0;
257 mc_comm_pattern_t comm_pattern;
260 /* Complete comm pattern */
261 xbt_dynar_foreach(xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, current_comm_pattern)
262 if (current_comm_pattern->comm_addr == comm_addr) {
263 update_comm_pattern(current_comm_pattern, comm_addr);
266 xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t),
267 cursor, &comm_pattern);
268 XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", issuer, cursor);
273 xbt_die("Corresponding communication not found!");
275 mc_list_comm_pattern_t pattern = xbt_dynar_get_as(
276 initial_communications_pattern, issuer, mc_list_comm_pattern_t);
278 if (!simgrid::mc::initial_global_state->initial_communications_pattern_done)
279 /* Store comm pattern */
280 xbt_dynar_push(pattern->list, &comm_pattern);
282 /* Evaluate comm determinism */
283 deterministic_comm_pattern(issuer, comm_pattern, backtracking);
284 pattern->index_comm++;
289 /************************ Main algorithm ************************/
294 CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session& session)
300 CommunicationDeterminismChecker::~CommunicationDeterminismChecker()
305 // TODO, deduplicate with SafetyChecker
306 RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override
309 for (auto const& state : stack_) {
311 smx_simcall_t saved_req = MC_state_get_executed_request(state.get(), &value);
312 const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
313 const int pid = issuer->pid;
314 res.push_back(RecordTraceElement(pid, value));
319 // TODO, deduplicate with SafetyChecker
320 std::vector<std::string> CommunicationDeterminismChecker::getTextualTrace() // override
322 std::vector<std::string> trace;
323 for (auto const& state : stack_) {
325 smx_simcall_t req = MC_state_get_executed_request(state.get(), &value);
327 trace.push_back(simgrid::mc::request_to_string(
328 req, value, simgrid::mc::RequestType::executed));
333 void CommunicationDeterminismChecker::prepare()
337 const int maxpid = MC_smx_get_maxpid();
339 // Create initial_communications_pattern elements:
340 initial_communications_pattern = xbt_dynar_new(sizeof(mc_list_comm_pattern_t), MC_list_comm_pattern_free_voidp);
341 for (i=0; i < maxpid; i++){
342 mc_list_comm_pattern_t process_list_pattern = xbt_new0(s_mc_list_comm_pattern_t, 1);
343 process_list_pattern->list = xbt_dynar_new(sizeof(mc_comm_pattern_t), MC_comm_pattern_free_voidp);
344 process_list_pattern->index_comm = 0;
345 xbt_dynar_insert_at(initial_communications_pattern, i, &process_list_pattern);
348 // Create incomplete_communications_pattern elements:
349 incomplete_communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
350 for (i=0; i < maxpid; i++){
351 xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), nullptr);
352 xbt_dynar_insert_at(incomplete_communications_pattern, i, &process_pattern);
355 std::unique_ptr<simgrid::mc::State> initial_state =
356 std::unique_ptr<simgrid::mc::State>(MC_state_new());
358 XBT_DEBUG("********* Start communication determinism verification *********");
360 /* Wait for requests (schedules processes) */
361 mc_model_checker->wait_for_requests();
363 /* Get an enabled process and insert it in the interleave set of the initial state */
364 for (auto& p : mc_model_checker->process().simix_processes())
365 if (simgrid::mc::process_is_enabled(&p.copy))
366 MC_state_interleave_process(initial_state.get(), &p.copy);
368 stack_.push_back(std::move(initial_state));
372 bool all_communications_are_finished()
374 for (size_t current_process = 1; current_process < MC_smx_get_maxpid(); current_process++) {
375 xbt_dynar_t pattern = xbt_dynar_get_as(
376 incomplete_communications_pattern, current_process, xbt_dynar_t);
377 if (!xbt_dynar_is_empty(pattern)) {
378 XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
385 int CommunicationDeterminismChecker::main(void)
388 std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
389 smx_simcall_t req = nullptr;
391 while (!stack_.empty()) {
393 /* Get current state */
394 simgrid::mc::State* state = stack_.back().get();
396 XBT_DEBUG("**************************************************");
397 XBT_DEBUG("Exploration depth = %zi (state = %d, interleaved processes = %zd)",
398 stack_.size(), state->num,
399 state->interleaveSize());
401 /* Update statistics */
402 mc_stats->visited_states++;
404 if (stack_.size() <= (std::size_t) _sg_mc_max_depth
405 && (req = MC_state_get_request(state, &value))
406 && (visited_state == nullptr)) {
408 XBT_DEBUG("Execute: %s",
409 simgrid::mc::request_to_string(
410 req, value, simgrid::mc::RequestType::simix).c_str());
412 char* req_str = nullptr;
413 if (dot_output != nullptr)
414 req_str = simgrid::mc::request_get_dot_output(req, value);
416 MC_state_set_executed_request(state, req, value);
417 mc_stats->executed_transitions++;
419 /* TODO : handle test and testany simcalls */
420 e_mc_call_type_t call = MC_CALL_TYPE_NONE;
421 if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
422 call = MC_get_call_type(req);
424 /* Answer the request */
425 simgrid::mc::handle_simcall(req, value); /* After this call req is no longer useful */
427 if(!initial_global_state->initial_communications_pattern_done)
428 MC_handle_comm_pattern(call, req, value, initial_communications_pattern, 0);
430 MC_handle_comm_pattern(call, req, value, nullptr, 0);
432 /* Wait for requests (schedules processes) */
433 mc_model_checker->wait_for_requests();
435 /* Create the new expanded state */
436 std::unique_ptr<simgrid::mc::State> next_state =
437 std::unique_ptr<simgrid::mc::State>(MC_state_new());
439 /* If comm determinism verification, we cannot stop the exploration if
440 some communications are not finished (at least, data are transfered).
441 These communications are incomplete and they cannot be analyzed and
442 compared with the initial pattern. */
443 bool compare_snapshots = all_communications_are_finished()
444 && initial_global_state->initial_communications_pattern_done;
446 if (_sg_mc_visited == 0
447 || (visited_state = visitedStates_.addVisitedState(next_state.get(), compare_snapshots)) == nullptr) {
449 /* Get enabled processes and insert them in the interleave set of the next state */
450 for (auto& p : mc_model_checker->process().simix_processes())
451 if (simgrid::mc::process_is_enabled(&p.copy))
452 MC_state_interleave_process(next_state.get(), &p.copy);
454 if (dot_output != nullptr)
455 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
457 } else if (dot_output != nullptr)
458 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
459 state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
461 stack_.push_back(std::move(next_state));
463 if (dot_output != nullptr)
468 if (stack_.size() > (std::size_t) _sg_mc_max_depth)
469 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
470 else if (visited_state != nullptr)
471 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);
473 XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
476 if (!initial_global_state->initial_communications_pattern_done)
477 initial_global_state->initial_communications_pattern_done = 1;
479 /* Trash the current state, no longer needed */
480 XBT_DEBUG("Delete state %d at depth %zi",
481 state->num, stack_.size());
484 visited_state = nullptr;
486 /* Check for deadlocks */
487 if (mc_model_checker->checkDeadlock()) {
489 return SIMGRID_MC_EXIT_DEADLOCK;
492 while (!stack_.empty()) {
493 std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
495 if (state->interleaveSize()
496 && stack_.size() < (std::size_t) _sg_mc_max_depth) {
497 /* We found a back-tracking point, let's loop */
498 XBT_DEBUG("Back-tracking to state %d at depth %zi",
499 state->num, stack_.size() + 1);
500 stack_.push_back(std::move(state));
502 simgrid::mc::replay(stack_);
504 XBT_DEBUG("Back-tracking to state %d at depth %zi done",
505 stack_.back()->num, stack_.size());
509 XBT_DEBUG("Delete state %d at depth %zi",
510 state->num, stack_.size() + 1);
516 MC_print_statistics(mc_stats);
517 return SIMGRID_MC_EXIT_SUCCESS;
520 int CommunicationDeterminismChecker::run()
522 XBT_INFO("Check communication determinism");
523 mc_model_checker->wait_for_requests();
525 if (mc_mode == MC_MODE_CLIENT)
526 // This will move somehwere else:
527 simgrid::mc::Client::get()->handleMessages();
531 initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
532 initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
533 initial_global_state->initial_communications_pattern_done = 0;
534 initial_global_state->recv_deterministic = 1;
535 initial_global_state->send_deterministic = 1;
536 initial_global_state->recv_diff = nullptr;
537 initial_global_state->send_diff = nullptr;
539 int res = this->main();
540 initial_global_state = nullptr;
544 Checker* createCommunicationDeterminismChecker(Session& session)
546 return new CommunicationDeterminismChecker(session);