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);
15 static int is_visited_state(){
17 if(_sg_mc_visited == 0)
20 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
24 mc_snapshot_t new_state = NULL;
25 new_state = MC_take_snapshot();
29 if(xbt_dynar_is_empty(visited_states)){
32 xbt_dynar_push(visited_states, &new_state);
44 size_t current_chunks_used = mmalloc_get_chunks_used((xbt_mheap_t)new_state->regions[get_heap_region_index(new_state)]->data);
46 unsigned int cursor = 0, previous_cursor = 0, next_cursor = 0;
48 int end = xbt_dynar_length(visited_states) - 1;
50 mc_snapshot_t state_test = NULL;
51 size_t chunks_used_test;
54 cursor = (start + end) / 2;
55 state_test = (mc_snapshot_t)xbt_dynar_get_as(visited_states, cursor, mc_snapshot_t);
56 chunks_used_test = mmalloc_get_chunks_used((xbt_mheap_t)state_test->regions[get_heap_region_index(state_test)]->data);
57 if(chunks_used_test == current_chunks_used){
58 if(snapshot_compare(new_state, state_test, NULL, NULL) == 0){
65 /* Search another state with same number of chunks used */
66 previous_cursor = cursor - 1;
67 while(previous_cursor >= 0){
68 state_test = (mc_snapshot_t)xbt_dynar_get_as(visited_states, previous_cursor, mc_snapshot_t);
69 chunks_used_test = mmalloc_get_chunks_used((xbt_mheap_t)state_test->regions[get_heap_region_index(state_test)]->data);
70 if(chunks_used_test != current_chunks_used)
72 if(snapshot_compare(new_state, state_test, NULL, NULL) == 0){
81 next_cursor = cursor + 1;
82 while(next_cursor < xbt_dynar_length(visited_states)){
83 state_test = (mc_snapshot_t)xbt_dynar_get_as(visited_states, next_cursor, mc_snapshot_t);
84 chunks_used_test = mmalloc_get_chunks_used((xbt_mheap_t)state_test->regions[get_heap_region_index(state_test)]->data);
85 if(chunks_used_test != current_chunks_used)
87 if(snapshot_compare(new_state, state_test, NULL, NULL) == 0){
98 if(chunks_used_test < current_chunks_used)
100 if(chunks_used_test > current_chunks_used)
104 if(xbt_dynar_length(visited_states) == _sg_mc_visited){
105 mc_snapshot_t state_to_remove = NULL;
106 xbt_dynar_shift(visited_states, &state_to_remove);
107 MC_free_snapshot(state_to_remove);
110 if(chunks_used_test < current_chunks_used)
111 xbt_dynar_insert_at(visited_states, cursor + 1, &new_state);
113 xbt_dynar_insert_at(visited_states, cursor, &new_state);
126 * \brief Initialize the DPOR exploration algorithm
131 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
133 mc_state_t initial_state = NULL;
134 smx_process_t process;
136 /* Create the initial state and push it into the exploration stack */
139 initial_state = MC_state_new();
140 visited_states = xbt_dynar_new(sizeof(mc_snapshot_t), NULL);
144 XBT_DEBUG("**************************************************");
145 XBT_DEBUG("Initial state");
147 /* Wait for requests (schedules processes) */
148 MC_wait_for_requests();
152 /* Get an enabled process and insert it in the interleave set of the initial state */
153 xbt_swag_foreach(process, simix_global->process_list){
154 if(MC_process_is_enabled(process)){
155 MC_state_interleave_process(initial_state, process);
156 XBT_DEBUG("Process %lu enabled with simcall %d", process->pid, process->simcall.call);
160 xbt_fifo_unshift(mc_stack_safety, initial_state);
173 * \brief Perform the model-checking operation using a depth-first search exploration
174 * with Dynamic Partial Order Reductions
181 smx_simcall_t req = NULL, prev_req = NULL;
182 s_smx_simcall_t req2;
183 mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restore_state=NULL;
184 smx_process_t process = NULL;
185 xbt_fifo_item_t item = NULL;
187 int interleave_proc[simix_process_maxpid];
189 while (xbt_fifo_size(mc_stack_safety) > 0) {
191 /* Get current state */
193 xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety));
195 XBT_DEBUG("**************************************************");
196 XBT_DEBUG("Exploration depth=%d (state=%p)(%u interleave)",
197 xbt_fifo_size(mc_stack_safety), state,
198 MC_state_interleave_size(state));
200 /* Update statistics */
201 mc_stats->visited_states++;
203 /* If there are processes to interleave and the maximum depth has not been reached
204 then perform one step of the exploration algorithm */
205 if (xbt_fifo_size(mc_stack_safety) < _sg_mc_max_depth &&
206 (req = MC_state_get_request(state, &value))) {
208 /* Debug information */
209 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
210 req_str = MC_request_to_string(req, value);
211 XBT_DEBUG("Execute: %s", req_str);
215 MC_state_set_executed_request(state, req, value);
216 mc_stats->executed_transitions++;
218 /* Answer the request */
219 SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
221 /* Wait for requests (schedules processes) */
222 MC_wait_for_requests();
224 /* Create the new expanded state */
227 next_state = MC_state_new();
229 if(!is_visited_state()){
231 /* Get an enabled process and insert it in the interleave set of the next state */
232 xbt_swag_foreach(process, simix_global->process_list){
233 if(MC_process_is_enabled(process)){
234 MC_state_interleave_process(next_state, process);
235 XBT_DEBUG("Process %lu enabled with simcall %d", process->pid, process->simcall.call);
239 if(_sg_mc_checkpoint && ((xbt_fifo_size(mc_stack_safety) + 1) % _sg_mc_checkpoint == 0)){
240 next_state->system_state = MC_take_snapshot();
245 XBT_DEBUG("State already visited !");
249 xbt_fifo_unshift(mc_stack_safety, next_state);
252 /* Let's loop again */
254 /* The interleave set is empty or the maximum depth is reached, let's back-track */
257 if(xbt_fifo_size(mc_stack_safety) == _sg_mc_max_depth)
258 XBT_WARN("/!\\ Max depth reached ! /!\\ ");
260 XBT_DEBUG("There are no more processes to interleave.");
262 /* Trash the current state, no longer needed */
264 xbt_fifo_shift(mc_stack_safety);
265 MC_state_delete(state);
268 /* Check for deadlocks */
269 if(MC_deadlock_check()){
270 MC_show_deadlock(NULL);
275 /* Traverse the stack backwards until a state with a non empty interleave
276 set is found, deleting all the states that have it empty in the way.
277 For each deleted state, check if the request that has generated it
278 (from it's predecesor state), depends on any other previous request
279 executed before it. If it does then add it to the interleave set of the
280 state that executed that previous request. */
282 while ((state = xbt_fifo_shift(mc_stack_safety)) != NULL) {
283 req = MC_state_get_internal_request(state);
284 xbt_fifo_foreach(mc_stack_safety, item, prev_state, mc_state_t) {
285 if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
286 if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
287 XBT_DEBUG("Dependent Transitions:");
288 prev_req = MC_state_get_executed_request(prev_state, &value);
289 req_str = MC_request_to_string(prev_req, value);
290 XBT_DEBUG("%s (state=%p)", req_str, prev_state);
292 prev_req = MC_state_get_executed_request(state, &value);
293 req_str = MC_request_to_string(prev_req, value);
294 XBT_DEBUG("%s (state=%p)", req_str, state);
300 }else if(req->issuer == MC_state_get_internal_request(prev_state)->issuer){
302 XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
307 MC_state_remove_interleave_process(prev_state, req->issuer);
308 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);
313 if (MC_state_interleave_size(state)) {
314 /* We found a back-tracking point, let's loop */
315 if(_sg_mc_checkpoint){
316 if(state->system_state != NULL){
317 MC_restore_snapshot(state->system_state);
318 xbt_fifo_unshift(mc_stack_safety, state);
321 pos = xbt_fifo_size(mc_stack_safety);
322 item = xbt_fifo_get_first_item(mc_stack_safety);
324 restore_state = (mc_state_t) xbt_fifo_get_item_content(item);
325 if(restore_state->system_state != NULL){
328 item = xbt_fifo_get_next_item(item);
332 MC_restore_snapshot(restore_state->system_state);
333 xbt_fifo_unshift(mc_stack_safety, state);
335 MC_replay(mc_stack_safety, pos);
338 xbt_fifo_unshift(mc_stack_safety, state);
340 MC_replay(mc_stack_safety, -1);
345 for(i=0; i<simix_process_maxpid; i++)
346 interleave_proc[i] = 0;
348 while((i < MC_state_interleave_size(state))){
350 prev_req = MC_state_get_request(state, &value);
351 if(prev_req != NULL){
352 MC_state_set_executed_request(state, prev_req, value);
353 prev_req = MC_state_get_internal_request(state);
354 if(MC_request_depend(&req2, prev_req)){
355 XBT_DEBUG("Simcall %d in process %lu dependant with simcall %d in process %lu", req2.call, req2.issuer->pid, prev_req->call, prev_req->issuer->pid);
356 interleave_proc[prev_req->issuer->pid] = 1;
358 XBT_DEBUG("Simcall %d in process %lu independant with simcall %d in process %lu", req2.call, req2.issuer->pid, prev_req->call, prev_req->issuer->pid);
359 MC_state_remove_interleave_process(state, prev_req->issuer);
363 xbt_swag_foreach(process, simix_global->process_list){
364 if(interleave_proc[process->pid] == 1)
365 MC_state_interleave_process(state, process);
367 XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
371 MC_state_delete(state);
377 MC_print_statistics(mc_stats);