[mc] Move liveness in MCer process

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

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 10f95d2..690ca5a 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", "*");
@@ -242,76 +244,54 @@ static void MC_modelcheck_comm_determinism_init(void)
   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();
 
   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();
+    // TODO, move this part in the MCer process
+    if (mc_mode == MC_MODE_SERVER)
+      MC_server_loop(mc_server);
+    else {
+      XBT_INFO("Check communication determinism");
+      mc_reduce_kind = e_mc_reduce_none;
+      MC_modelcheck_comm_determinism_init();
+    }
   }
 
   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 (mc_mode == MC_MODE_SERVER || mc_mode == MC_MODE_STANDALONE) {
+      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 {
+      // 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_none;
-    XBT_INFO("Check the liveness property %s", _sg_mc_property_file);
-    MC_automaton_load(_sg_mc_property_file);
-    MC_modelcheck_liveness_init();
+    if (mc_mode == MC_MODE_SERVER || mc_mode == MC_MODE_STANDALONE) {
+      XBT_INFO("Check the liveness property %s", _sg_mc_property_file);
+      MC_automaton_load(_sg_mc_property_file);
+      MC_modelcheck_liveness();
+    } else {
+      MC_init();
+      MC_client_main_loop();
+    }
   }
 }
 
@@ -766,6 +746,7 @@ void MC_automaton_new_propositional_symbol_callback(const char* id,
   mmalloc_set_current_heap(heap);
 }
 
+// TODO, fix cross-process access (this function is not used)
 void MC_dump_stacks(FILE* file)
 {
   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
@@ -784,7 +765,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));