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>
13 #include <xbt/sysdep.h>
15 #include "src/mc/mc_state.h"
16 #include "src/mc/mc_comm_pattern.h"
17 #include "src/mc/mc_request.h"
18 #include "src/mc/mc_safety.h"
19 #include "src/mc/mc_private.h"
20 #include "src/mc/mc_record.h"
21 #include "src/mc/mc_smx.h"
22 #include "src/mc/Client.hpp"
23 #include "src/mc/CommunicationDeterminismChecker.hpp"
24 #include "src/mc/mc_exit.h"
26 using simgrid::mc::remote;
28 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_determinism, mc,
29 "Logging specific to MC communication determinism detection");
31 XBT_PRIVATE static std::list<simgrid::mc::State*> mc_stack;
33 /********** Global variables **********/
35 xbt_dynar_t initial_communications_pattern;
36 xbt_dynar_t incomplete_communications_pattern;
38 /********** Static functions ***********/
40 static e_mc_comm_pattern_difference_t compare_comm_pattern(mc_comm_pattern_t comm1, mc_comm_pattern_t comm2) {
41 if(comm1->type != comm2->type)
43 if (strcmp(comm1->rdv, comm2->rdv) != 0)
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 == nullptr && comm2->data == NULL)
55 if(comm1->data != nullptr && comm2->data !=NULL) {
56 if (!memcmp(comm1->data, comm2->data, comm1->data_size))
64 static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int process, mc_comm_pattern_t comm, unsigned int cursor) {
67 if(comm->type == SIMIX_COMM_SEND)
68 type = bprintf("The send communications pattern of the process %d is different!", process - 1);
70 type = bprintf("The recv communications pattern of the process %d is different!", process - 1);
74 res = bprintf("%s Different type for communication #%d", type, cursor);
77 res = bprintf("%s Different rdv for communication #%d", type, cursor);
80 res = bprintf("%s Different tag for communication #%d", type, cursor);
83 res = bprintf("%s Different source for communication #%d", type, cursor);
86 res = bprintf("%s Different destination for communication #%d", type, cursor);
89 res = bprintf("%s\n Different data size for communication #%d", type, cursor);
92 res = bprintf("%s\n Different data for communication #%d", type, cursor);
102 static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t comm_addr)
104 s_smx_synchro_t comm;
105 mc_model_checker->process().read(&comm, remote(comm_addr));
107 smx_process_t src_proc = MC_smx_resolve_process(comm.comm.src_proc);
108 smx_process_t dst_proc = MC_smx_resolve_process(comm.comm.dst_proc);
109 comm_pattern->src_proc = src_proc->pid;
110 comm_pattern->dst_proc = dst_proc->pid;
111 comm_pattern->src_host = MC_smx_process_get_host_name(src_proc);
112 comm_pattern->dst_host = MC_smx_process_get_host_name(dst_proc);
113 if (comm_pattern->data_size == -1 && comm.comm.src_buff != nullptr) {
115 mc_model_checker->process().read(
116 &buff_size, remote(comm.comm.dst_buff_size));
117 comm_pattern->data_size = buff_size;
118 comm_pattern->data = xbt_malloc0(comm_pattern->data_size);
119 mc_model_checker->process().read_bytes(
120 comm_pattern->data, comm_pattern->data_size,
121 remote(comm.comm.src_buff));
125 static void deterministic_comm_pattern(int process, mc_comm_pattern_t comm, int backtracking) {
127 mc_list_comm_pattern_t list =
128 xbt_dynar_get_as(initial_communications_pattern, process, mc_list_comm_pattern_t);
131 mc_comm_pattern_t initial_comm =
132 xbt_dynar_get_as(list->list, list->index_comm, mc_comm_pattern_t);
133 e_mc_comm_pattern_difference_t diff =
134 compare_comm_pattern(initial_comm, comm);
136 if (diff != NONE_DIFF) {
137 if (comm->type == SIMIX_COMM_SEND){
138 simgrid::mc::initial_global_state->send_deterministic = 0;
139 if(simgrid::mc::initial_global_state->send_diff != nullptr)
140 xbt_free(simgrid::mc::initial_global_state->send_diff);
141 simgrid::mc::initial_global_state->send_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
143 simgrid::mc::initial_global_state->recv_deterministic = 0;
144 if(simgrid::mc::initial_global_state->recv_diff != nullptr)
145 xbt_free(simgrid::mc::initial_global_state->recv_diff);
146 simgrid::mc::initial_global_state->recv_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
148 if(_sg_mc_send_determinism && !simgrid::mc::initial_global_state->send_deterministic){
149 XBT_INFO("*********************************************************");
150 XBT_INFO("***** Non-send-deterministic communications pattern *****");
151 XBT_INFO("*********************************************************");
152 XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff);
153 xbt_free(simgrid::mc::initial_global_state->send_diff);
154 simgrid::mc::initial_global_state->send_diff = nullptr;
155 MC_print_statistics(mc_stats);
156 mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
157 }else if(_sg_mc_comms_determinism
158 && (!simgrid::mc::initial_global_state->send_deterministic
159 && !simgrid::mc::initial_global_state->recv_deterministic)) {
160 XBT_INFO("****************************************************");
161 XBT_INFO("***** Non-deterministic communications pattern *****");
162 XBT_INFO("****************************************************");
163 XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff);
164 XBT_INFO("%s", simgrid::mc::initial_global_state->recv_diff);
165 xbt_free(simgrid::mc::initial_global_state->send_diff);
166 simgrid::mc::initial_global_state->send_diff = nullptr;
167 xbt_free(simgrid::mc::initial_global_state->recv_diff);
168 simgrid::mc::initial_global_state->recv_diff = nullptr;
169 MC_print_statistics(mc_stats);
170 mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
175 MC_comm_pattern_free(comm);
179 /********** Non Static functions ***********/
181 void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking)
183 const smx_process_t issuer = MC_smx_simcall_get_issuer(request);
184 mc_list_comm_pattern_t initial_pattern = xbt_dynar_get_as(
185 initial_communications_pattern, issuer->pid, mc_list_comm_pattern_t);
186 xbt_dynar_t incomplete_pattern = xbt_dynar_get_as(
187 incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
189 mc_comm_pattern_t pattern = xbt_new0(s_mc_comm_pattern_t, 1);
190 pattern->data_size = -1;
191 pattern->data = nullptr;
193 initial_pattern->index_comm + xbt_dynar_length(incomplete_pattern);
195 if (call_type == MC_CALL_TYPE_SEND) {
196 /* Create comm pattern */
197 pattern->type = SIMIX_COMM_SEND;
198 pattern->comm_addr = simcall_comm_isend__get__result(request);
200 s_smx_synchro_t synchro = mc_model_checker->process().read<s_smx_synchro_t>(
201 (std::uint64_t) pattern->comm_addr);
203 char* remote_name = mc_model_checker->process().read<char*>(
204 (std::uint64_t)(synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name));
205 pattern->rdv = mc_model_checker->process().read_string(remote_name);
206 pattern->src_proc = MC_smx_resolve_process(synchro.comm.src_proc)->pid;
207 pattern->src_host = MC_smx_process_get_host_name(issuer);
209 struct s_smpi_mpi_request mpi_request =
210 mc_model_checker->process().read<s_smpi_mpi_request>(
211 (std::uint64_t) simcall_comm_isend__get__data(request));
212 pattern->tag = mpi_request.tag;
214 if(synchro.comm.src_buff != nullptr){
215 pattern->data_size = synchro.comm.src_buff_size;
216 pattern->data = xbt_malloc0(pattern->data_size);
217 mc_model_checker->process().read_bytes(
218 pattern->data, pattern->data_size, remote(synchro.comm.src_buff));
220 if(mpi_request.detached){
221 if (!simgrid::mc::initial_global_state->initial_communications_pattern_done) {
222 /* Store comm pattern */
225 initial_communications_pattern, pattern->src_proc, mc_list_comm_pattern_t
229 /* Evaluate comm determinism */
230 deterministic_comm_pattern(pattern->src_proc, pattern, backtracking);
232 initial_communications_pattern, pattern->src_proc, mc_list_comm_pattern_t
237 } else if (call_type == MC_CALL_TYPE_RECV) {
238 pattern->type = SIMIX_COMM_RECEIVE;
239 pattern->comm_addr = simcall_comm_irecv__get__result(request);
241 struct s_smpi_mpi_request mpi_request;
242 mc_model_checker->process().read(
243 &mpi_request, remote((struct s_smpi_mpi_request*)simcall_comm_irecv__get__data(request)));
244 pattern->tag = mpi_request.tag;
246 s_smx_synchro_t synchro;
247 mc_model_checker->process().read(&synchro, remote(pattern->comm_addr));
250 mc_model_checker->process().read(&remote_name,
251 remote(synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name));
252 pattern->rdv = mc_model_checker->process().read_string(remote_name);
253 pattern->dst_proc = MC_smx_resolve_process(synchro.comm.dst_proc)->pid;
254 pattern->dst_host = MC_smx_process_get_host_name(issuer);
256 xbt_die("Unexpected call_type %i", (int) call_type);
259 xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t),
262 XBT_DEBUG("Insert incomplete comm pattern %p for process %lu", pattern, issuer->pid);
265 void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking) {
266 mc_comm_pattern_t current_comm_pattern;
267 unsigned int cursor = 0;
268 mc_comm_pattern_t comm_pattern;
271 /* Complete comm pattern */
272 xbt_dynar_foreach(xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, current_comm_pattern)
273 if (current_comm_pattern->comm_addr == comm_addr) {
274 update_comm_pattern(current_comm_pattern, comm_addr);
277 xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t),
278 cursor, &comm_pattern);
279 XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", issuer, cursor);
284 xbt_die("Corresponding communication not found!");
286 mc_list_comm_pattern_t pattern = xbt_dynar_get_as(
287 initial_communications_pattern, issuer, mc_list_comm_pattern_t);
289 if (!simgrid::mc::initial_global_state->initial_communications_pattern_done)
290 /* Store comm pattern */
291 xbt_dynar_push(pattern->list, &comm_pattern);
293 /* Evaluate comm determinism */
294 deterministic_comm_pattern(issuer, comm_pattern, backtracking);
295 pattern->index_comm++;
300 /************************ Main algorithm ************************/
305 CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session& session)
311 CommunicationDeterminismChecker::~CommunicationDeterminismChecker()
316 // TODO, deduplicate with SafetyChecker
317 RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override
320 for (simgrid::mc::State* state : mc_stack) {
322 smx_simcall_t saved_req = MC_state_get_executed_request(state, &value);
323 const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
324 const int pid = issuer->pid;
325 res.push_back(RecordTraceElement(pid, value));
330 // TODO, deduplicate with SafetyChecker
331 std::vector<std::string> CommunicationDeterminismChecker::getTextualTrace() // override
333 std::vector<std::string> trace;
334 for (simgrid::mc::State* state : mc_stack) {
336 smx_simcall_t req = MC_state_get_executed_request(state, &value);
338 char* req_str = simgrid::mc::request_to_string(
339 req, value, simgrid::mc::RequestType::executed);
340 trace.push_back(req_str);
347 void CommunicationDeterminismChecker::prepare()
349 simgrid::mc::State* initial_state = nullptr;
351 const int maxpid = MC_smx_get_maxpid();
353 simgrid::mc::visited_states.clear();
355 // Create initial_communications_pattern elements:
356 initial_communications_pattern = xbt_dynar_new(sizeof(mc_list_comm_pattern_t), MC_list_comm_pattern_free_voidp);
357 for (i=0; i < maxpid; i++){
358 mc_list_comm_pattern_t process_list_pattern = xbt_new0(s_mc_list_comm_pattern_t, 1);
359 process_list_pattern->list = xbt_dynar_new(sizeof(mc_comm_pattern_t), MC_comm_pattern_free_voidp);
360 process_list_pattern->index_comm = 0;
361 xbt_dynar_insert_at(initial_communications_pattern, i, &process_list_pattern);
364 // Create incomplete_communications_pattern elements:
365 incomplete_communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
366 for (i=0; i < maxpid; i++){
367 xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), nullptr);
368 xbt_dynar_insert_at(incomplete_communications_pattern, i, &process_pattern);
371 initial_state = MC_state_new();
373 XBT_DEBUG("********* Start communication determinism verification *********");
375 /* Wait for requests (schedules processes) */
376 mc_model_checker->wait_for_requests();
378 /* Get an enabled process and insert it in the interleave set of the initial state */
379 for (auto& p : mc_model_checker->process().simix_processes())
380 if (simgrid::mc::process_is_enabled(&p.copy))
381 MC_state_interleave_process(initial_state, &p.copy);
383 mc_stack.push_back(initial_state);
387 bool all_communications_are_finished()
389 for (size_t current_process = 1; current_process < MC_smx_get_maxpid(); current_process++) {
390 xbt_dynar_t pattern = xbt_dynar_get_as(
391 incomplete_communications_pattern, current_process, xbt_dynar_t);
392 if (!xbt_dynar_is_empty(pattern)) {
393 XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
400 int CommunicationDeterminismChecker::main(void)
403 char *req_str = nullptr;
405 std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
406 smx_simcall_t req = nullptr;
407 simgrid::mc::State* next_state = nullptr;
409 while (!mc_stack.empty()) {
411 /* Get current state */
412 simgrid::mc::State* state = mc_stack.back();
414 XBT_DEBUG("**************************************************");
415 XBT_DEBUG("Exploration depth = %zi (state = %d, interleaved processes = %d)",
416 mc_stack.size(), state->num,
417 MC_state_interleave_size(state));
419 /* Update statistics */
420 mc_stats->visited_states++;
422 if (mc_stack.size() <= _sg_mc_max_depth
423 && (req = MC_state_get_request(state, &value))
424 && (visited_state == nullptr)) {
426 req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
427 XBT_DEBUG("Execute: %s", req_str);
430 if (dot_output != nullptr)
431 req_str = simgrid::mc::request_get_dot_output(req, value);
433 MC_state_set_executed_request(state, req, value);
434 mc_stats->executed_transitions++;
436 /* TODO : handle test and testany simcalls */
437 e_mc_call_type_t call = MC_CALL_TYPE_NONE;
438 if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
439 call = MC_get_call_type(req);
441 /* Answer the request */
442 simgrid::mc::handle_simcall(req, value); /* After this call req is no longer useful */
444 if(!initial_global_state->initial_communications_pattern_done)
445 MC_handle_comm_pattern(call, req, value, initial_communications_pattern, 0);
447 MC_handle_comm_pattern(call, req, value, nullptr, 0);
449 /* Wait for requests (schedules processes) */
450 mc_model_checker->wait_for_requests();
452 /* Create the new expanded state */
453 next_state = MC_state_new();
455 /* If comm determinism verification, we cannot stop the exploration if
456 some communications are not finished (at least, data are transfered).
457 These communications are incomplete and they cannot be analyzed and
458 compared with the initial pattern. */
459 bool compare_snapshots = all_communications_are_finished()
460 && initial_global_state->initial_communications_pattern_done;
462 if (_sg_mc_visited == 0 || (visited_state = simgrid::mc::is_visited_state(next_state, compare_snapshots)) == nullptr) {
464 /* Get enabled processes and insert them in the interleave set of the next state */
465 for (auto& p : mc_model_checker->process().simix_processes())
466 if (simgrid::mc::process_is_enabled(&p.copy))
467 MC_state_interleave_process(next_state, &p.copy);
469 if (dot_output != nullptr)
470 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
472 } else if (dot_output != nullptr)
473 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
474 state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
476 mc_stack.push_back(next_state);
478 if (dot_output != nullptr)
483 if (mc_stack.size() > _sg_mc_max_depth)
484 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
485 else if (visited_state != nullptr)
486 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);
488 XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
491 if (!initial_global_state->initial_communications_pattern_done)
492 initial_global_state->initial_communications_pattern_done = 1;
494 /* Trash the current state, no longer needed */
496 MC_state_delete(state, !state->in_visited_states ? 1 : 0);
497 XBT_DEBUG("Delete state %d at depth %zi",
498 state->num, mc_stack.size() + 1);
500 visited_state = nullptr;
502 /* Check for deadlocks */
503 if (mc_model_checker->checkDeadlock()) {
505 return SIMGRID_MC_EXIT_DEADLOCK;
508 while (!mc_stack.empty()) {
509 simgrid::mc::State* state = mc_stack.back();
511 if (MC_state_interleave_size(state)
512 && mc_stack.size() < _sg_mc_max_depth) {
513 /* We found a back-tracking point, let's loop */
514 XBT_DEBUG("Back-tracking to state %d at depth %zi",
515 state->num, mc_stack.size() + 1);
516 mc_stack.push_back(state);
518 simgrid::mc::replay(mc_stack);
520 XBT_DEBUG("Back-tracking to state %d at depth %zi done",
521 state->num, mc_stack.size());
525 XBT_DEBUG("Delete state %d at depth %zi",
526 state->num, mc_stack.size() + 1);
527 MC_state_delete(state, !state->in_visited_states ? 1 : 0);
533 MC_print_statistics(mc_stats);
534 return SIMGRID_MC_EXIT_SUCCESS;
537 int CommunicationDeterminismChecker::run()
539 XBT_INFO("Check communication determinism");
540 mc_model_checker->wait_for_requests();
542 if (mc_mode == MC_MODE_CLIENT)
543 // This will move somehwere else:
544 simgrid::mc::Client::get()->handleMessages();
546 /* Create exploration stack */
551 initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
552 initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
553 initial_global_state->initial_communications_pattern_done = 0;
554 initial_global_state->recv_deterministic = 1;
555 initial_global_state->send_deterministic = 1;
556 initial_global_state->recv_diff = nullptr;
557 initial_global_state->send_diff = nullptr;
559 int res = this->main();
560 initial_global_state = nullptr;