This fixes #14976 (thanks to LucasN for the report)
17 files changed:
int node(int argc, char *argv[])
{
/* Reduce the run size for the MC */
int node(int argc, char *argv[])
{
/* Reduce the run size for the MC */
periodic_stabilize_delay = 8;
periodic_fix_fingers_delay = 8;
periodic_check_predecessor_delay = 8;
periodic_stabilize_delay = 8;
periodic_fix_fingers_delay = 8;
periodic_check_predecessor_delay = 8;
XBT_DEBUG("Received a task (%p)", task_received);
task_data_t ans_data = MSG_task_get_data(task_received);
XBT_DEBUG("Received a task (%p)", task_received);
task_data_t ans_data = MSG_task_get_data(task_received);
// the model-checker is expected to find a counter-example here.
//
// As you can see in the test right below, task_received is not always equal to task_sent
// the model-checker is expected to find a counter-example here.
//
// As you can see in the test right below, task_received is not always equal to task_sent
msg_task_t task_received = MSG_comm_get_task(node->comm_receive);
task_data_t ans_data = MSG_task_get_data(task_received);
msg_task_t task_received = MSG_comm_get_task(node->comm_receive);
task_data_t ans_data = MSG_task_get_data(task_received);
MC_assert(task_received == task_sent);
}
MC_assert(task_received == task_sent);
}
int node(int argc, char *argv[])
{
/* Reduce the run size for the MC */
int node(int argc, char *argv[])
{
/* Reduce the run size for the MC */
periodic_stabilize_delay = 8;
periodic_fix_fingers_delay = 8;
periodic_check_predecessor_delay = 8;
periodic_stabilize_delay = 8;
periodic_fix_fingers_delay = 8;
periodic_check_predecessor_delay = 8;
XBT_DEBUG("Received a task (%p)", task_received);
task_data_t ans_data = MSG_task_get_data(task_received);
XBT_DEBUG("Received a task (%p)", task_received);
task_data_t ans_data = MSG_task_get_data(task_received);
MC_assert(task_received == task_sent);
}
MC_assert(task_received == task_sent);
}
msg_task_t task_received = MSG_comm_get_task(node->comm_receive);
task_data_t ans_data = MSG_task_get_data(task_received);
msg_task_t task_received = MSG_comm_get_task(node->comm_receive);
task_data_t ans_data = MSG_task_get_data(task_received);
MC_assert(task_received == task_sent);
}
MC_assert(task_received == task_sent);
}
-extern int _surf_do_model_check;
-#define MC_IS_ENABLED _surf_do_model_check
+extern int _surf_do_model_check; /* please don't use directly: we inline MC_is_active, but that's what you should use */
+
+static int MC_is_active(void) {
+ return _surf_do_model_check;
+}
XBT_PUBLIC(void) MC_assert(int);
XBT_PUBLIC(int) MC_random(int min, int max);
XBT_PUBLIC(void) MC_assert(int);
XBT_PUBLIC(int) MC_random(int min, int max);
#define MC_assert(a) xbt_assert(a)
#define MC_assert(a) xbt_assert(a)
+static int MC_is_active(void) {
+ return 0;
+}
+
/* Configuration support */
e_mc_reduce_t mc_reduce_kind=e_mc_reduce_unset;
/* Configuration support */
e_mc_reduce_t mc_reduce_kind=e_mc_reduce_unset;
extern int _surf_init_status;
void _mc_cfg_cb_reduce(const char *name, int pos) {
if (_surf_init_status && !_surf_do_model_check) {
extern int _surf_init_status;
void _mc_cfg_cb_reduce(const char *name, int pos) {
if (_surf_init_status && !_surf_do_model_check) {
void MC_assert(int prop)
{
void MC_assert(int prop)
{
- if (MC_IS_ENABLED && !prop){
+ if (MC_is_active() && !prop){
XBT_INFO("**************************");
XBT_INFO("*** PROPERTY NOT VALID ***");
XBT_INFO("**************************");
XBT_INFO("**************************");
XBT_INFO("*** PROPERTY NOT VALID ***");
XBT_INFO("**************************");
}
static void MC_assert_pair(int prop){
}
static void MC_assert_pair(int prop){
- if (MC_IS_ENABLED && !prop) {
+ if (MC_is_active() && !prop) {
XBT_INFO("**************************");
XBT_INFO("*** PROPERTY NOT VALID ***");
XBT_INFO("**************************");
XBT_INFO("**************************");
XBT_INFO("*** PROPERTY NOT VALID ***");
XBT_INFO("**************************");
sg_platf_postparse_add_cb(MSG_post_create_environment);
}
sg_platf_postparse_add_cb(MSG_post_create_environment);
}
/* Ignore total amount of messages sent during the simulation for heap comparison */
MC_ignore(&(msg_global->sent_msg), sizeof(msg_global->sent_msg));
}
/* Ignore total amount of messages sent during the simulation for heap comparison */
MC_ignore(&(msg_global->sent_msg), sizeof(msg_global->sent_msg));
}
fflush(stdout);
fflush(stderr);
fflush(stdout);
fflush(stderr);
MC_do_the_modelcheck_for_real();
} else {
SIMIX_run();
MC_do_the_modelcheck_for_real();
} else {
SIMIX_run();
smx_context_t context = xbt_malloc0(size);
/* Store the address of the stack in heap to compare it apart of heap comparison */
smx_context_t context = xbt_malloc0(size);
/* Store the address of the stack in heap to compare it apart of heap comparison */
MC_ignore(context, size);
/* If the user provided a function for the process then use it.
MC_ignore(context, size);
/* If the user provided a function for the process then use it.
} else {
raw_maestro_context = context;
} else {
raw_maestro_context = context;
MC_ignore(&(raw_maestro_context->stack_top), sizeof(raw_maestro_context->stack_top));
}
MC_ignore(&(raw_maestro_context->stack_top), sizeof(raw_maestro_context->stack_top));
}
sysv_maestro_context = context;
}
sysv_maestro_context = context;
}
- if(MC_IS_ENABLED && code)
+ if(MC_is_active() && code)
MC_new_stack_area(context, ((smx_process_t)((smx_context_t)context)->data)->name, &(context->uc));
return (smx_context_t) context;
MC_new_stack_area(context, ((smx_process_t)((smx_context_t)context)->data)->name, &(context->uc));
return (smx_context_t) context;
*/
XBT_INLINE double SIMIX_get_clock(void)
{
*/
XBT_INLINE double SIMIX_get_clock(void)
{
return MC_process_clock_get(SIMIX_process_self());
}else{
return surf_get_clock();
return MC_process_clock_get(SIMIX_process_self());
}else{
return surf_get_clock();
#endif
/* set surf's action */
#endif
/* set surf's action */
action->execution.surf_exec =
surf_workstation_model->extension.workstation.execute(host->host,
computation_amount);
action->execution.surf_exec =
surf_workstation_model->extension.workstation.execute(host->host,
computation_amount);
workstation_list[i] = host_list[i]->host;
/* set surf's action */
workstation_list[i] = host_list[i]->host;
/* set surf's action */
action->execution.surf_exec =
surf_workstation_model->extension.workstation.
execute_parallel_task(host_nb, workstation_list, computation_amount,
action->execution.surf_exec =
surf_workstation_model->extension.workstation.
execute_parallel_task(host_nb, workstation_list, computation_amount,
simcall->issuer->waiting_action = action;
/* set surf's action */
simcall->issuer->waiting_action = action;
/* set surf's action */
action->state = SIMIX_DONE;
SIMIX_execution_finish(action);
return;
action->state = SIMIX_DONE;
SIMIX_execution_finish(action);
return;
void SIMIX_network_init(void)
{
rdv_points = xbt_dict_new_homogeneous(SIMIX_rdv_free);
void SIMIX_network_init(void)
{
rdv_points = xbt_dict_new_homogeneous(SIMIX_rdv_free);
MC_ignore(&smx_total_comms, sizeof(smx_total_comms));
}
MC_ignore(&smx_total_comms, sizeof(smx_total_comms));
}
other_action->comm.match_fun = match_fun;
other_action->comm.match_fun = match_fun;
other_action->state = SIMIX_RUNNING;
return other_action;
}
other_action->state = SIMIX_RUNNING;
return other_action;
}
SIMIX_comm_copy_data(other_action);*/
SIMIX_comm_copy_data(other_action);*/
other_action->state = SIMIX_RUNNING;
return other_action;
}
other_action->state = SIMIX_RUNNING;
return other_action;
}
xbt_fifo_push(action->simcalls, simcall);
simcall->issuer->waiting_action = action;
xbt_fifo_push(action->simcalls, simcall);
simcall->issuer->waiting_action = action;
if (idx == 0) {
action->state = SIMIX_DONE;
} else {
if (idx == 0) {
action->state = SIMIX_DONE;
} else {
{
smx_action_t action = simcall->comm_test.comm;
{
smx_action_t action = simcall->comm_test.comm;
simcall->comm_test.result = action->comm.src_proc && action->comm.dst_proc;
if(simcall->comm_test.result){
action->state = SIMIX_DONE;
simcall->comm_test.result = action->comm.src_proc && action->comm.dst_proc;
if(simcall->comm_test.result){
action->state = SIMIX_DONE;
xbt_dynar_t actions = simcall->comm_testany.comms;
simcall->comm_testany.result = -1;
xbt_dynar_t actions = simcall->comm_testany.comms;
simcall->comm_testany.result = -1;
if(idx == -1){
SIMIX_simcall_answer(simcall);
}else{
if(idx == -1){
SIMIX_simcall_answer(simcall);
}else{
unsigned int cursor = 0;
xbt_dynar_t actions = simcall->comm_waitany.comms;
unsigned int cursor = 0;
xbt_dynar_t actions = simcall->comm_waitany.comms;
action = xbt_dynar_get_as(actions, idx, smx_action_t);
xbt_fifo_push(action->simcalls, simcall);
simcall->comm_waitany.result = idx;
action = xbt_dynar_get_as(actions, idx, smx_action_t);
xbt_fifo_push(action->simcalls, simcall);
simcall->comm_waitany.result = idx;
return it as the result of the simcall */
if (simcall->call == SIMCALL_COMM_WAITANY) {
SIMIX_waitany_remove_simcall_from_actions(simcall);
return it as the result of the simcall */
if (simcall->call == SIMCALL_COMM_WAITANY) {
SIMIX_waitany_remove_simcall_from_actions(simcall);
simcall->comm_waitany.result = xbt_dynar_search(simcall->comm_waitany.comms, &action);
}
simcall->comm_waitany.result = xbt_dynar_search(simcall->comm_waitany.comms, &action);
}
SIMIX_rdv_remove(action->comm.rdv, action);
action->state = SIMIX_CANCELED;
}
SIMIX_rdv_remove(action->comm.rdv, action);
action->state = SIMIX_CANCELED;
}
- else if (!MC_IS_ENABLED /* when running the MC there are no surf actions */
+ else if (!MC_is_active() /* when running the MC there are no surf actions */
&& (action->state == SIMIX_READY || action->state == SIMIX_RUNNING)) {
surf_workstation_model->action_cancel(action->comm.surf_comm);
&& (action->state == SIMIX_READY || action->state == SIMIX_RUNNING)) {
surf_workstation_model->action_cancel(action->comm.surf_comm);
void SIMIX_pre_process_sleep(smx_simcall_t simcall)
{
void SIMIX_pre_process_sleep(smx_simcall_t simcall)
{
MC_process_clock_add(simcall->issuer, simcall->process_sleep.duration);
simcall->process_sleep.result = SIMIX_DONE;
SIMIX_simcall_answer(simcall);
MC_process_clock_add(simcall->issuer, simcall->process_sleep.duration);
simcall->process_sleep.result = SIMIX_DONE;
SIMIX_simcall_answer(simcall);
/* smx_user.c - public interface to simix */
/* smx_user.c - public interface to simix */
-/* Copyright (c) 2010, 2011. Da SimGrid team. All rights reserved. */
+/* Copyright (c) 2010-2012. Da SimGrid team. All rights reserved. */
/* 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. */
/* 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. */
simcall->call = SIMCALL_HOST_GET_BY_NAME;
simcall->host_get_by_name.name = name;
simcall->call = SIMCALL_HOST_GET_BY_NAME;
simcall->host_get_by_name.name = name;
- if(MC_IS_ENABLED) /* Initialize result to NULL for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to NULL for snapshot comparison done during simcall */
simcall->host_get_by_name.result = NULL;
SIMIX_simcall_push(simcall->issuer);
return simcall->host_get_by_name.result;
simcall->host_get_by_name.result = NULL;
SIMIX_simcall_push(simcall->issuer);
return simcall->host_get_by_name.result;
simcall->call = SIMCALL_HOST_GET_NAME;
simcall->host_get_name.host = host;
simcall->call = SIMCALL_HOST_GET_NAME;
simcall->host_get_name.host = host;
- if(MC_IS_ENABLED) /* Initialize result to NULL for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to NULL for snapshot comparison done during simcall */
simcall->host_get_name.result = NULL;
SIMIX_simcall_push(simcall->issuer);
return simcall->host_get_name.result;
simcall->host_get_name.result = NULL;
SIMIX_simcall_push(simcall->issuer);
return simcall->host_get_name.result;
simcall->call = SIMCALL_HOST_GET_PROPERTIES;
simcall->host_get_properties.host = host;
simcall->call = SIMCALL_HOST_GET_PROPERTIES;
simcall->host_get_properties.host = host;
- if(MC_IS_ENABLED) /* Initialize result to NULL for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to NULL for snapshot comparison done during simcall */
simcall->host_get_properties.result = NULL;
SIMIX_simcall_push(simcall->issuer);
return simcall->host_get_properties.result;
simcall->host_get_properties.result = NULL;
SIMIX_simcall_push(simcall->issuer);
return simcall->host_get_properties.result;
simcall->call = SIMCALL_ASR_GET_PROPERTIES;
simcall->asr_get_properties.name = name;
simcall->call = SIMCALL_ASR_GET_PROPERTIES;
simcall->asr_get_properties.name = name;
- if(MC_IS_ENABLED) /* Initialize result to NULL for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to NULL for snapshot comparison done during simcall */
simcall->asr_get_properties.result = NULL;
SIMIX_simcall_push(simcall->issuer);
return simcall->asr_get_properties.result;
simcall->asr_get_properties.result = NULL;
SIMIX_simcall_push(simcall->issuer);
return simcall->asr_get_properties.result;
simcall->call = SIMCALL_HOST_GET_SPEED;
simcall->host_get_speed.host = host;
simcall->call = SIMCALL_HOST_GET_SPEED;
simcall->host_get_speed.host = host;
- if(MC_IS_ENABLED) /* Initialize result to a default value for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to a default value for snapshot comparison done during simcall */
simcall->host_get_speed.result = 0.0;
SIMIX_simcall_push(simcall->issuer);
return simcall->host_get_speed.result;
simcall->host_get_speed.result = 0.0;
SIMIX_simcall_push(simcall->issuer);
return simcall->host_get_speed.result;
simcall->call = SIMCALL_HOST_GET_AVAILABLE_SPEED;
simcall->host_get_available_speed.host = host;
simcall->call = SIMCALL_HOST_GET_AVAILABLE_SPEED;
simcall->host_get_available_speed.host = host;
- if(MC_IS_ENABLED) /* Initialize result to a default value for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to a default value for snapshot comparison done during simcall */
simcall->host_get_available_speed.result = 0.0;
SIMIX_simcall_push(simcall->issuer);
return simcall->host_get_available_speed.result;
simcall->host_get_available_speed.result = 0.0;
SIMIX_simcall_push(simcall->issuer);
return simcall->host_get_available_speed.result;
simcall->call = SIMCALL_HOST_GET_STATE;
simcall->host_get_state.host = host;
simcall->call = SIMCALL_HOST_GET_STATE;
simcall->host_get_state.host = host;
- if(MC_IS_ENABLED) /* Initialize result to a default value for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to a default value for snapshot comparison done during simcall */
simcall->host_get_state.result = -1;
SIMIX_simcall_push(simcall->issuer);
return simcall->host_get_state.result;
simcall->host_get_state.result = -1;
SIMIX_simcall_push(simcall->issuer);
return simcall->host_get_state.result;
simcall->call = SIMCALL_HOST_GET_DATA;
simcall->host_get_data.host = host;
simcall->call = SIMCALL_HOST_GET_DATA;
simcall->host_get_data.host = host;
- if(MC_IS_ENABLED) /* Initialize result to NULL for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to NULL for snapshot comparison done during simcall */
simcall->host_get_data.result = NULL;
SIMIX_simcall_push(simcall->issuer);
return simcall->host_get_data.result;
simcall->host_get_data.result = NULL;
SIMIX_simcall_push(simcall->issuer);
return simcall->host_get_data.result;
simcall->host_execute.host = host;
simcall->host_execute.computation_amount = computation_amount;
simcall->host_execute.priority = priority;
simcall->host_execute.host = host;
simcall->host_execute.computation_amount = computation_amount;
simcall->host_execute.priority = priority;
- if(MC_IS_ENABLED) /* Initialize result to NULL for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to NULL for snapshot comparison done during simcall */
simcall->host_execute.result = NULL;
SIMIX_simcall_push(simcall->issuer);
return simcall->host_execute.result;
simcall->host_execute.result = NULL;
SIMIX_simcall_push(simcall->issuer);
return simcall->host_execute.result;
simcall->host_parallel_execute.communication_amount = communication_amount;
simcall->host_parallel_execute.amount = amount;
simcall->host_parallel_execute.rate = rate;
simcall->host_parallel_execute.communication_amount = communication_amount;
simcall->host_parallel_execute.amount = amount;
simcall->host_parallel_execute.rate = rate;
- if(MC_IS_ENABLED) /* Initialize result to NULL for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to NULL for snapshot comparison done during simcall */
simcall->host_parallel_execute.result = NULL;
SIMIX_simcall_push(simcall->issuer);
return simcall->host_parallel_execute.result;
simcall->host_parallel_execute.result = NULL;
SIMIX_simcall_push(simcall->issuer);
return simcall->host_parallel_execute.result;
simcall->call = SIMCALL_HOST_EXECUTION_GET_REMAINS;
simcall->host_execution_get_remains.execution = execution;
simcall->call = SIMCALL_HOST_EXECUTION_GET_REMAINS;
simcall->host_execution_get_remains.execution = execution;
- if(MC_IS_ENABLED) /* Initializeialize result to a default value for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initializeialize result to a default value for snapshot comparison done during simcall */
simcall->host_execution_get_remains.result = 0.0;
SIMIX_simcall_push(simcall->issuer);
return simcall->host_execution_get_remains.result;
simcall->host_execution_get_remains.result = 0.0;
SIMIX_simcall_push(simcall->issuer);
return simcall->host_execution_get_remains.result;
simcall->call = SIMCALL_HOST_EXECUTION_WAIT;
simcall->host_execution_wait.execution = execution;
simcall->call = SIMCALL_HOST_EXECUTION_WAIT;
simcall->host_execution_wait.execution = execution;
- if(MC_IS_ENABLED) /* Initialize result to a default value for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to a default value for snapshot comparison done during simcall */
simcall->host_execution_wait.result = -1;
SIMIX_simcall_push(simcall->issuer);
return simcall->host_execution_wait.result;
simcall->host_execution_wait.result = -1;
SIMIX_simcall_push(simcall->issuer);
return simcall->host_execution_wait.result;
smx_simcall_t simcall = SIMIX_simcall_mine();
simcall->call = SIMCALL_PROCESS_COUNT;
smx_simcall_t simcall = SIMIX_simcall_mine();
simcall->call = SIMCALL_PROCESS_COUNT;
- if(MC_IS_ENABLED) /* Initialize result to a default value for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to a default value for snapshot comparison done during simcall */
simcall->process_count.result = -1;
SIMIX_simcall_push(simcall->issuer);
return simcall->process_count.result;
simcall->process_count.result = -1;
SIMIX_simcall_push(simcall->issuer);
return simcall->process_count.result;
simcall->call = SIMCALL_PROCESS_GET_DATA;
simcall->process_get_data.process = process;
simcall->call = SIMCALL_PROCESS_GET_DATA;
simcall->process_get_data.process = process;
- if(MC_IS_ENABLED) /* Initialize result to NULL for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to NULL for snapshot comparison done during simcall */
simcall->process_get_data.result = NULL;
SIMIX_simcall_push(simcall->issuer);
return simcall->process_get_data.result;
simcall->process_get_data.result = NULL;
SIMIX_simcall_push(simcall->issuer);
return simcall->process_get_data.result;
simcall->call = SIMCALL_PROCESS_GET_HOST;
simcall->process_get_host.process = process;
simcall->call = SIMCALL_PROCESS_GET_HOST;
simcall->process_get_host.process = process;
- if(MC_IS_ENABLED) /* Initialize result to NULL for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to NULL for snapshot comparison done during simcall */
simcall->process_get_host.result = NULL;
SIMIX_simcall_push(simcall->issuer);
return simcall->process_get_host.result;
simcall->process_get_host.result = NULL;
SIMIX_simcall_push(simcall->issuer);
return simcall->process_get_host.result;
simcall->call = SIMCALL_PROCESS_GET_NAME;
simcall->process_get_name.process = process;
simcall->call = SIMCALL_PROCESS_GET_NAME;
simcall->process_get_name.process = process;
- if(MC_IS_ENABLED) /* Initialize result to NULL for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to NULL for snapshot comparison done during simcall */
simcall->process_get_name.result = NULL;
SIMIX_simcall_push(simcall->issuer);
return simcall->process_get_name.result;
simcall->process_get_name.result = NULL;
SIMIX_simcall_push(simcall->issuer);
return simcall->process_get_name.result;
simcall->call = SIMCALL_PROCESS_IS_SUSPENDED;
simcall->process_is_suspended.process = process;
simcall->call = SIMCALL_PROCESS_IS_SUSPENDED;
simcall->process_is_suspended.process = process;
- if(MC_IS_ENABLED) /* Initialize result to a default value for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to a default value for snapshot comparison done during simcall */
simcall->process_is_suspended.result = -1;
SIMIX_simcall_push(simcall->issuer);
return simcall->process_is_suspended.result;
simcall->process_is_suspended.result = -1;
SIMIX_simcall_push(simcall->issuer);
return simcall->process_is_suspended.result;
simcall->call = SIMCALL_PROCESS_GET_PROPERTIES;
simcall->process_get_properties.process = process;
simcall->call = SIMCALL_PROCESS_GET_PROPERTIES;
simcall->process_get_properties.process = process;
- if(MC_IS_ENABLED) /* Initialize result to NULL for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to NULL for snapshot comparison done during simcall */
simcall->process_get_properties.result = NULL;
SIMIX_simcall_push(simcall->issuer);
return simcall->process_get_properties.result;
simcall->process_get_properties.result = NULL;
SIMIX_simcall_push(simcall->issuer);
return simcall->process_get_properties.result;
simcall->call = SIMCALL_PROCESS_RESTART;
simcall->process_restart.process = process;
simcall->call = SIMCALL_PROCESS_RESTART;
simcall->process_restart.process = process;
- if(MC_IS_ENABLED) /* Initialize result to NULL for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to NULL for snapshot comparison done during simcall */
simcall->process_restart.result = NULL;
SIMIX_simcall_push(simcall->issuer);
simcall->process_restart.result = NULL;
SIMIX_simcall_push(simcall->issuer);
simcall->call = SIMCALL_PROCESS_SLEEP;
simcall->process_sleep.duration = duration;
simcall->call = SIMCALL_PROCESS_SLEEP;
simcall->process_sleep.duration = duration;
- if(MC_IS_ENABLED) /* Initialize result to a default value for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to a default value for snapshot comparison done during simcall */
simcall->process_sleep.result = -1;
SIMIX_simcall_push(simcall->issuer);
return simcall->process_sleep.result;
simcall->process_sleep.result = -1;
SIMIX_simcall_push(simcall->issuer);
return simcall->process_sleep.result;
simcall->call = SIMCALL_RDV_CREATE;
simcall->rdv_create.name = name;
simcall->call = SIMCALL_RDV_CREATE;
simcall->rdv_create.name = name;
- if(MC_IS_ENABLED) /* Initialize result to NULL for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to NULL for snapshot comparison done during simcall */
simcall->rdv_create.result = NULL;
SIMIX_simcall_push(simcall->issuer);
simcall->rdv_create.result = NULL;
SIMIX_simcall_push(simcall->issuer);
simcall->call = SIMCALL_RDV_COMM_COUNT_BY_HOST;
simcall->rdv_comm_count_by_host.rdv = rdv;
simcall->rdv_comm_count_by_host.host = host;
simcall->call = SIMCALL_RDV_COMM_COUNT_BY_HOST;
simcall->rdv_comm_count_by_host.rdv = rdv;
simcall->rdv_comm_count_by_host.host = host;
- if(MC_IS_ENABLED) /* Initialize result to a default value for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to a default value for snapshot comparison done during simcall */
simcall->rdv_comm_count_by_host.result = -1;
SIMIX_simcall_push(simcall->issuer);
simcall->rdv_comm_count_by_host.result = -1;
SIMIX_simcall_push(simcall->issuer);
simcall->call = SIMCALL_RDV_GET_HEAD;
simcall->rdv_get_head.rdv = rdv;
simcall->call = SIMCALL_RDV_GET_HEAD;
simcall->rdv_get_head.rdv = rdv;
- if(MC_IS_ENABLED) /* Initialize result to NULL for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to NULL for snapshot comparison done during simcall */
simcall->rdv_get_head.result = NULL;
SIMIX_simcall_push(simcall->issuer);
simcall->rdv_get_head.result = NULL;
SIMIX_simcall_push(simcall->issuer);
simcall->call = SIMCALL_RDV_GET_RECV;
simcall->rdv_get_rcv_proc.rdv = rdv;
simcall->call = SIMCALL_RDV_GET_RECV;
simcall->rdv_get_rcv_proc.rdv = rdv;
- if(MC_IS_ENABLED) /* Initialize result to NULL for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to NULL for snapshot comparison done during simcall */
simcall->rdv_get_rcv_proc.result = NULL;
SIMIX_simcall_push(simcall->issuer);
simcall->rdv_get_rcv_proc.result = NULL;
SIMIX_simcall_push(simcall->issuer);
xbt_assert(rdv, "No rendez-vous point defined for send");
xbt_assert(rdv, "No rendez-vous point defined for send");
/* the model-checker wants two separate simcalls */
smx_action_t comm = simcall_comm_isend(rdv, task_size, rate,
src_buff, src_buff_size, match_fun, NULL, data, 0);
/* the model-checker wants two separate simcalls */
smx_action_t comm = simcall_comm_isend(rdv, task_size, rate,
src_buff, src_buff_size, match_fun, NULL, data, 0);
simcall->comm_isend.clean_fun = clean_fun;
simcall->comm_isend.data = data;
simcall->comm_isend.detached = detached;
simcall->comm_isend.clean_fun = clean_fun;
simcall->comm_isend.data = data;
simcall->comm_isend.detached = detached;
- if(MC_IS_ENABLED) /* Initialize result to NULL for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to NULL for snapshot comparison done during simcall */
simcall->comm_isend.result = NULL;
SIMIX_simcall_push(simcall->issuer);
simcall->comm_isend.result = NULL;
SIMIX_simcall_push(simcall->issuer);
xbt_assert(isfinite(timeout), "timeout is not finite!");
xbt_assert(rdv, "No rendez-vous point defined for recv");
xbt_assert(isfinite(timeout), "timeout is not finite!");
xbt_assert(rdv, "No rendez-vous point defined for recv");
/* the model-checker wants two separate simcalls */
smx_action_t comm = simcall_comm_irecv(rdv, dst_buff, dst_buff_size,
match_fun, data);
/* the model-checker wants two separate simcalls */
smx_action_t comm = simcall_comm_irecv(rdv, dst_buff, dst_buff_size,
match_fun, data);
simcall->comm_irecv.dst_buff_size = dst_buff_size;
simcall->comm_irecv.match_fun = match_fun;
simcall->comm_irecv.data = data;
simcall->comm_irecv.dst_buff_size = dst_buff_size;
simcall->comm_irecv.match_fun = match_fun;
simcall->comm_irecv.data = data;
- if(MC_IS_ENABLED) /* Initialize result to NULL for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to NULL for snapshot comparison done during simcall */
simcall->comm_irecv.result = NULL;
SIMIX_simcall_push(simcall->issuer);
simcall->comm_irecv.result = NULL;
SIMIX_simcall_push(simcall->issuer);
simcall->comm_iprobe.src = src;
simcall->comm_iprobe.match_fun = match_fun;
simcall->comm_iprobe.data = data;
simcall->comm_iprobe.src = src;
simcall->comm_iprobe.match_fun = match_fun;
simcall->comm_iprobe.data = data;
- if(MC_IS_ENABLED) /* Initialize result to NULL for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to NULL for snapshot comparison done during simcall */
simcall->comm_iprobe.result = NULL;
SIMIX_simcall_push(simcall->issuer);
return simcall->comm_iprobe.result;
simcall->comm_iprobe.result = NULL;
SIMIX_simcall_push(simcall->issuer);
return simcall->comm_iprobe.result;
simcall->call = SIMCALL_COMM_WAITANY;
simcall->comm_waitany.comms = comms;
simcall->call = SIMCALL_COMM_WAITANY;
simcall->comm_waitany.comms = comms;
- if(MC_IS_ENABLED) /* Initialize result to a default value for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to a default value for snapshot comparison done during simcall */
simcall->comm_waitany.result = -1;
SIMIX_simcall_push(simcall->issuer);
simcall->comm_waitany.result = -1;
SIMIX_simcall_push(simcall->issuer);
simcall->call = SIMCALL_COMM_TESTANY;
simcall->comm_testany.comms = comms;
simcall->call = SIMCALL_COMM_TESTANY;
simcall->comm_testany.comms = comms;
- if(MC_IS_ENABLED) /* Initialize result to a default value for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to a default value for snapshot comparison done during simcall */
simcall->comm_testany.result = -1;
SIMIX_simcall_push(simcall->issuer);
simcall->comm_testany.result = -1;
SIMIX_simcall_push(simcall->issuer);
simcall->call = SIMCALL_COMM_TEST;
simcall->comm_test.comm = comm;
simcall->call = SIMCALL_COMM_TEST;
simcall->comm_test.comm = comm;
- if(MC_IS_ENABLED) /* Initialize result to a default value for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to a default value for snapshot comparison done during simcall */
simcall->comm_test.result = -1;
SIMIX_simcall_push(simcall->issuer);
simcall->comm_test.result = -1;
SIMIX_simcall_push(simcall->issuer);
simcall->call = SIMCALL_COMM_GET_REMAINS;
simcall->comm_get_remains.comm = comm;
simcall->call = SIMCALL_COMM_GET_REMAINS;
simcall->comm_get_remains.comm = comm;
- if(MC_IS_ENABLED) /* Initialize result to a default value for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to a default value for snapshot comparison done during simcall */
simcall->comm_get_remains.result = 0.0;
SIMIX_simcall_push(simcall->issuer);
simcall->comm_get_remains.result = 0.0;
SIMIX_simcall_push(simcall->issuer);
simcall->call = SIMCALL_COMM_GET_STATE;
simcall->comm_get_state.comm = comm;
simcall->call = SIMCALL_COMM_GET_STATE;
simcall->comm_get_state.comm = comm;
- if(MC_IS_ENABLED) /* Initialize result to a default value for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to a default value for snapshot comparison done during simcall */
simcall->comm_get_state.result = -1;
SIMIX_simcall_push(simcall->issuer);
simcall->comm_get_state.result = -1;
SIMIX_simcall_push(simcall->issuer);
simcall->call = SIMCALL_COMM_GET_SRC_DATA;
simcall->comm_get_src_data.comm = comm;
simcall->call = SIMCALL_COMM_GET_SRC_DATA;
simcall->comm_get_src_data.comm = comm;
- if(MC_IS_ENABLED) /* Initialize result to NULL for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to NULL for snapshot comparison done during simcall */
simcall->comm_get_src_data.result = NULL;
SIMIX_simcall_push(simcall->issuer);
simcall->comm_get_src_data.result = NULL;
SIMIX_simcall_push(simcall->issuer);
simcall->call = SIMCALL_COMM_GET_DST_DATA;
simcall->comm_get_dst_data.comm = comm;
simcall->call = SIMCALL_COMM_GET_DST_DATA;
simcall->comm_get_dst_data.comm = comm;
- if(MC_IS_ENABLED) /* Initialize result to NULL for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to NULL for snapshot comparison done during simcall */
simcall->comm_get_dst_data.result = NULL;
SIMIX_simcall_push(simcall->issuer);
simcall->comm_get_dst_data.result = NULL;
SIMIX_simcall_push(simcall->issuer);
simcall->call = SIMCALL_COMM_GET_SRC_PROC;
simcall->comm_get_src_proc.comm = comm;
simcall->call = SIMCALL_COMM_GET_SRC_PROC;
simcall->comm_get_src_proc.comm = comm;
- if(MC_IS_ENABLED) /* Initialize result to NULL for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to NULL for snapshot comparison done during simcall */
simcall->comm_get_src_proc.result = NULL;
SIMIX_simcall_push(simcall->issuer);
simcall->comm_get_src_proc.result = NULL;
SIMIX_simcall_push(simcall->issuer);
simcall->call = SIMCALL_COMM_GET_DST_PROC;
simcall->comm_get_dst_proc.comm = comm;
simcall->call = SIMCALL_COMM_GET_DST_PROC;
simcall->comm_get_dst_proc.comm = comm;
- if(MC_IS_ENABLED) /* Initialize result to NULL for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to NULL for snapshot comparison done during simcall */
simcall->comm_get_dst_proc.result = NULL;
SIMIX_simcall_push(simcall->issuer);
simcall->comm_get_dst_proc.result = NULL;
SIMIX_simcall_push(simcall->issuer);
simcall->call = SIMCALL_COMM_IS_LATENCY_BOUNDED;
simcall->comm_is_latency_bounded.comm = comm;
simcall->call = SIMCALL_COMM_IS_LATENCY_BOUNDED;
simcall->comm_is_latency_bounded.comm = comm;
- if(MC_IS_ENABLED) /* Initialize result to a default value for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to a default value for snapshot comparison done during simcall */
simcall->comm_is_latency_bounded.result = -1;
SIMIX_simcall_push(simcall->issuer);
simcall->comm_is_latency_bounded.result = -1;
SIMIX_simcall_push(simcall->issuer);
smx_simcall_t simcall = SIMIX_simcall_mine();
simcall->call = SIMCALL_MUTEX_INIT;
smx_simcall_t simcall = SIMIX_simcall_mine();
simcall->call = SIMCALL_MUTEX_INIT;
- if(MC_IS_ENABLED) /* Initialize result to NULL for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to NULL for snapshot comparison done during simcall */
simcall->mutex_init.result = NULL;
SIMIX_simcall_push(simcall->issuer);
simcall->mutex_init.result = NULL;
SIMIX_simcall_push(simcall->issuer);
simcall->call = SIMCALL_MUTEX_TRYLOCK;
simcall->mutex_trylock.mutex = mutex;
simcall->call = SIMCALL_MUTEX_TRYLOCK;
simcall->mutex_trylock.mutex = mutex;
- if(MC_IS_ENABLED) /* Initialize result to a default value for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to a default value for snapshot comparison done during simcall */
simcall->mutex_trylock.result = -1;
SIMIX_simcall_push(simcall->issuer);
simcall->mutex_trylock.result = -1;
SIMIX_simcall_push(simcall->issuer);
smx_simcall_t simcall = SIMIX_simcall_mine();
simcall->call = SIMCALL_COND_INIT;
smx_simcall_t simcall = SIMIX_simcall_mine();
simcall->call = SIMCALL_COND_INIT;
- if(MC_IS_ENABLED) /* Initialize result to NULL for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to NULL for snapshot comparison done during simcall */
simcall->cond_init.result = NULL;
SIMIX_simcall_push(simcall->issuer);
simcall->cond_init.result = NULL;
SIMIX_simcall_push(simcall->issuer);
simcall->call = SIMCALL_SEM_INIT;
simcall->sem_init.capacity = capacity;
simcall->call = SIMCALL_SEM_INIT;
simcall->sem_init.capacity = capacity;
- if(MC_IS_ENABLED) /* Initialize result to NULL for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to NULL for snapshot comparison done during simcall */
simcall->sem_init.result = NULL;
SIMIX_simcall_push(simcall->issuer);
simcall->sem_init.result = NULL;
SIMIX_simcall_push(simcall->issuer);
simcall->call = SIMCALL_SEM_WOULD_BLOCK;
simcall->sem_would_block.sem = sem;
simcall->call = SIMCALL_SEM_WOULD_BLOCK;
simcall->sem_would_block.sem = sem;
- if(MC_IS_ENABLED) /* Initialize result to a default value for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to a default value for snapshot comparison done during simcall */
simcall->sem_would_block.result = -1;
SIMIX_simcall_push(simcall->issuer);
simcall->sem_would_block.result = -1;
SIMIX_simcall_push(simcall->issuer);
simcall->call = SIMCALL_SEM_GET_CAPACITY;
simcall->sem_get_capacity.sem = sem;
simcall->call = SIMCALL_SEM_GET_CAPACITY;
simcall->sem_get_capacity.sem = sem;
- if(MC_IS_ENABLED) /* Initialize result to a default value for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to a default value for snapshot comparison done during simcall */
simcall->sem_get_capacity.result = -1;
SIMIX_simcall_push(simcall->issuer);
simcall->sem_get_capacity.result = -1;
SIMIX_simcall_push(simcall->issuer);
simcall->file_read.size = size;
simcall->file_read.nmemb = nmemb;
simcall->file_read.stream = stream;
simcall->file_read.size = size;
simcall->file_read.nmemb = nmemb;
simcall->file_read.stream = stream;
- if(MC_IS_ENABLED) /* Initialize result to a default value for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to a default value for snapshot comparison done during simcall */
simcall->file_read.result = 0.0;
SIMIX_simcall_push(simcall->issuer);
simcall->file_read.result = 0.0;
SIMIX_simcall_push(simcall->issuer);
simcall->file_write.size = size;
simcall->file_write.nmemb = nmemb;
simcall->file_write.stream = stream;
simcall->file_write.size = size;
simcall->file_write.nmemb = nmemb;
simcall->file_write.stream = stream;
- if(MC_IS_ENABLED) /* Initialize result to a default value for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to a default value for snapshot comparison done during simcall */
simcall->file_write.result = 0;
SIMIX_simcall_push(simcall->issuer);
simcall->file_write.result = 0;
SIMIX_simcall_push(simcall->issuer);
simcall->file_open.mount = mount;
simcall->file_open.path = path;
simcall->file_open.mode = mode;
simcall->file_open.mount = mount;
simcall->file_open.path = path;
simcall->file_open.mode = mode;
- if(MC_IS_ENABLED) /* Initialize result to NULL for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to NULL for snapshot comparison done during simcall */
simcall->file_open.result = NULL;
SIMIX_simcall_push(simcall->issuer);
simcall->file_open.result = NULL;
SIMIX_simcall_push(simcall->issuer);
simcall->call = SIMCALL_FILE_CLOSE;
simcall->file_close.fp = fp;
simcall->call = SIMCALL_FILE_CLOSE;
simcall->file_close.fp = fp;
- if(MC_IS_ENABLED) /* Initialize result to a default value for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to a default value for snapshot comparison done during simcall */
simcall->file_close.result = -1;
SIMIX_simcall_push(simcall->issuer);
simcall->file_close.result = -1;
SIMIX_simcall_push(simcall->issuer);
smx_simcall_t simcall = SIMIX_simcall_mine();
simcall->call = SIMCALL_FILE_STAT;
simcall->file_stat.fd = fd;
smx_simcall_t simcall = SIMIX_simcall_mine();
simcall->call = SIMCALL_FILE_STAT;
simcall->file_stat.fd = fd;
- if(MC_IS_ENABLED) /* Initialize result to a default value for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to a default value for snapshot comparison done during simcall */
simcall->file_stat.result = -1;
SIMIX_simcall_push(simcall->issuer);
simcall->file_stat.result = -1;
SIMIX_simcall_push(simcall->issuer);
smx_simcall_t simcall = SIMIX_simcall_mine();
simcall->call = SIMCALL_FILE_UNLINK;
simcall->file_unlink.fd = fd;
smx_simcall_t simcall = SIMIX_simcall_mine();
simcall->call = SIMCALL_FILE_UNLINK;
simcall->file_unlink.fd = fd;
- if(MC_IS_ENABLED) /* Initialize result to a default value for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to a default value for snapshot comparison done during simcall */
simcall->file_unlink.result = -1;
SIMIX_simcall_push(simcall->issuer);
simcall->file_unlink.result = -1;
SIMIX_simcall_push(simcall->issuer);
simcall->call = SIMCALL_FILE_LS;
simcall->file_ls.mount = mount;
simcall->file_ls.path = path;
simcall->call = SIMCALL_FILE_LS;
simcall->file_ls.mount = mount;
simcall->file_ls.path = path;
- if(MC_IS_ENABLED) /* Initialize result to a default value for snapshot comparison done during simcall */
+ if(MC_is_active()) /* Initialize result to a default value for snapshot comparison done during simcall */
simcall->file_ls.result = NULL;
SIMIX_simcall_push(simcall->issuer);
simcall->file_ls.result = NULL;
SIMIX_simcall_push(simcall->issuer);
}
for(c = 0; c < count; c++) {
}
for(c = 0; c < count; c++) {
smpi_mpi_wait(&requests[c], pstat);
index = c;
} else {
smpi_mpi_wait(&requests[c], pstat);
index = c;
} else {
fflush(stdout);
fflush(stderr);
fflush(stdout);
fflush(stderr);
MC_modelcheck();
else
SIMIX_run();
MC_modelcheck();
else
SIMIX_run();
surf_config_init(argc, argv);
surf_action_init();
surf_config_init(argc, argv);
surf_action_init();
* memory (so these blocks are killed on restore) and the contrary (so these
* blocks will leak accross restores).
*/
* memory (so these blocks are killed on restore) and the contrary (so these
* blocks will leak accross restores).
*/
-#define MALLOCATOR_IS_ENABLED (MALLOCATOR_IS_WANTED && !MC_IS_ENABLED)
+#define MALLOCATOR_IS_ENABLED (MALLOCATOR_IS_WANTED && !MC_is_active())