Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Improve independence detection and request pretty printing.
[simgrid.git] / src / mc / mc_dpor.c
1 /* Copyright (c) 2008 Martin Quinson, Cristian Rosa.
2    All rights reserved.                                          */
3
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. */
6
7 #include "private.h"
8
9 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc,
10                                 "Logging specific to MC DPOR exploration");
11
12 /**
13  *  \brief Initialize the DPOR exploration algorithm
14  */
15 void MC_dpor_init()
16 {
17   mc_state_t initial_state = NULL;
18   smx_process_t process;
19   
20   /* Create the initial state and push it into the exploration stack */
21   MC_SET_RAW_MEM;
22   initial_state = MC_state_new();
23   xbt_fifo_unshift(mc_stack, initial_state);
24   MC_UNSET_RAW_MEM;
25
26   DEBUG0("**************************************************");
27   DEBUG0("Initial state");
28
29   /* Wait for requests (schedules processes) */
30   MC_wait_for_requests();
31
32   MC_SET_RAW_MEM;
33   /* Get an enabled process and insert it in the interleave set of the initial state */
34   xbt_swag_foreach(process, simix_global->process_list){
35     if(MC_process_is_enabled(process)){
36       MC_state_interleave_process(initial_state, process);
37       break;
38     }
39   }
40   MC_UNSET_RAW_MEM;
41     
42   /* FIXME: Update Statistics 
43   mc_stats->state_size +=
44       xbt_setset_set_size(initial_state->enabled_transitions); */
45 }
46
47
48 /**
49  *      \brief Perform the model-checking operation using a depth-first search exploration
50  *         with Dynamic Partial Order Reductions
51  */
52 void MC_dpor(void)
53 {
54   char *req_str;
55   int value;
56   smx_req_t req = NULL, prev_req = NULL;
57   mc_state_t state = NULL, prev_state = NULL, next_state = NULL;
58   smx_process_t process = NULL;
59   xbt_fifo_item_t item = NULL;
60
61   while (xbt_fifo_size(mc_stack) > 0) {
62
63     /* Get current state */
64     state = (mc_state_t) 
65       xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
66
67     DEBUG0("**************************************************");
68     DEBUG3("Exploration detph=%d (state=%p)(%u interleave)",
69            xbt_fifo_size(mc_stack), state,
70            MC_state_interleave_size(state));
71
72     /* Update statistics */
73     mc_stats->visited_states++;
74
75     /* If there are processes to interleave and the maximum depth has not been reached
76        then perform one step of the exploration algorithm */
77     if (xbt_fifo_size(mc_stack) < MAX_DEPTH &&
78         (req = MC_state_get_request(state, &value))) {
79
80       /* Debug information */
81       if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
82         req_str = MC_request_to_string(req, value);
83         if(req->call == REQ_COMM_WAITANY)
84           DEBUG3("Execute: %s (%u of %lu)", req_str, value, xbt_dynar_length(req->comm_waitany.comms));
85         else if(req->call == REQ_COMM_TESTANY)
86           DEBUG3("Execute: %s (%u of %lu)", req_str, value, xbt_dynar_length(req->comm_testany.comms));
87         else
88           DEBUG1("Execute: %s", req_str);
89         xbt_free(req_str);
90       }
91
92       MC_state_set_executed_request(state, req, value);
93       mc_stats->executed_transitions++;
94
95       /* Answer the request */
96       SIMIX_request_pre(req, value); /* After this call req is no longer usefull */
97
98       /* Wait for requests (schedules processes) */
99       MC_wait_for_requests();
100
101       /* Create the new expanded state */
102       MC_SET_RAW_MEM;
103       next_state = MC_state_new();
104       xbt_fifo_unshift(mc_stack, next_state);
105
106       /* Get an enabled process and insert it in the interleave set of the next state */
107       xbt_swag_foreach(process, simix_global->process_list){
108         if(MC_process_is_enabled(process)){
109           MC_state_interleave_process(next_state, process);
110           break;
111         }
112       }
113       MC_UNSET_RAW_MEM;
114
115       /* FIXME: Update Statistics
116       mc_stats->state_size +=
117           xbt_setset_set_size(next_state->enabled_transitions);*/
118
119       /* Let's loop again */
120
121       /* The interleave set is empty or the maximum depth is reached, let's back-track */
122     } else {
123       DEBUG0("There are no more processes to interleave.");
124
125       /* Trash the current state, no longer needed */
126       MC_SET_RAW_MEM;
127       xbt_fifo_shift(mc_stack);
128       MC_state_delete(state);
129       MC_UNSET_RAW_MEM;
130
131       /* Check for deadlocks */
132       if(MC_deadlock_check()){
133         MC_show_deadlock(NULL);
134         return;
135       }
136
137       MC_SET_RAW_MEM;
138       /* Traverse the stack backwards until a state with a non empty interleave
139          set is found, deleting all the states that have it empty in the way.
140          For each deleted state, check if the request that has generated it 
141          (from it's predecesor state), depends on any other previous request 
142          executed before it. If it does then add it to the interleave set of the
143          state that executed that previous request. */
144       while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
145         req = MC_state_get_internal_request(state);
146         xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
147           if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
148             if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
149               DEBUG0("Dependent Transitions:");
150               prev_req = MC_state_get_executed_request(prev_state, &value);
151               req_str = MC_request_to_string(prev_req, value);
152               DEBUG2("%s (state=%p)", req_str, prev_state);
153               xbt_free(req_str);
154               prev_req = MC_state_get_executed_request(state, &value);
155               req_str = MC_request_to_string(prev_req, value);
156               DEBUG2("%s (state=%p)", req_str, state);
157               xbt_free(req_str);              
158             }
159
160             if(!MC_state_process_is_done(prev_state, req->issuer))
161               MC_state_interleave_process(prev_state, req->issuer);
162             else
163               DEBUG1("Process %p is in done set", req->issuer);
164
165             break;
166           }
167         }
168         if (MC_state_interleave_size(state)) {
169           /* We found a back-tracking point, let's loop */
170           xbt_fifo_unshift(mc_stack, state);
171           DEBUG1("Back-tracking to depth %d", xbt_fifo_size(mc_stack));
172           MC_UNSET_RAW_MEM;
173           MC_replay(mc_stack);
174           break;
175         } else {
176           MC_state_delete(state);
177         }
178       }
179       MC_UNSET_RAW_MEM;
180     }
181   }
182   MC_UNSET_RAW_MEM;
183   return;
184 }