}
-static void MC_init_mode(void)
-{
- if (mc_mode == MC_MODE_NONE) {
- if (getenv(MC_ENV_SOCKET_FD)) {
- mc_mode = MC_MODE_CLIENT;
- } else {
- mc_mode = MC_MODE_STANDALONE;
- }
- }
-}
-
#ifdef HAVE_MC
void MC_init()
{
iteration of the model-checker (in RAW memory) */
xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
- mc_model_checker = MC_model_checker_new(pid, socket);
+ mc_model_checker = new simgrid::mc::ModelChecker(pid, socket);
// It's not useful anymore:
if (0 && mc_mode == MC_MODE_SERVER) {
unsigned long maxpid;
- MC_process_read_variable(&mc_model_checker->process, "simix_process_maxpid",
+ MC_process_read_variable(&mc_model_checker->process(), "simix_process_maxpid",
&maxpid, sizeof(maxpid));
simix_process_maxpid = maxpid;
}
/* Init parmap */
//parmap = xbt_parmap_mc_new(xbt_os_get_numcores(), XBT_PARMAP_DEFAULT);
- MC_SET_STD_HEAP;
+ mmalloc_set_current_heap(std_heap);
if (_sg_mc_visited > 0 || _sg_mc_liveness || _sg_mc_termination || mc_mode == MC_MODE_SERVER) {
/* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
/* SIMIX */
MC_ignore_global_variable("smx_total_comms");
- if (mc_mode == MC_MODE_STANDALONE || mc_mode == MC_MODE_CLIENT) {
+ if (mc_mode == MC_MODE_CLIENT) {
/* Those requests are handled on the client side and propagated by message
* to the server: */
/******************************* Core of MC *******************************/
/**************************************************************************/
-void MC_do_the_modelcheck_for_real()
+void MC_run()
{
- MC_init_mode();
-
- switch(mc_mode) {
- default:
- xbt_die("Unexpected mc mode");
- break;
- case MC_MODE_CLIENT:
- MC_init();
- MC_client_main_loop();
- return;
- case MC_MODE_SERVER:
- break;
- case MC_MODE_STANDALONE:
- MC_init();
- break;
- }
-
- if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
- XBT_INFO("Check communication determinism");
- mc_reduce_kind = e_mc_reduce_none;
- MC_wait_for_requests();
- MC_modelcheck_comm_determinism();
- }
-
- else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') {
- if(_sg_mc_termination)
- mc_reduce_kind = e_mc_reduce_none;
- else if (mc_reduce_kind == e_mc_reduce_unset)
- mc_reduce_kind = e_mc_reduce_dpor;
- _sg_mc_safety = 1;
- if (_sg_mc_termination)
- XBT_INFO("Check non progressive cycles");
- else
- XBT_INFO("Check a safety property");
- MC_wait_for_requests();
- MC_modelcheck_safety();
- }
-
- else {
- if (mc_reduce_kind == e_mc_reduce_unset)
- mc_reduce_kind = e_mc_reduce_none;
- XBT_INFO("Check the liveness property %s", _sg_mc_property_file);
- MC_automaton_load(_sg_mc_property_file);
- MC_wait_for_requests();
- MC_modelcheck_liveness();
- }
-
+ mc_mode = MC_MODE_CLIENT;
+ MC_init();
+ MC_client_main_loop();
}
-
void MC_exit(void)
{
xbt_free(mc_time);
{
if (mc_mode == MC_MODE_SERVER) {
int res;
- if ((res = MC_protocol_send_simple_message(mc_model_checker->process.socket,
+ if ((res = MC_protocol_send_simple_message(mc_model_checker->process().socket,
MC_MESSAGE_DEADLOCK_CHECK)))
xbt_die("Could not check deadlock state");
s_mc_int_message_t message;
- ssize_t s = MC_receive_message(mc_model_checker->process.socket, &message, sizeof(message), 0);
+ ssize_t s = MC_receive_message(mc_model_checker->process().socket, &message, sizeof(message), 0);
if (s == -1)
xbt_die("Could not receive message");
else if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY) {
MC_restore_snapshot(state->system_state);
if(_sg_mc_comms_determinism || _sg_mc_send_determinism)
MC_restore_communications_pattern(state);
- MC_SET_STD_HEAP;
+ mmalloc_set_current_heap(std_heap);
return;
}
}
MC_restore_snapshot(initial_global_state->snapshot);
/* At the moment of taking the snapshot the raw heap was set, so restoring
* it will set it back again, we have to unset it to continue */
- MC_SET_STD_HEAP;
+ mmalloc_set_current_heap(std_heap);
start_item = xbt_fifo_get_last_item(stack);
- MC_SET_MC_HEAP;
+ mmalloc_set_current_heap(mc_heap);
if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
// int n = xbt_dynar_length(incomplete_communications_pattern);
}
}
- MC_SET_STD_HEAP;
+ mmalloc_set_current_heap(std_heap);
/* Traverse the stack from the state at position start and re-execute the transitions */
for (item = start_item;
MC_simcall_handle(req, value);
- MC_SET_MC_HEAP;
+ mmalloc_set_current_heap(mc_heap);
if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
MC_handle_comm_pattern(call, req, value, NULL, 1);
- MC_SET_STD_HEAP;
+ mmalloc_set_current_heap(std_heap);
MC_wait_for_requests();
pair = (mc_pair_t) xbt_fifo_get_item_content(item);
if(pair->graph_state->system_state){
MC_restore_snapshot(pair->graph_state->system_state);
- MC_SET_STD_HEAP;
+ mmalloc_set_current_heap(std_heap);
return;
}
}
/* At the moment of taking the snapshot the raw heap was set, so restoring
* it will set it back again, we have to unset it to continue */
if (!initial_global_state->raw_mem_set)
- MC_SET_STD_HEAP;
+ mmalloc_set_current_heap(std_heap);
/* Traverse the stack from the initial state and re-execute the transitions */
for (item = xbt_fifo_get_last_item(stack);
XBT_DEBUG("**** End Replay ****");
if (initial_global_state->raw_mem_set)
- MC_SET_MC_HEAP;
+ mmalloc_set_current_heap(mc_heap);
else
- MC_SET_STD_HEAP;
+ mmalloc_set_current_heap(std_heap);
}
mc_state_t state;
- MC_SET_MC_HEAP;
+ mmalloc_set_current_heap(mc_heap);
while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
MC_state_delete(state, !state->in_visited_states ? 1 : 0);
mmalloc_set_current_heap(heap);
MC_dump_stack_safety(mc_stack);
MC_print_statistics(mc_stats);
}
+
+void MC_invalidate_cache(void)
+{
+ if (mc_model_checker)
+ mc_model_checker->process().cache_flags = 0;
+}
#endif
}
