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 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc,
10 "Logging specific to MC DPOR exploration");
12 /********** Global variables **********/
14 xbt_dynar_t visited_states;
15 xbt_dict_t first_enabled_state;
17 /********** Static functions ***********/
19 static void visited_state_free(mc_visited_state_t state){
21 MC_free_snapshot(state->system_state);
26 static void visited_state_free_voidp(void *s){
27 visited_state_free((mc_visited_state_t) * (void **) s);
30 static mc_visited_state_t visited_state_new(){
32 mc_visited_state_t new_state = NULL;
33 new_state = xbt_new0(s_mc_visited_state_t, 1);
34 new_state->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
35 new_state->nb_processes = xbt_swag_size(simix_global->process_list);
36 new_state->system_state = MC_take_snapshot(mc_stats->expanded_states);
37 new_state->num = mc_stats->expanded_states;
38 new_state->other_num = -1;
44 static int get_search_interval(xbt_dynar_t all_states, mc_visited_state_t state, int *min, int *max){
46 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
50 int cursor = 0, previous_cursor, next_cursor;
51 mc_visited_state_t state_test;
53 int end = xbt_dynar_length(all_states) - 1;
56 cursor = (start + end) / 2;
57 state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, cursor, mc_visited_state_t);
58 if(state_test->nb_processes < state->nb_processes){
60 }else if(state_test->nb_processes > state->nb_processes){
63 if(state_test->heap_bytes_used < state->heap_bytes_used){
65 }else if(state_test->heap_bytes_used > state->heap_bytes_used){
69 previous_cursor = cursor - 1;
70 while(previous_cursor >= 0){
71 state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, previous_cursor, mc_visited_state_t);
72 if(state_test->nb_processes != state->nb_processes || state_test->heap_bytes_used != state->heap_bytes_used)
74 *min = previous_cursor;
77 next_cursor = cursor + 1;
78 while(next_cursor < xbt_dynar_length(all_states)){
79 state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, next_cursor, mc_visited_state_t);
80 if(state_test->nb_processes != state->nb_processes || state_test->heap_bytes_used != state->heap_bytes_used)
98 static int is_visited_state(){
100 if(_sg_mc_visited == 0)
103 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
107 mc_visited_state_t new_state = visited_state_new();
109 if(xbt_dynar_is_empty(visited_states)){
111 xbt_dynar_push(visited_states, &new_state);
120 int min = -1, max = -1, index;
122 mc_visited_state_t state_test;
125 index = get_search_interval(visited_states, new_state, &min, &max);
127 if(min != -1 && max != -1){
128 /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
130 state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
131 if(state_test->other_num == -1)
132 new_state->other_num = state_test->num;
134 new_state->other_num = state_test->other_num;
135 if(dot_output == NULL)
136 XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
138 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);
139 xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
140 xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
143 return new_state->other_num;
146 while(cursor <= max){
147 state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
148 if(snapshot_compare(state_test, new_state) == 0){
149 if(state_test->other_num == -1)
150 new_state->other_num = state_test->num;
152 new_state->other_num = state_test->other_num;
153 if(dot_output == NULL)
154 XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
156 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);
157 xbt_dynar_remove_at(visited_states, cursor, NULL);
158 xbt_dynar_insert_at(visited_states, cursor, &new_state);
161 return new_state->other_num;
165 xbt_dynar_insert_at(visited_states, min, &new_state);
167 state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, index, mc_visited_state_t);
168 if(state_test->nb_processes < new_state->nb_processes){
169 xbt_dynar_insert_at(visited_states, index+1, &new_state);
171 if(state_test->heap_bytes_used < new_state->heap_bytes_used)
172 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
174 xbt_dynar_insert_at(visited_states, index, &new_state);
178 if(xbt_dynar_length(visited_states) > _sg_mc_visited){
179 int min2 = mc_stats->expanded_states;
180 unsigned int cursor2 = 0;
181 unsigned int index2 = 0;
182 xbt_dynar_foreach(visited_states, cursor2, state_test){
183 if(state_test->num < min2){
185 min2 = state_test->num;
188 xbt_dynar_remove_at(visited_states, index2, NULL);
200 * \brief Initialize the DPOR exploration algorithm
205 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
207 mc_state_t initial_state = NULL;
208 smx_process_t process;
210 /* Create the initial state and push it into the exploration stack */
213 initial_state = MC_state_new();
214 if(_sg_mc_visited > 0)
215 visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
217 first_enabled_state = xbt_dict_new_homogeneous(&xbt_free_f);
221 XBT_DEBUG("**************************************************");
222 XBT_DEBUG("Initial state");
224 /* Wait for requests (schedules processes) */
225 MC_wait_for_requests();
227 MC_ignore_heap(simix_global->process_to_run->data, 0);
228 MC_ignore_heap(simix_global->process_that_ran->data, 0);
232 /* Get an enabled process and insert it in the interleave set of the initial state */
233 xbt_swag_foreach(process, simix_global->process_list){
234 if(MC_process_is_enabled(process)){
235 MC_state_interleave_process(initial_state, process);
236 if(mc_reduce_kind != e_mc_reduce_none)
241 xbt_fifo_unshift(mc_stack_safety, initial_state);
243 /* To ensure the soundness of DPOR, we have to keep a list of
244 processes which are still enabled at each step of the exploration.
245 If max depth is reached, we interleave them in the state in which they have
246 been enabled for the first time. */
247 xbt_swag_foreach(process, simix_global->process_list){
248 if(MC_process_is_enabled(process)){
249 char *key = bprintf("%lu", process->pid);
250 char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety));
251 xbt_dict_set(first_enabled_state, key, data, NULL);
267 * \brief Perform the model-checking operation using a depth-first search exploration
268 * with Dynamic Partial Order Reductions
273 char *req_str = NULL;
275 smx_simcall_t req = NULL, prev_req = NULL;
276 mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restore_state=NULL;
277 smx_process_t process = NULL;
278 xbt_fifo_item_t item = NULL;
279 mc_state_t state_test = NULL;
281 int visited_state = -1;
284 while (xbt_fifo_size(mc_stack_safety) > 0) {
286 /* Get current state */
288 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
290 XBT_DEBUG("**************************************************");
291 XBT_DEBUG("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d, first_enabled_state size : %d)",
292 xbt_fifo_size(mc_stack_safety), state, state->num,
293 MC_state_interleave_size(state), user_max_depth_reached, xbt_dict_size(first_enabled_state));
295 /* Update statistics */
296 mc_stats->visited_states++;
298 /* If there are processes to interleave and the maximum depth has not been reached
299 then perform one step of the exploration algorithm */
300 if (xbt_fifo_size(mc_stack_safety) <= _sg_mc_max_depth && !user_max_depth_reached &&
301 (req = MC_state_get_request(state, &value)) && visited_state == -1) {
303 /* Debug information */
304 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
305 req_str = MC_request_to_string(req, value);
306 XBT_DEBUG("Execute: %s", req_str);
311 if(dot_output != NULL)
312 req_str = MC_request_get_dot_output(req, value);
315 MC_state_set_executed_request(state, req, value);
316 mc_stats->executed_transitions++;
319 char *key = bprintf("%lu", req->issuer->pid);
320 xbt_dict_remove(first_enabled_state, key);
324 /* Answer the request */
325 SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
327 /* Wait for requests (schedules processes) */
328 MC_wait_for_requests();
330 /* Create the new expanded state */
333 next_state = MC_state_new();
335 if((visited_state = is_visited_state()) == -1){
337 /* Get an enabled process and insert it in the interleave set of the next state */
338 xbt_swag_foreach(process, simix_global->process_list){
339 if(MC_process_is_enabled(process)){
340 MC_state_interleave_process(next_state, process);
341 if(mc_reduce_kind != e_mc_reduce_none)
346 if(_sg_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _sg_mc_checkpoint == 0)){
347 next_state->system_state = MC_take_snapshot(next_state->num);
350 if(dot_output != NULL)
351 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
355 if(dot_output != NULL)
356 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state, req_str);
360 xbt_fifo_unshift(mc_stack_safety, next_state);
362 /* Insert in dict all enabled processes, if not included yet */
363 xbt_swag_foreach(process, simix_global->process_list){
364 if(MC_process_is_enabled(process)){
365 char *key = bprintf("%lu", process->pid);
366 if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
367 char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety));
368 xbt_dict_set(first_enabled_state, key, data, NULL);
374 if(dot_output != NULL)
379 /* Let's loop again */
381 /* The interleave set is empty or the maximum depth is reached, let's back-track */
384 if((xbt_fifo_size(mc_stack_safety) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != -1){
386 if(user_max_depth_reached && visited_state == -1)
387 XBT_DEBUG("User max depth reached !");
388 else if(visited_state == -1)
389 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
393 /* Interleave enabled processes in the state in which they have been enabled for the first time */
394 xbt_swag_foreach(process, simix_global->process_list){
395 if(MC_process_is_enabled(process)){
396 char *key = bprintf("%lu", process->pid);
397 enabled = (int)strtoul(xbt_dict_get_or_null(first_enabled_state, key), 0, 10);
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 done", 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);