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());
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",
456 state->num, next_state->num, req_str.c_str());
458 } else if (dot_output != nullptr)
459 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
460 state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str.c_str());
462 stack_.push_back(std::move(next_state));
466 if (stack_.size() > (std::size_t) _sg_mc_max_depth)
467 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
468 else if (visited_state != nullptr)
469 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);
471 XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
474 if (!initial_global_state->initial_communications_pattern_done)
475 initial_global_state->initial_communications_pattern_done = 1;
477 /* Trash the current state, no longer needed */
478 XBT_DEBUG("Delete state %d at depth %zi",
479 state->num, stack_.size());
482 visited_state = nullptr;
484 /* Check for deadlocks */
485 if (mc_model_checker->checkDeadlock()) {
487 return SIMGRID_MC_EXIT_DEADLOCK;
490 while (!stack_.empty()) {
491 std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
493 if (state->interleaveSize()
494 && stack_.size() < (std::size_t) _sg_mc_max_depth) {
495 /* We found a back-tracking point, let's loop */
496 XBT_DEBUG("Back-tracking to state %d at depth %zi",
497 state->num, stack_.size() + 1);
498 stack_.push_back(std::move(state));
500 simgrid::mc::replay(stack_);
502 XBT_DEBUG("Back-tracking to state %d at depth %zi done",
503 stack_.back()->num, stack_.size());
507 XBT_DEBUG("Delete state %d at depth %zi",
508 state->num, stack_.size() + 1);
514 MC_print_statistics(mc_stats);
515 return SIMGRID_MC_EXIT_SUCCESS;
518 int CommunicationDeterminismChecker::run()
520 XBT_INFO("Check communication determinism");
521 mc_model_checker->wait_for_requests();
525 initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
526 initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
527 initial_global_state->initial_communications_pattern_done = 0;
528 initial_global_state->recv_deterministic = 1;
529 initial_global_state->send_deterministic = 1;
530 initial_global_state->recv_diff = nullptr;
531 initial_global_state->send_diff = nullptr;
533 int res = this->main();
534 initial_global_state = nullptr;
538 Checker* createCommunicationDeterminismChecker(Session& session)
540 return new CommunicationDeterminismChecker(session);