[mc] Have a more complete/accurate view of an given object mapping in memory

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

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index a44dec1..7bf5c97 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -178,11 +178,7 @@ void dw_variable_free_voidp(void *t){
 // object_info
 
 mc_object_info_t MC_new_object_info(void) {
-  mc_object_info_t res = xbt_new(s_mc_object_info_t, 1);
-  res->file_name = NULL;
-  res->start_text = NULL;
-  res->start_data = NULL;
-  res->start_bss = NULL;
+  mc_object_info_t res = xbt_new0(s_mc_object_info_t, 1);
   res->local_variables = xbt_dict_new_homogeneous(NULL);
   res->global_variables = xbt_dynar_new(sizeof(dw_variable_t), dw_variable_free_voidp);
   res->types = xbt_dict_new_homogeneous(NULL);
@@ -195,7 +191,7 @@ void MC_free_object_info(mc_object_info_t* info) {
   xbt_dynar_free(&(*info)->global_variables);
   xbt_dict_free(&(*info)->types);
   xbt_free(info);
-  info = NULL;
+  *info = NULL;
 }
 
 /*************************************************************************/
@@ -1106,6 +1102,9 @@ void MC_modelcheck_safety(void)
   /* Save the initial state */
   initial_state_safety = xbt_new0(s_mc_global_t, 1);
   initial_state_safety->snapshot = MC_take_snapshot(0);
+  initial_state_safety->initial_communications_pattern_done = 0;
+  initial_state_safety->comm_deterministic = 1;
+  initial_state_safety->send_deterministic = 1;
   MC_UNSET_RAW_MEM;
 
   MC_dpor();
@@ -1160,6 +1159,7 @@ void MC_modelcheck_liveness(){
 void MC_exit(void)
 {
   xbt_free(mc_time);
+
   MC_memory_exit();
   //xbt_abort();
 }
@@ -1228,6 +1228,7 @@ void MC_replay(xbt_fifo_t stack, int start)
   xbt_fifo_item_t item, start_item;
   mc_state_t state;
   smx_process_t process = NULL;
+  int comm_pattern = 0;
 
   XBT_DEBUG("**** Begin Replay ****");
 
@@ -1257,6 +1258,7 @@ void MC_replay(xbt_fifo_t stack, int start)
       xbt_free(key);
     }
   }
+  xbt_dynar_reset(communications_pattern);
   MC_UNSET_RAW_MEM;
   
 
@@ -1286,8 +1288,22 @@ void MC_replay(xbt_fifo_t stack, int start)
         xbt_free(req_str);
       }
     }
+
+    if(req->call == SIMCALL_COMM_ISEND)
+      comm_pattern = 1;
+    else if(req->call == SIMCALL_COMM_IRECV)
+      comm_pattern = 2;
     
     SIMIX_simcall_pre(req, value);
+
+    MC_SET_RAW_MEM;
+    if(comm_pattern != 0){
+      get_comm_pattern(communications_pattern, req, comm_pattern);
+    }
+    MC_UNSET_RAW_MEM;
+
+    comm_pattern = 0;
+    
     MC_wait_for_requests();
 
     count++;
@@ -1568,6 +1584,10 @@ void MC_print_statistics(mc_stats_t stats)
     fprintf(dot_output, "}\n");
     fclose(dot_output);
   }
+  if(initial_state_safety != NULL){
+    // XBT_INFO("Communication-deterministic : %s", !initial_state_safety->comm_deterministic ? "No" : "Yes");
+    // XBT_INFO("Send-deterministic : %s", !initial_state_safety->send_deterministic ? "No" : "Yes");
+  }
   MC_UNSET_RAW_MEM;
 }