Logo AND Algorithmique Numérique Distribuée
Public GIT Repository
projects / simgrid.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
[mc] Cross process access to simcall synchro
[simgrid.git] / src / mc / mc_request.c
diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c
index 1b12665..b656a4d 100644 (file)
--- a/src/mc/mc_request.c
+++ b/src/mc/mc_request.c
@@ -35,6 +35,25 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2)
   if (r1->call == SIMCALL_COMM_IRECV && r2->call == SIMCALL_COMM_ISEND)
     return FALSE;
 
+  // Read object from MCed memory:
+  s_smx_synchro_t synchro1, synchro2;
+  if (r1->call == SIMCALL_COMM_WAIT) {
+    MC_process_read_simple(&mc_model_checker->process, &synchro1,
+      simcall_comm_wait__get__comm(r1), sizeof(synchro1));
+  }
+  if (r2->call == SIMCALL_COMM_WAIT) {
+    MC_process_read_simple(&mc_model_checker->process, &synchro2,
+      simcall_comm_wait__get__comm(r2), sizeof(synchro2));
+  }
+  if (r1->call == SIMCALL_COMM_TEST) {
+    MC_process_read_simple(&mc_model_checker->process, &synchro1,
+      simcall_comm_test__get__comm(r1), sizeof(synchro1));
+  }
+  if (r2->call == SIMCALL_COMM_TEST) {
+    MC_process_read_simple(&mc_model_checker->process, &synchro2,
+      simcall_comm_test__get__comm(r2), sizeof(synchro2));
+  }
+
   if ((r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV)
       && r2->call == SIMCALL_COMM_WAIT) {
 
@@ -45,26 +64,25 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2)
 
     // FIXME, remote access to comm object
 
-    if (rdv != simcall_comm_wait__get__comm(r2)->comm.rdv_cpy
+    if (rdv != synchro2.comm.rdv_cpy
         && simcall_comm_wait__get__timeout(r2) <= 0)
       return FALSE;
 
-    if ((r1->issuer != simcall_comm_wait__get__comm(r2)->comm.src_proc)
-        && (r1->issuer != simcall_comm_wait__get__comm(r2)->comm.dst_proc)
+    if ((r1->issuer != synchro2.comm.src_proc)
+        && (r1->issuer != synchro2.comm.dst_proc)
         && simcall_comm_wait__get__timeout(r2) <= 0)
       return FALSE;
 
     if ((r1->call == SIMCALL_COMM_ISEND)
-        && (simcall_comm_wait__get__comm(r2)->comm.type == SIMIX_COMM_SEND)
-        && (simcall_comm_wait__get__comm(r2)->comm.src_buff !=
+        && (synchro2.comm.type == SIMIX_COMM_SEND)
+        && (synchro2.comm.src_buff !=
             simcall_comm_isend__get__src_buff(r1))
         && simcall_comm_wait__get__timeout(r2) <= 0)
       return FALSE;
 
     if ((r1->call == SIMCALL_COMM_IRECV)
-        && (simcall_comm_wait__get__comm(r2)->comm.type == SIMIX_COMM_RECEIVE)
-        && (simcall_comm_wait__get__comm(r2)->comm.dst_buff !=
-            simcall_comm_irecv__get__dst_buff(r1))
+        && (synchro2.comm.type == SIMIX_COMM_RECEIVE)
+        && (synchro2.comm.dst_buff != simcall_comm_irecv__get__dst_buff(r1))
         && simcall_comm_wait__get__timeout(r2) <= 0)
       return FALSE;
   }
@@ -77,25 +95,25 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2)
         SIMCALL_COMM_ISEND ? simcall_comm_isend__get__rdv(r2) :
         simcall_comm_irecv__get__rdv(r2);
 
-    if (rdv != simcall_comm_wait__get__comm(r1)->comm.rdv_cpy
+    if (rdv != synchro1.comm.rdv_cpy
         && simcall_comm_wait__get__timeout(r1) <= 0)
       return FALSE;
 
-    if ((r2->issuer != simcall_comm_wait__get__comm(r1)->comm.src_proc)
-        && (r2->issuer != simcall_comm_wait__get__comm(r1)->comm.dst_proc)
+    if ((r2->issuer != synchro1.comm.src_proc)
+        && (r2->issuer != synchro1.comm.dst_proc)
         && simcall_comm_wait__get__timeout(r1) <= 0)
       return FALSE;
 
     if ((r2->call == SIMCALL_COMM_ISEND)
-        && (simcall_comm_wait__get__comm(r1)->comm.type == SIMIX_COMM_SEND)
-        && (simcall_comm_wait__get__comm(r1)->comm.src_buff !=
+        && (synchro1.comm.type == SIMIX_COMM_SEND)
+        && (synchro1.comm.src_buff !=
             simcall_comm_isend__get__src_buff(r2))
         && simcall_comm_wait__get__timeout(r1) <= 0)
       return FALSE;
 
     if ((r2->call == SIMCALL_COMM_IRECV)
-        && (simcall_comm_wait__get__comm(r1)->comm.type == SIMIX_COMM_RECEIVE)
-        && (simcall_comm_wait__get__comm(r1)->comm.dst_buff !=
+        && (synchro1.comm.type == SIMIX_COMM_RECEIVE)
+        && (synchro1.comm.dst_buff !=
             simcall_comm_irecv__get__dst_buff(r2))
         && simcall_comm_wait__get__timeout(r1) <= 0)
       return FALSE;
@@ -125,89 +143,71 @@ int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2)
 
   if (r1->call == SIMCALL_COMM_WAIT
       && (r2->call == SIMCALL_COMM_WAIT || r2->call == SIMCALL_COMM_TEST)
-      && (simcall_comm_wait__get__comm(r1)->comm.src_proc == NULL
-          || simcall_comm_wait__get__comm(r1)->comm.dst_proc == NULL))
+      && (synchro1.comm.src_proc == NULL || synchro1.comm.dst_proc == NULL))
     return FALSE;
 
   if (r2->call == SIMCALL_COMM_WAIT
       && (r1->call == SIMCALL_COMM_WAIT || r1->call == SIMCALL_COMM_TEST)
-      && (simcall_comm_wait__get__comm(r2)->comm.src_proc == NULL
-          || simcall_comm_wait__get__comm(r2)->comm.dst_proc == NULL))
-    return FALSE;
+      && (synchro2.comm.src_proc == NULL || synchro2.comm.dst_proc == NULL))
+      return FALSE;
 
   if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_WAIT
-      && simcall_comm_wait__get__comm(r1)->comm.src_buff ==
-      simcall_comm_wait__get__comm(r2)->comm.src_buff
-      && simcall_comm_wait__get__comm(r1)->comm.dst_buff ==
-      simcall_comm_wait__get__comm(r2)->comm.dst_buff)
+      && synchro1.comm.src_buff == synchro2.comm.src_buff
+      && synchro2.comm.dst_buff == synchro2.comm.dst_buff)
     return FALSE;
 
   if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_WAIT
-      && simcall_comm_wait__get__comm(r1)->comm.src_buff != NULL
-      && simcall_comm_wait__get__comm(r1)->comm.dst_buff != NULL
-      && simcall_comm_wait__get__comm(r2)->comm.src_buff != NULL
-      && simcall_comm_wait__get__comm(r2)->comm.dst_buff != NULL
-      && simcall_comm_wait__get__comm(r1)->comm.dst_buff !=
-      simcall_comm_wait__get__comm(r2)->comm.src_buff
-      && simcall_comm_wait__get__comm(r1)->comm.dst_buff !=
-      simcall_comm_wait__get__comm(r2)->comm.dst_buff
-      && simcall_comm_wait__get__comm(r2)->comm.dst_buff !=
-      simcall_comm_wait__get__comm(r1)->comm.src_buff)
+      && synchro1.comm.src_buff != NULL
+      && synchro1.comm.dst_buff != NULL
+      && synchro2.comm.src_buff != NULL
+      && synchro2.comm.dst_buff != NULL
+      && synchro1.comm.dst_buff != synchro2.comm.src_buff
+      && synchro1.comm.dst_buff != synchro2.comm.dst_buff
+      && synchro2.comm.dst_buff != synchro1.comm.src_buff)
     return FALSE;
 
   if (r1->call == SIMCALL_COMM_TEST &&
       (simcall_comm_test__get__comm(r1) == NULL
-       || simcall_comm_test__get__comm(r1)->comm.src_buff == NULL
-       || simcall_comm_test__get__comm(r1)->comm.dst_buff == NULL))
+       || synchro1.comm.src_buff == NULL
+       || synchro1.comm.dst_buff == NULL))
     return FALSE;
 
   if (r2->call == SIMCALL_COMM_TEST &&
       (simcall_comm_test__get__comm(r2) == NULL
-       || simcall_comm_test__get__comm(r2)->comm.src_buff == NULL
-       || simcall_comm_test__get__comm(r2)->comm.dst_buff == NULL))
+       || synchro2.comm.src_buff == NULL
+       || synchro2.comm.dst_buff == NULL))
     return FALSE;
 
   if (r1->call == SIMCALL_COMM_TEST && r2->call == SIMCALL_COMM_WAIT
-      && simcall_comm_test__get__comm(r1)->comm.src_buff ==
-      simcall_comm_wait__get__comm(r2)->comm.src_buff
-      && simcall_comm_test__get__comm(r1)->comm.dst_buff ==
-      simcall_comm_wait__get__comm(r2)->comm.dst_buff)
+      && synchro1.comm.src_buff == synchro2.comm.src_buff
+      && synchro1.comm.dst_buff == synchro2.comm.dst_buff)
     return FALSE;
 
   if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_TEST
-      && simcall_comm_wait__get__comm(r1)->comm.src_buff ==
-      simcall_comm_test__get__comm(r2)->comm.src_buff
-      && simcall_comm_wait__get__comm(r1)->comm.dst_buff ==
-      simcall_comm_test__get__comm(r2)->comm.dst_buff)
+      && synchro1.comm.src_buff == synchro2.comm.src_buff
+      && synchro1.comm.dst_buff == synchro2.comm.dst_buff)
     return FALSE;
 
   if (r1->call == SIMCALL_COMM_WAIT && r2->call == SIMCALL_COMM_TEST
-      && simcall_comm_wait__get__comm(r1)->comm.src_buff != NULL
-      && simcall_comm_wait__get__comm(r1)->comm.dst_buff != NULL
-      && simcall_comm_test__get__comm(r2)->comm.src_buff != NULL
-      && simcall_comm_test__get__comm(r2)->comm.dst_buff != NULL
-      && simcall_comm_wait__get__comm(r1)->comm.dst_buff !=
-      simcall_comm_test__get__comm(r2)->comm.src_buff
-      && simcall_comm_wait__get__comm(r1)->comm.dst_buff !=
-      simcall_comm_test__get__comm(r2)->comm.dst_buff
-      && simcall_comm_test__get__comm(r2)->comm.dst_buff !=
-      simcall_comm_wait__get__comm(r1)->comm.src_buff)
+      && synchro1.comm.src_buff != NULL
+      && synchro1.comm.dst_buff != NULL
+      && synchro2.comm.src_buff != NULL
+      && synchro2.comm.dst_buff != NULL
+      && synchro1.comm.dst_buff != synchro2.comm.src_buff
+      && synchro1.comm.dst_buff != synchro2.comm.dst_buff
+      && synchro2.comm.dst_buff != synchro1.comm.src_buff)
     return FALSE;
 
   if (r1->call == SIMCALL_COMM_TEST && r2->call == SIMCALL_COMM_WAIT
-      && simcall_comm_test__get__comm(r1)->comm.src_buff != NULL
-      && simcall_comm_test__get__comm(r1)->comm.dst_buff != NULL
-      && simcall_comm_wait__get__comm(r2)->comm.src_buff != NULL
-      && simcall_comm_wait__get__comm(r2)->comm.dst_buff != NULL
-      && simcall_comm_test__get__comm(r1)->comm.dst_buff !=
-      simcall_comm_wait__get__comm(r2)->comm.src_buff
-      && simcall_comm_test__get__comm(r1)->comm.dst_buff !=
-      simcall_comm_wait__get__comm(r2)->comm.dst_buff
-      && simcall_comm_wait__get__comm(r2)->comm.dst_buff !=
-      simcall_comm_test__get__comm(r1)->comm.src_buff)
+      && synchro1.comm.src_buff != NULL
+      && synchro1.comm.dst_buff != NULL
+      && synchro2.comm.src_buff != NULL
+      && synchro2.comm.dst_buff != NULL
+      && synchro1.comm.dst_buff != synchro2.comm.src_buff
+      && synchro1.comm.dst_buff != synchro2.comm.dst_buff
+      && synchro2.comm.dst_buff != synchro1.comm.src_buff)
     return FALSE;
 
-
   return TRUE;
 }
 
@@ -234,6 +234,7 @@ char *MC_request_to_string(smx_simcall_t req, int value)
 {
   char *type = NULL, *args = NULL, *str = NULL, *p = NULL, *bs = NULL;
   smx_synchro_t act = NULL;
+  smx_mutex_t mutex = NULL;
   size_t size = 0;
 
   smx_process_t issuer = MC_smx_simcall_get_issuer(req);
@@ -342,6 +343,12 @@ char *MC_request_to_string(smx_simcall_t req, int value)
     }
     break;
 
+  case SIMCALL_MUTEX_LOCK:
+    mutex = simcall_mutex_lock__get__mutex(req);
+    type = xbt_strdup("Mutex LOCK");
+    args = bprintf("locked = %d, owner = %d, sleeping = %d", mutex->locked, mutex->owner != NULL ? (int)mutex->owner->pid : -1, xbt_swag_size(mutex->sleeping));
+    break;
+
   case SIMCALL_MC_SNAPSHOT:
     type = xbt_strdup("MC_SNAPSHOT");
     args = NULL;
@@ -542,6 +549,10 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value)
     }
     break;
 
+  case SIMCALL_MUTEX_LOCK:
+    label = bprintf("[(%lu)] Mutex LOCK", req->issuer->pid);
+    break;
+
   case SIMCALL_MC_RANDOM:
     if (issuer->smx_host)
       label =
Clone of SimGrid repository with local patches