1 /* Copyright (c) 2008 Martin Quinson, Cristian Rosa.
2 All rights reserved. */
4 /* This program is free software; you can redistribute it and/or modify it
5 * under the terms of the license (GNU LGPL) which comes with this package. */
9 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dpor, mc,
10 "Logging specific to MC DPOR exploration");
13 * \brief Initialize the DPOR exploration algorithm
17 mc_state_t initial_state = NULL;
18 smx_process_t process;
20 /* Create the initial state and push it into the exploration stack */
22 initial_state = MC_state_new();
23 xbt_fifo_unshift(mc_stack, initial_state);
26 DEBUG0("**************************************************");
27 DEBUG0("Initial state");
29 /* Wait for requests (schedules processes) */
30 MC_wait_for_requests();
33 /* Get an enabled process and insert it in the interleave set of the initial state */
34 xbt_swag_foreach(process, simix_global->process_list){
35 if(SIMIX_process_is_enabled(process)){
36 xbt_setset_set_insert(initial_state->interleave, process);
42 /* FIXME: Update Statistics
43 mc_stats->state_size +=
44 xbt_setset_set_size(initial_state->enabled_transitions); */
49 * \brief Perform the model-checking operation using a depth-first search exploration
50 * with Dynamic Partial Order Reductions
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) > 0) {
62 DEBUG0("**************************************************");
64 /* Get current state */
66 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
68 /* If there are processes to interleave and the maximun depth has not been reached
69 then perform one step of the exploration algorithm */
70 if (xbt_setset_set_size(state->interleave) > 0
71 && xbt_fifo_size(mc_stack) < MAX_DEPTH) {
73 DEBUG3("Exploration detph=%d (state=%p)(%d interleave)",
74 xbt_fifo_size(mc_stack), state,
75 xbt_setset_set_size(state->interleave));
77 /* Update statistics */
78 mc_stats->visited_states++;
79 mc_stats->executed_transitions++;
82 /* Choose a request to execute from the the current state */
83 req = MC_state_get_request(state);
87 /* Answer the request */
88 /* Debug information */
89 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
90 req_str = MC_request_to_string(req);
91 DEBUG1("Execute: %s", req_str);
95 SIMIX_request_pre(req);
97 MC_state_set_executed_request(state, req);
99 /* Wait for requests (schedules processes) */
100 MC_wait_for_requests();
102 /* Create the new expanded state */
104 next_state = MC_state_new();
105 xbt_fifo_unshift(mc_stack, next_state);
108 /* Get an enabled process and insert it in the interleave set of the next state */
109 xbt_swag_foreach(process, simix_global->process_list){
110 if(SIMIX_process_is_enabled(process)){
111 xbt_setset_set_insert(next_state->interleave, process);
117 /* FIXME: Update Statistics
118 mc_stats->state_size +=
119 xbt_setset_set_size(next_state->enabled_transitions);*/
121 /* Let's loop again */
123 /* The interleave set is empty or the maximum depth is reached, let's back-track */
125 DEBUG0("There are no more processes to interleave.");
127 /* Check for deadlocks */
128 xbt_swag_foreach(process, simix_global->process_list){
129 /* FIXME: use REQ_NO_REQ instead of NULL for comparison */
130 if(&process->request && !SIMIX_request_is_enabled(&process->request)){
131 MC_show_deadlock(&process->request);
137 INFO0("*********************************");
138 MC_show_stack(mc_stack); */
140 /* Trash the current state, no longer needed */
142 xbt_fifo_shift(mc_stack);
143 MC_state_delete(state);
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)) != NULL) {
152 req = MC_state_get_executed_request(state);
153 xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
154 if(MC_request_depend(req, MC_state_get_executed_request(prev_state))){
155 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
156 DEBUG0("Dependent Transitions:");
157 req_str = MC_request_to_string(MC_state_get_executed_request(prev_state));
158 DEBUG1("%s", req_str);
160 req_str = MC_request_to_string(req);
161 DEBUG1("%s", req_str);
164 xbt_setset_set_insert(prev_state->interleave, req->issuer);
168 if (xbt_setset_set_size(state->interleave) > 0) {
169 /* We found a back-tracking point, let's loop */
170 xbt_fifo_unshift(mc_stack, state);
171 DEBUG1("Back-tracking to depth %d", xbt_fifo_size(mc_stack));
176 MC_state_delete(state);