extern int _sg_mc_visited;
extern char* _sg_mc_dot_output_file;
extern int _sg_mc_comms_determinism;
+extern int _sg_mc_send_determinism;
extern xbt_dynar_t mc_heap_comparison_ignore;
extern xbt_dynar_t stacks_areas;
void _mc_cfg_cb_visited(const char *name, int pos);
void _mc_cfg_cb_dot_output(const char *name, int pos);
void _mc_cfg_cb_comms_determinism(const char *name, int pos);
+void _mc_cfg_cb_send_determinism(const char *name, int pos);
XBT_PUBLIC(void) MC_do_the_modelcheck_for_real(void);
recv_index = 0;
current_process++;
}
- // XBT_DEBUG("Communication-deterministic : %d, Send-deterministic : %d", initial_state_safety->comm_deterministic, initial_state_safety->send_deterministic);
}
static int complete_comm_pattern(xbt_dynar_t list, mc_comm_pattern_t pattern){
xbt_free(key);
MC_UNSET_RAW_MEM;
- if(_sg_mc_comms_determinism){
+ if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
if(req->call == SIMCALL_COMM_ISEND)
comm_pattern = 1;
else if(req->call == SIMCALL_COMM_IRECV)
/* Answer the request */
SIMIX_simcall_pre(req, value); /* After this call req is no longer usefull */
- if(_sg_mc_comms_determinism){
+ if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
MC_SET_RAW_MEM;
if(comm_pattern != 0){
if(!initial_state_safety->initial_communications_pattern_done)
MC_SET_RAW_MEM;
- if(_sg_mc_comms_determinism){
- if(!initial_state_safety->initial_communications_pattern_done){
- //print_communications_pattern(initial_communications_pattern);
- }else{
+ if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
+ if(initial_state_safety->initial_communications_pattern_done){
if(interleave_size == 0){ /* if (interleave_size > 0), process interleaved but not enabled => "incorrect" path, determinism not evaluated */
//print_communications_pattern(communications_pattern);
deterministic_pattern(initial_communications_pattern, communications_pattern);
+ if(initial_state_safety->comm_deterministic == 0 && _sg_mc_comms_determinism){
+ XBT_INFO("****************************************************");
+ XBT_INFO("***** Non-deterministic communications pattern *****");
+ XBT_INFO("****************************************************");
+ XBT_INFO("Initial communications pattern:");
+ print_communications_pattern(initial_communications_pattern);
+ XBT_INFO("Communications pattern counter-example:");
+ print_communications_pattern(communications_pattern);
+ MC_print_statistics(mc_stats);
+ return;
+ }else if(initial_state_safety->send_deterministic == 0 && _sg_mc_send_determinism){
+ XBT_INFO("****************************************************");
+ XBT_INFO("***** Non-send-deterministic communications pattern *****");
+ XBT_INFO("****************************************************");
+ XBT_INFO("Initial communications pattern:");
+ print_communications_pattern(initial_communications_pattern);
+ XBT_INFO("Communications pattern counter-example:");
+ print_communications_pattern(communications_pattern);
+ MC_print_statistics(mc_stats);
+ return;
+ }
}
+ }else{
+ initial_state_safety->initial_communications_pattern_done = 1;
}
- initial_state_safety->initial_communications_pattern_done = 1;
}
/* Trash the current state, no longer needed */
int _sg_mc_visited=0;
char *_sg_mc_dot_output_file = NULL;
int _sg_mc_comms_determinism=0;
+int _sg_mc_send_determinism=0;
int user_max_depth_reached = 0;
_sg_mc_comms_determinism= xbt_cfg_get_boolean(_sg_cfg_set, name);
}
+void _mc_cfg_cb_send_determinism(const char *name, int pos) {
+ if (_sg_cfg_init_status && !_sg_do_model_check) {
+ xbt_die("You are specifying a value to enable/disable the detection of send-determinism in the communications schemes after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
+ }
+ _sg_mc_send_determinism= xbt_cfg_get_boolean(_sg_cfg_set, name);
+}
+
/* MC global data structures */
mc_state_t mc_current_state = NULL;
char mc_replay_mode = FALSE;
xbt_free(key);
}
}
- if(_sg_mc_comms_determinism)
+ if(_sg_mc_comms_determinism || _sg_mc_send_determinism)
xbt_dynar_reset(communications_pattern);
MC_UNSET_RAW_MEM;
}
}
- if(_sg_mc_comms_determinism){
+ if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
if(req->call == SIMCALL_COMM_ISEND)
comm_pattern = 1;
else if(req->call == SIMCALL_COMM_IRECV)
SIMIX_simcall_pre(req, value);
- if(_sg_mc_comms_determinism){
+ if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
MC_SET_RAW_MEM;
if(comm_pattern != 0){
get_comm_pattern(communications_pattern, req, comm_pattern);
fprintf(dot_output, "}\n");
fclose(dot_output);
}
- if(initial_state_safety != NULL && _sg_mc_comms_determinism){
- XBT_INFO("Communication-deterministic : %s", !initial_state_safety->comm_deterministic ? "No" : "Yes");
- XBT_INFO("Send-deterministic : %s", !initial_state_safety->send_deterministic ? "No" : "Yes");
+ if(initial_state_safety != NULL){
+ if(_sg_mc_comms_determinism)
+ XBT_INFO("Communication-deterministic : %s", !initial_state_safety->comm_deterministic ? "No" : "Yes");
+ if (_sg_mc_send_determinism)
+ XBT_INFO("Send-deterministic : %s", !initial_state_safety->send_deterministic ? "No" : "Yes");
}
MC_UNSET_RAW_MEM;
}
xbt_cfgelm_string, 0, 1, _mc_cfg_cb_property, NULL);
xbt_cfg_setdefault_string(_sg_cfg_set, "model-check/property", "");
- /* do determinism model-checking */
- xbt_cfg_register(&_sg_cfg_set, "model-check/communications_determinism",
+ /* do communications determinism model-checking */
+ xbt_cfg_register(&_sg_cfg_set, "model-check/communications_determinism",
"Enable/disable the detection of determinism in the communications schemes",
xbt_cfgelm_boolean, 0, 1, _mc_cfg_cb_comms_determinism, NULL);
xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/communications_determinism", "no");
+ /* do send determinism model-checking */
+ xbt_cfg_register(&_sg_cfg_set, "model-check/send_determinism",
+ "Enable/disable the detection of send-determinism in the communications schemes",
+ xbt_cfgelm_boolean, 0, 1, _mc_cfg_cb_send_determinism, NULL);
+ xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/send_determinism", "no");
+
/* Specify the kind of model-checking reduction */
xbt_cfg_register(&_sg_cfg_set, "model-check/reduction",
"Specify the kind of exploration reduction (either none or DPOR)",