[mc] Cross-process MC/safety implementation

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

diff --git a/src/mc/mc_safety.c b/src/mc/mc_safety.c
index 3dea427..01c1d6b 100644 (file)
--- a/src/mc/mc_safety.c
+++ b/src/mc/mc_safety.c
@@ -12,6 +12,7 @@
 #include "mc_private.h"
 #include "mc_record.h"
 #include "mc_smx.h"
+#include "mc_client.h"
 
 #include "xbt/mmalloc/mmprivate.h"
 
@@ -35,17 +36,14 @@ static int is_exploration_stack_state(mc_state_t current_state){
 /**
  *  \brief Initialize the DPOR exploration algorithm
  */
-void MC_pre_modelcheck_safety()
+static void MC_pre_modelcheck_safety()
 {
-  mc_state_t initial_state = NULL;
-  smx_process_t process;
-
   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 
   if (_sg_mc_visited > 0)
     visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
 
-  initial_state = MC_state_new();
+  mc_state_t initial_state = MC_state_new();
   MC_SET_STD_HEAP;
 
   XBT_DEBUG("**************************************************");
@@ -57,6 +55,7 @@ void MC_pre_modelcheck_safety()
   MC_SET_MC_HEAP;
 
   /* Get an enabled process and insert it in the interleave set of the initial state */
+  smx_process_t process;
   MC_EACH_SIMIX_PROCESS(process,
     if (MC_process_is_enabled(process)) {
       MC_state_interleave_process(initial_state, process);
@@ -73,14 +72,12 @@ void MC_pre_modelcheck_safety()
 /** \brief Model-check the application using a DFS exploration
  *         with DPOR (Dynamic Partial Order Reductions)
  */
-void MC_modelcheck_safety(void)
+static void MC_modelcheck_safety_main(void)
 {
-
   char *req_str = NULL;
   int value;
-  smx_simcall_t req = NULL, prev_req = NULL;
+  smx_simcall_t req = NULL;
   mc_state_t state = NULL, prev_state = NULL, next_state = NULL;
-  smx_process_t process = NULL;
   xbt_fifo_item_t item = NULL;
   mc_visited_state_t visited_state = NULL;
 
@@ -103,8 +100,8 @@ void MC_modelcheck_safety(void)
     if (xbt_fifo_size(mc_stack) <= _sg_mc_max_depth && !user_max_depth_reached
         && (req = MC_state_get_request(state, &value)) && visited_state == NULL) {
 
-      char* req_str = MC_request_to_string(req, value);  
-      XBT_DEBUG("Execute: %s", req_str);                 
+      req_str = MC_request_to_string(req, value, MC_REQUEST_SIMIX);
+      XBT_DEBUG("Execute: %s", req_str);
       xbt_free(req_str);
 
       if (dot_output != NULL) {
@@ -116,10 +113,11 @@ void MC_modelcheck_safety(void)
       MC_state_set_executed_request(state, req, value);
       mc_stats->executed_transitions++;
 
+      // TODO, bundle both operations in a single message
+      //   MC_execute_transition(req, value)
+
       /* Answer the request */
       MC_simcall_handle(req, value);
-
-      /* Wait for requests (schedules processes) */
       MC_wait_for_requests();
 
       /* Create the new expanded state */
@@ -135,6 +133,7 @@ void MC_modelcheck_safety(void)
       if ((visited_state = is_visited_state(next_state)) == NULL) {
 
         /* Get an enabled process and insert it in the interleave set of the next state */
+        smx_process_t process = NULL;
         MC_EACH_SIMIX_PROCESS(process,
           if (MC_process_is_enabled(process)) {
             MC_state_interleave_process(next_state, process);
@@ -184,8 +183,8 @@ void MC_modelcheck_safety(void)
 
       /* Trash the current state, no longer needed */
       xbt_fifo_shift(mc_stack);
-      MC_state_delete(state, !state->in_visited_states ? 1 : 0);
       XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
+      MC_state_delete(state, !state->in_visited_states ? 1 : 0);
 
       MC_SET_STD_HEAP;
 
@@ -213,12 +212,12 @@ void MC_modelcheck_safety(void)
             if (MC_request_depend(req, MC_state_get_internal_request(prev_state))) {
               if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
                 XBT_DEBUG("Dependent Transitions:");
-                prev_req = MC_state_get_executed_request(prev_state, &value);
-                req_str = MC_request_to_string(prev_req, value);
+                smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
+                req_str = MC_request_to_string(prev_req, value, MC_REQUEST_INTERNAL);
                 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
                 xbt_free(req_str);
                 prev_req = MC_state_get_executed_request(state, &value);
-                req_str = MC_request_to_string(prev_req, value);
+                req_str = MC_request_to_string(prev_req, value, MC_REQUEST_EXECUTED);
                 XBT_DEBUG("%s (state=%d)", req_str, state->num);
                 xbt_free(req_str);
               }
@@ -268,3 +267,33 @@ void MC_modelcheck_safety(void)
 
   return;
 }
+
+void MC_modelcheck_safety(void)
+{
+  XBT_DEBUG("Starting the safety algorithm");
+  xbt_assert(mc_mode == MC_MODE_SERVER);
+
+  _sg_mc_safety = 1;
+
+  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_safety();
+
+  MC_SET_MC_HEAP;
+  /* Save the initial state */
+  initial_global_state = xbt_new0(s_mc_global_t, 1);
+  initial_global_state->snapshot = MC_take_snapshot(0);
+  MC_SET_STD_HEAP;
+
+  MC_modelcheck_safety_main();
+
+  mmalloc_set_current_heap(heap);
+
+  xbt_abort();
+  //MC_exit();
+}