Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : intermediate backtracking with model-check/checkpoint cfg flag
authorMarion Guthmuller <marion.guthmuller@inria.fr>
Mon, 9 Feb 2015 18:37:14 +0000 (19:37 +0100)
committerMarion Guthmuller <marion.guthmuller@inria.fr>
Mon, 9 Feb 2015 18:40:38 +0000 (19:40 +0100)
src/mc/mc_global.c
src/mc/mc_pair.c
src/mc/mc_private.h
src/mc/mc_safety.c
src/mc/mc_safety.h
src/mc/mc_state.c
src/mc/mc_state.h
src/mc/mc_visited.c

index 3776138..81c594f 100644 (file)
@@ -441,63 +441,45 @@ static void MC_restore_communications_pattern(mc_state_t state) {
  *        a given model-checker stack.
  * \param stack The stack with the transitions to execute.
  * \param start Start index to begin the re-execution.
- *
- *  If start==-1, restore the initial state and replay the actions the
- *  the transitions in the stack.
- *
- *  Otherwise, we only replay a part of the transitions of the stacks
- *  without restoring the state: it is assumed that the current state
- *  match with the transitions to execute.
  */
-void MC_replay(xbt_fifo_t stack, int start)
+void MC_replay(xbt_fifo_t stack)
 {
   int raw_mem = (mmalloc_get_current_heap() == mc_heap);
 
-  int value, i = 1, count = 1, j;
+  int value, count = 1, j;
   char *req_str;
   smx_simcall_t req = NULL, saved_req = NULL;
   xbt_fifo_item_t item, start_item;
   mc_state_t state;
-  smx_process_t process = NULL;
-
+  
   XBT_DEBUG("**** Begin Replay ****");
 
-  if (start == -1) {
-    /* Restore the initial state */
-    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  */
+  /* Intermediate backtracking */
+  start_item = xbt_fifo_get_first_item(stack);
+  state = (mc_state_t)xbt_fifo_get_item_content(start_item);
+  if(state->system_state){
+    MC_restore_snapshot(state->system_state);
+    if(_sg_mc_comms_determinism || _sg_mc_send_determinism) 
+      MC_restore_communications_pattern(state);
     MC_SET_STD_HEAP;
+    return;
   }
 
-  start_item = xbt_fifo_get_last_item(stack);
-  if (start != -1) {
-    while (i != start) {
-      start_item = xbt_fifo_get_prev_item(start_item);
-      i++;
-    }
-  }
 
-  MC_SET_MC_HEAP;
+  /* Restore the initial state */
+  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;
 
-  if (mc_reduce_kind == e_mc_reduce_dpor) {
-    xbt_dict_reset(first_enabled_state);
-    xbt_swag_foreach(process, simix_global->process_list) {
-      if (MC_process_is_enabled(process)) {
-        char *key = bprintf("%lu", process->pid);
-        char *data = bprintf("%d", count);
-        xbt_dict_set(first_enabled_state, key, data, NULL);
-        xbt_free(key);
-      }
-    }
-  }
+  start_item = xbt_fifo_get_last_item(stack);
+  
+  MC_SET_MC_HEAP;
 
   if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
-    for (j=0; j<simix_process_maxpid; j++) {
-      xbt_dynar_reset((xbt_dynar_t)xbt_dynar_get_as(communications_pattern, j, xbt_dynar_t));
-    }
     for (j=0; j<simix_process_maxpid; j++) {
       xbt_dynar_reset((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, j, xbt_dynar_t));
+      ((mc_list_comm_pattern_t)xbt_dynar_get_as(initial_communications_pattern, j, mc_list_comm_pattern_t))->index_comm = 0;
     }
   }
 
@@ -510,16 +492,7 @@ void MC_replay(xbt_fifo_t stack, int start)
 
     state = (mc_state_t) xbt_fifo_get_item_content(item);
     saved_req = MC_state_get_executed_request(state, &value);
-
-    if (mc_reduce_kind == e_mc_reduce_dpor) {
-      MC_SET_MC_HEAP;
-      char *key = bprintf("%lu", saved_req->issuer->pid);
-      if(xbt_dict_get_or_null(first_enabled_state, key))
-         xbt_dict_remove(first_enabled_state, key);
-      xbt_free(key);
-      MC_SET_STD_HEAP;
-    }
-
+    
     if (saved_req) {
       /* because we got a copy of the executed request, we have to fetch the  
          real one, pointed by the request field of the issuer process */
@@ -533,38 +506,20 @@ void MC_replay(xbt_fifo_t stack, int start)
       }
 
       /* TODO : handle test and testany simcalls */
-      mc_call_type call = MC_CALL_TYPE_NONE;
-      if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
+      e_mc_call_type_t call = MC_CALL_TYPE_NONE;
+      if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
         call = mc_get_call_type(req);
-      }
 
       SIMIX_simcall_handle(req, value);
 
-      if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
-        MC_SET_MC_HEAP;
-        mc_update_comm_pattern(call, req, value, communications_pattern);
-        MC_SET_STD_HEAP;
-      }
-
+      MC_SET_MC_HEAP;
+      if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
+        handle_comm_pattern(call, req, value, NULL, 1);
+      MC_SET_STD_HEAP;
+      
       MC_wait_for_requests();
 
       count++;
-
-      if (mc_reduce_kind == e_mc_reduce_dpor) {
-        MC_SET_MC_HEAP;
-        /* Insert in dict all enabled processes */
-        xbt_swag_foreach(process, simix_global->process_list) {
-          if (MC_process_is_enabled(process) ) {
-            char *key = bprintf("%lu", process->pid);
-            if (xbt_dict_get_or_null(first_enabled_state, key) == NULL) {
-              char *data = bprintf("%d", count);
-              xbt_dict_set(first_enabled_state, key, data, NULL);
-            }
-            xbt_free(key);
-          }
-        }
-        MC_SET_STD_HEAP;
-      }
     }
 
     /* Update statistics */
@@ -583,16 +538,29 @@ void MC_replay(xbt_fifo_t stack, int start)
 
 }
 
-void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
+void MC_replay_liveness(xbt_fifo_t stack)
 {
 
   initial_global_state->raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
 
   xbt_fifo_item_t item;
-  int depth = 1;
+  mc_pair_t pair = NULL;
+  mc_state_t state = NULL;
+  smx_simcall_t req = NULL, saved_req = NULL;
+  int value, depth = 1;
+  char *req_str;
 
   XBT_DEBUG("**** Begin Replay ****");
 
+  /* Intermediate backtracking */
+  item = xbt_fifo_get_first_item(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;
+    return;
+  }
+
   /* Restore the initial state */
   MC_restore_snapshot(initial_global_state->snapshot);
 
@@ -603,26 +571,21 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
 
     /* Traverse the stack from the initial state and re-execute the transitions */
     for (item = xbt_fifo_get_last_item(stack);
-         all_stack ? depth <= xbt_fifo_size(stack) : item != xbt_fifo_get_first_item(stack);
+         item != xbt_fifo_get_first_item(stack);
          item = xbt_fifo_get_prev_item(item)) {
 
-      mc_pair_t pair = (mc_pair_t) xbt_fifo_get_item_content(item);
+      pair = (mc_pair_t) xbt_fifo_get_item_content(item);
 
-      mc_state_t state = (mc_state_t) pair->graph_state;
-      smx_simcall_t req = NULL, saved_req = NULL;
-      int value;
-      char *req_str;
+      state = (mc_state_t) pair->graph_state;
 
-      if (pair->requests > 0) {
+      if (pair->exploration_started) {
 
         saved_req = MC_state_get_executed_request(state, &value);
-        //XBT_DEBUG("SavedReq->call %u", saved_req->call);
 
         if (saved_req != NULL) {
           /* because we got a copy of the executed request, we have to fetch the
              real one, pointed by the request field of the issuer process */
           req = &saved_req->issuer->simcall;
-          //XBT_DEBUG("Req->call %u", req->call);
 
           /* Debug information */
           if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) {
@@ -642,7 +605,7 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
       mc_stats->executed_transitions++;
 
       depth++;
-
+      
     }
 
   XBT_DEBUG("**** End Replay ****");
@@ -665,17 +628,13 @@ void MC_dump_stack_safety(xbt_fifo_t stack)
   int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
 
   MC_show_stack_safety(stack);
-
-  if (!_sg_mc_checkpoint) {
-
-    mc_state_t state;
-
-    MC_SET_MC_HEAP;
-    while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
-      MC_state_delete(state);
-    MC_SET_STD_HEAP;
-
-  }
+  
+  mc_state_t state;
+  
+  MC_SET_MC_HEAP;
+  while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
+    MC_state_delete(state, !state->in_visited_states ? 1 : 0);
+  MC_SET_STD_HEAP;
 
   if (raw_mem_set)
     MC_SET_MC_HEAP;
@@ -738,21 +697,18 @@ void MC_show_stack_liveness(xbt_fifo_t stack)
   char *req_str = NULL;
 
   for (item = xbt_fifo_get_last_item(stack);
-       (item ? (pair = (mc_pair_t) (xbt_fifo_get_item_content(item)))
-        : (NULL)); item = xbt_fifo_get_prev_item(item)) {
+       (item ? (pair = (mc_pair_t) (xbt_fifo_get_item_content(item))) : (NULL));
+       item = xbt_fifo_get_prev_item(item)) {
     req = MC_state_get_executed_request(pair->graph_state, &value);
-    if (req) {
-      if (pair->requests > 0) {
-        req_str = MC_request_to_string(req, value);
-        XBT_INFO("%s", req_str);
-        xbt_free(req_str);
-      } else {
-        XBT_INFO("End of system requests but evolution in B├╝chi automaton");
-      }
+    if (req && req->call != SIMCALL_NONE) {
+      req_str = MC_request_to_string(req, value);
+      XBT_INFO("%s", req_str);
+      xbt_free(req_str);
     }
   }
 }
 
+
 void MC_dump_stack_liveness(xbt_fifo_t stack)
 {
 
index 62e1f38..fa023f1 100644 (file)
@@ -13,14 +13,16 @@ mc_pair_t MC_pair_new()
   mc_pair_t p = NULL;
   p = xbt_new0(s_mc_pair_t, 1);
   p->num = ++mc_stats->expanded_pairs;
+  p->exploration_started = 0;
   p->search_cycle = 0;
+  p->visited_pair_removed = _sg_mc_visited > 0 ? 0 : 1;
   return p;
 }
 
 void MC_pair_delete(mc_pair_t p)
 {
   p->automaton_state = NULL;
-  MC_state_delete(p->graph_state);
+  MC_state_delete(p->graph_state, p->visited_pair_removed);
   xbt_dynar_free(&(p->atomic_propositions));
   xbt_free(p);
   p = NULL;
index 9e3d9ca..4a86245 100644 (file)
@@ -51,8 +51,8 @@ extern xbt_parmap_t parmap;
 extern int user_max_depth_reached;
 
 int MC_deadlock_check(void);
-void MC_replay(xbt_fifo_t stack, int start);
-void MC_replay_liveness(xbt_fifo_t stack, int all_stack);
+void MC_replay(xbt_fifo_t stack);
+void MC_replay_liveness(xbt_fifo_t stack);
 void MC_show_deadlock(smx_simcall_t req);
 void MC_show_stack_safety(xbt_fifo_t stack);
 void MC_dump_stack_safety(xbt_fifo_t stack);
@@ -141,15 +141,6 @@ bool mc_address_test(mc_address_set_t p, const void* value);
  * */
 uint64_t mc_hash_processes_state(int num_state, xbt_dynar_t stacks);
 
-/* *********** Snapshot *********** */
-
-#define MC_LOG_REQUEST(log, req, value) \
-  if (XBT_LOG_ISENABLED(log, xbt_log_priority_debug)) { \
-    char* req_str = MC_request_to_string(req, value); \
-    XBT_DEBUG("Execute: %s", req_str); \
-    xbt_free(req_str); \
-  }
-
 /** @brief Dump the stacks of the application processes
  *
  *   This functions is currently not used but it is quite convenient
index 658c185..83460ff 100644 (file)
@@ -15,8 +15,6 @@
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
                                 "Logging specific to MC safety verification ");
 
-xbt_dict_t first_enabled_state;
-
 /**
  *  \brief Initialize the DPOR exploration algorithm
  */
@@ -33,11 +31,7 @@ void MC_pre_modelcheck_safety()
     MC_SET_MC_HEAP;
 
   if (_sg_mc_visited > 0)
-    visited_states =
-        xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
-
-  if (mc_reduce_kind == e_mc_reduce_dpor)
-    first_enabled_state = xbt_dict_new_homogeneous(&xbt_free_f);
+    visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
 
   initial_state = MC_state_new();
 
@@ -62,21 +56,6 @@ void MC_pre_modelcheck_safety()
 
   xbt_fifo_unshift(mc_stack, initial_state);
 
-  if (mc_reduce_kind == e_mc_reduce_dpor) {
-    /* To ensure the soundness of DPOR, we have to keep a list of 
-       processes which are still enabled at each step of the exploration. 
-       If max depth is reached, we interleave them in the state in which they have 
-       been enabled for the first time. */
-    xbt_swag_foreach(process, simix_global->process_list) {
-      if (MC_process_is_enabled(process)) {
-        char *key = bprintf("%lu", process->pid);
-        char *data = bprintf("%d", xbt_fifo_size(mc_stack));
-        xbt_dict_set(first_enabled_state, key, data, NULL);
-        xbt_free(key);
-      }
-    }
-  }
-
   if (!mc_mem_set)
     MC_SET_STD_HEAP;
 }
@@ -91,27 +70,21 @@ void MC_modelcheck_safety(void)
   char *req_str = NULL;
   int value;
   smx_simcall_t req = NULL, prev_req = NULL;
-  mc_state_t state = NULL, prev_state = NULL, next_state =
-      NULL, restored_state = NULL;
+  mc_state_t state = NULL, prev_state = NULL, next_state = NULL;
   smx_process_t process = NULL;
   xbt_fifo_item_t item = NULL;
-  mc_state_t state_test = NULL;
-  int pos;
   mc_visited_state_t visited_state = NULL;
-  int enabled = 0;
 
   while (xbt_fifo_size(mc_stack) > 0) {
 
     /* Get current state */
-    state = (mc_state_t)
-        xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
+    state = (mc_state_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
 
     XBT_DEBUG("**************************************************");
     XBT_DEBUG
-        ("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d, first_enabled_state size : %d)",
+        ("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d)",
          xbt_fifo_size(mc_stack), state, state->num,
-         MC_state_interleave_size(state), user_max_depth_reached,
-         xbt_dict_size(first_enabled_state));
+         MC_state_interleave_size(state), user_max_depth_reached);
 
     /* Update statistics */
     mc_stats->visited_states++;
@@ -121,7 +94,9 @@ 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) {
 
-      MC_LOG_REQUEST(mc_safety, req, value);
+      char* req_str = MC_request_to_string(req, value);  
+      XBT_DEBUG("Execute: %s", req_str);                 
+      xbt_free(req_str);
 
       if (dot_output != NULL) {
         MC_SET_MC_HEAP;
@@ -132,14 +107,6 @@ void MC_modelcheck_safety(void)
       MC_state_set_executed_request(state, req, value);
       mc_stats->executed_transitions++;
 
-      if (mc_reduce_kind == e_mc_reduce_dpor) {
-        MC_SET_MC_HEAP;
-        char *key = bprintf("%lu", req->issuer->pid);
-        xbt_dict_remove(first_enabled_state, key);
-        xbt_free(key);
-        MC_SET_STD_HEAP;
-      }
-
       /* Answer the request */
       SIMIX_simcall_handle(req, value);
 
@@ -151,7 +118,7 @@ void MC_modelcheck_safety(void)
 
       next_state = MC_state_new();
 
-      if ((visited_state = is_visited_state()) == NULL) {
+      if ((visited_state = is_visited_state(next_state)) == NULL) {
 
         /* Get an enabled process and insert it in the interleave set of the next state */
         xbt_swag_foreach(process, simix_global->process_list) {
@@ -162,39 +129,18 @@ void MC_modelcheck_safety(void)
           }
         }
 
-        if (_sg_mc_checkpoint
-            && ((xbt_fifo_size(mc_stack) + 1) % _sg_mc_checkpoint == 0)) {
-          next_state->system_state = MC_take_snapshot(next_state->num);
-        }
-
         if (dot_output != NULL)
-          fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
-                  next_state->num, req_str);
+          fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
 
       } else {
 
         if (dot_output != NULL)
-          fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,
-                  visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
+          fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
 
       }
 
       xbt_fifo_unshift(mc_stack, next_state);
 
-      if (mc_reduce_kind == e_mc_reduce_dpor) {
-        /* Insert in dict all enabled processes, if not included yet */
-        xbt_swag_foreach(process, simix_global->process_list) {
-          if (MC_process_is_enabled(process)) {
-            char *key = bprintf("%lu", process->pid);
-            if (xbt_dict_get_or_null(first_enabled_state, key) == NULL) {
-              char *data = bprintf("%d", xbt_fifo_size(mc_stack));
-              xbt_dict_set(first_enabled_state, key, data, NULL);
-            }
-            xbt_free(key);
-          }
-        }
-      }
-
       if (dot_output != NULL)
         xbt_free(req_str);
 
@@ -205,8 +151,7 @@ void MC_modelcheck_safety(void)
       /* The interleave set is empty or the maximum depth is reached, let's back-track */
     } else {
 
-      if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached
-          || visited_state != NULL) {
+      if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != NULL) {
 
         if (user_max_depth_reached && visited_state == NULL)
           XBT_DEBUG("User max depth reached !");
@@ -215,35 +160,9 @@ void MC_modelcheck_safety(void)
         else
           XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num);
 
-        if (mc_reduce_kind == e_mc_reduce_dpor) {
-          /* Interleave enabled processes in the state in which they have been enabled for the first time */
-          xbt_swag_foreach(process, simix_global->process_list) {
-            if (MC_process_is_enabled(process)) {
-              char *key = bprintf("%lu", process->pid);
-              enabled =
-                  (int) strtoul(xbt_dict_get_or_null(first_enabled_state, key),
-                                0, 10);
-              xbt_free(key);
-              int cursor = xbt_fifo_size(mc_stack);
-              xbt_fifo_foreach(mc_stack, item, state_test, mc_state_t) {
-                if (cursor-- == enabled) {
-                  if (!MC_state_process_is_done(state_test, process)
-                      && state_test->num != state->num) {
-                    XBT_DEBUG("Interleave process %lu in state %d",
-                              process->pid, state_test->num);
-                    MC_state_interleave_process(state_test, process);
-                    break;
-                  }
-                }
-              }
-            }
-          }
-        }
-
       } else {
 
-        XBT_DEBUG("There are no more processes to interleave. (depth %d)",
-                  xbt_fifo_size(mc_stack) + 1);
+        XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack) + 1);
 
       }
 
@@ -251,9 +170,8 @@ void MC_modelcheck_safety(void)
 
       /* Trash the current state, no longer needed */
       xbt_fifo_shift(mc_stack);
-      MC_state_delete(state);
-      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);
+      XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
 
       MC_SET_STD_HEAP;
 
@@ -277,8 +195,7 @@ void MC_modelcheck_safety(void)
         if (mc_reduce_kind == e_mc_reduce_dpor) {
           req = MC_state_get_internal_request(state);
           xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
-            if (MC_request_depend
-                (req, MC_state_get_internal_request(prev_state))) {
+            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);
@@ -298,65 +215,33 @@ void MC_modelcheck_safety(void)
 
               break;
 
-            } else if (req->issuer ==
-                       MC_state_get_internal_request(prev_state)->issuer) {
+            } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) {
 
-              XBT_DEBUG("Simcall %d and %d with same issuer", req->call,
-                        MC_state_get_internal_request(prev_state)->call);
+              XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call);
               break;
 
             } else {
 
-              XBT_DEBUG
-                  ("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
-                   req->call, req->issuer->pid, state->num,
-                   MC_state_get_internal_request(prev_state)->call,
-                   MC_state_get_internal_request(prev_state)->issuer->pid,
-                   prev_state->num);
+              XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
+                        req->call, req->issuer->pid, state->num,
+                        MC_state_get_internal_request(prev_state)->call,
+                        MC_state_get_internal_request(prev_state)->issuer->pid,
+                        prev_state->num);
 
             }
           }
         }
 
-        if (MC_state_interleave_size(state)
-            && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
+        if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
           /* We found a back-tracking point, let's loop */
-          XBT_DEBUG("Back-tracking to state %d at depth %d", state->num,
-                    xbt_fifo_size(mc_stack) + 1);
-          if (_sg_mc_checkpoint) {
-            if (state->system_state != NULL) {
-              MC_restore_snapshot(state->system_state);
-              xbt_fifo_unshift(mc_stack, state);
-              MC_SET_STD_HEAP;
-            } else {
-              pos = xbt_fifo_size(mc_stack);
-              item = xbt_fifo_get_first_item(mc_stack);
-              while (pos > 0) {
-                restored_state = (mc_state_t) xbt_fifo_get_item_content(item);
-                if (restored_state->system_state != NULL) {
-                  break;
-                } else {
-                  item = xbt_fifo_get_next_item(item);
-                  pos--;
-                }
-              }
-              MC_restore_snapshot(restored_state->system_state);
-              xbt_fifo_unshift(mc_stack, state);
-              MC_SET_STD_HEAP;
-              MC_replay(mc_stack, pos);
-            }
-          } else {
-            xbt_fifo_unshift(mc_stack, state);
-            MC_SET_STD_HEAP;
-            MC_replay(mc_stack, -1);
-          }
-          XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num,
-                    xbt_fifo_size(mc_stack));
+          XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
+          xbt_fifo_unshift(mc_stack, state);
+          MC_replay(mc_stack);
+          XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack));
           break;
         } else {
-          XBT_DEBUG("Delete state %d at depth %d", state->num,
-                    xbt_fifo_size(mc_stack) + 1);
-          MC_state_delete(state);
+          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;
index b8aa3b4..183ebac 100644 (file)
@@ -12,6 +12,7 @@
 #include <simgrid_config.h>
 #include <xbt/dict.h>
 #include "mc_interface.h"
+#include "mc_state.h"
 
 SG_BEGIN_DECL()
 
@@ -22,7 +23,6 @@ typedef enum {
 } e_mc_reduce_t;
 
 extern e_mc_reduce_t mc_reduce_kind;
-extern xbt_dict_t first_enabled_state;
 
 void MC_pre_modelcheck_safety(void);
 void MC_modelcheck_safety(void);
@@ -36,7 +36,7 @@ typedef struct s_mc_visited_state{
 }s_mc_visited_state_t, *mc_visited_state_t;
 
 extern xbt_dynar_t visited_states;
-mc_visited_state_t is_visited_state(void);
+mc_visited_state_t is_visited_state(mc_state_t graph_state);
 void visited_state_free(mc_visited_state_t state);
 void visited_state_free_voidp(void *s);
 
index 1f3abce..84db3e8 100644 (file)
@@ -68,7 +68,16 @@ mc_state_t MC_state_new()
   state->proc_status = xbt_new0(s_mc_procstate_t, state->max_pid);
   state->system_state = NULL;
   state->num = ++mc_stats->expanded_states;
-
+  state->in_visited_states = 0;
+  state->incomplete_comm_pattern = NULL;
+  /* Stateful model checking */
+  if(_sg_mc_checkpoint > 0 && mc_stats->expanded_states % _sg_mc_checkpoint == 0){
+    state->system_state = MC_take_snapshot(state->num);
+    if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
+      copy_incomplete_communications_pattern(state);
+      copy_index_communications_pattern(state);
+    }
+  }
   return state;
 }
 
@@ -76,10 +85,14 @@ mc_state_t MC_state_new()
  * \brief Deletes a state data structure
  * \param trans The state to be deleted
  */
-void MC_state_delete(mc_state_t state)
-{
-  if (state->system_state)
+void MC_state_delete(mc_state_t state, int free_snapshot){
+  if (state->system_state && free_snapshot){
     MC_free_snapshot(state->system_state);
+  }
+  if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
+    xbt_free(state->index_comm);
+    xbt_free(state->incomplete_comm_pattern);
+  }
   xbt_free(state->proc_status);
   xbt_free(state);
 }
index 1bc0316..863a21a 100644 (file)
@@ -46,10 +46,13 @@ typedef struct mc_state {
                                        multi-request like waitany ) */
   mc_snapshot_t system_state;      /* Snapshot of system state */
   int num;
+  int in_visited_states;
+  xbt_dynar_t incomplete_comm_pattern; // comm determinism verification
+  xbt_dynar_t index_comm; // comm determinism verification
 } s_mc_state_t, *mc_state_t;
 
 mc_state_t MC_state_new(void);
-void MC_state_delete(mc_state_t state);
+void MC_state_delete(mc_state_t state, int free_snapshot);
 void MC_state_interleave_process(mc_state_t state, smx_process_t process);
 unsigned int MC_state_interleave_size(mc_state_t state);
 int MC_state_process_is_done(mc_state_t state, smx_process_t process);
index 0c3c971..765a48a 100644 (file)
@@ -18,10 +18,24 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_visited, mc,
 xbt_dynar_t visited_pairs;
 xbt_dynar_t visited_states;
 
+static int is_exploration_stack_state(mc_visited_state_t state){
+  xbt_fifo_item_t item = xbt_fifo_get_last_item(mc_stack);
+  while (item) {
+    if (((mc_state_t)xbt_fifo_get_item_content(item))->num == state->num){
+      ((mc_state_t)xbt_fifo_get_item_content(item))->in_visited_states = 0;
+      return 1;
+    }
+    item = xbt_fifo_get_prev_item(item);
+  }
+  return 0;
+}
+
 void visited_state_free(mc_visited_state_t state)
 {
   if (state) {
-    MC_free_snapshot(state->system_state);
+    if(!is_exploration_stack_state(state)){
+      MC_free_snapshot(state->system_state);
+    }
     xbt_free(state);
   }
 }
@@ -47,15 +61,12 @@ static mc_visited_state_t visited_state_new()
   return new_state;
 }
 
-
-mc_visited_pair_t MC_visited_pair_new(int pair_num,
-                                      xbt_automaton_state_t automaton_state,
-                                      xbt_dynar_t atomic_propositions)
+mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_snapshot_t system_state)
 {
   mc_visited_pair_t pair = NULL;
   pair = xbt_new0(s_mc_visited_pair_t, 1);
   pair->graph_state = MC_state_new();
-  pair->graph_state->system_state = MC_take_snapshot(pair_num);
+  pair->graph_state->system_state = (system_state == NULL) ? MC_take_snapshot(pair_num) : system_state;
   pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
   pair->nb_processes = xbt_swag_size(simix_global->process_list);
   pair->automaton_state = automaton_state;
@@ -64,6 +75,7 @@ mc_visited_pair_t MC_visited_pair_new(int pair_num,
   pair->acceptance_removed = 0;
   pair->visited_removed = 0;
   pair->acceptance_pair = 0;
+  pair->in_exploration_stack = 1;
   pair->atomic_propositions = xbt_dynar_new(sizeof(int), NULL);
   unsigned int cursor = 0;
   int value;
@@ -72,10 +84,22 @@ mc_visited_pair_t MC_visited_pair_new(int pair_num,
   return pair;
 }
 
+static int is_exploration_stack_pair(mc_visited_pair_t pair){
+  xbt_fifo_item_t item = xbt_fifo_get_last_item(mc_stack);
+  while (item) {
+    if (((mc_pair_t)xbt_fifo_get_item_content(item))->num == pair->num){
+      ((mc_pair_t)xbt_fifo_get_item_content(item))->visited_pair_removed = 1;
+      return 1;
+    }
+    item = xbt_fifo_get_prev_item(item);
+  }
+  return 0;
+}
+
 void MC_visited_pair_delete(mc_visited_pair_t p)
 {
   p->automaton_state = NULL;
-  MC_state_delete(p->graph_state);
+  MC_state_delete(p->graph_state, !is_exploration_stack_pair(p));
   xbt_dynar_free(&(p->atomic_propositions));
   xbt_free(p);
   p = NULL;
@@ -122,14 +146,11 @@ int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
   while (start <= end) {
     cursor = (start + end) / 2;
     if (_sg_mc_liveness) {
-      ref_test =
-        (mc_visited_pair_t) xbt_dynar_get_as(list, cursor, mc_visited_pair_t);
+      ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, cursor, mc_visited_pair_t);
       nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
       heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
     } else {
-      ref_test =
-        (mc_visited_state_t) xbt_dynar_get_as(list, cursor,
-                                              mc_visited_state_t);
+      ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, cursor, mc_visited_state_t);
       nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
       heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
     }
@@ -147,22 +168,15 @@ int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
         previous_cursor = cursor - 1;
         while (previous_cursor >= 0) {
           if (_sg_mc_liveness) {
-            ref_test =
-              (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor,
-                                                   mc_visited_pair_t);
+            ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor, mc_visited_pair_t);
             nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
-            heap_bytes_used_test =
-              ((mc_visited_pair_t) ref_test)->heap_bytes_used;
+            heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
           } else {
-            ref_test =
-                (mc_visited_state_t) xbt_dynar_get_as(list, previous_cursor,
-                                                      mc_visited_state_t);
+            ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, previous_cursor, mc_visited_state_t);
             nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
-            heap_bytes_used_test =
-                ((mc_visited_state_t) ref_test)->heap_bytes_used;
+            heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
           }
-          if (nb_processes_test != nb_processes
-              || heap_bytes_used_test != heap_bytes_used)
+          if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
             break;
           *min = previous_cursor;
           previous_cursor--;
@@ -170,22 +184,15 @@ int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
         next_cursor = cursor + 1;
         while (next_cursor < xbt_dynar_length(list)) {
           if (_sg_mc_liveness) {
-            ref_test =
-                (mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor,
-                                                     mc_visited_pair_t);
+            ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor, mc_visited_pair_t);
             nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
-            heap_bytes_used_test =
-                ((mc_visited_pair_t) ref_test)->heap_bytes_used;
+            heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
           } else {
-            ref_test =
-              (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor,
-                                                    mc_visited_state_t);
+            ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor, mc_visited_state_t);
             nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
-            heap_bytes_used_test =
-              ((mc_visited_state_t) ref_test)->heap_bytes_used;
+            heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
           }
-          if (nb_processes_test != nb_processes
-              || heap_bytes_used_test != heap_bytes_used)
+          if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
             break;
           *max = next_cursor;
           next_cursor++;
@@ -236,6 +243,9 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
   MC_SET_MC_HEAP;
 
   mc_visited_state_t new_state = visited_state_new();
+  graph_state->system_state = new_state->system_state;
+  graph_state->in_visited_states = 1;
+  XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", new_state->system_state, new_state->num, graph_state->num);
 
   if (xbt_dynar_is_empty(visited_states)) {
 
@@ -276,48 +286,45 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
          return new_state->other_num;
          } */
 
-      cursor = min;
-      while (cursor <= max) {
-        state_test =
-            (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor,
-                                                  mc_visited_state_t);
-        if (snapshot_compare(state_test, new_state) == 0) {
-          // The state has been visited:
-
-          if (state_test->other_num == -1)
-            new_state->other_num = state_test->num;
-          else
-            new_state->other_num = state_test->other_num;
-          if (dot_output == NULL)
-            XBT_DEBUG("State %d already visited ! (equal to state %d)",
-                      new_state->num, state_test->num);
-          else
-            XBT_DEBUG
-                ("State %d already visited ! (equal to state %d (state %d in dot_output))",
-                 new_state->num, state_test->num, new_state->other_num);
-
-          /* Replace the old state with the new one (with a bigger num) 
-             (when the max number of visited states is reached,  the oldest 
-             one is removed according to its number (= with the min number) */
-          xbt_dynar_remove_at(visited_states, cursor, NULL);
-          xbt_dynar_insert_at(visited_states, cursor, &new_state);
-
-          if (!mc_mem_set)
-            MC_SET_STD_HEAP;
-          return state_test;
+      if(!partial_comm && initial_global_state->initial_communications_pattern_done){
+
+        cursor = min;
+        while (cursor <= max) {
+          state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
+          if (snapshot_compare(state_test, new_state) == 0) {
+            // The state has been visited:
+
+            if (state_test->other_num == -1)
+              new_state->other_num = state_test->num;
+            else
+              new_state->other_num = state_test->other_num;
+            if (dot_output == NULL)
+              XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
+            else
+              XBT_DEBUG("State %d already visited ! (equal to state %d (state %d in dot_output))", new_state->num, state_test->num, new_state->other_num);
+
+            /* Replace the old state with the new one (with a bigger num) 
+               (when the max number of visited states is reached,  the oldest 
+               one is removed according to its number (= with the min number) */
+            xbt_dynar_remove_at(visited_states, cursor, NULL);
+            xbt_dynar_insert_at(visited_states, cursor, &new_state);
+            XBT_DEBUG("Replace visited state %d with the new visited state %d", state_test->num, new_state->num);
+
+            if (!mc_mem_set)
+              MC_SET_STD_HEAP;
+            return state_test;
+          }
+          cursor++;
         }
-        cursor++;
       }
-
-      // The state has not been visited: insert the state in the dynamic array.
+      
       xbt_dynar_insert_at(visited_states, min, &new_state);
-
+      XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
+      
     } else {
 
       // The state has not been visited: insert the state in the dynamic array.
-      state_test =
-          (mc_visited_state_t) xbt_dynar_get_as(visited_states, index,
-                                                mc_visited_state_t);
+      state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, index, mc_visited_state_t);
       if (state_test->nb_processes < new_state->nb_processes) {
         xbt_dynar_insert_at(visited_states, index + 1, &new_state);
       } else {
@@ -327,11 +334,15 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
           xbt_dynar_insert_at(visited_states, index, &new_state);
       }
 
+       XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
+
     }
 
     // We have reached the maximum number of stored states;
     if (xbt_dynar_length(visited_states) > _sg_mc_visited) {
 
+      XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)");
+
       // Find the (index of the) older state (with the smallest num):
       int min2 = mc_stats->expanded_states;
       unsigned int cursor2 = 0;
@@ -345,6 +356,7 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
 
       // and drop it:
       xbt_dynar_remove_at(visited_states, index2, NULL);
+      XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
     }
 
     if (!mc_mem_set)
@@ -358,10 +370,7 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
 /**
  * \brief Checks whether a given pair has already been visited by the algorithm.
  */
-int is_visited_pair(mc_visited_pair_t pair, int pair_num,
-                    xbt_automaton_state_t automaton_state,
-                    xbt_dynar_t atomic_propositions)
-{
+int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
 
   if (_sg_mc_visited == 0)
     return -1;
@@ -370,18 +379,17 @@ int is_visited_pair(mc_visited_pair_t pair, int pair_num,
 
   MC_SET_MC_HEAP;
 
-  mc_visited_pair_t new_pair = NULL;
+  mc_visited_pair_t new_visited_pair = NULL;
 
-  if (pair == NULL) {
-    new_pair =
-        MC_visited_pair_new(pair_num, automaton_state, atomic_propositions);
+  if (visited_pair == NULL) {
+    new_visited_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state->system_state);
   } else {
-    new_pair = pair;
+    new_visited_pair = visited_pair;
   }
 
   if (xbt_dynar_is_empty(visited_pairs)) {
 
-    xbt_dynar_push(visited_pairs, &new_pair);
+    xbt_dynar_push(visited_pairs, &new_visited_pair);
 
   } else {
 
@@ -390,7 +398,7 @@ int is_visited_pair(mc_visited_pair_t pair, int pair_num,
     mc_visited_pair_t pair_test;
     int cursor;
 
-    index = get_search_interval(visited_pairs, new_pair, &min, &max);
+    index = get_search_interval(visited_pairs, new_visited_pair, &min, &max);
 
     if (min != -1 && max != -1) {       // Visited pair with same number of processes and same heap bytes used exists
       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_pairs, min), (max-min)+1, pair);
@@ -422,28 +430,20 @@ int is_visited_pair(mc_visited_pair_t pair, int pair_num,
          } */
       cursor = min;
       while (cursor <= max) {
-        pair_test =
-            (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor,
-                                                 mc_visited_pair_t);
-        if (xbt_automaton_state_compare
-            (pair_test->automaton_state, new_pair->automaton_state) == 0) {
-          if (xbt_automaton_propositional_symbols_compare_value
-              (pair_test->atomic_propositions,
-               new_pair->atomic_propositions) == 0) {
-            if (snapshot_compare(pair_test, new_pair) == 0) {
+        pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t);
+        if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) {
+          if (xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, new_visited_pair->atomic_propositions) == 0) {
+            if (snapshot_compare(pair_test, new_visited_pair) == 0) {
               if (pair_test->other_num == -1)
-                new_pair->other_num = pair_test->num;
+                new_visited_pair->other_num = pair_test->num;
               else
-                new_pair->other_num = pair_test->other_num;
+                new_visited_pair->other_num = pair_test->other_num;
               if (dot_output == NULL)
-                XBT_DEBUG("Pair %d already visited ! (equal to pair %d)",
-                          new_pair->num, pair_test->num);
+                XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
               else
-                XBT_DEBUG
-                    ("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))",
-                     new_pair->num, pair_test->num, new_pair->other_num);
-              xbt_dynar_remove_at(visited_pairs, cursor, NULL);
-              xbt_dynar_insert_at(visited_pairs, cursor, &new_pair);
+                XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", new_visited_pair->num, pair_test->num, new_visited_pair->other_num);
+              xbt_dynar_remove_at(visited_pairs, cursor, &pair_test);
+              xbt_dynar_insert_at(visited_pairs, cursor, &new_visited_pair);
               pair_test->visited_removed = 1;
               if (pair_test->acceptance_pair) {
                 if (pair_test->acceptance_removed == 1)
@@ -453,24 +453,22 @@ int is_visited_pair(mc_visited_pair_t pair, int pair_num,
               }
               if (!mc_mem_set)
                 MC_SET_STD_HEAP;
-              return new_pair->other_num;
+              return new_visited_pair->other_num;
             }
           }
         }
         cursor++;
       }
-      xbt_dynar_insert_at(visited_pairs, min, &new_pair);
+      xbt_dynar_insert_at(visited_pairs, min, &new_visited_pair);
     } else {
-      pair_test =
-          (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index,
-                                               mc_visited_pair_t);
-      if (pair_test->nb_processes < new_pair->nb_processes) {
-        xbt_dynar_insert_at(visited_pairs, index + 1, &new_pair);
+      pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index, mc_visited_pair_t);
+      if (pair_test->nb_processes < new_visited_pair->nb_processes) {
+        xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
       } else {
-        if (pair_test->heap_bytes_used < new_pair->heap_bytes_used)
-          xbt_dynar_insert_at(visited_pairs, index + 1, &new_pair);
+        if (pair_test->heap_bytes_used < new_visited_pair->heap_bytes_used)
+          xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
         else
-          xbt_dynar_insert_at(visited_pairs, index, &new_pair);
+          xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair);
       }
     }