[mc] Do not take NULL to mean 'the current address space' in dwarf expressions

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

diff --git a/src/mc/mc_safety.c b/src/mc/mc_safety.c
index 83460ff..3dea427 100644 (file)
--- a/src/mc/mc_safety.c
+++ b/src/mc/mc_safety.c
@@ -4,37 +4,48 @@
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
+#include <assert.h>
+
 #include "mc_state.h"
 #include "mc_request.h"
 #include "mc_safety.h"
 #include "mc_private.h"
 #include "mc_record.h"
+#include "mc_smx.h"
 
 #include "xbt/mmalloc/mmprivate.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
                                 "Logging specific to MC safety verification ");
 
+static int is_exploration_stack_state(mc_state_t current_state){
+
+  xbt_fifo_item_t item;
+  mc_state_t stack_state;
+  for(item = xbt_fifo_get_first_item(mc_stack); item != NULL; item = xbt_fifo_get_next_item(item)) {
+    stack_state = (mc_state_t) xbt_fifo_get_item_content(item);
+    if(snapshot_compare(stack_state, current_state) == 0){
+      XBT_INFO("Non-progressive cycle : state %d -> state %d", stack_state->num, current_state->num);
+      return 1;
+    }
+  }
+  return 0;
+}
+
 /**
  *  \brief Initialize the DPOR exploration algorithm
  */
 void MC_pre_modelcheck_safety()
 {
-
-  int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
   mc_state_t initial_state = NULL;
   smx_process_t process;
 
-  /* Create the initial state and push it into the exploration stack */
-  if (!mc_mem_set)
-    MC_SET_MC_HEAP;
+  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_SET_STD_HEAP;
 
   XBT_DEBUG("**************************************************");
@@ -46,18 +57,16 @@ void MC_pre_modelcheck_safety()
   MC_SET_MC_HEAP;
 
   /* Get an enabled process and insert it in the interleave set of the initial state */
-  xbt_swag_foreach(process, simix_global->process_list) {
+  MC_EACH_SIMIX_PROCESS(process,
     if (MC_process_is_enabled(process)) {
       MC_state_interleave_process(initial_state, process);
       if (mc_reduce_kind != e_mc_reduce_none)
         break;
     }
-  }
+  );
 
   xbt_fifo_unshift(mc_stack, initial_state);
-
-  if (!mc_mem_set)
-    MC_SET_STD_HEAP;
+  mmalloc_set_current_heap(heap);
 }
 
 
@@ -108,7 +117,7 @@ void MC_modelcheck_safety(void)
       mc_stats->executed_transitions++;
 
       /* Answer the request */
-      SIMIX_simcall_handle(req, value);
+      MC_simcall_handle(req, value);
 
       /* Wait for requests (schedules processes) */
       MC_wait_for_requests();
@@ -118,16 +127,21 @@ void MC_modelcheck_safety(void)
 
       next_state = MC_state_new();
 
+      if(_sg_mc_termination && is_exploration_stack_state(next_state)){
+          MC_show_non_termination();
+          return;
+      }
+
       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) {
+        MC_EACH_SIMIX_PROCESS(process,
           if (MC_process_is_enabled(process)) {
             MC_state_interleave_process(next_state, process);
             if (mc_reduce_kind != e_mc_reduce_none)
               break;
           }
-        }
+        );
 
         if (dot_output != NULL)
           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
@@ -194,6 +208,7 @@ void MC_modelcheck_safety(void)
       while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
         if (mc_reduce_kind == e_mc_reduce_dpor) {
           req = MC_state_get_internal_request(state);
+          const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
           xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
             if (MC_request_depend(req, MC_state_get_internal_request(prev_state))) {
               if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
@@ -208,8 +223,8 @@ void MC_modelcheck_safety(void)
                 xbt_free(req_str);
               }
 
-              if (!MC_state_process_is_done(prev_state, req->issuer))
-                MC_state_interleave_process(prev_state, req->issuer);
+              if (!MC_state_process_is_done(prev_state, issuer))
+                MC_state_interleave_process(prev_state, issuer);
               else
                 XBT_DEBUG("Process %p is in done set", req->issuer);
 
@@ -222,10 +237,11 @@ void MC_modelcheck_safety(void)
 
             } else {
 
+              const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state));
               XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant",
-                        req->call, req->issuer->pid, state->num,
+                        req->call, issuer->pid, state->num,
                         MC_state_get_internal_request(prev_state)->call,
-                        MC_state_get_internal_request(prev_state)->issuer->pid,
+                        previous_issuer->pid,
                         prev_state->num);
 
             }