Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Merge remote-tracking branch 'origin/libdw2'
[simgrid.git] / src / mc / mc_global.c
index f35ac68..930098f 100644 (file)
@@ -1106,6 +1106,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();
@@ -1229,6 +1232,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 ****");
 
@@ -1258,6 +1262,7 @@ void MC_replay(xbt_fifo_t stack, int start)
       xbt_free(key);
     }
   }
+  xbt_dynar_reset(communications_pattern);
   MC_UNSET_RAW_MEM;
   
 
@@ -1287,8 +1292,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++;
@@ -1569,6 +1588,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;
 }