[mc] Make SIMCALL_MUTEX_TRYLOCK visible and forbid usage of MUTEX operations with...

[simgrid.git] / src / mc / mc_request.cpp

diff --git a/src/mc/mc_request.cpp b/src/mc/mc_request.cpp
index e28f119..9791660 100644 (file)
--- a/src/mc/mc_request.cpp
+++ b/src/mc/mc_request.cpp
@@ -1,4 +1,4 @@
-/* Copyright (c) 2008-2014. The SimGrid Team.
+/* Copyright (c) 2008-2015. The SimGrid Team.
  * All rights reserved.                                                     */
 
 /* This program is free software; you can redistribute it and/or modify it
@@ -10,6 +10,7 @@
 #include "mc_safety.h"
 #include "mc_private.h"
 #include "mc_smx.h"
+#include "mc_xbt.hpp"
 
 using simgrid::mc::remote;
 
@@ -256,7 +257,7 @@ char *MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t req
     type = "iSend";
     char* p = pointer_to_string(simcall_comm_isend__get__src_buff(req));
     char* bs = buff_size_to_string(simcall_comm_isend__get__src_buff_size(req));
-    if (issuer->smx_host)
+    if (issuer->host)
       args =
           bprintf("src=(%lu)%s (%s), buff=%s, size=%s", issuer->pid,
                   MC_smx_process_get_host_name(issuer),
@@ -283,7 +284,7 @@ char *MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t req
     type = "iRecv";
     char* p = pointer_to_string(simcall_comm_irecv__get__dst_buff(req));
     char* bs = buff_size_to_string(size);
-    if (issuer->smx_host)
+    if (issuer->host)
       args =
           bprintf("dst=(%lu)%s (%s), buff=%s, size=%s", issuer->pid,
                   MC_smx_process_get_host_name(issuer),
@@ -374,8 +375,8 @@ char *MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t req
       &comms, sizeof(comms), remote(simcall_comm_waitany__get__comms(req)));
     if (!xbt_dynar_is_empty(&comms)) {
       smx_synchro_t remote_sync;
-      MC_process_read_dynar_element(&mc_model_checker->process(),
-        &remote_sync, simcall_comm_waitany__get__comms(req), value,
+      read_element(mc_model_checker->process(),
+        &remote_sync, remote(simcall_comm_waitany__get__comms(req)), value,
         sizeof(remote_sync));
       char* p = pointer_to_string(remote_sync);
       args = bprintf("comm=%s (%d of %lu)",
@@ -394,18 +395,26 @@ char *MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t req
     } else {
       type = "TestAny";
       args =
-          bprintf("(%d of %lu)", value + 1,
-                  MC_process_read_dynar_length(&mc_model_checker->process(),
+          bprintf("(%d of %zu)", value + 1,
+                  read_length(mc_model_checker->process(),
                     simcall_comm_testany__get__comms(req)));
     }
     break;
 
+  case SIMCALL_MUTEX_TRYLOCK:
   case SIMCALL_MUTEX_LOCK: {
-    type = "Mutex LOCK";
+    if (req->call == SIMCALL_MUTEX_LOCK)
+      type = "Mutex LOCK";
+    else
+      type = "Mutex TRYLOCK";
 
     s_smx_mutex_t mutex;
     mc_model_checker->process().read_bytes(&mutex, sizeof(mutex),
-      remote(simcall_mutex_lock__get__mutex(req)));
+      remote(
+        req->call == SIMCALL_MUTEX_LOCK
+        ? simcall_mutex_lock__get__mutex(req)
+        : simcall_mutex_trylock__get__mutex(req)
+      ));
     s_xbt_swag_t mutex_sleeping;
     mc_model_checker->process().read_bytes(&mutex_sleeping, sizeof(mutex_sleeping),
       remote(mutex.sleeping));
@@ -502,15 +511,17 @@ int MC_request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx)
     break;
 
   case SIMCALL_COMM_WAITANY: {
-    MC_process_read_dynar_element(
-      &mc_model_checker->process(), &remote_act, simcall_comm_waitany__get__comms(req),
+    read_element(
+      mc_model_checker->process(), &remote_act,
+      remote(simcall_comm_waitany__get__comms(req)),
       idx, sizeof(remote_act));
     }
     break;
 
   case SIMCALL_COMM_TESTANY: {
-    MC_process_read_dynar_element(
-      &mc_model_checker->process(), &remote_act, simcall_comm_testany__get__comms(req),
+    read_element(
+      mc_model_checker->process(), &remote_act,
+      remote(simcall_comm_testany__get__comms(req)),
       idx, sizeof(remote_act));
     }
     break;
@@ -538,7 +549,7 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value)
 
   switch (req->call) {
   case SIMCALL_COMM_ISEND:
-    if (issuer->smx_host)
+    if (issuer->host)
       label =
           bprintf("[(%lu)%s] iSend", issuer->pid,
                   MC_smx_process_get_host_name(issuer));
@@ -547,7 +558,7 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value)
     break;
 
   case SIMCALL_COMM_IRECV:
-    if (issuer->smx_host)
+    if (issuer->host)
       label =
           bprintf("[(%lu)%s] iRecv", issuer->pid,
                   MC_smx_process_get_host_name(issuer));
@@ -557,7 +568,7 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value)
 
   case SIMCALL_COMM_WAIT: {
     if (value == -1) {
-      if (issuer->smx_host)
+      if (issuer->host)
         label =
             bprintf("[(%lu)%s] WaitTimeout", issuer->pid,
                     MC_smx_process_get_host_name(issuer));
@@ -571,7 +582,7 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value)
 
       smx_process_t src_proc = MC_smx_resolve_process(synchro.comm.src_proc);
       smx_process_t dst_proc = MC_smx_resolve_process(synchro.comm.dst_proc);
-      if (issuer->smx_host)
+      if (issuer->host)
         label =
             bprintf("[(%lu)%s] Wait [(%lu)->(%lu)]", issuer->pid,
                     MC_smx_process_get_host_name(issuer),
@@ -592,14 +603,14 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value)
     mc_model_checker->process().read_bytes(&synchro,
       sizeof(synchro), remote(remote_act));
     if (synchro.comm.src_proc == NULL || synchro.comm.dst_proc == NULL) {
-      if (issuer->smx_host)
+      if (issuer->host)
         label =
             bprintf("[(%lu)%s] Test FALSE", issuer->pid,
                     MC_smx_process_get_host_name(issuer));
       else
         label = bprintf("[(%lu)] Test FALSE", issuer->pid);
     } else {
-      if (issuer->smx_host)
+      if (issuer->host)
         label =
             bprintf("[(%lu)%s] Test TRUE", issuer->pid,
                     MC_smx_process_get_host_name(issuer));
@@ -610,9 +621,9 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value)
   }
 
   case SIMCALL_COMM_WAITANY: {
-    unsigned long comms_size = MC_process_read_dynar_length(
-      &mc_model_checker->process(), simcall_comm_waitany__get__comms(req));
-    if (issuer->smx_host)
+    unsigned long comms_size = read_length(
+      mc_model_checker->process(), remote(simcall_comm_waitany__get__comms(req)));
+    if (issuer->host)
       label =
           bprintf("[(%lu)%s] WaitAny [%d of %lu]", issuer->pid,
                   MC_smx_process_get_host_name(issuer), value + 1,
@@ -626,14 +637,14 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value)
 
   case SIMCALL_COMM_TESTANY:
     if (value == -1) {
-      if (issuer->smx_host)
+      if (issuer->host)
         label =
             bprintf("[(%lu)%s] TestAny FALSE", issuer->pid,
                     MC_smx_process_get_host_name(issuer));
       else
         label = bprintf("[(%lu)] TestAny FALSE", issuer->pid);
     } else {
-      if (issuer->smx_host)
+      if (issuer->host)
         label =
             bprintf("[(%lu)%s] TestAny TRUE [%d of %lu]", issuer->pid,
                     MC_smx_process_get_host_name(issuer), value + 1,
@@ -646,12 +657,16 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value)
     }
     break;
 
+  case SIMCALL_MUTEX_TRYLOCK:
+    label = bprintf("[(%lu)] Mutex TRYLOCK", issuer->pid);
+    break;
+
   case SIMCALL_MUTEX_LOCK:
-    label = bprintf("[(%lu)] Mutex LOCK", req->issuer->pid);
+    label = bprintf("[(%lu)] Mutex LOCK", issuer->pid);
     break;
 
   case SIMCALL_MC_RANDOM:
-    if (issuer->smx_host)
+    if (issuer->host)
       label =
           bprintf("[(%lu)%s] MC_RANDOM (%d)", issuer->pid,
                   MC_smx_process_get_host_name(issuer), value);
@@ -660,7 +675,7 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value)
     break;
 
   case SIMCALL_MC_SNAPSHOT:
-    if (issuer->smx_host)
+    if (issuer->host)
       label =
           bprintf("[(%lu)%s] MC_SNAPSHOT", issuer->pid,
                   MC_smx_process_get_host_name(issuer));
@@ -669,7 +684,7 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value)
     break;
 
   case SIMCALL_MC_COMPARE_SNAPSHOTS:
-    if (issuer->smx_host)
+    if (issuer->host)
       label =
           bprintf("[(%lu)%s] MC_COMPARE_SNAPSHOTS", issuer->pid,
                   MC_smx_process_get_host_name(issuer));