1 /* Copyright (c) 2008-2014. 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. */
7 #include "mc_private.h"
9 #include "xbt/mmalloc/mmprivate.h"
11 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc,
12 "Logging specific to MC DPOR exploration");
14 /********** Global variables **********/
16 xbt_dynar_t visited_states;
17 xbt_dict_t first_enabled_state;
19 /********** Static functions ***********/
22 static void visited_state_free(mc_visited_state_t state)
25 MC_free_snapshot(state->system_state);
30 static void visited_state_free_voidp(void *s)
32 visited_state_free((mc_visited_state_t) * (void **) s);
35 /** \brief Save the current state
37 * \return Snapshot of the current state.
39 static mc_visited_state_t visited_state_new()
42 mc_visited_state_t new_state = NULL;
43 new_state = xbt_new0(s_mc_visited_state_t, 1);
44 new_state->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
45 new_state->nb_processes = xbt_swag_size(simix_global->process_list);
46 new_state->system_state = MC_take_snapshot(mc_stats->expanded_states);
47 new_state->num = mc_stats->expanded_states;
48 new_state->other_num = -1;
54 /** \brief Find a suitable subrange of candidate duplicates for a given state
56 * \param all_ pairs dynamic array of states with candidate duplicates of the current state;
57 * \param pair current state;
58 * \param min (output) index of the beginning of the the subrange
59 * \param max (output) index of the enf of the subrange
61 * Given a suitably ordered array of state, this function extracts a subrange
62 * (with index *min <= i <= *max) with candidate duplicates of the given state.
63 * This function uses only fast discriminating criterions and does not use the
64 * full state comparison algorithms.
66 * The states in all_pairs MUST be ordered using a (given) weak order
67 * (based on nb_processes and heap_bytes_used).
68 * The subrange is the subrange of "equivalence" of the given state.
70 static int get_search_interval(xbt_dynar_t all_states, mc_visited_state_t state,
74 ("Searching interval for state %i: nd_processes=%zu heap_bytes_used=%zu",
75 state->num, (size_t) state->nb_processes,
76 (size_t) state->heap_bytes_used);
78 int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
82 int cursor = 0, previous_cursor, next_cursor;
83 mc_visited_state_t state_test;
85 int end = xbt_dynar_length(all_states) - 1;
87 while (start <= end) {
88 cursor = (start + end) / 2;
90 (mc_visited_state_t) xbt_dynar_get_as(all_states, cursor,
92 if (state_test->nb_processes < state->nb_processes) {
94 } else if (state_test->nb_processes > state->nb_processes) {
97 if (state_test->heap_bytes_used < state->heap_bytes_used) {
99 } else if (state_test->heap_bytes_used > state->heap_bytes_used) {
102 *min = *max = cursor;
103 previous_cursor = cursor - 1;
104 while (previous_cursor >= 0) {
106 (mc_visited_state_t) xbt_dynar_get_as(all_states, previous_cursor,
108 if (state_test->nb_processes != state->nb_processes
109 || state_test->heap_bytes_used != state->heap_bytes_used)
111 *min = previous_cursor;
114 next_cursor = cursor + 1;
115 while (next_cursor < xbt_dynar_length(all_states)) {
117 (mc_visited_state_t) xbt_dynar_get_as(all_states, next_cursor,
119 if (state_test->nb_processes != state->nb_processes
120 || state_test->heap_bytes_used != state->heap_bytes_used)
138 /** \brief Take a snapshot the current state and process it.
140 * \return number of the duplicate state or -1 (not visited)
142 static int is_visited_state()
145 /* Reduction on visited states disabled for the first execution
146 path if the detection of the communication determinism is
147 enabled (we need to a complete initial communication pattern) */
148 if ((_sg_mc_visited == 0) ||
149 ((_sg_mc_comms_determinism || _sg_mc_send_determinism)
150 && !initial_state_safety->initial_communications_pattern_done))
153 int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
157 mc_visited_state_t new_state = visited_state_new();
159 if (xbt_dynar_is_empty(visited_states)) {
161 xbt_dynar_push(visited_states, &new_state);
170 int min = -1, max = -1, index;
172 mc_visited_state_t state_test;
175 index = get_search_interval(visited_states, new_state, &min, &max);
177 if (min != -1 && max != -1) {
179 // Parallell implementation
180 /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
182 state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
183 if(state_test->other_num == -1)
184 new_state->other_num = state_test->num;
186 new_state->other_num = state_test->other_num;
187 if(dot_output == NULL)
188 XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
190 XBT_DEBUG("State %d already visited ! (equal to state %d (state %d in dot_output))", new_state->num, state_test->num, new_state->other_num);
191 xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
192 xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
195 return new_state->other_num;
199 while (cursor <= max) {
201 (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor,
203 if (snapshot_compare(state_test, new_state) == 0) {
204 // The state has been visited:
206 if (state_test->other_num == -1)
207 new_state->other_num = state_test->num;
209 new_state->other_num = state_test->other_num;
210 if (dot_output == NULL)
211 XBT_DEBUG("State %d already visited ! (equal to state %d)",
212 new_state->num, state_test->num);
215 ("State %d already visited ! (equal to state %d (state %d in dot_output))",
216 new_state->num, state_test->num, new_state->other_num);
218 // Replace the old state with the new one (why?):
219 xbt_dynar_remove_at(visited_states, cursor, NULL);
220 xbt_dynar_insert_at(visited_states, cursor, &new_state);
224 return new_state->other_num;
229 // The state has not been visited, add it to the list:
230 xbt_dynar_insert_at(visited_states, min, &new_state);
234 // The state has not been visited: insert the state in the dynamic array.
236 (mc_visited_state_t) xbt_dynar_get_as(visited_states, index,
238 if (state_test->nb_processes < new_state->nb_processes) {
239 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
241 if (state_test->heap_bytes_used < new_state->heap_bytes_used)
242 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
244 xbt_dynar_insert_at(visited_states, index, &new_state);
249 // We have reached the maximum number of stored states;
250 if (xbt_dynar_length(visited_states) > _sg_mc_visited) {
252 // Find the (index of the) older state:
253 int min2 = mc_stats->expanded_states;
254 unsigned int cursor2 = 0;
255 unsigned int index2 = 0;
256 xbt_dynar_foreach(visited_states, cursor2, state_test) {
257 if (state_test->num < min2) {
259 min2 = state_test->num;
264 xbt_dynar_remove_at(visited_states, index2, NULL);
276 * \brief Initialize the DPOR exploration algorithm
281 int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
283 mc_state_t initial_state = NULL;
284 smx_process_t process;
286 /* Create the initial state and push it into the exploration stack */
289 if (_sg_mc_visited > 0)
291 xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
293 if (mc_reduce_kind == e_mc_reduce_dpor)
294 first_enabled_state = xbt_dict_new_homogeneous(&xbt_free_f);
296 if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
297 initial_communications_pattern =
298 xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
299 communications_pattern =
300 xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
301 incomplete_communications_pattern = xbt_dynar_new(sizeof(int), NULL);
305 initial_state = MC_state_new();
309 XBT_DEBUG("**************************************************");
310 XBT_DEBUG("Initial state");
312 /* Wait for requests (schedules processes) */
313 MC_wait_for_requests();
315 MC_ignore_heap(simix_global->process_to_run->data, 0);
316 MC_ignore_heap(simix_global->process_that_ran->data, 0);
320 /* Get an enabled process and insert it in the interleave set of the initial state */
321 xbt_swag_foreach(process, simix_global->process_list) {
322 if (MC_process_is_enabled(process)) {
323 MC_state_interleave_process(initial_state, process);
324 if (mc_reduce_kind != e_mc_reduce_none)
329 xbt_fifo_unshift(mc_stack_safety, initial_state);
331 if (mc_reduce_kind == e_mc_reduce_dpor) {
332 /* To ensure the soundness of DPOR, we have to keep a list of
333 processes which are still enabled at each step of the exploration.
334 If max depth is reached, we interleave them in the state in which they have
335 been enabled for the first time. */
336 xbt_swag_foreach(process, simix_global->process_list) {
337 if (MC_process_is_enabled(process)) {
338 char *key = bprintf("%lu", process->pid);
339 char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety));
340 xbt_dict_set(first_enabled_state, key, data, NULL);
356 /** \brief Model-check the application using a DFS exploration
357 * with DPOR (Dynamic Partial Order Reductions)
362 char *req_str = NULL;
364 smx_simcall_t req = NULL, prev_req = NULL;
365 mc_state_t state = NULL, prev_state = NULL, next_state =
366 NULL, restored_state = NULL;
367 smx_process_t process = NULL;
368 xbt_fifo_item_t item = NULL;
369 mc_state_t state_test = NULL;
371 int visited_state = -1;
373 int comm_pattern = 0;
374 smx_action_t current_comm;
376 while (xbt_fifo_size(mc_stack_safety) > 0) {
378 /* Get current state */
380 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
382 XBT_DEBUG("**************************************************");
384 ("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d, first_enabled_state size : %d)",
385 xbt_fifo_size(mc_stack_safety), state, state->num,
386 MC_state_interleave_size(state), user_max_depth_reached,
387 xbt_dict_size(first_enabled_state));
389 /* Update statistics */
390 mc_stats->visited_states++;
392 /* If there are processes to interleave and the maximum depth has not been reached
393 then perform one step of the exploration algorithm */
394 if (xbt_fifo_size(mc_stack_safety) <= _sg_mc_max_depth
395 && !user_max_depth_reached
396 && (req = MC_state_get_request(state, &value)) && visited_state == -1) {
398 /* Debug information */
399 if (XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)) {
400 req_str = MC_request_to_string(req, value);
401 XBT_DEBUG("Execute: %s", req_str);
406 if (dot_output != NULL)
407 req_str = MC_request_get_dot_output(req, value);
410 MC_state_set_executed_request(state, req, value);
411 mc_stats->executed_transitions++;
413 if (mc_reduce_kind == e_mc_reduce_dpor) {
415 char *key = bprintf("%lu", req->issuer->pid);
416 xbt_dict_remove(first_enabled_state, key);
421 /* TODO : handle test and testany simcalls */
422 if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
423 if (req->call == SIMCALL_COMM_ISEND)
425 else if (req->call == SIMCALL_COMM_IRECV)
427 else if (req->call == SIMCALL_COMM_WAIT)
429 else if (req->call == SIMCALL_COMM_WAITANY)
433 /* Answer the request */
434 SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
436 if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
438 if (comm_pattern == 1 || comm_pattern == 2) {
439 if (!initial_state_safety->initial_communications_pattern_done)
440 get_comm_pattern(initial_communications_pattern, req, comm_pattern);
442 get_comm_pattern(communications_pattern, req, comm_pattern);
443 } else if (comm_pattern == 3) {
444 current_comm = simcall_comm_wait__get__comm(req);
445 if (current_comm->comm.refcount == 1) { /* First wait only must be considered */
446 if (!initial_state_safety->initial_communications_pattern_done)
447 complete_comm_pattern(initial_communications_pattern,
450 complete_comm_pattern(communications_pattern, current_comm);
452 } else if (comm_pattern == 4) {
454 xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value,
456 if (current_comm->comm.refcount == 1) { /* First wait only must be considered */
457 if (!initial_state_safety->initial_communications_pattern_done)
458 complete_comm_pattern(initial_communications_pattern,
461 complete_comm_pattern(communications_pattern, current_comm);
468 /* Wait for requests (schedules processes) */
469 MC_wait_for_requests();
471 /* Create the new expanded state */
474 next_state = MC_state_new();
476 if ((visited_state = is_visited_state()) == -1) {
478 /* Get an enabled process and insert it in the interleave set of the next state */
479 xbt_swag_foreach(process, simix_global->process_list) {
480 if (MC_process_is_enabled(process)) {
481 MC_state_interleave_process(next_state, process);
482 if (mc_reduce_kind != e_mc_reduce_none)
487 if (_sg_mc_checkpoint
488 && ((xbt_fifo_size(mc_stack_safety) + 1) % _sg_mc_checkpoint ==
490 next_state->system_state = MC_take_snapshot(next_state->num);
493 if (dot_output != NULL)
494 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
495 next_state->num, req_str);
499 if (dot_output != NULL)
500 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
501 visited_state, req_str);
505 xbt_fifo_unshift(mc_stack_safety, next_state);
507 if (mc_reduce_kind == e_mc_reduce_dpor) {
508 /* Insert in dict all enabled processes, if not included yet */
509 xbt_swag_foreach(process, simix_global->process_list) {
510 if (MC_process_is_enabled(process)) {
511 char *key = bprintf("%lu", process->pid);
512 if (xbt_dict_get_or_null(first_enabled_state, key) == NULL) {
513 char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety));
514 xbt_dict_set(first_enabled_state, key, data, NULL);
521 if (dot_output != NULL)
526 /* Let's loop again */
528 /* The interleave set is empty or the maximum depth is reached, let's back-track */
531 if ((xbt_fifo_size(mc_stack_safety) > _sg_mc_max_depth)
532 || user_max_depth_reached || visited_state != -1) {
534 if (user_max_depth_reached && visited_state == -1)
535 XBT_DEBUG("User max depth reached !");
536 else if (visited_state == -1)
537 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
539 if (mc_reduce_kind == e_mc_reduce_dpor) {
540 /* Interleave enabled processes in the state in which they have been enabled for the first time */
541 xbt_swag_foreach(process, simix_global->process_list) {
542 if (MC_process_is_enabled(process)) {
543 char *key = bprintf("%lu", process->pid);
545 (int) strtoul(xbt_dict_get_or_null(first_enabled_state, key),
548 int cursor = xbt_fifo_size(mc_stack_safety);
549 xbt_fifo_foreach(mc_stack_safety, item, state_test, mc_state_t) {
550 if (cursor-- == enabled) {
551 if (!MC_state_process_is_done(state_test, process)
552 && state_test->num != state->num) {
553 XBT_DEBUG("Interleave process %lu in state %d",
554 process->pid, state_test->num);
555 MC_state_interleave_process(state_test, process);
566 XBT_DEBUG("There are no more processes to interleave. (depth %d)",
567 xbt_fifo_size(mc_stack_safety) + 1);
573 if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
574 if (initial_state_safety->initial_communications_pattern_done) {
575 if (visited_state == -1) {
576 deterministic_pattern(initial_communications_pattern,
577 communications_pattern);
578 if (initial_state_safety->comm_deterministic == 0
579 && _sg_mc_comms_determinism) {
580 XBT_INFO("****************************************************");
581 XBT_INFO("***** Non-deterministic communications pattern *****");
582 XBT_INFO("****************************************************");
583 XBT_INFO("Initial communications pattern:");
584 print_communications_pattern(initial_communications_pattern);
585 XBT_INFO("Communications pattern counter-example:");
586 print_communications_pattern(communications_pattern);
587 MC_print_statistics(mc_stats);
589 } else if (initial_state_safety->send_deterministic == 0
590 && _sg_mc_send_determinism) {
592 ("*********************************************************");
594 ("***** Non-send-deterministic communications pattern *****");
596 ("*********************************************************");
597 XBT_INFO("Initial communications pattern:");
598 print_communications_pattern(initial_communications_pattern);
599 XBT_INFO("Communications pattern counter-example:");
600 print_communications_pattern(communications_pattern);
601 MC_print_statistics(mc_stats);
608 initial_state_safety->initial_communications_pattern_done = 1;
612 /* Trash the current state, no longer needed */
613 xbt_fifo_shift(mc_stack_safety);
614 MC_state_delete(state);
615 XBT_DEBUG("Delete state %d at depth %d", state->num,
616 xbt_fifo_size(mc_stack_safety) + 1);
622 /* Check for deadlocks */
623 if (MC_deadlock_check()) {
624 MC_show_deadlock(NULL);
629 /* Traverse the stack backwards until a state with a non empty interleave
630 set is found, deleting all the states that have it empty in the way.
631 For each deleted state, check if the request that has generated it
632 (from it's predecesor state), depends on any other previous request
633 executed before it. If it does then add it to the interleave set of the
634 state that executed that previous request. */
636 while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
637 if (mc_reduce_kind == e_mc_reduce_dpor) {
638 req = MC_state_get_internal_request(state);
639 xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
640 if (MC_request_depend
641 (req, MC_state_get_internal_request(prev_state))) {
642 if (XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)) {
643 XBT_DEBUG("Dependent Transitions:");
644 prev_req = MC_state_get_executed_request(prev_state, &value);
645 req_str = MC_request_to_string(prev_req, value);
646 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
648 prev_req = MC_state_get_executed_request(state, &value);
649 req_str = MC_request_to_string(prev_req, value);
650 XBT_DEBUG("%s (state=%d)", req_str, state->num);
654 if (!MC_state_process_is_done(prev_state, req->issuer))
655 MC_state_interleave_process(prev_state, req->issuer);
657 XBT_DEBUG("Process %p is in done set", req->issuer);
661 } else if (req->issuer ==
662 MC_state_get_internal_request(prev_state)->issuer) {
664 XBT_DEBUG("Simcall %d and %d with same issuer", req->call,
665 MC_state_get_internal_request(prev_state)->call);
671 ("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
672 req->call, req->issuer->pid, state->num,
673 MC_state_get_internal_request(prev_state)->call,
674 MC_state_get_internal_request(prev_state)->issuer->pid,
681 if (MC_state_interleave_size(state)
682 && xbt_fifo_size(mc_stack_safety) < _sg_mc_max_depth) {
683 /* We found a back-tracking point, let's loop */
684 XBT_DEBUG("Back-tracking to state %d at depth %d", state->num,
685 xbt_fifo_size(mc_stack_safety) + 1);
686 if (_sg_mc_checkpoint) {
687 if (state->system_state != NULL) {
688 MC_restore_snapshot(state->system_state);
689 xbt_fifo_unshift(mc_stack_safety, state);
692 pos = xbt_fifo_size(mc_stack_safety);
693 item = xbt_fifo_get_first_item(mc_stack_safety);
695 restored_state = (mc_state_t) xbt_fifo_get_item_content(item);
696 if (restored_state->system_state != NULL) {
699 item = xbt_fifo_get_next_item(item);
703 MC_restore_snapshot(restored_state->system_state);
704 xbt_fifo_unshift(mc_stack_safety, state);
706 MC_replay(mc_stack_safety, pos);
709 xbt_fifo_unshift(mc_stack_safety, state);
711 MC_replay(mc_stack_safety, -1);
713 XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num,
714 xbt_fifo_size(mc_stack_safety));
717 /*req = MC_state_get_internal_request(state);
718 if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
719 if(req->call == SIMCALL_COMM_ISEND || req->call == SIMCALL_COMM_IRECV){
720 if(!xbt_dynar_is_empty(communications_pattern))
721 xbt_dynar_remove_at(communications_pattern, xbt_dynar_length(communications_pattern) - 1, NULL);
724 XBT_DEBUG("Delete state %d at depth %d", state->num,
725 xbt_fifo_size(mc_stack_safety) + 1);
726 MC_state_delete(state);
732 MC_print_statistics(mc_stats);