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) {
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 == SIMIX_COMM_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(simgrid::mc::PatternCommunication* comm_pattern, smx_synchro_t comm_addr)
98 mc_model_checker->process().read(&comm, remote(comm_addr));
100 smx_process_t src_proc = mc_model_checker->process().resolveProcess(
101 simgrid::mc::remote(comm.comm.src_proc));
102 smx_process_t dst_proc = mc_model_checker->process().resolveProcess(
103 simgrid::mc::remote(comm.comm.dst_proc));
104 comm_pattern->src_proc = src_proc->pid;
105 comm_pattern->dst_proc = dst_proc->pid;
106 comm_pattern->src_host = MC_smx_process_get_host_name(src_proc);
107 comm_pattern->dst_host = MC_smx_process_get_host_name(dst_proc);
108 if (comm_pattern->data.size() == 0 && comm.comm.src_buff != nullptr) {
110 mc_model_checker->process().read(
111 &buff_size, remote(comm.comm.dst_buff_size));
112 comm_pattern->data.resize(buff_size);
113 mc_model_checker->process().read_bytes(
114 comm_pattern->data.data(), comm_pattern->data.size(),
115 remote(comm.comm.src_buff));
119 static void deterministic_comm_pattern(int process, simgrid::mc::PatternCommunication* comm, int backtracking) {
121 simgrid::mc::PatternCommunicationList* list =
122 xbt_dynar_get_as(initial_communications_pattern, process, simgrid::mc::PatternCommunicationList*);
125 e_mc_comm_pattern_difference_t diff =
126 compare_comm_pattern(list->list[list->index_comm].get(), comm);
128 if (diff != NONE_DIFF) {
129 if (comm->type == SIMIX_COMM_SEND){
130 simgrid::mc::initial_global_state->send_deterministic = 0;
131 if(simgrid::mc::initial_global_state->send_diff != nullptr)
132 xbt_free(simgrid::mc::initial_global_state->send_diff);
133 simgrid::mc::initial_global_state->send_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
135 simgrid::mc::initial_global_state->recv_deterministic = 0;
136 if(simgrid::mc::initial_global_state->recv_diff != nullptr)
137 xbt_free(simgrid::mc::initial_global_state->recv_diff);
138 simgrid::mc::initial_global_state->recv_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
140 if(_sg_mc_send_determinism && !simgrid::mc::initial_global_state->send_deterministic){
141 XBT_INFO("*********************************************************");
142 XBT_INFO("***** Non-send-deterministic communications pattern *****");
143 XBT_INFO("*********************************************************");
144 XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff);
145 xbt_free(simgrid::mc::initial_global_state->send_diff);
146 simgrid::mc::initial_global_state->send_diff = nullptr;
147 MC_print_statistics(mc_stats);
148 mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
149 }else if(_sg_mc_comms_determinism
150 && (!simgrid::mc::initial_global_state->send_deterministic
151 && !simgrid::mc::initial_global_state->recv_deterministic)) {
152 XBT_INFO("****************************************************");
153 XBT_INFO("***** Non-deterministic communications pattern *****");
154 XBT_INFO("****************************************************");
155 XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff);
156 XBT_INFO("%s", simgrid::mc::initial_global_state->recv_diff);
157 xbt_free(simgrid::mc::initial_global_state->send_diff);
158 simgrid::mc::initial_global_state->send_diff = nullptr;
159 xbt_free(simgrid::mc::initial_global_state->recv_diff);
160 simgrid::mc::initial_global_state->recv_diff = nullptr;
161 MC_print_statistics(mc_stats);
162 mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
168 /********** Non Static functions ***********/
170 void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking)
172 const smx_process_t issuer = MC_smx_simcall_get_issuer(request);
173 simgrid::mc::PatternCommunicationList* initial_pattern = xbt_dynar_get_as(
174 initial_communications_pattern, issuer->pid, simgrid::mc::PatternCommunicationList*);
175 xbt_dynar_t incomplete_pattern = xbt_dynar_get_as(
176 incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
178 std::unique_ptr<simgrid::mc::PatternCommunication> pattern =
179 std::unique_ptr<simgrid::mc::PatternCommunication>(
180 new simgrid::mc::PatternCommunication());
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_model_checker->process().resolveProcess(
196 simgrid::mc::remote(synchro.comm.src_proc))->pid;
197 pattern->src_host = MC_smx_process_get_host_name(issuer);
199 struct s_smpi_mpi_request mpi_request =
200 mc_model_checker->process().read<s_smpi_mpi_request>(
201 (std::uint64_t) simcall_comm_isend__get__data(request));
202 pattern->tag = mpi_request.tag;
204 if(synchro.comm.src_buff != nullptr){
205 pattern->data.resize(synchro.comm.src_buff_size);
206 mc_model_checker->process().read_bytes(
207 pattern->data.data(), pattern->data.size(),
208 remote(synchro.comm.src_buff));
210 if(mpi_request.detached){
211 if (!simgrid::mc::initial_global_state->initial_communications_pattern_done) {
212 /* Store comm pattern */
213 simgrid::mc::PatternCommunicationList* list = xbt_dynar_get_as(
214 initial_communications_pattern, pattern->src_proc,
215 simgrid::mc::PatternCommunicationList*);
216 list->list.push_back(std::move(pattern));
218 /* Evaluate comm determinism */
219 deterministic_comm_pattern(pattern->src_proc, pattern.get(), backtracking);
221 initial_communications_pattern, pattern->src_proc, simgrid::mc::PatternCommunicationList*
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_model_checker->process().resolveProcess(
243 simgrid::mc::remote(synchro.comm.dst_proc))->pid;
244 pattern->dst_host = MC_smx_process_get_host_name(issuer);
246 xbt_die("Unexpected call_type %i", (int) call_type);
248 XBT_DEBUG("Insert incomplete comm pattern %p for process %lu",
249 pattern.get(), issuer->pid);
251 xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
252 simgrid::mc::PatternCommunication* pattern2 = pattern.release();
253 xbt_dynar_push(dynar, &pattern2);
256 void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking) {
257 simgrid::mc::PatternCommunication* current_comm_pattern;
258 unsigned int cursor = 0;
259 std::unique_ptr<simgrid::mc::PatternCommunication> comm_pattern;
262 /* Complete comm pattern */
263 xbt_dynar_foreach(xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, current_comm_pattern)
264 if (current_comm_pattern->comm_addr == comm_addr) {
265 update_comm_pattern(current_comm_pattern, comm_addr);
267 simgrid::mc::PatternCommunication* temp;
269 xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t),
271 comm_pattern = std::unique_ptr<simgrid::mc::PatternCommunication>(temp);
272 XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", issuer, cursor);
277 xbt_die("Corresponding communication not found!");
279 simgrid::mc::PatternCommunicationList* pattern = xbt_dynar_get_as(
280 initial_communications_pattern, issuer, simgrid::mc::PatternCommunicationList*);
282 if (!simgrid::mc::initial_global_state->initial_communications_pattern_done)
283 /* Store comm pattern */
284 pattern->list.push_back(std::move(comm_pattern));
286 /* Evaluate comm determinism */
287 deterministic_comm_pattern(issuer, comm_pattern.get(), backtracking);
288 pattern->index_comm++;
293 /************************ Main algorithm ************************/
298 CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session& session)
304 CommunicationDeterminismChecker::~CommunicationDeterminismChecker()
309 RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override
312 for (auto const& state : stack_)
313 res.push_back(state->getTransition());
317 std::vector<std::string> CommunicationDeterminismChecker::getTextualTrace() // override
319 std::vector<std::string> trace;
320 for (auto const& state : stack_) {
321 smx_simcall_t req = &state->executed_req;
323 trace.push_back(simgrid::mc::request_to_string(
324 req, state->transition.argument, simgrid::mc::RequestType::executed));
329 void CommunicationDeterminismChecker::prepare()
333 const int maxpid = MC_smx_get_maxpid();
335 // Create initial_communications_pattern elements:
336 initial_communications_pattern = simgrid::xbt::newDeleteDynar<simgrid::mc::PatternCommunicationList*>();
337 for (i=0; i < maxpid; i++){
338 simgrid::mc::PatternCommunicationList* process_list_pattern = new simgrid::mc::PatternCommunicationList();
339 xbt_dynar_insert_at(initial_communications_pattern, i, &process_list_pattern);
342 // Create incomplete_communications_pattern elements:
343 incomplete_communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
344 for (i=0; i < maxpid; i++){
345 xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(simgrid::mc::PatternCommunication*), nullptr);
346 xbt_dynar_insert_at(incomplete_communications_pattern, i, &process_pattern);
349 std::unique_ptr<simgrid::mc::State> initial_state =
350 std::unique_ptr<simgrid::mc::State>(MC_state_new());
352 XBT_DEBUG("********* Start communication determinism verification *********");
354 /* Get an enabled process and insert it in the interleave set of the initial state */
355 for (auto& p : mc_model_checker->process().simix_processes())
356 if (simgrid::mc::process_is_enabled(&p.copy))
357 initial_state->interleave(&p.copy);
359 stack_.push_back(std::move(initial_state));
363 bool all_communications_are_finished()
365 for (size_t current_process = 1; current_process < MC_smx_get_maxpid(); current_process++) {
366 xbt_dynar_t pattern = xbt_dynar_get_as(
367 incomplete_communications_pattern, current_process, xbt_dynar_t);
368 if (!xbt_dynar_is_empty(pattern)) {
369 XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
376 int CommunicationDeterminismChecker::main(void)
378 std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
379 smx_simcall_t req = nullptr;
381 while (!stack_.empty()) {
383 /* Get current state */
384 simgrid::mc::State* state = stack_.back().get();
386 XBT_DEBUG("**************************************************");
387 XBT_DEBUG("Exploration depth = %zi (state = %d, interleaved processes = %zd)",
388 stack_.size(), state->num,
389 state->interleaveSize());
391 /* Update statistics */
392 mc_stats->visited_states++;
394 if (stack_.size() <= (std::size_t) _sg_mc_max_depth
395 && (req = MC_state_get_request(state)) != nullptr
396 && (visited_state == nullptr)) {
398 int req_num = state->transition.argument;
400 XBT_DEBUG("Execute: %s",
401 simgrid::mc::request_to_string(
402 req, req_num, simgrid::mc::RequestType::simix).c_str());
405 if (dot_output != nullptr)
406 req_str = simgrid::mc::request_get_dot_output(req, req_num);
408 mc_stats->executed_transitions++;
410 /* TODO : handle test and testany simcalls */
411 e_mc_call_type_t call = MC_CALL_TYPE_NONE;
412 if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
413 call = MC_get_call_type(req);
415 /* Answer the request */
416 mc_model_checker->handle_simcall(state->transition);
417 /* After this call req is no longer useful */
419 if(!initial_global_state->initial_communications_pattern_done)
420 MC_handle_comm_pattern(call, req, req_num, initial_communications_pattern, 0);
422 MC_handle_comm_pattern(call, req, req_num, nullptr, 0);
424 /* Wait for requests (schedules processes) */
425 mc_model_checker->wait_for_requests();
427 /* Create the new expanded state */
428 std::unique_ptr<simgrid::mc::State> next_state =
429 std::unique_ptr<simgrid::mc::State>(MC_state_new());
431 /* If comm determinism verification, we cannot stop the exploration if
432 some communications are not finished (at least, data are transfered).
433 These communications are incomplete and they cannot be analyzed and
434 compared with the initial pattern. */
435 bool compare_snapshots = all_communications_are_finished()
436 && initial_global_state->initial_communications_pattern_done;
438 if (_sg_mc_visited == 0
439 || (visited_state = visitedStates_.addVisitedState(next_state.get(), compare_snapshots)) == nullptr) {
441 /* Get enabled processes and insert them in the interleave set of the next state */
442 for (auto& p : mc_model_checker->process().simix_processes())
443 if (simgrid::mc::process_is_enabled(&p.copy))
444 next_state->interleave(&p.copy);
446 if (dot_output != nullptr)
447 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
448 state->num, next_state->num, req_str.c_str());
450 } else if (dot_output != nullptr)
451 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
452 state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str.c_str());
454 stack_.push_back(std::move(next_state));
458 if (stack_.size() > (std::size_t) _sg_mc_max_depth)
459 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
460 else if (visited_state != nullptr)
461 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);
463 XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
466 if (!initial_global_state->initial_communications_pattern_done)
467 initial_global_state->initial_communications_pattern_done = 1;
469 /* Trash the current state, no longer needed */
470 XBT_DEBUG("Delete state %d at depth %zi",
471 state->num, stack_.size());
474 visited_state = nullptr;
476 /* Check for deadlocks */
477 if (mc_model_checker->checkDeadlock()) {
479 return SIMGRID_MC_EXIT_DEADLOCK;
482 while (!stack_.empty()) {
483 std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
485 if (state->interleaveSize()
486 && stack_.size() < (std::size_t) _sg_mc_max_depth) {
487 /* We found a back-tracking point, let's loop */
488 XBT_DEBUG("Back-tracking to state %d at depth %zi",
489 state->num, stack_.size() + 1);
490 stack_.push_back(std::move(state));
492 simgrid::mc::replay(stack_);
494 XBT_DEBUG("Back-tracking to state %d at depth %zi done",
495 stack_.back()->num, stack_.size());
499 XBT_DEBUG("Delete state %d at depth %zi",
500 state->num, stack_.size() + 1);
506 MC_print_statistics(mc_stats);
507 return SIMGRID_MC_EXIT_SUCCESS;
510 int CommunicationDeterminismChecker::run()
512 XBT_INFO("Check communication determinism");
513 mc_model_checker->wait_for_requests();
517 initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
518 initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
519 initial_global_state->initial_communications_pattern_done = 0;
520 initial_global_state->recv_deterministic = 1;
521 initial_global_state->send_deterministic = 1;
522 initial_global_state->recv_diff = nullptr;
523 initial_global_state->send_diff = nullptr;
525 int res = this->main();
526 initial_global_state = nullptr;
530 Checker* createCommunicationDeterminismChecker(Session& session)
532 return new CommunicationDeterminismChecker(session);