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_chunks_used = new_state->system_state->heap_chunks_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 chunks_used_test;
68 int same_chunks_not_found = 1;
70 while(start <= end && same_chunks_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 chunks_used_test = state_test->system_state->heap_chunks_used;
74 if(chunks_used_test < current_chunks_used)
76 if(chunks_used_test > current_chunks_used)
78 if(chunks_used_test == current_chunks_used){
79 same_chunks_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);
89 /* Search another state with same number of chunks used */
90 previous_cursor = cursor - 1;
91 while(previous_cursor >= 0){
92 state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, previous_cursor, mc_safety_visited_state_t);
93 chunks_used_test = state_test->system_state->heap_chunks_used;
94 if(chunks_used_test != current_chunks_used)
96 if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){
97 xbt_dynar_remove_at(visited_states, previous_cursor, NULL);
98 xbt_dynar_insert_at(visited_states, previous_cursor, &new_state);
107 next_cursor = cursor + 1;
108 while(next_cursor < xbt_dynar_length(visited_states)){
109 state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, next_cursor, mc_safety_visited_state_t);
110 chunks_used_test = state_test->system_state->heap_chunks_used;
111 if(chunks_used_test != current_chunks_used)
113 if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){
114 xbt_dynar_remove_at(visited_states, next_cursor, NULL);
115 xbt_dynar_insert_at(visited_states, next_cursor, &new_state);
128 state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_safety_visited_state_t);
129 chunks_used_test = state_test->system_state->heap_chunks_used;
131 if(chunks_used_test < current_chunks_used)
132 xbt_dynar_insert_at(visited_states, cursor + 1, &new_state);
134 xbt_dynar_insert_at(visited_states, cursor, &new_state);
136 if(xbt_dynar_length(visited_states) > _sg_mc_visited){
137 int min = mc_stats->expanded_states;
138 unsigned int cursor2 = 0;
139 unsigned int index = 0;
140 xbt_dynar_foreach(visited_states, cursor2, state_test){
141 if(state_test->num < min){
143 min = state_test->num;
146 xbt_dynar_remove_at(visited_states, index, NULL);
160 * \brief Initialize the DPOR exploration algorithm
165 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
167 mc_state_t initial_state = NULL;
168 smx_process_t process;
170 /* Create the initial state and push it into the exploration stack */
173 initial_state = MC_state_new();
174 visited_states = xbt_dynar_new(sizeof(mc_safety_visited_state_t), visited_state_free_voidp);
178 XBT_DEBUG("**************************************************");
179 XBT_DEBUG("Initial state");
181 /* Wait for requests (schedules processes) */
182 MC_wait_for_requests();
186 /* Get an enabled process and insert it in the interleave set of the initial state */
187 xbt_swag_foreach(process, simix_global->process_list){
188 if(MC_process_is_enabled(process)){
189 MC_state_interleave_process(initial_state, process);
190 XBT_DEBUG("Process %lu enabled with simcall %d", process->pid, process->simcall.call);
194 xbt_fifo_unshift(mc_stack_safety, initial_state);
207 * \brief Perform the model-checking operation using a depth-first search exploration
208 * with Dynamic Partial Order Reductions
215 smx_simcall_t req = NULL, prev_req = NULL, req2 = NULL;
216 s_smx_simcall_t req3;
217 mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restore_state=NULL;
218 smx_process_t process = NULL;
219 xbt_fifo_item_t item = NULL;
220 int pos, i, interleave_size;
221 int interleave_proc[simix_process_maxpid];
223 while (xbt_fifo_size(mc_stack_safety) > 0) {
225 /* Get current state */
227 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
229 XBT_DEBUG("**************************************************");
230 XBT_DEBUG("Exploration depth=%d (state=%p)(%u interleave)",
231 xbt_fifo_size(mc_stack_safety), state,
232 MC_state_interleave_size(state));
234 /* Update statistics */
235 mc_stats->visited_states++;
237 /* If there are processes to interleave and the maximum depth has not been reached
238 then perform one step of the exploration algorithm */
239 if (xbt_fifo_size(mc_stack_safety) < _sg_mc_max_depth &&
240 (req = MC_state_get_request(state, &value))) {
242 /* Debug information */
243 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
244 req_str = MC_request_to_string(req, value);
245 XBT_DEBUG("Execute: %s", req_str);
249 MC_state_set_executed_request(state, req, value);
250 mc_stats->executed_transitions++;
252 if(MC_state_interleave_size(state)){
254 req2 = MC_state_get_internal_request(state);
256 for(i=0; i<simix_process_maxpid; i++)
257 interleave_proc[i] = 0;
259 interleave_size = MC_state_interleave_size(state);
260 while(i < interleave_size){
262 prev_req = MC_state_get_request(state, &value2);
263 if(prev_req != NULL){
264 MC_state_set_executed_request(state, prev_req, value2);
265 prev_req = MC_state_get_internal_request(state);
266 if(MC_request_depend(&req3, prev_req)){
267 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);
268 interleave_proc[prev_req->issuer->pid] = 1;
270 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);
271 MC_state_remove_interleave_process(state, prev_req->issuer);
275 xbt_swag_foreach(process, simix_global->process_list){
276 if(interleave_proc[process->pid] == 1)
277 MC_state_interleave_process(state, process);
282 MC_state_set_executed_request(state, req, value);
284 /* Answer the request */
285 SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
287 /* Wait for requests (schedules processes) */
288 MC_wait_for_requests();
290 /* Create the new expanded state */
293 next_state = MC_state_new();
295 if(!is_visited_state()){
297 /* Get an enabled process and insert it in the interleave set of the next state */
298 xbt_swag_foreach(process, simix_global->process_list){
299 if(MC_process_is_enabled(process)){
300 MC_state_interleave_process(next_state, process);
301 XBT_DEBUG("Process %lu enabled with simcall %d", process->pid, process->simcall.call);
305 if(_sg_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _sg_mc_checkpoint == 0)){
306 next_state->system_state = MC_take_snapshot();
311 XBT_DEBUG("State already visited !");
315 xbt_fifo_unshift(mc_stack_safety, next_state);
318 /* Let's loop again */
320 /* The interleave set is empty or the maximum depth is reached, let's back-track */
323 if(xbt_fifo_size(mc_stack_safety) == _sg_mc_max_depth)
324 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
326 XBT_DEBUG("There are no more processes to interleave.");
328 /* Trash the current state, no longer needed */
330 xbt_fifo_shift(mc_stack_safety);
331 MC_state_delete(state);
334 /* Check for deadlocks */
335 if(MC_deadlock_check()){
336 MC_show_deadlock(NULL);
341 /* Traverse the stack backwards until a state with a non empty interleave
342 set is found, deleting all the states that have it empty in the way.
343 For each deleted state, check if the request that has generated it
344 (from it's predecesor state), depends on any other previous request
345 executed before it. If it does then add it to the interleave set of the
346 state that executed that previous request. */
348 while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
349 req = MC_state_get_internal_request(state);
350 xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
351 if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
352 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
353 XBT_DEBUG("Dependent Transitions:");
354 prev_req = MC_state_get_executed_request(prev_state, &value);
355 req_str = MC_request_to_string(prev_req, value);
356 XBT_DEBUG("%s (state=%p)", req_str, prev_state);
358 prev_req = MC_state_get_executed_request(state, &value);
359 req_str = MC_request_to_string(prev_req, value);
360 XBT_DEBUG("%s (state=%p)", req_str, state);
366 }else if(req->issuer == MC_state_get_internal_request(prev_state)->issuer){
368 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
373 MC_state_remove_interleave_process(prev_state, req->issuer);
374 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);
379 if (MC_state_interleave_size(state)) {
380 /* We found a back-tracking point, let's loop */
381 if(_sg_mc_checkpoint){
382 if(state->system_state != NULL){
383 MC_restore_snapshot(state->system_state);
384 xbt_fifo_unshift(mc_stack_safety, state);
387 pos = xbt_fifo_size(mc_stack_safety);
388 item = xbt_fifo_get_first_item(mc_stack_safety);
390 restore_state = (mc_state_t) xbt_fifo_get_item_content(item);
391 if(restore_state->system_state != NULL){
394 item = xbt_fifo_get_next_item(item);
398 MC_restore_snapshot(restore_state->system_state);
399 xbt_fifo_unshift(mc_stack_safety, state);
401 MC_replay(mc_stack_safety, pos);
404 xbt_fifo_unshift(mc_stack_safety, state);
406 MC_replay(mc_stack_safety, -1);
408 XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
411 MC_state_delete(state);
417 MC_print_statistics(mc_stats);