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();
22 xbt_fifo_unshift(mc_stack_safety_stateless, initial_state);
25 XBT_DEBUG("**************************************************");
26 XBT_DEBUG("Initial state");
28 /* Wait for requests (schedules processes) */
29 MC_wait_for_requests();
32 /* Get an enabled process and insert it in the interleave set of the initial state */
33 xbt_swag_foreach(process, simix_global->process_list){
34 if(MC_process_is_enabled(process)){
35 MC_state_interleave_process(initial_state, process);
41 /* FIXME: Update Statistics
42 mc_stats->state_size +=
43 xbt_setset_set_size(initial_state->enabled_transitions); */
48 * \brief Perform the model-checking operation using a depth-first search exploration
49 * with Dynamic Partial Order Reductions
55 smx_simcall_t req = NULL, prev_req = NULL;
56 mc_state_t state = NULL, prev_state = NULL, next_state = NULL;
57 smx_process_t process = NULL;
58 xbt_fifo_item_t item = NULL;
60 while (xbt_fifo_size(mc_stack_safety_stateless) > 0) {
62 /* Get current state */
64 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety_stateless));
66 XBT_DEBUG("**************************************************");
67 XBT_DEBUG("Exploration depth=%d (state=%p)(%u interleave)",
68 xbt_fifo_size(mc_stack_safety_stateless), state,
69 MC_state_interleave_size(state));
71 /* Update statistics */
72 mc_stats->visited_states++;
74 /* If there are processes to interleave and the maximum depth has not been reached
75 then perform one step of the exploration algorithm */
76 if (xbt_fifo_size(mc_stack_safety_stateless) < MAX_DEPTH &&
77 (req = MC_state_get_request(state, &value))) {
79 /* Debug information */
80 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
81 req_str = MC_request_to_string(req, value);
82 XBT_DEBUG("Execute: %s", req_str);
86 MC_state_set_executed_request(state, req, value);
87 mc_stats->executed_transitions++;
89 /* Answer the request */
90 SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
92 /* Wait for requests (schedules processes) */
93 MC_wait_for_requests();
95 /* Create the new expanded state */
97 next_state = MC_state_new();
98 xbt_fifo_unshift(mc_stack_safety_stateless, next_state);
100 /* Get an enabled process and insert it in the interleave set of the next state */
101 xbt_swag_foreach(process, simix_global->process_list){
102 if(MC_process_is_enabled(process)){
103 MC_state_interleave_process(next_state, process);
109 /* FIXME: Update Statistics
110 mc_stats->state_size +=
111 xbt_setset_set_size(next_state->enabled_transitions);*/
113 /* Let's loop again */
115 /* The interleave set is empty or the maximum depth is reached, let's back-track */
117 XBT_DEBUG("There are no more processes to interleave.");
119 /* Trash the current state, no longer needed */
121 xbt_fifo_shift(mc_stack_safety_stateless);
122 MC_state_delete(state);
125 /* Check for deadlocks */
126 if(MC_deadlock_check()){
127 MC_show_deadlock(NULL);
132 /* Traverse the stack backwards until a state with a non empty interleave
133 set is found, deleting all the states that have it empty in the way.
134 For each deleted state, check if the request that has generated it
135 (from it's predecesor state), depends on any other previous request
136 executed before it. If it does then add it to the interleave set of the
137 state that executed that previous request. */
138 while ((state = xbt_fifo_shift(mc_stack_safety_stateless)) != NULL) {
139 req = MC_state_get_internal_request(state);
140 xbt_fifo_foreach(mc_stack_safety_stateless, item, prev_state, mc_state_t) {
141 if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
142 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
143 XBT_DEBUG("Dependent Transitions:");
144 prev_req = MC_state_get_executed_request(prev_state, &value);
145 req_str = MC_request_to_string(prev_req, value);
146 XBT_DEBUG("%s (state=%p)", req_str, prev_state);
148 prev_req = MC_state_get_executed_request(state, &value);
149 req_str = MC_request_to_string(prev_req, value);
150 XBT_DEBUG("%s (state=%p)", req_str, state);
154 if(!MC_state_process_is_done(prev_state, req->issuer))
155 MC_state_interleave_process(prev_state, req->issuer);
157 XBT_DEBUG("Process %p is in done set", req->issuer);
162 if (MC_state_interleave_size(state)) {
163 /* We found a back-tracking point, let's loop */
164 xbt_fifo_unshift(mc_stack_safety_stateless, state);
165 XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety_stateless));
167 MC_replay(mc_stack_safety_stateless);
170 MC_state_delete(state);
181 /********************* DPOR stateful *********************/
183 mc_state_ws_t new_state_ws(mc_snapshot_t s, mc_state_t gs){
184 mc_state_ws_t sws = NULL;
185 sws = xbt_new0(s_mc_state_ws_t, 1);
186 sws->system_state = s;
187 sws->graph_state = gs;
191 void MC_dpor_stateful_init(){
193 XBT_DEBUG("**************************************************");
194 XBT_DEBUG("DPOR (stateful) init");
195 XBT_DEBUG("**************************************************");
197 mc_state_t initial_graph_state;
198 smx_process_t process;
199 mc_snapshot_t initial_system_snapshot;
200 mc_state_ws_t initial_state ;
202 MC_wait_for_requests();
206 initial_system_snapshot = xbt_new0(s_mc_snapshot_t, 1);
208 initial_graph_state = MC_state_new();
209 xbt_swag_foreach(process, simix_global->process_list){
210 if(MC_process_is_enabled(process)){
211 MC_state_interleave_process(initial_graph_state, process);
216 MC_take_snapshot(initial_system_snapshot);
218 initial_state = new_state_ws(initial_system_snapshot, initial_graph_state);
219 xbt_fifo_unshift(mc_stack_safety_stateful, initial_state);
225 void MC_dpor_stateful(){
227 smx_process_t process = NULL;
229 if(xbt_fifo_size(mc_stack_safety_stateful) == 0)
233 mc_state_t next_graph_state = NULL;
234 smx_simcall_t req = NULL, prev_req = NULL;
236 xbt_fifo_item_t item = NULL;
238 mc_snapshot_t next_snapshot;
239 mc_state_ws_t current_state;
240 mc_state_ws_t prev_state;
241 mc_state_ws_t next_state;
243 while(xbt_fifo_size(mc_stack_safety_stateful) > 0){
245 current_state = (mc_state_ws_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety_stateful));
248 XBT_DEBUG("**************************************************");
249 XBT_DEBUG("Depth : %d, State : %p , %u interleave", xbt_fifo_size(mc_stack_safety_stateful),current_state, MC_state_interleave_size(current_state->graph_state));
251 mc_stats->visited_states++;
252 if(mc_stats->expanded_states>1100)
256 if((xbt_fifo_size(mc_stack_safety_stateful) < MAX_DEPTH) && (req = MC_state_get_request(current_state->graph_state, &value))){
258 /* Debug information */
259 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
260 req_str = MC_request_to_string(req, value);
261 //XBT_INFO("Visited states = %lu",mc_stats->visited_states );
262 XBT_DEBUG("Execute: %s",req_str);
266 MC_state_set_executed_request(current_state->graph_state, req, value);
267 mc_stats->executed_transitions++;
269 /* Answer the request */
270 SIMIX_simcall_pre(req, value);
272 /* Wait for requests (schedules processes) */
273 MC_wait_for_requests();
275 /* Create the new expanded graph_state */
278 next_graph_state = MC_state_new();
280 /* Get an enabled process and insert it in the interleave set of the next graph_state */
281 xbt_swag_foreach(process, simix_global->process_list){
282 if(MC_process_is_enabled(process)){
283 MC_state_interleave_process(next_graph_state, process);
288 next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
289 MC_take_snapshot(next_snapshot);
291 next_state = new_state_ws(next_snapshot, next_graph_state);
292 xbt_fifo_unshift(mc_stack_safety_stateful, next_state);
297 XBT_DEBUG("There are no more processes to interleave.");
299 /* Trash the current state, no longer needed */
301 xbt_fifo_shift(mc_stack_safety_stateful);
304 /* Check for deadlocks */
305 if(MC_deadlock_check()){
306 MC_show_deadlock_stateful(NULL);
311 while((current_state = xbt_fifo_shift(mc_stack_safety_stateful)) != NULL){
312 req = MC_state_get_internal_request(current_state->graph_state);
313 xbt_fifo_foreach(mc_stack_safety_stateful, item, prev_state, mc_state_ws_t) {
314 if(MC_request_depend(req, MC_state_get_internal_request(prev_state->graph_state))){
315 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
316 XBT_DEBUG("Dependent Transitions:");
317 prev_req = MC_state_get_executed_request(prev_state->graph_state, &value);
318 req_str = MC_request_to_string(prev_req, value);
319 XBT_DEBUG("%s (state=%p)", req_str, prev_state->graph_state);
321 prev_req = MC_state_get_executed_request(current_state->graph_state, &value);
322 req_str = MC_request_to_string(prev_req, value);
323 XBT_DEBUG("%s (state=%p)", req_str, current_state->graph_state);
327 if(!MC_state_process_is_done(prev_state->graph_state, req->issuer)){
328 MC_state_interleave_process(prev_state->graph_state, req->issuer);
331 XBT_DEBUG("Process %p is in done set", req->issuer);
338 if(MC_state_interleave_size(current_state->graph_state)){
339 MC_restore_snapshot(current_state->system_state);
340 xbt_fifo_unshift(mc_stack_safety_stateful, current_state);
341 XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety_stateful));