X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/ea9cce21b6d3f37823143217f1ca183bb2f0c9ac..1ee68a7d44ca89e57734578a1aa91c11ddb27de1:/src/mc/mc_global.cpp

diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index 28cbc9d3c2..d6e4ca154a 100644
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -106,17 +106,6 @@ static void MC_init_dot_output()
 
 }
 
-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()
 {
@@ -129,12 +118,12 @@ void MC_init_pid(pid_t pid, int socket)
      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;
   }
@@ -155,7 +144,7 @@ void MC_init_pid(pid_t pid, int socket)
   /* 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 */
@@ -196,7 +185,7 @@ void MC_init_pid(pid_t pid, int socket)
     /* 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: */
 
@@ -217,58 +206,13 @@ void MC_init_pid(pid_t pid, int socket)
 /*******************************  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);
@@ -282,11 +226,11 @@ int MC_deadlock_check()
 {
   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) {
@@ -342,7 +286,7 @@ void MC_replay(xbt_fifo_t stack)
       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;
     }
   }
@@ -352,11 +296,11 @@ void MC_replay(xbt_fifo_t stack)
   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);
@@ -369,7 +313,7 @@ void MC_replay(xbt_fifo_t stack)
     }
   }
 
-  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;
@@ -400,10 +344,10 @@ void MC_replay(xbt_fifo_t stack)
 
       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();
 
@@ -440,7 +384,7 @@ void MC_replay_liveness(xbt_fifo_t stack)
     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;
     }
   }
@@ -451,7 +395,7 @@ void MC_replay_liveness(xbt_fifo_t stack)
   /* 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);
@@ -496,9 +440,9 @@ void MC_replay_liveness(xbt_fifo_t 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);
 
 }
 
@@ -515,7 +459,7 @@ void MC_dump_stack_safety(xbt_fifo_t stack)
   
   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);
@@ -765,6 +709,12 @@ void MC_report_assertion_error(void)
   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
 
 }