[mc] DRY MC_do_the_modelcheck_for_real()

[simgrid.git] / src / mc / mc_global.c

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index da02e1d..7ca082e 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -5,6 +5,7 @@
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include <string.h>
+#include <stdint.h>
 
 #include "mc_base.h"
 
@@ -20,6 +21,7 @@
 #include "xbt/fifo.h"
 #include "xbt/automaton.h"
 #include "xbt/dict.h"
+#include "mc_server.h"
 
 #ifdef HAVE_MC
 #include <libunwind.h>
@@ -150,7 +152,7 @@ void MC_init_pid(pid_t pid, int socket)
 
   MC_SET_STD_HEAP;
 
-  if (_sg_mc_visited > 0 || _sg_mc_liveness  || _sg_mc_termination) {
+  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 */
     MC_ignore_local_variable("e", "*");
     MC_ignore_local_variable("__ex_cleanup", "*");
@@ -209,101 +211,42 @@ void MC_init_pid(pid_t pid, int socket)
 /*******************************  Core of MC *******************************/
 /**************************************************************************/
 
-static void MC_modelcheck_comm_determinism_init(void)
-{
-  MC_init();
-  if (mc_mode == MC_MODE_CLIENT) {
-    // This will move somehwere else:
-    MC_client_handle_messages();
-  }
-
-  xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-
-  /* Create exploration stack */
-  mc_stack = xbt_fifo_new();
-
-  MC_SET_STD_HEAP;
-
-  MC_pre_modelcheck_comm_determinism();
-
-  MC_SET_MC_HEAP;
-  initial_global_state = xbt_new0(s_mc_global_t, 1);
-  initial_global_state->snapshot = MC_take_snapshot(0);
-  initial_global_state->initial_communications_pattern_done = 0;
-  initial_global_state->recv_deterministic = 1;
-  initial_global_state->send_deterministic = 1;
-  initial_global_state->recv_diff = NULL;
-  initial_global_state->send_diff = NULL;
-
-  MC_SET_STD_HEAP;
-
-  MC_modelcheck_comm_determinism();
-
-  mmalloc_set_current_heap(heap);
-}
-
-static void MC_modelcheck_liveness_init()
-{
-  _sg_mc_liveness = 1;
-
-  MC_init();
-  if (mc_mode == MC_MODE_CLIENT) {
-    // This will move somehwere else:
-    MC_client_handle_messages();
-  }
-
-  xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-
-  /* Create exploration stack */
-  mc_stack = xbt_fifo_new();
-
-  /* Create the initial state */
-  initial_global_state = xbt_new0(s_mc_global_t, 1);
-
-  MC_SET_STD_HEAP;
-
-  MC_pre_modelcheck_liveness();
-
-  /* We're done */
-  MC_print_statistics(mc_stats);
-  xbt_free(mc_time);
-
-  mmalloc_set_current_heap(heap);
-
-}
-
 void MC_do_the_modelcheck_for_real()
 {
   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:
+  case MC_MODE_STANDALONE:
+    break;
+  }
+
   if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
     XBT_INFO("Check communication determinism");
     mc_reduce_kind = e_mc_reduce_none;
-    MC_modelcheck_comm_determinism_init();
+    MC_wait_for_requests();
+    MC_modelcheck_comm_determinism();
   }
 
   else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') {
-    if(_sg_mc_termination){
-      XBT_INFO("Check non progressive cycles");
+    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;
-      else {
-        _sg_mc_safety = 1;
-        mc_reduce_kind = e_mc_reduce_dpor;
-        if (mc_mode == MC_MODE_SERVER || mc_mode == MC_MODE_STANDALONE) {
-          XBT_INFO("Check a safety property");
-          MC_modelcheck_safety();
-        }
-        else {
-          // Most of this is not needed:
-          MC_init();
-          // Main event loop:
-          MC_client_main_loop();
-        }
-      }
-    }
+    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 {
@@ -311,8 +254,10 @@ void MC_do_the_modelcheck_for_real()
       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_modelcheck_liveness_init();
+    MC_wait_for_requests();
+    MC_modelcheck_liveness();
   }
+
 }
 
 
@@ -785,7 +730,16 @@ void MC_dump_stacks(FILE* file)
     unw_word_t off;
     do {
       const char * name = !unw_get_proc_name(&c, buffer, 100, &off) ? buffer : "?";
+#if defined(__x86_64__)
+      unw_word_t rip = 0;
+      unw_word_t rsp = 0;
+      unw_get_reg(&c, UNW_X86_64_RIP, &rip);
+      unw_get_reg(&c, UNW_X86_64_RSP, &rsp);
+      fprintf(file, "  %i: %s (RIP=0x%" PRIx64 " RSP=0x%" PRIx64 ")\n",
+        nframe, name, rip, rsp);
+#else
       fprintf(file, "  %i: %s\n", nframe, name);
+#endif
       ++nframe;
     } while(unw_step(&c));