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(simgrid::mc::PatternCommunication* comm1, simgrid::mc::PatternCommunication* 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, simgrid::mc::PatternCommunication* 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(simgrid::mc::PatternCommunication* comm_pattern, smx_synchro_t comm_addr)
97 mc_model_checker->process().read(&comm, remote(comm_addr));
99 smx_process_t src_proc = mc_model_checker->process().resolveProcess(
100 simgrid::mc::remote(comm.comm.src_proc));
101 smx_process_t dst_proc = mc_model_checker->process().resolveProcess(
102 simgrid::mc::remote(comm.comm.dst_proc));
103 comm_pattern->src_proc = src_proc->pid;
104 comm_pattern->dst_proc = dst_proc->pid;
105 comm_pattern->src_host = MC_smx_process_get_host_name(src_proc);
106 comm_pattern->dst_host = MC_smx_process_get_host_name(dst_proc);
107 if (comm_pattern->data.size() == 0 && comm.comm.src_buff != nullptr) {
109 mc_model_checker->process().read(
110 &buff_size, remote(comm.comm.dst_buff_size));
111 comm_pattern->data.resize(buff_size);
112 mc_model_checker->process().read_bytes(
113 comm_pattern->data.data(), comm_pattern->data.size(),
114 remote(comm.comm.src_buff));
118 static void deterministic_comm_pattern(int process, simgrid::mc::PatternCommunication* comm, int backtracking) {
120 simgrid::mc::PatternCommunicationList* list =
121 xbt_dynar_get_as(initial_communications_pattern, process, simgrid::mc::PatternCommunicationList*);
124 e_mc_comm_pattern_difference_t diff =
125 compare_comm_pattern(list->list[list->index_comm].get(), 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);
167 /********** Non Static functions ***********/
169 void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking)
171 const smx_process_t issuer = MC_smx_simcall_get_issuer(request);
172 simgrid::mc::PatternCommunicationList* initial_pattern = xbt_dynar_get_as(
173 initial_communications_pattern, issuer->pid, simgrid::mc::PatternCommunicationList*);
174 xbt_dynar_t incomplete_pattern = xbt_dynar_get_as(
175 incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
177 std::unique_ptr<simgrid::mc::PatternCommunication> pattern =
178 std::unique_ptr<simgrid::mc::PatternCommunication>(
179 new simgrid::mc::PatternCommunication());
181 initial_pattern->index_comm + xbt_dynar_length(incomplete_pattern);
183 if (call_type == MC_CALL_TYPE_SEND) {
184 /* Create comm pattern */
185 pattern->type = SIMIX_COMM_SEND;
186 pattern->comm_addr = simcall_comm_isend__get__result(request);
188 s_smx_synchro_t synchro = mc_model_checker->process().read<s_smx_synchro_t>(
189 (std::uint64_t) pattern->comm_addr);
191 char* remote_name = mc_model_checker->process().read<char*>(
192 (std::uint64_t)(synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name));
193 pattern->rdv = mc_model_checker->process().read_string(remote_name);
194 pattern->src_proc = mc_model_checker->process().resolveProcess(
195 simgrid::mc::remote(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 */
212 simgrid::mc::PatternCommunicationList* list = xbt_dynar_get_as(
213 initial_communications_pattern, pattern->src_proc,
214 simgrid::mc::PatternCommunicationList*);
215 list->list.push_back(std::move(pattern));
217 /* Evaluate comm determinism */
218 deterministic_comm_pattern(pattern->src_proc, pattern.get(), backtracking);
220 initial_communications_pattern, pattern->src_proc, simgrid::mc::PatternCommunicationList*
225 } else if (call_type == MC_CALL_TYPE_RECV) {
226 pattern->type = SIMIX_COMM_RECEIVE;
227 pattern->comm_addr = simcall_comm_irecv__get__result(request);
229 struct s_smpi_mpi_request mpi_request;
230 mc_model_checker->process().read(
231 &mpi_request, remote((struct s_smpi_mpi_request*)simcall_comm_irecv__get__data(request)));
232 pattern->tag = mpi_request.tag;
234 s_smx_synchro_t synchro;
235 mc_model_checker->process().read(&synchro, remote(pattern->comm_addr));
238 mc_model_checker->process().read(&remote_name,
239 remote(synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name));
240 pattern->rdv = mc_model_checker->process().read_string(remote_name);
241 pattern->dst_proc = mc_model_checker->process().resolveProcess(
242 simgrid::mc::remote(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);
247 XBT_DEBUG("Insert incomplete comm pattern %p for process %lu",
248 pattern.get(), issuer->pid);
250 xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
251 simgrid::mc::PatternCommunication* pattern2 = pattern.release();
252 xbt_dynar_push(dynar, &pattern2);
255 void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking) {
256 simgrid::mc::PatternCommunication* current_comm_pattern;
257 unsigned int cursor = 0;
258 std::unique_ptr<simgrid::mc::PatternCommunication> comm_pattern;
261 /* Complete comm pattern */
262 xbt_dynar_foreach(xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, current_comm_pattern)
263 if (current_comm_pattern->comm_addr == comm_addr) {
264 update_comm_pattern(current_comm_pattern, comm_addr);
266 simgrid::mc::PatternCommunication* temp;
268 xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t),
270 comm_pattern = std::unique_ptr<simgrid::mc::PatternCommunication>(temp);
271 XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", issuer, cursor);
276 xbt_die("Corresponding communication not found!");
278 simgrid::mc::PatternCommunicationList* pattern = xbt_dynar_get_as(
279 initial_communications_pattern, issuer, simgrid::mc::PatternCommunicationList*);
281 if (!simgrid::mc::initial_global_state->initial_communications_pattern_done)
282 /* Store comm pattern */
283 pattern->list.push_back(std::move(comm_pattern));
285 /* Evaluate comm determinism */
286 deterministic_comm_pattern(issuer, comm_pattern.get(), backtracking);
287 pattern->index_comm++;
292 /************************ Main algorithm ************************/
297 CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session& session)
303 CommunicationDeterminismChecker::~CommunicationDeterminismChecker()
308 RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override
311 for (auto const& state : stack_)
312 res.push_back(state->getRecordElement());
316 std::vector<std::string> CommunicationDeterminismChecker::getTextualTrace() // override
318 std::vector<std::string> trace;
319 for (auto const& state : stack_) {
320 smx_simcall_t req = &state->executed_req;
322 trace.push_back(simgrid::mc::request_to_string(
323 req, state->req_num, simgrid::mc::RequestType::executed));
328 void CommunicationDeterminismChecker::prepare()
332 const int maxpid = MC_smx_get_maxpid();
334 // Create initial_communications_pattern elements:
335 initial_communications_pattern = simgrid::xbt::newDeleteDynar<simgrid::mc::PatternCommunicationList*>();
336 for (i=0; i < maxpid; i++){
337 simgrid::mc::PatternCommunicationList* process_list_pattern = new simgrid::mc::PatternCommunicationList();
338 xbt_dynar_insert_at(initial_communications_pattern, i, &process_list_pattern);
341 // Create incomplete_communications_pattern elements:
342 incomplete_communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
343 for (i=0; i < maxpid; i++){
344 xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(simgrid::mc::PatternCommunication*), nullptr);
345 xbt_dynar_insert_at(incomplete_communications_pattern, i, &process_pattern);
348 std::unique_ptr<simgrid::mc::State> initial_state =
349 std::unique_ptr<simgrid::mc::State>(MC_state_new());
351 XBT_DEBUG("********* Start communication determinism verification *********");
353 /* Wait for requests (schedules processes) */
354 mc_model_checker->wait_for_requests();
356 /* Get an enabled process and insert it in the interleave set of the initial state */
357 for (auto& p : mc_model_checker->process().simix_processes())
358 if (simgrid::mc::process_is_enabled(&p.copy))
359 initial_state->interleave(&p.copy);
361 stack_.push_back(std::move(initial_state));
365 bool all_communications_are_finished()
367 for (size_t current_process = 1; current_process < MC_smx_get_maxpid(); current_process++) {
368 xbt_dynar_t pattern = xbt_dynar_get_as(
369 incomplete_communications_pattern, current_process, xbt_dynar_t);
370 if (!xbt_dynar_is_empty(pattern)) {
371 XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
378 int CommunicationDeterminismChecker::main(void)
380 std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
381 smx_simcall_t req = nullptr;
383 while (!stack_.empty()) {
385 /* Get current state */
386 simgrid::mc::State* state = stack_.back().get();
388 XBT_DEBUG("**************************************************");
389 XBT_DEBUG("Exploration depth = %zi (state = %d, interleaved processes = %zd)",
390 stack_.size(), state->num,
391 state->interleaveSize());
393 /* Update statistics */
394 mc_stats->visited_states++;
396 if (stack_.size() <= (std::size_t) _sg_mc_max_depth
397 && (req = MC_state_get_request(state)) != nullptr
398 && (visited_state == nullptr)) {
400 int req_num = state->req_num;
402 XBT_DEBUG("Execute: %s",
403 simgrid::mc::request_to_string(
404 req, req_num, simgrid::mc::RequestType::simix).c_str());
407 if (dot_output != nullptr)
408 req_str = simgrid::mc::request_get_dot_output(req, req_num);
410 mc_stats->executed_transitions++;
412 /* TODO : handle test and testany simcalls */
413 e_mc_call_type_t call = MC_CALL_TYPE_NONE;
414 if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
415 call = MC_get_call_type(req);
417 /* Answer the request */
418 simgrid::mc::handle_simcall(req, req_num); /* After this call req is no longer useful */
420 if(!initial_global_state->initial_communications_pattern_done)
421 MC_handle_comm_pattern(call, req, req_num, initial_communications_pattern, 0);
423 MC_handle_comm_pattern(call, req, req_num, nullptr, 0);
425 /* Wait for requests (schedules processes) */
426 mc_model_checker->wait_for_requests();
428 /* Create the new expanded state */
429 std::unique_ptr<simgrid::mc::State> next_state =
430 std::unique_ptr<simgrid::mc::State>(MC_state_new());
432 /* If comm determinism verification, we cannot stop the exploration if
433 some communications are not finished (at least, data are transfered).
434 These communications are incomplete and they cannot be analyzed and
435 compared with the initial pattern. */
436 bool compare_snapshots = all_communications_are_finished()
437 && initial_global_state->initial_communications_pattern_done;
439 if (_sg_mc_visited == 0
440 || (visited_state = visitedStates_.addVisitedState(next_state.get(), compare_snapshots)) == nullptr) {
442 /* Get enabled processes and insert them in the interleave set of the next state */
443 for (auto& p : mc_model_checker->process().simix_processes())
444 if (simgrid::mc::process_is_enabled(&p.copy))
445 next_state->interleave(&p.copy);
447 if (dot_output != nullptr)
448 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
449 state->num, next_state->num, req_str.c_str());
451 } else if (dot_output != nullptr)
452 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
453 state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str.c_str());
455 stack_.push_back(std::move(next_state));
459 if (stack_.size() > (std::size_t) _sg_mc_max_depth)
460 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
461 else if (visited_state != nullptr)
462 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);
464 XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
467 if (!initial_global_state->initial_communications_pattern_done)
468 initial_global_state->initial_communications_pattern_done = 1;
470 /* Trash the current state, no longer needed */
471 XBT_DEBUG("Delete state %d at depth %zi",
472 state->num, stack_.size());
475 visited_state = nullptr;
477 /* Check for deadlocks */
478 if (mc_model_checker->checkDeadlock()) {
480 return SIMGRID_MC_EXIT_DEADLOCK;
483 while (!stack_.empty()) {
484 std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
486 if (state->interleaveSize()
487 && stack_.size() < (std::size_t) _sg_mc_max_depth) {
488 /* We found a back-tracking point, let's loop */
489 XBT_DEBUG("Back-tracking to state %d at depth %zi",
490 state->num, stack_.size() + 1);
491 stack_.push_back(std::move(state));
493 simgrid::mc::replay(stack_);
495 XBT_DEBUG("Back-tracking to state %d at depth %zi done",
496 stack_.back()->num, stack_.size());
500 XBT_DEBUG("Delete state %d at depth %zi",
501 state->num, stack_.size() + 1);
507 MC_print_statistics(mc_stats);
508 return SIMGRID_MC_EXIT_SUCCESS;
511 int CommunicationDeterminismChecker::run()
513 XBT_INFO("Check communication determinism");
514 mc_model_checker->wait_for_requests();
518 initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
519 initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
520 initial_global_state->initial_communications_pattern_done = 0;
521 initial_global_state->recv_deterministic = 1;
522 initial_global_state->send_deterministic = 1;
523 initial_global_state->recv_diff = nullptr;
524 initial_global_state->send_diff = nullptr;
526 int res = this->main();
527 initial_global_state = nullptr;
531 Checker* createCommunicationDeterminismChecker(Session& session)
533 return new CommunicationDeterminismChecker(session);