A
lgorithmique
N
umérique
D
istribuée
Public GIT Repository
projects
/
simgrid.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
| inline |
side by side
Merge branch 'master' of git+ssh://scm.gforge.inria.fr//gitroot/simgrid/simgrid
[simgrid.git]
/
src
/
mc
/
mc_global.c
diff --git
a/src/mc/mc_global.c
b/src/mc/mc_global.c
index
970ef80
..
562eb37
100644
(file)
--- a/
src/mc/mc_global.c
+++ b/
src/mc/mc_global.c
@@
-406,11
+406,12
@@
void MC_replay(xbt_fifo_t stack, int start)
{
int raw_mem = (mmalloc_get_current_heap() == raw_heap);
- int value, i = 1;
+ int value, i = 1
, count = 1
;
char *req_str;
smx_simcall_t req = NULL, saved_req = NULL;
xbt_fifo_item_t item, start_item;
mc_state_t state;
+ smx_process_t process = NULL;
XBT_DEBUG("**** Begin Replay ****");
@@
-430,6
+431,19
@@
void MC_replay(xbt_fifo_t stack, int start)
}
}
+ MC_SET_RAW_MEM;
+ xbt_dict_reset(first_enabled_state);
+ xbt_swag_foreach(process, simix_global->process_list){
+ if(MC_process_is_enabled(process)){
+ char *key = bprintf("%lu", process->pid);
+ char *data = bprintf("%d", count);
+ xbt_dict_set(first_enabled_state, key, data, NULL);
+ xbt_free(key);
+ }
+ }
+ MC_UNSET_RAW_MEM;
+
+
/* Traverse the stack from the state at position start and re-execute the transitions */
for (item = start_item;
item != xbt_fifo_get_first_item(stack);
@@
-438,6
+452,12
@@
void MC_replay(xbt_fifo_t stack, int start)
state = (mc_state_t) xbt_fifo_get_item_content(item);
saved_req = MC_state_get_executed_request(state, &value);
+ MC_SET_RAW_MEM;
+ char *key = bprintf("%lu", saved_req->issuer->pid);
+ xbt_dict_remove(first_enabled_state, key);
+ xbt_free(key);
+ MC_UNSET_RAW_MEM;
+
if(saved_req){
/* because we got a copy of the executed request, we have to fetch the
real one, pointed by the request field of the issuer process */
@@
-450,14
+470,32
@@
void MC_replay(xbt_fifo_t stack, int start)
xbt_free(req_str);
}
}
-
+
SIMIX_simcall_pre(req, value);
MC_wait_for_requests();
+
+ count++;
+
+ MC_SET_RAW_MEM;
+ /* Insert in dict all enabled processes */
+ xbt_swag_foreach(process, simix_global->process_list){
+ if(MC_process_is_enabled(process) /*&& !MC_state_process_is_done(state, process)*/){
+ char *key = bprintf("%lu", process->pid);
+ if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
+ char *data = bprintf("%d", count);
+ xbt_dict_set(first_enabled_state, key, data, NULL);
+ }
+ xbt_free(key);
+ }
+ }
+ MC_UNSET_RAW_MEM;
/* Update statistics */
mc_stats->visited_states++;
mc_stats->executed_transitions++;
+
}
+
XBT_DEBUG("**** End Replay ****");
if(raw_mem)
@@
-527,7
+565,7
@@
void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
depth++;
/* Update statistics */
- mc_stats->visited_
state
s++;
+ mc_stats->visited_
pair
s++;
mc_stats->executed_transitions++;
item = xbt_fifo_get_prev_item(item);
@@
-570,7
+608,7
@@
void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
depth++;
/* Update statistics */
- mc_stats->visited_
state
s++;
+ mc_stats->visited_
pair
s++;
mc_stats->executed_transitions++;
}
}
@@
-692,14
+730,14
@@
void MC_dump_stack_liveness(xbt_fifo_t stack){
void MC_print_statistics(mc_stats_t stats)
{
- //XBT_INFO("State space size ~= %lu", stats->state_size);
- XBT_INFO("Expanded states = %lu", stats->expanded_states);
- XBT_INFO("Visited states = %lu", stats->visited_states);
+ if(stats->expanded_pairs == 0){
+ XBT_INFO("Expanded states = %lu", stats->expanded_states);
+ XBT_INFO("Visited states = %lu", stats->visited_states);
+ }else{
+ XBT_INFO("Expanded pairs = %lu", stats->expanded_pairs);
+ XBT_INFO("Visited pairs = %lu", stats->visited_pairs);
+ }
XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
- XBT_INFO("Expanded / Visited = %lf",
- (double) stats->visited_states / stats->expanded_states);
- /*XBT_INFO("Exploration coverage = %lf",
- (double)stats->expanded_states / stats->state_size); */
}
void MC_assert(int prop)
@@
-821,7
+859,7
@@
void MC_ignore_heap(void *address, size_t size){
}
unsigned int cursor = 0;
- mc_heap_ignore_region_t current_region;
+ mc_heap_ignore_region_t current_region
= NULL
;
int start = 0;
int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;