1 /* Copyright (c) 2008-2012. Da SimGrid Team. All rights reserved. */
3 /* This program is free software; you can redistribute it and/or modify it
4 * under the terms of the license (GNU LGPL) which comes with this package. */
6 #include "mc_private.h"
8 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc,
9 "Logging specific to MC DPOR exploration");
11 xbt_dynar_t visited_states;
13 static int is_visited_state(void);
15 static int is_visited_state(){
17 if(_sg_mc_visited == 0)
20 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
24 mc_snapshot_t new_state = NULL;
25 new_state = MC_take_snapshot();
29 if(xbt_dynar_is_empty(visited_states)){
32 xbt_dynar_push(visited_states, &new_state);
44 unsigned int cursor = 0;
45 mc_snapshot_t state_test = NULL;
47 xbt_dynar_foreach(visited_states, cursor, state_test){
48 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug))
49 XBT_DEBUG("****** Pair visited #%d ******", cursor + 1);
50 if(snapshot_compare(new_state, state_test, NULL, NULL) == 0){
60 if(xbt_dynar_length(visited_states) == _sg_mc_visited){
61 mc_snapshot_t state_to_remove = NULL;
62 xbt_dynar_shift(visited_states, &state_to_remove);
63 MC_free_snapshot(state_to_remove);
66 xbt_dynar_push(visited_states, &new_state);
79 * \brief Initialize the DPOR exploration algorithm
84 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
86 mc_state_t initial_state = NULL;
87 smx_process_t process;
89 /* Create the initial state and push it into the exploration stack */
92 initial_state = MC_state_new();
93 visited_states = xbt_dynar_new(sizeof(mc_snapshot_t), NULL);
97 XBT_DEBUG("**************************************************");
98 XBT_DEBUG("Initial state");
100 /* Wait for requests (schedules processes) */
101 MC_wait_for_requests();
105 /* Get an enabled process and insert it in the interleave set of the initial state */
106 xbt_swag_foreach(process, simix_global->process_list){
107 if(MC_process_is_enabled(process)){
108 MC_state_interleave_process(initial_state, process);
112 xbt_fifo_unshift(mc_stack_safety, initial_state);
125 * \brief Perform the model-checking operation using a depth-first search exploration
126 * with Dynamic Partial Order Reductions
133 smx_simcall_t req = NULL, prev_req = NULL;
134 mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restore_state=NULL;
135 smx_process_t process = NULL;
136 xbt_fifo_item_t item = NULL;
138 int proc_eval[simix_process_maxpid];
140 while (xbt_fifo_size(mc_stack_safety) > 0) {
142 /* Get current state */
144 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
146 XBT_DEBUG("**************************************************");
147 XBT_DEBUG("Exploration depth=%d (state=%p)(%u interleave)",
148 xbt_fifo_size(mc_stack_safety), state,
149 MC_state_interleave_size(state));
151 /* Update statistics */
152 mc_stats->visited_states++;
154 /* If there are processes to interleave and the maximum depth has not been reached
155 then perform one step of the exploration algorithm */
156 if (xbt_fifo_size(mc_stack_safety) < _sg_mc_max_depth &&
157 (req = MC_state_get_request(state, &value))) {
159 /* Debug information */
160 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
161 req_str = MC_request_to_string(req, value);
162 XBT_DEBUG("Execute: %s", req_str);
166 MC_state_set_executed_request(state, req, value);
167 mc_stats->executed_transitions++;
169 /* Answer the request */
170 SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
172 /* Wait for requests (schedules processes) */
173 MC_wait_for_requests();
175 /* Create the new expanded state */
178 next_state = MC_state_new();
180 if(!is_visited_state()){
182 /* Get an enabled process and insert it in the interleave set of the next state */
183 xbt_swag_foreach(process, simix_global->process_list){
184 if(MC_process_is_enabled(process)){
185 MC_state_interleave_process(next_state, process);
189 if(_sg_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _sg_mc_checkpoint == 0)){
190 next_state->system_state = MC_take_snapshot();
195 XBT_DEBUG("State already visited !");
199 xbt_fifo_unshift(mc_stack_safety, next_state);
202 /* FIXME: Update Statistics
203 mc_stats->state_size +=
204 xbt_setset_set_size(next_state->enabled_transitions);*/
206 /* Let's loop again */
208 /* The interleave set is empty or the maximum depth is reached, let's back-track */
211 if(xbt_fifo_size(mc_stack_safety) == _sg_mc_max_depth)
212 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
214 XBT_DEBUG("There are no more processes to interleave.");
216 /* Trash the current state, no longer needed */
218 xbt_fifo_shift(mc_stack_safety);
219 MC_state_delete(state);
222 /* Check for deadlocks */
223 if(MC_deadlock_check()){
224 MC_show_deadlock(NULL);
229 /* Traverse the stack backwards until a state with a non empty interleave
230 set is found, deleting all the states that have it empty in the way.
231 For each deleted state, check if the request that has generated it
232 (from it's predecesor state), depends on any other previous request
233 executed before it. If it does then add it to the interleave set of the
234 state that executed that previous request. */
236 while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
238 for(i=0; i<simix_process_maxpid; i++)
241 if(MC_state_interleave_size(state) == 0){
242 req = MC_state_get_internal_request(state);
243 xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
244 if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
245 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
246 XBT_DEBUG("Dependent Transitions:");
247 prev_req = MC_state_get_executed_request(prev_state, &value);
248 req_str = MC_request_to_string(prev_req, value);
249 XBT_DEBUG("%s (state=%p)", req_str, prev_state);
251 prev_req = MC_state_get_executed_request(state, &value);
252 req_str = MC_request_to_string(prev_req, value);
253 XBT_DEBUG("%s (state=%p)", req_str, state);
259 }else if(req->issuer == MC_state_get_executed_request(prev_state, &value)->issuer){
263 }else if(proc_eval[MC_state_get_executed_request(prev_state, &value)->issuer->pid] == 0){
265 MC_state_remove_interleave_process(prev_state, MC_state_get_executed_request(prev_state, &value)->issuer);
269 proc_eval[MC_state_get_executed_request(prev_state, &value)->issuer->pid] = 1;
274 if (MC_state_interleave_size(state)) {
275 /* We found a back-tracking point, let's loop */
276 if(_sg_mc_checkpoint){
277 if(state->system_state != NULL){
278 MC_restore_snapshot(state->system_state);
279 xbt_fifo_unshift(mc_stack_safety, state);
280 XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
283 pos = xbt_fifo_size(mc_stack_safety);
284 item = xbt_fifo_get_first_item(mc_stack_safety);
286 restore_state = (mc_state_t) xbt_fifo_get_item_content(item);
287 if(restore_state->system_state != NULL){
290 item = xbt_fifo_get_next_item(item);
294 MC_restore_snapshot(restore_state->system_state);
295 xbt_fifo_unshift(mc_stack_safety, state);
296 XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
298 MC_replay(mc_stack_safety, pos);
301 xbt_fifo_unshift(mc_stack_safety, state);
302 XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
304 MC_replay(mc_stack_safety, -1);
308 MC_state_delete(state);
314 MC_print_statistics(mc_stats);