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 /********** Global variables **********/
14 xbt_dynar_t visited_states;
15 xbt_dict_t first_enabled_state;
16 xbt_dynar_t initial_communications_pattern;
17 xbt_dynar_t communications_pattern;
20 /********** Static functions ***********/
22 static void comm_pattern_free(mc_comm_pattern_t p){
29 static void comm_pattern_free_voidp( void *p){
30 comm_pattern_free((mc_comm_pattern_t) * (void **)p);
33 static mc_comm_pattern_t get_comm_pattern_from_idx(xbt_dynar_t pattern, unsigned int *idx, e_smx_comm_type_t type, unsigned long proc){
34 mc_comm_pattern_t current_comm;
35 while(*idx < xbt_dynar_length(pattern)){
36 current_comm = (mc_comm_pattern_t)xbt_dynar_get_as(pattern, *idx, mc_comm_pattern_t);
37 if(current_comm->type == type && type == SIMIX_COMM_SEND){
38 if(current_comm->src_proc == proc)
40 }else if(current_comm->type == type && type == SIMIX_COMM_RECEIVE){
41 if(current_comm->dst_proc == proc)
49 static int compare_comm_pattern(mc_comm_pattern_t comm1, mc_comm_pattern_t comm2){
50 if(strcmp(comm1->rdv, comm2->rdv) != 0)
52 if(comm1->src_proc != comm2->src_proc)
54 if(comm1->dst_proc != comm2->dst_proc)
56 if(comm1->data_size != comm2->data_size)
58 if(memcmp(comm1->data, comm2->data, comm1->data_size) != 0)
63 static void deterministic_pattern(xbt_dynar_t initial_pattern, xbt_dynar_t pattern){
64 unsigned int cursor = 0, send_index = 0, recv_index = 0;
65 mc_comm_pattern_t comm1, comm2;
66 int comm_comparison = 0;
67 int current_process = 0;
68 while(current_process < simix_process_maxpid){
69 while(cursor < xbt_dynar_length(initial_pattern)){
70 comm1 = (mc_comm_pattern_t)xbt_dynar_get_as(initial_pattern, cursor, mc_comm_pattern_t);
71 if(comm1->type == SIMIX_COMM_SEND && comm1->src_proc == current_process){
72 comm2 = get_comm_pattern_from_idx(pattern, &send_index, comm1->type, current_process);
73 comm_comparison = compare_comm_pattern(comm1, comm2);
74 if(comm_comparison == 1){
75 initial_state_safety->send_deterministic = 0;
76 initial_state_safety->comm_deterministic = 0;
80 }else if(comm1->type == SIMIX_COMM_RECEIVE && comm1->dst_proc == current_process){
81 comm2 = get_comm_pattern_from_idx(pattern, &recv_index, comm1->type, current_process);
82 comm_comparison = compare_comm_pattern(comm1, comm2);
83 if(comm_comparison == 1){
84 initial_state_safety->comm_deterministic = 0;
95 XBT_DEBUG("Communication-deterministic : %d, Send-deterministic : %d", initial_state_safety->comm_deterministic, initial_state_safety->send_deterministic);
98 static int complete_comm_pattern(xbt_dynar_t list, mc_comm_pattern_t pattern){
99 mc_comm_pattern_t current_pattern;
100 unsigned int cursor = 0;
101 xbt_dynar_foreach(list, cursor, current_pattern){
102 if(current_pattern->comm == pattern->comm){
103 if(!current_pattern->completed){
104 current_pattern->src_proc = pattern->comm->comm.src_proc->pid;
105 current_pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
106 current_pattern->data_size = pattern->comm->comm.src_buff_size;
107 current_pattern->data = xbt_malloc0(current_pattern->data_size);
108 current_pattern->matched_comm = pattern->num;
109 memcpy(current_pattern->data, current_pattern->comm->comm.src_buff, current_pattern->data_size);
110 current_pattern->completed = 1;
111 return current_pattern->num;
118 void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, int call){
119 mc_comm_pattern_t pattern = NULL;
120 pattern = xbt_new0(s_mc_comm_pattern_t, 1);
121 pattern->num = ++nb_comm_pattern;
122 pattern->completed = 0;
123 if(call == 1){ // ISEND
124 pattern->comm = simcall_comm_isend__get__result(request);
125 pattern->type = SIMIX_COMM_SEND;
126 if(pattern->comm->comm.dst_proc != NULL){
128 pattern->matched_comm = complete_comm_pattern(list, pattern);
129 pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
130 pattern->completed = 1;
132 pattern->src_proc = pattern->comm->comm.src_proc->pid;
133 pattern->data_size = pattern->comm->comm.src_buff_size;
134 pattern->data=xbt_malloc0(pattern->data_size);
135 memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
137 pattern->comm = simcall_comm_irecv__get__result(request);
138 pattern->type = SIMIX_COMM_RECEIVE;
139 if(pattern->comm->comm.src_proc != NULL){
140 pattern->matched_comm = complete_comm_pattern(list, pattern);
141 pattern->src_proc = pattern->comm->comm.src_proc->pid;
142 pattern->completed = 1;
143 pattern->data_size = pattern->comm->comm.src_buff_size;
144 pattern->data=xbt_malloc0(pattern->data_size);
145 memcpy(pattern->data, pattern->comm->comm.src_buff, pattern->data_size);
147 pattern->dst_proc = pattern->comm->comm.dst_proc->pid;
149 if(pattern->comm->comm.rdv != NULL)
150 pattern->rdv = strdup(pattern->comm->comm.rdv->name);
152 pattern->rdv = strdup(pattern->comm->comm.rdv_cpy->name);
153 xbt_dynar_push(list, &pattern);
156 static void print_communications_pattern(xbt_dynar_t comms_pattern){
157 unsigned int cursor = 0;
158 mc_comm_pattern_t current_comm;
159 xbt_dynar_foreach(comms_pattern, cursor, current_comm){
160 fprintf(stderr, "%s (%d - comm %p, src : %lu, dst %lu, rdv name %s, data %p, matched with %d)\n", current_comm->type == SIMIX_COMM_SEND ? "iSend" : "iRecv", current_comm->num, current_comm->comm, current_comm->src_proc, current_comm->dst_proc, current_comm->rdv, current_comm->data, current_comm->matched_comm);
164 static void visited_state_free(mc_visited_state_t state){
166 MC_free_snapshot(state->system_state);
171 static void visited_state_free_voidp(void *s){
172 visited_state_free((mc_visited_state_t) * (void **) s);
175 static mc_visited_state_t visited_state_new(){
177 mc_visited_state_t new_state = NULL;
178 new_state = xbt_new0(s_mc_visited_state_t, 1);
179 new_state->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
180 new_state->nb_processes = xbt_swag_size(simix_global->process_list);
181 new_state->system_state = MC_take_snapshot(mc_stats->expanded_states);
182 new_state->num = mc_stats->expanded_states;
183 new_state->other_num = -1;
189 static int get_search_interval(xbt_dynar_t all_states, mc_visited_state_t state, int *min, int *max){
191 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
195 int cursor = 0, previous_cursor, next_cursor;
196 mc_visited_state_t state_test;
198 int end = xbt_dynar_length(all_states) - 1;
201 cursor = (start + end) / 2;
202 state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, cursor, mc_visited_state_t);
203 if(state_test->nb_processes < state->nb_processes){
205 }else if(state_test->nb_processes > state->nb_processes){
208 if(state_test->heap_bytes_used < state->heap_bytes_used){
210 }else if(state_test->heap_bytes_used > state->heap_bytes_used){
213 *min = *max = cursor;
214 previous_cursor = cursor - 1;
215 while(previous_cursor >= 0){
216 state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, previous_cursor, mc_visited_state_t);
217 if(state_test->nb_processes != state->nb_processes || state_test->heap_bytes_used != state->heap_bytes_used)
219 *min = previous_cursor;
222 next_cursor = cursor + 1;
223 while(next_cursor < xbt_dynar_length(all_states)){
224 state_test = (mc_visited_state_t)xbt_dynar_get_as(all_states, next_cursor, mc_visited_state_t);
225 if(state_test->nb_processes != state->nb_processes || state_test->heap_bytes_used != state->heap_bytes_used)
243 static int is_visited_state(){
245 if(_sg_mc_visited == 0)
248 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
252 mc_visited_state_t new_state = visited_state_new();
254 if(xbt_dynar_is_empty(visited_states)){
256 xbt_dynar_push(visited_states, &new_state);
265 int min = -1, max = -1, index;
267 mc_visited_state_t state_test;
270 index = get_search_interval(visited_states, new_state, &min, &max);
272 if(min != -1 && max != -1){
273 /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
275 state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
276 if(state_test->other_num == -1)
277 new_state->other_num = state_test->num;
279 new_state->other_num = state_test->other_num;
280 if(dot_output == NULL)
281 XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
283 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);
284 xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
285 xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
288 return new_state->other_num;
291 while(cursor <= max){
292 state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
293 if(snapshot_compare(state_test, new_state) == 0){
294 if(state_test->other_num == -1)
295 new_state->other_num = state_test->num;
297 new_state->other_num = state_test->other_num;
298 if(dot_output == NULL)
299 XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
301 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);
302 xbt_dynar_remove_at(visited_states, cursor, NULL);
303 xbt_dynar_insert_at(visited_states, cursor, &new_state);
306 return new_state->other_num;
310 xbt_dynar_insert_at(visited_states, min, &new_state);
312 state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, index, mc_visited_state_t);
313 if(state_test->nb_processes < new_state->nb_processes){
314 xbt_dynar_insert_at(visited_states, index+1, &new_state);
316 if(state_test->heap_bytes_used < new_state->heap_bytes_used)
317 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
319 xbt_dynar_insert_at(visited_states, index, &new_state);
323 if(xbt_dynar_length(visited_states) > _sg_mc_visited){
324 int min2 = mc_stats->expanded_states;
325 unsigned int cursor2 = 0;
326 unsigned int index2 = 0;
327 xbt_dynar_foreach(visited_states, cursor2, state_test){
328 if(state_test->num < min2){
330 min2 = state_test->num;
333 xbt_dynar_remove_at(visited_states, index2, NULL);
345 * \brief Initialize the DPOR exploration algorithm
350 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
352 mc_state_t initial_state = NULL;
353 smx_process_t process;
355 /* Create the initial state and push it into the exploration stack */
358 if(_sg_mc_visited > 0)
359 visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
361 first_enabled_state = xbt_dict_new_homogeneous(&xbt_free_f);
363 initial_communications_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
364 communications_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), comm_pattern_free_voidp);
367 initial_state = MC_state_new();
371 XBT_DEBUG("**************************************************");
372 XBT_DEBUG("Initial state");
374 /* Wait for requests (schedules processes) */
375 MC_wait_for_requests();
377 MC_ignore_heap(simix_global->process_to_run->data, 0);
378 MC_ignore_heap(simix_global->process_that_ran->data, 0);
382 /* Get an enabled process and insert it in the interleave set of the initial state */
383 xbt_swag_foreach(process, simix_global->process_list){
384 if(MC_process_is_enabled(process)){
385 MC_state_interleave_process(initial_state, process);
386 if(mc_reduce_kind != e_mc_reduce_none)
391 xbt_fifo_unshift(mc_stack_safety, initial_state);
393 /* To ensure the soundness of DPOR, we have to keep a list of
394 processes which are still enabled at each step of the exploration.
395 If max depth is reached, we interleave them in the state in which they have
396 been enabled for the first time. */
397 xbt_swag_foreach(process, simix_global->process_list){
398 if(MC_process_is_enabled(process)){
399 char *key = bprintf("%lu", process->pid);
400 char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety));
401 xbt_dict_set(first_enabled_state, key, data, NULL);
417 * \brief Perform the model-checking operation using a depth-first search exploration
418 * with Dynamic Partial Order Reductions
423 char *req_str = NULL;
425 smx_simcall_t req = NULL, prev_req = NULL;
426 mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restore_state=NULL;
427 smx_process_t process = NULL;
428 xbt_fifo_item_t item = NULL;
429 mc_state_t state_test = NULL;
431 int visited_state = -1;
433 int comm_pattern = 0;
434 int interleave_size = 0;
436 while (xbt_fifo_size(mc_stack_safety) > 0) {
438 /* Get current state */
440 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
442 XBT_DEBUG("**************************************************");
443 XBT_DEBUG("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d, first_enabled_state size : %d)",
444 xbt_fifo_size(mc_stack_safety), state, state->num,
445 MC_state_interleave_size(state), user_max_depth_reached, xbt_dict_size(first_enabled_state));
447 interleave_size = MC_state_interleave_size(state);
449 /* Update statistics */
450 mc_stats->visited_states++;
452 /* If there are processes to interleave and the maximum depth has not been reached
453 then perform one step of the exploration algorithm */
454 if (xbt_fifo_size(mc_stack_safety) <= _sg_mc_max_depth && !user_max_depth_reached &&
455 (req = MC_state_get_request(state, &value)) && visited_state == -1) {
457 /* Debug information */
458 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
459 req_str = MC_request_to_string(req, value);
460 XBT_DEBUG("Execute: %s", req_str);
465 if(dot_output != NULL)
466 req_str = MC_request_get_dot_output(req, value);
469 MC_state_set_executed_request(state, req, value);
470 mc_stats->executed_transitions++;
473 char *key = bprintf("%lu", req->issuer->pid);
474 xbt_dict_remove(first_enabled_state, key);
478 if(req->call == SIMCALL_COMM_ISEND)
480 else if(req->call == SIMCALL_COMM_IRECV)
483 /* Answer the request */
484 SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
487 if(comm_pattern != 0){
488 if(!initial_state_safety->initial_communications_pattern_done)
489 get_comm_pattern(initial_communications_pattern, req, comm_pattern);
491 get_comm_pattern(communications_pattern, req, comm_pattern);
497 /* Wait for requests (schedules processes) */
498 MC_wait_for_requests();
500 /* Create the new expanded state */
503 next_state = MC_state_new();
505 if((visited_state = is_visited_state()) == -1){
507 /* Get an enabled process and insert it in the interleave set of the next state */
508 xbt_swag_foreach(process, simix_global->process_list){
509 if(MC_process_is_enabled(process)){
510 MC_state_interleave_process(next_state, process);
511 if(mc_reduce_kind != e_mc_reduce_none)
516 if(_sg_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _sg_mc_checkpoint == 0)){
517 next_state->system_state = MC_take_snapshot(next_state->num);
520 if(dot_output != NULL)
521 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
525 if(dot_output != NULL)
526 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state, req_str);
530 xbt_fifo_unshift(mc_stack_safety, next_state);
532 /* Insert in dict all enabled processes, if not included yet */
533 xbt_swag_foreach(process, simix_global->process_list){
534 if(MC_process_is_enabled(process)){
535 char *key = bprintf("%lu", process->pid);
536 if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
537 char *data = bprintf("%d", xbt_fifo_size(mc_stack_safety));
538 xbt_dict_set(first_enabled_state, key, data, NULL);
544 if(dot_output != NULL)
549 /* Let's loop again */
551 /* The interleave set is empty or the maximum depth is reached, let's back-track */
554 if((xbt_fifo_size(mc_stack_safety) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != -1){
556 if(user_max_depth_reached && visited_state == -1)
557 XBT_DEBUG("User max depth reached !");
558 else if(visited_state == -1)
559 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
563 /* Interleave enabled processes in the state in which they have been enabled for the first time */
564 xbt_swag_foreach(process, simix_global->process_list){
565 if(MC_process_is_enabled(process)){
566 char *key = bprintf("%lu", process->pid);
567 enabled = (int)strtoul(xbt_dict_get_or_null(first_enabled_state, key), 0, 10);
569 int cursor = xbt_fifo_size(mc_stack_safety);
570 xbt_fifo_foreach(mc_stack_safety, item, state_test, mc_state_t){
571 if(cursor-- == enabled){
572 if(!MC_state_process_is_done(state_test, process) && state_test->num != state->num){
573 XBT_DEBUG("Interleave process %lu in state %d", process->pid, state_test->num);
574 MC_state_interleave_process(state_test, process);
584 XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack_safety) + 1);
589 if(!initial_state_safety->initial_communications_pattern_done){
590 print_communications_pattern(initial_communications_pattern);
592 if(interleave_size == 0){ /* if (interleave_size > 0), process interleaved but not enabled => "incorrect" path, determinism not evaluated */
593 print_communications_pattern(communications_pattern);
594 deterministic_pattern(initial_communications_pattern, communications_pattern);
597 initial_state_safety->initial_communications_pattern_done = 1;
600 /* Trash the current state, no longer needed */
602 xbt_fifo_shift(mc_stack_safety);
603 MC_state_delete(state);
604 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
607 /* Check for deadlocks */
608 if(MC_deadlock_check()){
609 MC_show_deadlock(NULL);
614 /* Traverse the stack backwards until a state with a non empty interleave
615 set is found, deleting all the states that have it empty in the way.
616 For each deleted state, check if the request that has generated it
617 (from it's predecesor state), depends on any other previous request
618 executed before it. If it does then add it to the interleave set of the
619 state that executed that previous request. */
621 while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
622 if(mc_reduce_kind != e_mc_reduce_none){
623 req = MC_state_get_internal_request(state);
624 xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
625 if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
626 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
627 XBT_DEBUG("Dependent Transitions:");
628 prev_req = MC_state_get_executed_request(prev_state, &value);
629 req_str = MC_request_to_string(prev_req, value);
630 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
632 prev_req = MC_state_get_executed_request(state, &value);
633 req_str = MC_request_to_string(prev_req, value);
634 XBT_DEBUG("%s (state=%d)", req_str, state->num);
638 if(!MC_state_process_is_done(prev_state, req->issuer))
639 MC_state_interleave_process(prev_state, req->issuer);
641 XBT_DEBUG("Process %p is in done set", req->issuer);
645 }else if(req->issuer == MC_state_get_internal_request(prev_state)->issuer){
647 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
652 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);
658 if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack_safety) < _sg_mc_max_depth) {
659 /* We found a back-tracking point, let's loop */
660 XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
661 if(_sg_mc_checkpoint){
662 if(state->system_state != NULL){
663 MC_restore_snapshot(state->system_state);
664 xbt_fifo_unshift(mc_stack_safety, state);
667 pos = xbt_fifo_size(mc_stack_safety);
668 item = xbt_fifo_get_first_item(mc_stack_safety);
670 restore_state = (mc_state_t) xbt_fifo_get_item_content(item);
671 if(restore_state->system_state != NULL){
674 item = xbt_fifo_get_next_item(item);
678 MC_restore_snapshot(restore_state->system_state);
679 xbt_fifo_unshift(mc_stack_safety, state);
681 MC_replay(mc_stack_safety, pos);
684 xbt_fifo_unshift(mc_stack_safety, state);
686 MC_replay(mc_stack_safety, -1);
688 XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack_safety));
691 req = MC_state_get_internal_request(state);
692 if(req->call == SIMCALL_COMM_ISEND || req->call == SIMCALL_COMM_IRECV){
693 fprintf(stderr, "Remove state with isend or irecv\n");
694 if(!xbt_dynar_is_empty(communications_pattern))
695 xbt_dynar_remove_at(communications_pattern, xbt_dynar_length(communications_pattern) - 1, NULL);
697 XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack_safety) + 1);
698 MC_state_delete(state);
704 MC_print_statistics(mc_stats);