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");
12 * \brief Initialize the DPOR exploration algorithm
16 mc_state_t initial_state = NULL;
17 smx_process_t process;
19 /* Create the initial state and push it into the exploration stack */
21 initial_state = MC_state_new();
24 XBT_DEBUG("**************************************************");
25 XBT_DEBUG("Initial state");
27 /* Wait for requests (schedules processes) */
28 MC_wait_for_requests();
31 /* Get an enabled process and insert it in the interleave set of the initial state */
32 xbt_swag_foreach(process, simix_global->process_list){
33 if(MC_process_is_enabled(process)){
34 MC_state_interleave_process(initial_state, process);
39 initial_state->system_state = xbt_new0(s_mc_snapshot_t, 1);
40 MC_take_snapshot(initial_state->system_state);
42 xbt_fifo_unshift(mc_stack_safety, initial_state);
46 /* FIXME: Update Statistics
47 mc_stats->state_size +=
48 xbt_setset_set_size(initial_state->enabled_transitions); */
53 * \brief Perform the model-checking operation using a depth-first search exploration
54 * with Dynamic Partial Order Reductions
60 smx_simcall_t req = NULL, prev_req = NULL;
61 mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restore_state=NULL;
62 smx_process_t process = NULL;
63 xbt_fifo_item_t item = NULL;
66 while (xbt_fifo_size(mc_stack_safety) > 0) {
68 /* Get current state */
70 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
72 XBT_DEBUG("**************************************************");
73 XBT_DEBUG("Exploration depth=%d (state=%p)(%u interleave)",
74 xbt_fifo_size(mc_stack_safety), state,
75 MC_state_interleave_size(state));
77 /* Update statistics */
78 mc_stats->visited_states++;
80 /* If there are processes to interleave and the maximum depth has not been reached
81 then perform one step of the exploration algorithm */
82 if (xbt_fifo_size(mc_stack_safety) < MAX_DEPTH &&
83 (req = MC_state_get_request(state, &value))) {
85 /* Debug information */
86 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
87 req_str = MC_request_to_string(req, value);
88 XBT_DEBUG("Execute: %s", req_str);
92 MC_state_set_executed_request(state, req, value);
93 mc_stats->executed_transitions++;
95 /* Answer the request */
96 SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
98 /* Wait for requests (schedules processes) */
99 MC_wait_for_requests();
101 /* Create the new expanded state */
104 next_state = MC_state_new();
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);
114 if(_surf_do_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _surf_do_mc_checkpoint == 0)){
115 next_state->system_state = xbt_new0(s_mc_snapshot_t, 1);
116 MC_take_snapshot(next_state->system_state);
119 xbt_fifo_unshift(mc_stack_safety, next_state);
122 /* FIXME: Update Statistics
123 mc_stats->state_size +=
124 xbt_setset_set_size(next_state->enabled_transitions);*/
126 /* Let's loop again */
128 /* The interleave set is empty or the maximum depth is reached, let's back-track */
130 XBT_DEBUG("There are no more processes to interleave.");
132 /* Trash the current state, no longer needed */
134 xbt_fifo_shift(mc_stack_safety);
135 MC_state_delete(state);
138 /* Check for deadlocks */
139 if(MC_deadlock_check()){
140 MC_show_deadlock(NULL);
145 /* Traverse the stack backwards until a state with a non empty interleave
146 set is found, deleting all the states that have it empty in the way.
147 For each deleted state, check if the request that has generated it
148 (from it's predecesor state), depends on any other previous request
149 executed before it. If it does then add it to the interleave set of the
150 state that executed that previous request. */
151 while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
152 req = MC_state_get_internal_request(state);
153 xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
154 if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
155 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
156 XBT_DEBUG("Dependent Transitions:");
157 prev_req = MC_state_get_executed_request(prev_state, &value);
158 req_str = MC_request_to_string(prev_req, value);
159 XBT_DEBUG("%s (state=%p)", req_str, prev_state);
161 prev_req = MC_state_get_executed_request(state, &value);
162 req_str = MC_request_to_string(prev_req, value);
163 XBT_DEBUG("%s (state=%p)", req_str, state);
167 if(!MC_state_process_is_done(prev_state, req->issuer))
168 MC_state_interleave_process(prev_state, req->issuer);
170 XBT_DEBUG("Process %p is in done set", req->issuer);
175 if (MC_state_interleave_size(state)) {
176 /* We found a back-tracking point, let's loop */
177 if(_surf_do_mc_checkpoint){
178 if(state->system_state != NULL){
179 MC_restore_snapshot(state->system_state);
180 xbt_fifo_unshift(mc_stack_safety, state);
181 XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
184 pos = xbt_fifo_size(mc_stack_safety);
185 item = xbt_fifo_get_first_item(mc_stack_safety);
187 restore_state = (mc_state_t) xbt_fifo_get_item_content(item);
188 if(restore_state->system_state != NULL){
191 item = xbt_fifo_get_next_item(item);
195 MC_restore_snapshot(restore_state->system_state);
196 xbt_fifo_unshift(mc_stack_safety, state);
197 XBT_DEBUG("Back-tracking to depth %d", pos);
199 MC_replay(mc_stack_safety, pos);
202 xbt_fifo_unshift(mc_stack_safety, state);
203 XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
205 MC_replay(mc_stack_safety, -1);
209 MC_state_delete(state);
215 MC_print_statistics(mc_stats);