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 int 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
67 smx_simcall_t req = NULL, prev_req = NULL;
68 mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restore_state=NULL;
69 smx_process_t process = NULL;
70 xbt_fifo_item_t item = NULL;
73 while (xbt_fifo_size(mc_stack_safety) > 0) {
75 /* Get current state */
77 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
79 XBT_DEBUG("**************************************************");
80 XBT_DEBUG("Exploration depth=%d (state=%p)(%u interleave)",
81 xbt_fifo_size(mc_stack_safety), state,
82 MC_state_interleave_size(state));
84 /* Update statistics */
85 mc_stats->visited_states++;
87 /* If there are processes to interleave and the maximum depth has not been reached
88 then perform one step of the exploration algorithm */
89 if (xbt_fifo_size(mc_stack_safety) < _surf_mc_max_depth &&
90 (req = MC_state_get_request(state, &value))) {
92 /* Debug information */
93 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
94 req_str = MC_request_to_string(req, value);
95 XBT_DEBUG("Execute: %s", req_str);
99 MC_state_set_executed_request(state, req, value);
100 mc_stats->executed_transitions++;
102 /* Answer the request */
103 SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
105 /* Wait for requests (schedules processes) */
106 MC_wait_for_requests();
108 /* Create the new expanded state */
111 next_state = MC_state_new();
113 /* Get an enabled process and insert it in the interleave set of the next state */
114 xbt_swag_foreach(process, simix_global->process_list){
115 if(MC_process_is_enabled(process)){
116 MC_state_interleave_process(next_state, process);
121 if(_surf_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _surf_mc_checkpoint == 0)){
122 next_state->system_state = xbt_new0(s_mc_snapshot_t, 1);
123 MC_take_snapshot(next_state->system_state);
126 xbt_fifo_unshift(mc_stack_safety, next_state);
129 /* FIXME: Update Statistics
130 mc_stats->state_size +=
131 xbt_setset_set_size(next_state->enabled_transitions);*/
133 /* Let's loop again */
135 /* The interleave set is empty or the maximum depth is reached, let's back-track */
137 XBT_DEBUG("There are no more processes to interleave.");
139 /* Trash the current state, no longer needed */
141 xbt_fifo_shift(mc_stack_safety);
142 MC_state_delete(state);
145 /* Check for deadlocks */
146 if(MC_deadlock_check()){
147 MC_show_deadlock(NULL);
152 /* Traverse the stack backwards until a state with a non empty interleave
153 set is found, deleting all the states that have it empty in the way.
154 For each deleted state, check if the request that has generated it
155 (from it's predecesor state), depends on any other previous request
156 executed before it. If it does then add it to the interleave set of the
157 state that executed that previous request. */
158 while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
159 req = MC_state_get_internal_request(state);
160 xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
161 if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
162 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
163 XBT_DEBUG("Dependent Transitions:");
164 prev_req = MC_state_get_executed_request(prev_state, &value);
165 req_str = MC_request_to_string(prev_req, value);
166 XBT_DEBUG("%s (state=%p)", req_str, prev_state);
168 prev_req = MC_state_get_executed_request(state, &value);
169 req_str = MC_request_to_string(prev_req, value);
170 XBT_DEBUG("%s (state=%p)", req_str, state);
174 if(!MC_state_process_is_done(prev_state, req->issuer))
175 MC_state_interleave_process(prev_state, req->issuer);
177 XBT_DEBUG("Process %p is in done set", req->issuer);
182 if (MC_state_interleave_size(state)) {
183 /* We found a back-tracking point, let's loop */
184 if(_surf_mc_checkpoint){
185 if(state->system_state != NULL){
186 MC_restore_snapshot(state->system_state);
187 xbt_fifo_unshift(mc_stack_safety, state);
188 XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
191 pos = xbt_fifo_size(mc_stack_safety);
192 item = xbt_fifo_get_first_item(mc_stack_safety);
194 restore_state = (mc_state_t) xbt_fifo_get_item_content(item);
195 if(restore_state->system_state != NULL){
198 item = xbt_fifo_get_next_item(item);
202 MC_restore_snapshot(restore_state->system_state);
203 xbt_fifo_unshift(mc_stack_safety, state);
204 XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
206 MC_replay(mc_stack_safety, pos);
209 xbt_fifo_unshift(mc_stack_safety, state);
210 XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
212 MC_replay(mc_stack_safety, -1);
216 MC_state_delete(state);
222 MC_print_statistics(mc_stats);