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 remote-tracking branch 'origin/libdw2'
[simgrid.git]
/
src
/
mc
/
mc_global.c
diff --git
a/src/mc/mc_global.c
b/src/mc/mc_global.c
index
f35ac68
..
930098f
100644
(file)
--- a/
src/mc/mc_global.c
+++ b/
src/mc/mc_global.c
@@
-1106,6
+1106,9
@@
void MC_modelcheck_safety(void)
/* Save the initial state */
initial_state_safety = xbt_new0(s_mc_global_t, 1);
initial_state_safety->snapshot = MC_take_snapshot(0);
/* Save the initial state */
initial_state_safety = xbt_new0(s_mc_global_t, 1);
initial_state_safety->snapshot = MC_take_snapshot(0);
+ initial_state_safety->initial_communications_pattern_done = 0;
+ initial_state_safety->comm_deterministic = 1;
+ initial_state_safety->send_deterministic = 1;
MC_UNSET_RAW_MEM;
MC_dpor();
MC_UNSET_RAW_MEM;
MC_dpor();
@@
-1229,6
+1232,7
@@
void MC_replay(xbt_fifo_t stack, int start)
xbt_fifo_item_t item, start_item;
mc_state_t state;
smx_process_t process = NULL;
xbt_fifo_item_t item, start_item;
mc_state_t state;
smx_process_t process = NULL;
+ int comm_pattern = 0;
XBT_DEBUG("**** Begin Replay ****");
XBT_DEBUG("**** Begin Replay ****");
@@
-1258,6
+1262,7
@@
void MC_replay(xbt_fifo_t stack, int start)
xbt_free(key);
}
}
xbt_free(key);
}
}
+ xbt_dynar_reset(communications_pattern);
MC_UNSET_RAW_MEM;
MC_UNSET_RAW_MEM;
@@
-1287,8
+1292,22
@@
void MC_replay(xbt_fifo_t stack, int start)
xbt_free(req_str);
}
}
xbt_free(req_str);
}
}
+
+ if(req->call == SIMCALL_COMM_ISEND)
+ comm_pattern = 1;
+ else if(req->call == SIMCALL_COMM_IRECV)
+ comm_pattern = 2;
SIMIX_simcall_pre(req, value);
SIMIX_simcall_pre(req, value);
+
+ MC_SET_RAW_MEM;
+ if(comm_pattern != 0){
+ get_comm_pattern(communications_pattern, req, comm_pattern);
+ }
+ MC_UNSET_RAW_MEM;
+
+ comm_pattern = 0;
+
MC_wait_for_requests();
count++;
MC_wait_for_requests();
count++;
@@
-1569,6
+1588,10
@@
void MC_print_statistics(mc_stats_t stats)
fprintf(dot_output, "}\n");
fclose(dot_output);
}
fprintf(dot_output, "}\n");
fclose(dot_output);
}
+ if(initial_state_safety != NULL){
+ XBT_INFO("Communication-deterministic : %s", !initial_state_safety->comm_deterministic ? "No" : "Yes");
+ XBT_INFO("Send-deterministic : %s", !initial_state_safety->send_deterministic ? "No" : "Yes");
+ }
MC_UNSET_RAW_MEM;
}
MC_UNSET_RAW_MEM;
}