src/mc/mc_base.h
src/mc/mc_record.c
src/mc/mc_config.c
+ src/mc/mc_global.c
)
set(MC_SRC
src/mc/mc_dwarf_attrnames.h
src/mc/mc_dwarf_expression.c
src/mc/mc_dwarf_tagnames.h
- src/mc/mc_global.c
src/mc/mc_hash.c
src/mc/mc_ignore.c
src/mc/mc_interface.h
{
/* Reduce the run size for the MC */
- if(MC_is_active()){
+ if(MC_is_active() || MC_record_replay_is_active()){
periodic_stabilize_delay = 8;
periodic_fix_fingers_delay = 8;
periodic_check_predecessor_delay = 8;
// no task was received: make some periodic calls
- if(MC_is_active()){
- if(!MC_visited_reduction() && no_op){
+ if(MC_is_active() || MC_record_replay_is_active()){
+ if(MC_is_active() && !MC_visited_reduction() && no_op){
MC_cut();
}
if(listen == 0 && (sub_protocol = MC_random(0, 4)) > 0){
/* This program is free software; you can redistribute it and/or modify it
* under the terms of the license (GNU LGPL) which comes with this package. */
+#include <stdbool.h>
+
#include <simgrid_config.h> /* HAVE_MC ? */
#include <xbt.h>
#include "xbt/automaton.h"
#endif
+/** Replay path (if any) in string representation
+ *
+ * This is a path as generated by `MC_record_stack_to_string()`.
+ */
+extern char* MC_record_path;
+
+/** Whether the replay mode is enabled */
+static inline bool MC_record_replay_is_active(void) {
+ return MC_record_path;
+}
+
SG_END_DECL()
#endif /* SIMGRID_MODELCHECKER_H */
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
"Logging specific to MC (global)");
+double *mc_time = NULL;
+
+#ifdef HAVE_MC
int user_max_depth_reached = 0;
/* MC global data structures */
mc_state_t mc_current_state = NULL;
char mc_replay_mode = FALSE;
-double *mc_time = NULL;
+
__thread mc_comparison_times_t mc_comp_times = NULL;
__thread double mc_snapshot_comparison_time;
mc_stats_t mc_stats = NULL;
mc_time[process->pid] += amount;
}
-double MC_process_clock_get(smx_process_t process)
-{
- if (mc_time) {
- if (process != NULL)
- return mc_time[process->pid];
- else
- return -1;
- } else {
- return 0;
- }
-}
-
void MC_automaton_load(const char *file)
{
if (raw_mem_set)
MC_SET_MC_HEAP;
}
+#endif
+
+double MC_process_clock_get(smx_process_t process)
+{
+ if (mc_time) {
+ if (process != NULL)
+ return mc_time[process->pid];
+ else
+ return -1;
+ } else {
+ return 0;
+ }
+}
MC_record_replay(start, xbt_dynar_length(path));
xbt_dynar_free(&path);
}
+
+void MC_record_replay_init()
+{
+ mc_time = xbt_new0(double, simix_process_maxpid);
+}
#include <stdbool.h>
#include "simgrid_config.h"
-#include "mc_record.h"
SG_BEGIN_DECL()
-/** Replay path (if any) in string representation
- *
- * This is a path as generated by `MC_record_stack_to_string()`.
- */
-extern char* MC_record_path;
-
/** Whether the MC record mode is enabled
*
* The behaviour is not changed. The only real difference is that
*/
#define MC_record_is_active() _sg_do_model_check_record
-/** Whether the replay mode is enabled */
-static inline bool MC_record_replay_is_active(void) {
- return MC_record_path;
-}
-
// **** Data conversion
/** An element in the recorded path
*/
void MC_record_replay_from_string(const char* data);
+void MC_record_replay_init(void);
+
SG_END_DECL()
#endif
xbt_assert(rdv, "No rendez-vous point defined for send");
- if (MC_is_active()) {
+ if (MC_is_active() || MC_record_replay_is_active()) {
/* the model-checker wants two separate simcalls */
smx_synchro_t comm = NULL; /* MC needs the comm to be set to NULL during the simcall */
comm = simcall_comm_isend(src, rdv, task_size, rate,
xbt_assert(isfinite(timeout), "timeout is not finite!");
xbt_assert(rdv, "No rendez-vous point defined for recv");
- if (MC_is_active()) {
+ if (MC_is_active() || MC_record_replay_is_active()) {
/* the model-checker wants two separate simcalls */
smx_synchro_t comm = NULL; /* MC needs the comm to be set to NULL during the simcall */
comm = simcall_comm_irecv(rdv, dst_buff, dst_buff_size,
*/
XBT_INLINE double SIMIX_get_clock(void)
{
- if(MC_is_active()){
+ if(MC_is_active() || MC_record_replay_is_active()){
return MC_process_clock_get(SIMIX_process_self());
}else{
return surf_get_clock();
void SIMIX_run(void)
{
if(MC_record_path) {
+ MC_record_replay_init();
MC_record_replay_from_string(MC_record_path);
return;
}
#endif
/* set surf's action */
- if (!MC_is_active()) {
+ if (!MC_is_active() && !MC_record_replay_is_active()) {
synchro->execution.surf_exec = surf_workstation_execute(host, computation_amount);
surf_action_set_data(synchro->execution.surf_exec, synchro);
}
/* set surf's synchro */
- if (!MC_is_active()) {
+ if (!MC_is_active() && !MC_record_replay_is_active()) {
synchro->execution.surf_exec =
surf_workstation_model_execute_parallel_task((surf_workstation_model_t)surf_workstation_model,
host_nb, workstation_list, computation_amount, communication_amount, rate);
simcall->issuer->waiting_synchro = synchro;
/* set surf's synchro */
- if (MC_is_active()) {
+ if (MC_is_active() || MC_record_replay_is_active()) {
synchro->state = SIMIX_DONE;
SIMIX_execution_finish(synchro);
return;
other_synchro->comm.copy_data_fun = copy_data_fun;
- if (MC_is_active()) {
+ if (MC_is_active() || MC_record_replay_is_active()) {
other_synchro->state = SIMIX_RUNNING;
return (detached ? NULL : other_synchro);
}
SIMIX_comm_copy_data(other_synchro);*/
- if (MC_is_active()) {
+ if (MC_is_active() || MC_record_replay_is_active()) {
other_synchro->state = SIMIX_RUNNING;
return other_synchro;
}
xbt_fifo_push(synchro->simcalls, simcall);
simcall->issuer->waiting_synchro = synchro;
- if (MC_is_active()) {
+ if (MC_is_active() || MC_record_replay_is_active()) {
int idx = SIMCALL_GET_MC_VALUE(simcall);
if (idx == 0) {
synchro->state = SIMIX_DONE;
void simcall_HANDLER_comm_test(smx_simcall_t simcall, smx_synchro_t synchro)
{
- if(MC_is_active()){
+ if(MC_is_active() || MC_record_replay_is_active()){
simcall_comm_test__set__result(simcall, synchro->comm.src_proc && synchro->comm.dst_proc);
if(simcall_comm_test__get__result(simcall)){
synchro->state = SIMIX_DONE;
smx_synchro_t synchro;
simcall_comm_testany__set__result(simcall, -1);
- if (MC_is_active()){
+ if (MC_is_active() || MC_record_replay_is_active()){
int idx = SIMCALL_GET_MC_VALUE(simcall);
if(idx == -1){
SIMIX_simcall_answer(simcall);
smx_synchro_t synchro;
unsigned int cursor = 0;
- if (MC_is_active()){
+ if (MC_is_active() || MC_record_replay_is_active()){
int idx = SIMCALL_GET_MC_VALUE(simcall);
synchro = xbt_dynar_get_as(synchros, idx, smx_synchro_t);
xbt_fifo_push(synchro->simcalls, simcall);
continue; // if process handling comm is killed
if (simcall->call == SIMCALL_COMM_WAITANY) {
SIMIX_waitany_remove_simcall_from_actions(simcall);
- if (!MC_is_active())
+ if (!MC_is_active() && !MC_record_replay_is_active())
simcall_comm_waitany__set__result(simcall, xbt_dynar_search(simcall_comm_waitany__get__comms(simcall), &synchro));
}
synchro->state = SIMIX_CANCELED;
}
else if (!MC_is_active() /* when running the MC there are no surf actions */
+ && !MC_record_replay_is_active()
&& (synchro->state == SIMIX_READY || synchro->state == SIMIX_RUNNING)) {
surf_action_cancel(synchro->comm.surf_comm);
void simcall_HANDLER_process_sleep(smx_simcall_t simcall, double duration)
{
- if (MC_is_active()) {
+ if (MC_is_active() || MC_record_replay_is_active()) {
MC_process_clock_add(simcall->issuer, duration);
simcall_process_sleep__set__result(simcall, SIMIX_DONE);
SIMIX_simcall_answer(simcall);
if ((*request)->action != NULL) { // this is not a detached send
simcall_comm_wait((*request)->action, -1.0);
-#ifdef HAVE_MC
- if(MC_is_active() && (*request)->action)
+
+ if((MC_is_active() || MC_record_replay_is_active()) && (*request)->action)
(*request)->action->comm.dst_data = NULL; // dangling pointer : dst_data is freed with a wait, need to set it to NULL for system state comparison
-#endif
}
finish_wait(request, status);
}
for(c = 0; c < count; c++) {
- if (MC_is_active()) {
+ if (MC_is_active() || MC_record_replay_is_active()) {
smpi_mpi_wait(&requests[c], pstat);
index = c;
} else {
xbt_free(tmpbufs);
xbt_free(requests);
}
-
{
smpi_switch_data_segment(smpi_process_index());
- if(MC_is_active())
+ if (MC_is_active() || MC_record_replay_is_active())
return;
xbt_os_threadtimer_start(smpi_process_timer());
void smpi_bench_end(void)
{
- if(MC_is_active())
+ if (MC_is_active() || MC_record_replay_is_active())
return;
xbt_os_timer_t timer = smpi_process_timer();
{
// This leads to an explosion of the search graph
// which cannot be reduced:
- if(MC_is_active())
+ if(MC_is_active() || MC_record_is_active())
return;
int index = smpi_process_index();