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
Add MC support for processes with multiple enabled transitions per state
[simgrid.git]
/
src
/
mc
/
mc_dpor.c
diff --git
a/src/mc/mc_dpor.c
b/src/mc/mc_dpor.c
index
9c84b30
..
364584e
100644
(file)
--- a/
src/mc/mc_dpor.c
+++ b/
src/mc/mc_dpor.c
@@
-16,7
+16,6
@@
void MC_dpor_init()
{
mc_state_t initial_state = NULL;
mc_transition_t trans = NULL;
- xbt_setset_cursor_t cursor = NULL;
/* Create the initial state and push it into the exploration stack */
MC_SET_RAW_MEM;
@@
-30,13
+29,8
@@
void MC_dpor_init()
MC_schedule_enabled_processes();
MC_SET_RAW_MEM;
- xbt_setset_add(initial_state->enabled_transitions, initial_state->transitions);
- xbt_setset_foreach(initial_state->enabled_transitions, cursor, trans){
- if(trans->type == mc_wait
- && (trans->comm->src_proc == NULL || trans->comm->dst_proc == NULL)){
- xbt_setset_set_remove(initial_state->enabled_transitions, trans);
- }
- }
+ MC_trans_compute_enabled(initial_state->enabled_transitions,
+ initial_state->transitions);
/* Fill the interleave set of the initial state with an enabled process */
trans = xbt_setset_set_choose(initial_state->enabled_transitions);
@@
-55,7
+49,7
@@
void MC_dpor_init()
*/
void MC_dpor(void)
{
- mc_transition_t trans = NULL;
+ mc_transition_t trans
, trans_tmp
= NULL;
mc_state_t next_state = NULL;
xbt_setset_cursor_t cursor = NULL;
@@
-90,7
+84,7
@@
void MC_dpor(void)
exploration stack. */
MC_SET_RAW_MEM;
trans = xbt_setset_set_choose(mc_current_state->interleave);
- if(
!trans->type =
= mc_random){
+ if(
trans->type !
= mc_random){
xbt_setset_set_remove(mc_current_state->interleave, trans);
/* Add the transition in the done set of the current state */
xbt_setset_set_insert(mc_current_state->done, trans);
@@
-111,34
+105,36
@@
void MC_dpor(void)
MC_execute_surf_actions(); /* Do surf's related black magic */
MC_schedule_enabled_processes();
- if(trans->type == mc_random && trans->
current_value < trans->max
){
- trans->current_value++;
+ if(trans->type == mc_random && trans->
random.current_value < trans->random.max
){
+ trans->
random.
current_value++;
}else{
-
trans->current_value = trans->
min;
+
//trans->random.current_value = trans->random.
min;
xbt_setset_set_remove(mc_current_state->interleave, trans);
xbt_setset_set_insert(mc_current_state->done, trans);
}
- /* Calculate the enabled transitions set of the next state:
- -add the transition sets of the current state and the next state
- -remove the executed transition from that set
- -remove all the transitions that are disabled (mc_wait only)
- -use the resulting set as the enabled transitions of the next state */
+ /* Calculate the enabled transitions set of the next state */
MC_SET_RAW_MEM;
- xbt_setset_add(next_state->transitions, mc_current_state->transitions);
- xbt_setset_set_remove(next_state->transitions, trans);
- xbt_setset_add(next_state->enabled_transitions, next_state->transitions);
- xbt_setset_foreach(next_state->enabled_transitions, cursor, trans){
- if(trans->type == mc_wait
- && (trans->comm->src_proc == NULL || trans->comm->dst_proc == NULL)){
- xbt_setset_set_remove(next_state->enabled_transitions, trans);
+
+ xbt_setset_foreach(mc_current_state->transitions, cursor, trans_tmp){
+ DEBUG1("Checking transition %s", trans_tmp->name);
+ if(trans_tmp->process != trans->process){
+ DEBUG2("Inherit transition %p (%lu)", trans_tmp, trans_tmp->ID);
+ xbt_setset_set_insert(next_state->transitions, trans_tmp);
}
}
-
+
+ MC_trans_compute_enabled(next_state->enabled_transitions, next_state->transitions);
+
/* Choose one transition to interleave from the enabled transition set */
trans = xbt_setset_set_choose(next_state->enabled_transitions);
- if(trans)
- xbt_setset_set_insert(next_state->interleave, trans);
+ if(trans){
+ DEBUG1("Choosing transition %p", trans);
+ xbt_setset_foreach(next_state->enabled_transitions, cursor, trans_tmp){
+ if(trans_tmp->process == trans->process)
+ xbt_setset_set_insert(next_state->interleave, trans_tmp);
+ }
+ }
MC_UNSET_RAW_MEM;
/* Update Statistics */
@@
-157,8
+153,14
@@
void MC_dpor(void)
INFO0("**************************");
INFO0("*** DEAD-LOCK DETECTED ***");
INFO0("**************************");
+ INFO0("Locked transitions:");
+ xbt_setset_foreach(mc_current_state->transitions, cursor, trans){
+ INFO1("%s", trans->name);
+ }
+
INFO0("Counter-example execution trace:");
MC_dump_stack(mc_stack);
+
MC_print_statistics(mc_stats);
xbt_abort();
}
@@
-184,11
+186,17
@@
void MC_dpor(void)
q = mc_current_state->executed_transition;
xbt_fifo_foreach(mc_stack, item, state, mc_state_t){
if(MC_transition_depend(q, state->executed_transition)){
- DEBUG3("Dependence found at state %p (%p,%p)", state, state->executed_transition, q);
+ DEBUG3("Dependence found at state %p (%p,%p)", state, state->executed_transition, q);
xbt_setset_foreach(state->enabled_transitions, cursor, trans){
if((trans->process == q->process) && !xbt_setset_set_belongs(state->done, trans)){
DEBUG2("Unexplored interleaving found at state %p (%p)", state, trans);
- xbt_setset_set_insert(state->interleave, trans);
+
+ xbt_setset_foreach(state->enabled_transitions, cursor, trans){
+ if(trans->process == q->process)
+ xbt_setset_set_insert(state->interleave, trans);
+ }
+ /* FIXME: hack to make it work*/
+ trans = q;
break;
}
}