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);
14 static void visited_state_free(mc_safety_visited_state_t state);
15 static void visited_state_free_voidp(void *s);
17 static void visited_state_free(mc_safety_visited_state_t state){
19 MC_free_snapshot(state->system_state);
24 static void visited_state_free_voidp(void *s){
25 visited_state_free((mc_safety_visited_state_t) * (void **) s);
28 static int is_visited_state(){
30 if(_sg_mc_visited == 0)
33 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
37 mc_safety_visited_state_t new_state = NULL;
38 new_state = xbt_new0(s_mc_safety_visited_state_t, 1);
39 new_state->system_state = MC_take_snapshot();
40 new_state->num = mc_stats->expanded_states;
44 if(xbt_dynar_is_empty(visited_states)){
47 xbt_dynar_push(visited_states, &new_state);
59 size_t current_bytes_used = new_state->system_state->heap_bytes_used;
61 unsigned int cursor = 0;
62 int previous_cursor = 0, next_cursor = 0;
64 int end = xbt_dynar_length(visited_states) - 1;
66 mc_safety_visited_state_t state_test = NULL;
67 size_t bytes_used_test;
68 int same_bytes_not_found = 1;
70 while(start <= end && same_bytes_not_found){
71 cursor = (start + end) / 2;
72 state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_safety_visited_state_t);
73 bytes_used_test = state_test->system_state->heap_bytes_used;
74 if(bytes_used_test < current_bytes_used)
76 if(bytes_used_test > current_bytes_used)
78 if(bytes_used_test == current_bytes_used){
79 same_bytes_not_found = 0;
80 if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){
81 xbt_dynar_remove_at(visited_states, cursor, NULL);
82 xbt_dynar_insert_at(visited_states, cursor, &new_state);
83 XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
88 return state_test->num;
90 /* Search another state with same number of bytes used */
91 previous_cursor = cursor - 1;
92 while(previous_cursor >= 0){
93 state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, previous_cursor, mc_safety_visited_state_t);
94 bytes_used_test = state_test->system_state->heap_bytes_used;
95 if(bytes_used_test != current_bytes_used)
97 if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){
98 xbt_dynar_remove_at(visited_states, previous_cursor, NULL);
99 xbt_dynar_insert_at(visited_states, previous_cursor, &new_state);
100 XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
105 return state_test->num;
109 next_cursor = cursor + 1;
110 while(next_cursor < xbt_dynar_length(visited_states)){
111 state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, next_cursor, mc_safety_visited_state_t);
112 bytes_used_test = state_test->system_state->heap_bytes_used;
113 if(bytes_used_test != current_bytes_used)
115 if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){
116 xbt_dynar_remove_at(visited_states, next_cursor, NULL);
117 xbt_dynar_insert_at(visited_states, next_cursor, &new_state);
118 XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
123 return state_test->num;
131 state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_safety_visited_state_t);
132 bytes_used_test = state_test->system_state->heap_bytes_used;
134 if(bytes_used_test < current_bytes_used)
135 xbt_dynar_insert_at(visited_states, cursor + 1, &new_state);
137 xbt_dynar_insert_at(visited_states, cursor, &new_state);
139 if(xbt_dynar_length(visited_states) > _sg_mc_visited){
140 int min = mc_stats->expanded_states;
141 unsigned int cursor2 = 0;
142 unsigned int index = 0;
143 xbt_dynar_foreach(visited_states, cursor2, state_test){
144 if(state_test->num < min){
146 min = state_test->num;
149 xbt_dynar_remove_at(visited_states, index, NULL);
163 * \brief Initialize the DPOR exploration algorithm
168 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
170 mc_state_t initial_state = NULL;
171 smx_process_t process;
173 /* Create the initial state and push it into the exploration stack */
176 initial_state = MC_state_new();
177 visited_states = xbt_dynar_new(sizeof(mc_safety_visited_state_t), visited_state_free_voidp);
181 XBT_DEBUG("**************************************************");
182 XBT_DEBUG("Initial state");
184 /* Wait for requests (schedules processes) */
185 MC_wait_for_requests();
189 /* Get an enabled process and insert it in the interleave set of the initial state */
190 xbt_swag_foreach(process, simix_global->process_list){
191 if(MC_process_is_enabled(process)){
192 MC_state_interleave_process(initial_state, process);
193 XBT_DEBUG("Process %lu enabled with simcall %d", process->pid, process->simcall.call);
197 xbt_fifo_unshift(mc_stack_safety, initial_state);
210 * \brief Perform the model-checking operation using a depth-first search exploration
211 * with Dynamic Partial Order Reductions
218 smx_simcall_t req = NULL, prev_req = NULL, req2 = NULL;
219 s_smx_simcall_t req3;
220 mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restore_state=NULL;
221 smx_process_t process = NULL;
222 xbt_fifo_item_t item = NULL;
223 int pos, i, interleave_size;
224 int interleave_proc[simix_process_maxpid];
227 while (xbt_fifo_size(mc_stack_safety) > 0) {
229 /* Get current state */
231 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
233 XBT_DEBUG("**************************************************");
234 XBT_DEBUG("Exploration depth=%d (state=%p)(%u interleave)",
235 xbt_fifo_size(mc_stack_safety), state,
236 MC_state_interleave_size(state));
238 /* Update statistics */
239 mc_stats->visited_states++;
241 /* If there are processes to interleave and the maximum depth has not been reached
242 then perform one step of the exploration algorithm */
243 if (xbt_fifo_size(mc_stack_safety) < _sg_mc_max_depth &&
244 (req = MC_state_get_request(state, &value))) {
246 /* Debug information */
247 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
248 req_str = MC_request_to_string(req, value);
249 XBT_DEBUG("Execute: %s", req_str);
253 req_str = MC_request_get_dot_output(req, value);
255 MC_state_set_executed_request(state, req, value);
256 mc_stats->executed_transitions++;
258 if(MC_state_interleave_size(state)){
260 req2 = MC_state_get_internal_request(state);
262 for(i=0; i<simix_process_maxpid; i++)
263 interleave_proc[i] = 0;
265 interleave_size = MC_state_interleave_size(state);
266 while(i < interleave_size){
268 prev_req = MC_state_get_request(state, &value2);
269 if(prev_req != NULL){
270 MC_state_set_executed_request(state, prev_req, value2);
271 prev_req = MC_state_get_internal_request(state);
272 if(MC_request_depend(&req3, prev_req)){
273 XBT_DEBUG("Simcall %d in process %lu dependant with simcall %d in process %lu", req3.call, req3.issuer->pid, prev_req->call, prev_req->issuer->pid);
274 interleave_proc[prev_req->issuer->pid] = 1;
276 XBT_DEBUG("Simcall %d in process %lu independant with simcall %d in process %lu", req3.call, req3.issuer->pid, prev_req->call, prev_req->issuer->pid);
277 MC_state_remove_interleave_process(state, prev_req->issuer);
281 xbt_swag_foreach(process, simix_global->process_list){
282 if(interleave_proc[process->pid] == 1)
283 MC_state_interleave_process(state, process);
288 MC_state_set_executed_request(state, req, value);
290 /* Answer the request */
291 SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
293 /* Wait for requests (schedules processes) */
294 MC_wait_for_requests();
296 /* Create the new expanded state */
299 next_state = MC_state_new();
301 if((visited_state = is_visited_state()) == -1){
303 /* Get an enabled process and insert it in the interleave set of the next state */
304 xbt_swag_foreach(process, simix_global->process_list){
305 if(MC_process_is_enabled(process)){
306 MC_state_interleave_process(next_state, process);
307 XBT_DEBUG("Process %lu enabled with simcall %d", process->pid, process->simcall.call);
311 if(_sg_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _sg_mc_checkpoint == 0)){
312 next_state->system_state = MC_take_snapshot();
315 if(dot_output != NULL)
316 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
320 if(dot_output != NULL)
321 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state, req_str);
327 xbt_fifo_unshift(mc_stack_safety, next_state);
332 /* Let's loop again */
334 /* The interleave set is empty or the maximum depth is reached, let's back-track */
337 if(xbt_fifo_size(mc_stack_safety) == _sg_mc_max_depth)
338 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
340 XBT_DEBUG("There are no more processes to interleave.");
342 /* Trash the current state, no longer needed */
344 xbt_fifo_shift(mc_stack_safety);
345 MC_state_delete(state);
348 /* Check for deadlocks */
349 if(MC_deadlock_check()){
350 MC_show_deadlock(NULL);
355 /* Traverse the stack backwards until a state with a non empty interleave
356 set is found, deleting all the states that have it empty in the way.
357 For each deleted state, check if the request that has generated it
358 (from it's predecesor state), depends on any other previous request
359 executed before it. If it does then add it to the interleave set of the
360 state that executed that previous request. */
362 while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
363 req = MC_state_get_internal_request(state);
364 xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
365 if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
366 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
367 XBT_DEBUG("Dependent Transitions:");
368 prev_req = MC_state_get_executed_request(prev_state, &value);
369 req_str = MC_request_to_string(prev_req, value);
370 XBT_DEBUG("%s (state=%p)", req_str, prev_state);
372 prev_req = MC_state_get_executed_request(state, &value);
373 req_str = MC_request_to_string(prev_req, value);
374 XBT_DEBUG("%s (state=%p)", req_str, state);
380 }else if(req->issuer == MC_state_get_internal_request(prev_state)->issuer){
382 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
387 MC_state_remove_interleave_process(prev_state, req->issuer);
388 XBT_DEBUG("Simcall %d in process %lu independant with simcall %d process %lu", req->call, req->issuer->pid, MC_state_get_internal_request(prev_state)->call, MC_state_get_internal_request(prev_state)->issuer->pid);
393 if (MC_state_interleave_size(state)) {
394 /* We found a back-tracking point, let's loop */
395 if(_sg_mc_checkpoint){
396 if(state->system_state != NULL){
397 MC_restore_snapshot(state->system_state);
398 xbt_fifo_unshift(mc_stack_safety, state);
401 pos = xbt_fifo_size(mc_stack_safety);
402 item = xbt_fifo_get_first_item(mc_stack_safety);
404 restore_state = (mc_state_t) xbt_fifo_get_item_content(item);
405 if(restore_state->system_state != NULL){
408 item = xbt_fifo_get_next_item(item);
412 MC_restore_snapshot(restore_state->system_state);
413 xbt_fifo_unshift(mc_stack_safety, state);
415 MC_replay(mc_stack_safety, pos);
418 xbt_fifo_unshift(mc_stack_safety, state);
420 MC_replay(mc_stack_safety, -1);
422 XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
425 MC_state_delete(state);
431 MC_print_statistics(mc_stats);