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
17 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
19 mc_state_t initial_state = NULL;
20 smx_process_t process;
22 /* Create the initial state and push it into the exploration stack */
24 initial_state = MC_state_new();
27 XBT_DEBUG("**************************************************");
28 XBT_DEBUG("Initial state");
30 /* Wait for requests (schedules processes) */
31 MC_wait_for_requests();
34 /* Get an enabled process and insert it in the interleave set of the initial state */
35 xbt_swag_foreach(process, simix_global->process_list){
36 if(MC_process_is_enabled(process)){
37 MC_state_interleave_process(initial_state, process);
42 xbt_fifo_unshift(mc_stack_safety, initial_state);
52 /* FIXME: Update Statistics
53 mc_stats->state_size +=
54 xbt_setset_set_size(initial_state->enabled_transitions); */
59 * \brief Perform the model-checking operation using a depth-first search exploration
60 * with Dynamic Partial Order Reductions
65 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
69 smx_simcall_t req = NULL, prev_req = NULL;
70 mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restore_state=NULL;
71 smx_process_t process = NULL;
72 xbt_fifo_item_t item = NULL;
75 while (xbt_fifo_size(mc_stack_safety) > 0) {
77 /* Get current state */
79 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
81 XBT_DEBUG("**************************************************");
82 XBT_DEBUG("Exploration depth=%d (state=%p)(%u interleave)",
83 xbt_fifo_size(mc_stack_safety), state,
84 MC_state_interleave_size(state));
86 /* Update statistics */
87 mc_stats->visited_states++;
89 /* If there are processes to interleave and the maximum depth has not been reached
90 then perform one step of the exploration algorithm */
91 if (xbt_fifo_size(mc_stack_safety) < MAX_DEPTH &&
92 (req = MC_state_get_request(state, &value))) {
94 /* Debug information */
95 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
96 req_str = MC_request_to_string(req, value);
97 XBT_DEBUG("Execute: %s", req_str);
101 MC_state_set_executed_request(state, req, value);
102 mc_stats->executed_transitions++;
104 /* Answer the request */
105 SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
107 /* Wait for requests (schedules processes) */
108 MC_wait_for_requests();
110 /* Create the new expanded state */
113 next_state = MC_state_new();
115 /* Get an enabled process and insert it in the interleave set of the next state */
116 xbt_swag_foreach(process, simix_global->process_list){
117 if(MC_process_is_enabled(process)){
118 MC_state_interleave_process(next_state, process);
123 if(_surf_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _surf_mc_checkpoint == 0)){
124 next_state->system_state = xbt_new0(s_mc_snapshot_t, 1);
125 MC_take_snapshot(next_state->system_state);
128 xbt_fifo_unshift(mc_stack_safety, next_state);
131 /* FIXME: Update Statistics
132 mc_stats->state_size +=
133 xbt_setset_set_size(next_state->enabled_transitions);*/
135 /* Let's loop again */
137 /* The interleave set is empty or the maximum depth is reached, let's back-track */
139 XBT_DEBUG("There are no more processes to interleave.");
141 /* Trash the current state, no longer needed */
143 xbt_fifo_shift(mc_stack_safety);
144 MC_state_delete(state);
147 /* Check for deadlocks */
148 if(MC_deadlock_check()){
149 MC_show_deadlock(NULL);
154 /* Traverse the stack backwards until a state with a non empty interleave
155 set is found, deleting all the states that have it empty in the way.
156 For each deleted state, check if the request that has generated it
157 (from it's predecesor state), depends on any other previous request
158 executed before it. If it does then add it to the interleave set of the
159 state that executed that previous request. */
160 while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
161 req = MC_state_get_internal_request(state);
162 xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
163 if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
164 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
165 XBT_DEBUG("Dependent Transitions:");
166 prev_req = MC_state_get_executed_request(prev_state, &value);
167 req_str = MC_request_to_string(prev_req, value);
168 XBT_DEBUG("%s (state=%p)", req_str, prev_state);
170 prev_req = MC_state_get_executed_request(state, &value);
171 req_str = MC_request_to_string(prev_req, value);
172 XBT_DEBUG("%s (state=%p)", req_str, state);
176 if(!MC_state_process_is_done(prev_state, req->issuer))
177 MC_state_interleave_process(prev_state, req->issuer);
179 XBT_DEBUG("Process %p is in done set", req->issuer);
184 if (MC_state_interleave_size(state)) {
185 /* We found a back-tracking point, let's loop */
186 if(_surf_mc_checkpoint){
187 if(state->system_state != NULL){
188 MC_restore_snapshot(state->system_state);
189 xbt_fifo_unshift(mc_stack_safety, state);
190 XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
193 pos = xbt_fifo_size(mc_stack_safety);
194 item = xbt_fifo_get_first_item(mc_stack_safety);
196 restore_state = (mc_state_t) xbt_fifo_get_item_content(item);
197 if(restore_state->system_state != NULL){
200 item = xbt_fifo_get_next_item(item);
204 MC_restore_snapshot(restore_state->system_state);
205 xbt_fifo_unshift(mc_stack_safety, state);
206 XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
208 MC_replay(mc_stack_safety, pos);
211 xbt_fifo_unshift(mc_stack_safety, state);
212 XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
214 MC_replay(mc_stack_safety, -1);
218 MC_state_delete(state);
224 MC_print_statistics(mc_stats);