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;
139 while (xbt_fifo_size(mc_stack_safety) > 0) {
141 /* Get current state */
143 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
145 XBT_DEBUG("**************************************************");
146 XBT_DEBUG("Exploration depth=%d (state=%p)(%u interleave)",
147 xbt_fifo_size(mc_stack_safety), state,
148 MC_state_interleave_size(state));
150 /* Update statistics */
151 mc_stats->visited_states++;
153 /* If there are processes to interleave and the maximum depth has not been reached
154 then perform one step of the exploration algorithm */
155 if (xbt_fifo_size(mc_stack_safety) < _sg_mc_max_depth &&
156 (req = MC_state_get_request(state, &value))) {
158 /* Debug information */
159 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
160 req_str = MC_request_to_string(req, value);
161 XBT_DEBUG("Execute: %s", req_str);
165 MC_state_set_executed_request(state, req, value);
166 mc_stats->executed_transitions++;
168 /* Answer the request */
169 SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
171 /* Wait for requests (schedules processes) */
172 MC_wait_for_requests();
174 /* Create the new expanded state */
177 next_state = MC_state_new();
179 if(!is_visited_state()){
181 /* Get an enabled process and insert it in the interleave set of the next state */
182 xbt_swag_foreach(process, simix_global->process_list){
183 if(MC_process_is_enabled(process)){
184 MC_state_interleave_process(next_state, process);
188 if(_sg_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _sg_mc_checkpoint == 0)){
189 next_state->system_state = MC_take_snapshot();
194 XBT_DEBUG("State already visited !");
198 xbt_fifo_unshift(mc_stack_safety, next_state);
201 /* FIXME: Update Statistics
202 mc_stats->state_size +=
203 xbt_setset_set_size(next_state->enabled_transitions);*/
205 /* Let's loop again */
207 /* The interleave set is empty or the maximum depth is reached, let's back-track */
210 if(xbt_fifo_size(mc_stack_safety) == _sg_mc_max_depth)
211 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
213 XBT_DEBUG("There are no more processes to interleave.");
215 /* Trash the current state, no longer needed */
217 xbt_fifo_shift(mc_stack_safety);
218 MC_state_delete(state);
221 /* Check for deadlocks */
222 if(MC_deadlock_check()){
223 MC_show_deadlock(NULL);
228 /* Traverse the stack backwards until a state with a non empty interleave
229 set is found, deleting all the states that have it empty in the way.
230 For each deleted state, check if the request that has generated it
231 (from it's predecesor state), depends on any other previous request
232 executed before it. If it does then add it to the interleave set of the
233 state that executed that previous request. */
235 while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
236 if(MC_state_interleave_size(state) == 0){
237 req = MC_state_get_internal_request(state);
238 xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
239 if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
240 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
241 XBT_DEBUG("Dependent Transitions:");
242 prev_req = MC_state_get_executed_request(prev_state, &value);
243 req_str = MC_request_to_string(prev_req, value);
244 XBT_DEBUG("%s (state=%p)", req_str, prev_state);
246 prev_req = MC_state_get_executed_request(state, &value);
247 req_str = MC_request_to_string(prev_req, value);
248 XBT_DEBUG("%s (state=%p)", req_str, state);
254 }else if(req->issuer == MC_state_get_executed_request(prev_state, &value)->issuer){
260 MC_state_remove_interleave_process(prev_state, req->issuer);
267 if (MC_state_interleave_size(state)) {
268 /* We found a back-tracking point, let's loop */
269 if(_sg_mc_checkpoint){
270 if(state->system_state != NULL){
271 MC_restore_snapshot(state->system_state);
272 xbt_fifo_unshift(mc_stack_safety, state);
273 XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
276 pos = xbt_fifo_size(mc_stack_safety);
277 item = xbt_fifo_get_first_item(mc_stack_safety);
279 restore_state = (mc_state_t) xbt_fifo_get_item_content(item);
280 if(restore_state->system_state != NULL){
283 item = xbt_fifo_get_next_item(item);
287 MC_restore_snapshot(restore_state->system_state);
288 xbt_fifo_unshift(mc_stack_safety, state);
289 XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
291 MC_replay(mc_stack_safety, pos);
294 xbt_fifo_unshift(mc_stack_safety, state);
295 XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
297 MC_replay(mc_stack_safety, -1);
301 MC_state_delete(state);
307 MC_print_statistics(mc_stats);