1 /* Copyright (c) 2008-2013. 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 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc,
10 "Logging specific to MC DPOR exploration");
12 xbt_dynar_t visited_states;
13 xbt_dict_t first_enabled_state;
15 static void visited_state_free(mc_visited_state_t state){
17 MC_free_snapshot(state->system_state);
22 static void visited_state_free_voidp(void *s){
23 visited_state_free((mc_visited_state_t) * (void **) s);
26 static mc_visited_state_t visited_state_new(){
28 mc_visited_state_t new_state = NULL;
29 new_state = xbt_new0(s_mc_visited_state_t, 1);
30 new_state->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
31 new_state->nb_processes = xbt_swag_size(simix_global->process_list);
32 new_state->system_state = MC_take_snapshot();
33 new_state->num = mc_stats->expanded_states;
34 new_state->other_num = -1;
40 /* Dichotomic search in visited_states dynar.
41 * States are ordered by the number of processes then the number of bytes used in std_heap */
43 static int is_visited_state(){
45 if(_sg_mc_visited == 0)
48 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
51 mc_visited_state_t new_state = visited_state_new();
54 if(xbt_dynar_is_empty(visited_states)){
57 xbt_dynar_push(visited_states, &new_state);
69 size_t current_bytes_used = new_state->heap_bytes_used;
70 int current_nb_processes = new_state->nb_processes;
72 unsigned int cursor = 0;
73 int previous_cursor = 0, next_cursor = 0;
75 int end = xbt_dynar_length(visited_states) - 1;
77 mc_visited_state_t state_test = NULL;
78 size_t bytes_used_test;
79 int nb_processes_test;
80 int same_processes_and_bytes_not_found = 1;
82 while(start <= end && same_processes_and_bytes_not_found){
83 cursor = (start + end) / 2;
84 state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
85 bytes_used_test = state_test->heap_bytes_used;
86 nb_processes_test = state_test->nb_processes;
87 if(nb_processes_test < current_nb_processes){
89 }else if(nb_processes_test > current_nb_processes){
91 }else if(nb_processes_test == current_nb_processes){
92 if(bytes_used_test < current_bytes_used)
94 if(bytes_used_test > current_bytes_used)
96 if(bytes_used_test == current_bytes_used){
97 same_processes_and_bytes_not_found = 0;
98 if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){
99 if(state_test->other_num == -1)
100 new_state->other_num = state_test->num;
102 new_state->other_num = state_test->other_num;
103 if(dot_output == NULL)
104 XBT_DEBUG("Next state %d already visited ! (equal to state %d)", new_state->num, state_test->num);
106 XBT_DEBUG("Next state %d already visited ! (equal to state %d (state %d in dot_output))", new_state->num, state_test->num, new_state->other_num);
107 xbt_dynar_remove_at(visited_states, cursor, NULL);
108 xbt_dynar_insert_at(visited_states, cursor, &new_state);
113 return new_state->other_num;
115 /* Search another state with same number of bytes used in std_heap */
116 previous_cursor = cursor - 1;
117 while(previous_cursor >= 0){
118 state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, previous_cursor, mc_visited_state_t);
119 bytes_used_test = state_test->system_state->heap_bytes_used;
120 if(bytes_used_test != current_bytes_used)
122 if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){
123 if(state_test->other_num == -1)
124 new_state->other_num = state_test->num;
126 new_state->other_num = state_test->other_num;
127 if(dot_output == NULL)
128 XBT_DEBUG("Next state %d already visited ! (equal to state %d)", new_state->num, state_test->num);
130 XBT_DEBUG("Next state %d already visited ! (equal to state %d (state %d in dot_output))", new_state->num, state_test->num, new_state->other_num);
131 xbt_dynar_remove_at(visited_states, previous_cursor, NULL);
132 xbt_dynar_insert_at(visited_states, cursor, &new_state);
137 return new_state->other_num;
141 next_cursor = cursor + 1;
142 while(next_cursor < xbt_dynar_length(visited_states)){
143 state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, next_cursor, mc_visited_state_t);
144 bytes_used_test = state_test->system_state->heap_bytes_used;
145 if(bytes_used_test != current_bytes_used)
147 if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){
148 if(state_test->other_num == -1)
149 new_state->other_num = state_test->num;
151 new_state->other_num = state_test->other_num;
152 if(dot_output == NULL)
153 XBT_DEBUG("Next state %d already visited ! (equal to state %d)", new_state->num, state_test->num);
155 XBT_DEBUG("Next state %d already visited ! (equal to state %d (state %d in dot_output))", new_state->num, state_test->num, new_state->other_num);
156 xbt_dynar_remove_at(visited_states, next_cursor, NULL);
157 xbt_dynar_insert_at(visited_states, next_cursor, &new_state);
162 return new_state->other_num;
171 state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
172 bytes_used_test = state_test->heap_bytes_used;
174 if(bytes_used_test < current_bytes_used)
175 xbt_dynar_insert_at(visited_states, cursor + 1, &new_state);
177 xbt_dynar_insert_at(visited_states, cursor, &new_state);
179 if(xbt_dynar_length(visited_states) > _sg_mc_visited){
180 int min = mc_stats->expanded_states;
181 unsigned int cursor2 = 0;
182 unsigned int index = 0;
183 xbt_dynar_foreach(visited_states, cursor2, state_test){
184 if(state_test->num < min){
186 min = state_test->num;
189 xbt_dynar_remove_at(visited_states, index, NULL);
203 * \brief Initialize the DPOR exploration algorithm
208 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
210 mc_state_t initial_state = NULL;
211 smx_process_t process;
213 /* Create the initial state and push it into the exploration stack */
216 initial_state = MC_state_new();
217 visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
219 first_enabled_state = xbt_dict_new_homogeneous(&xbt_free_f);
223 XBT_DEBUG("**************************************************");
224 XBT_DEBUG("Initial state");
226 /* Wait for requests (schedules processes) */
227 MC_wait_for_requests();
231 /* Get an enabled process and insert it in the interleave set of the initial state */
232 xbt_swag_foreach(process, simix_global->process_list){
233 if(MC_process_is_enabled(process)){
234 MC_state_interleave_process(initial_state, process);
235 if(mc_reduce_kind != e_mc_reduce_none)
240 xbt_fifo_unshift(mc_stack_safety, initial_state);
242 /* To ensure the soundness of DPOR, we have to keep a list of
243 processes which are still enabled at each step of the exploration.
244 If max depth is reached, we interleave them in the state in which they have
245 been enabled for the first time. */
246 xbt_swag_foreach(process, simix_global->process_list){
247 if(MC_process_is_enabled(process)){
248 char *key = bprintf("%lu", process->pid);
249 char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety));
250 xbt_dict_set(first_enabled_state, key, data, NULL);
266 * \brief Perform the model-checking operation using a depth-first search exploration
267 * with Dynamic Partial Order Reductions
272 char *req_str = NULL;
274 smx_simcall_t req = NULL, prev_req = NULL;
275 mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restore_state=NULL;
276 smx_process_t process = NULL;
277 xbt_fifo_item_t item = NULL;
279 int visited_state = -1;
282 while (xbt_fifo_size(mc_stack_safety) > 0) {
284 /* Get current state */
286 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
288 XBT_DEBUG("**************************************************");
289 XBT_DEBUG("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d)",
290 xbt_fifo_size(mc_stack_safety), state, state->num,
291 MC_state_interleave_size(state), user_max_depth_reached);
293 /* Update statistics */
294 mc_stats->visited_states++;
296 /* If there are processes to interleave and the maximum depth has not been reached
297 then perform one step of the exploration algorithm */
298 if (xbt_fifo_size(mc_stack_safety) <= _sg_mc_max_depth && !user_max_depth_reached &&
299 (req = MC_state_get_request(state, &value)) && visited_state == -1) {
301 /* Debug information */
302 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
303 req_str = MC_request_to_string(req, value);
304 XBT_DEBUG("Execute: %s", req_str);
309 if(dot_output != NULL)
310 req_str = MC_request_get_dot_output(req, value);
313 MC_state_set_executed_request(state, req, value);
314 mc_stats->executed_transitions++;
317 char *key = bprintf("%lu", req->issuer->pid);
318 xbt_dict_remove(first_enabled_state, key);
322 /* Answer the request */
323 SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
325 /* Wait for requests (schedules processes) */
326 MC_wait_for_requests();
328 /* Create the new expanded state */
331 next_state = MC_state_new();
333 if((visited_state = is_visited_state()) == -1){
335 /* Get an enabled process and insert it in the interleave set of the next state */
336 xbt_swag_foreach(process, simix_global->process_list){
337 if(MC_process_is_enabled(process)){
338 MC_state_interleave_process(next_state, process);
339 if(mc_reduce_kind != e_mc_reduce_none)
344 if(_sg_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _sg_mc_checkpoint == 0)){
345 next_state->system_state = MC_take_snapshot();
348 if(dot_output != NULL)
349 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
353 if(dot_output != NULL)
354 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state, req_str);
358 xbt_fifo_unshift(mc_stack_safety, next_state);
360 /* Insert in dict all enabled processes, if not included yet */
361 xbt_swag_foreach(process, simix_global->process_list){
362 if(MC_process_is_enabled(process)){
363 char *key = bprintf("%lu", process->pid);
364 if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
365 char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety));
366 xbt_dict_set(first_enabled_state, key, data, NULL);
372 if(dot_output != NULL)
377 /* Let's loop again */
379 /* The interleave set is empty or the maximum depth is reached, let's back-track */
382 if((xbt_fifo_size(mc_stack_safety) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != -1){
384 if(user_max_depth_reached && visited_state == -1)
385 XBT_DEBUG("User max depth reached !");
386 else if(visited_state == -1)
387 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
391 /* Interleave enabled processes in the state in which they have been enabled for the first time */
392 xbt_swag_foreach(process, simix_global->process_list){
393 if(MC_process_is_enabled(process)){
394 char *key = bprintf("%lu", process->pid);
395 enabled = (int)strtoul(xbt_dict_get_or_null(first_enabled_state, key), 0, 10);
397 mc_state_t state_test = NULL;
398 xbt_fifo_item_t item = NULL;
399 int cursor = xbt_fifo_size(mc_stack_safety);
400 xbt_fifo_foreach(mc_stack_safety, item, state_test, mc_state_t){
401 if(cursor-- == enabled){
402 if(!MC_state_process_is_done(state_test, process) && state_test->num != state->num){
403 XBT_DEBUG("Interleave process %lu in state %d", process->pid, state_test->num);
404 MC_state_interleave_process(state_test, process);
414 XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack_safety) + 1);
418 /* Trash the current state, no longer needed */
420 xbt_fifo_shift(mc_stack_safety);
421 MC_state_delete(state);
422 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
425 /* Check for deadlocks */
426 if(MC_deadlock_check()){
427 MC_show_deadlock(NULL);
432 /* Traverse the stack backwards until a state with a non empty interleave
433 set is found, deleting all the states that have it empty in the way.
434 For each deleted state, check if the request that has generated it
435 (from it's predecesor state), depends on any other previous request
436 executed before it. If it does then add it to the interleave set of the
437 state that executed that previous request. */
439 while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
440 if(mc_reduce_kind != e_mc_reduce_none){
441 req = MC_state_get_internal_request(state);
442 xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
443 if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
444 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
445 XBT_DEBUG("Dependent Transitions:");
446 prev_req = MC_state_get_executed_request(prev_state, &value);
447 req_str = MC_request_to_string(prev_req, value);
448 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
450 prev_req = MC_state_get_executed_request(state, &value);
451 req_str = MC_request_to_string(prev_req, value);
452 XBT_DEBUG("%s (state=%d)", req_str, state->num);
456 if(!MC_state_process_is_done(prev_state, req->issuer))
457 MC_state_interleave_process(prev_state, req->issuer);
459 XBT_DEBUG("Process %p is in done set", req->issuer);
463 }else if(req->issuer == MC_state_get_internal_request(prev_state)->issuer){
465 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
470 XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant", req->call, req->issuer->pid, state->num, MC_state_get_internal_request(prev_state)->call, MC_state_get_internal_request(prev_state)->issuer->pid, prev_state->num);
476 if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack_safety) < _sg_mc_max_depth) {
477 /* We found a back-tracking point, let's loop */
478 XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
479 if(_sg_mc_checkpoint){
480 if(state->system_state != NULL){
481 MC_restore_snapshot(state->system_state);
482 xbt_fifo_unshift(mc_stack_safety, state);
485 pos = xbt_fifo_size(mc_stack_safety);
486 item = xbt_fifo_get_first_item(mc_stack_safety);
488 restore_state = (mc_state_t) xbt_fifo_get_item_content(item);
489 if(restore_state->system_state != NULL){
492 item = xbt_fifo_get_next_item(item);
496 MC_restore_snapshot(restore_state->system_state);
497 xbt_fifo_unshift(mc_stack_safety, state);
499 MC_replay(mc_stack_safety, pos);
502 xbt_fifo_unshift(mc_stack_safety, state);
504 MC_replay(mc_stack_safety, -1);
506 XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety));
509 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
510 MC_state_delete(state);
516 MC_print_statistics(mc_stats);