From eca09d65271990fdae84e1d7da71916740a9c50b Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Thu, 26 Feb 2015 10:22:04 +0100 Subject: [PATCH] model-checker : MUTEX_UNLOCK is invisible for MC --- examples/smpi/mc/only_send_deterministic.tesh | 6 +++--- src/mc/mc_base.c | 1 - src/mc/mc_request.c | 10 ---------- 3 files changed, 3 insertions(+), 14 deletions(-) diff --git a/examples/smpi/mc/only_send_deterministic.tesh b/examples/smpi/mc/only_send_deterministic.tesh index 1174e5cc05..ac21435887 100644 --- a/examples/smpi/mc/only_send_deterministic.tesh +++ b/examples/smpi/mc/only_send_deterministic.tesh @@ -17,9 +17,9 @@ $ ../../../smpi_script/bin/smpirun -hostfile ${srcdir:=.}/hostfile_only_send_det > [0.000000] [mc_global/INFO] **** Only-send-deterministic communication pattern **** > [0.000000] [mc_global/INFO] ****************************************************** > [0.000000] [mc_global/INFO] The recv communications pattern of the process 0 is different! Different source for communication #2 -> [0.000000] [mc_global/INFO] Expanded states = 2966 -> [0.000000] [mc_global/INFO] Visited states = 13362 -> [0.000000] [mc_global/INFO] Executed transitions = 12576 +> [0.000000] [mc_global/INFO] Expanded states = 1025 +> [0.000000] [mc_global/INFO] Visited states = 3640 +> [0.000000] [mc_global/INFO] Executed transitions = 3360 > [0.000000] [mc_global/INFO] Send-deterministic : Yes > [0.000000] [mc_global/INFO] Recv-deterministic : No diff --git a/src/mc/mc_base.c b/src/mc/mc_base.c index 31dac0cc39..2a587228ab 100644 --- a/src/mc/mc_base.c +++ b/src/mc/mc_base.c @@ -87,7 +87,6 @@ int MC_request_is_visible(smx_simcall_t req) || req->call == SIMCALL_COMM_TESTANY || req->call == SIMCALL_MC_RANDOM || req->call == SIMCALL_MUTEX_LOCK - || req->call == SIMCALL_MUTEX_UNLOCK #ifdef HAVE_MC || req->call == SIMCALL_MC_SNAPSHOT || req->call == SIMCALL_MC_COMPARE_SNAPSHOTS diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c index 3d7638c581..5c7d573392 100644 --- a/src/mc/mc_request.c +++ b/src/mc/mc_request.c @@ -335,12 +335,6 @@ char *MC_request_to_string(smx_simcall_t req, int value) 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_MUTEX_UNLOCK: - type = xbt_strdup("Mutex UNLOCK"); - mutex = simcall_mutex_unlock__get__mutex(req); - 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; @@ -533,10 +527,6 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value) case SIMCALL_MUTEX_LOCK: label = bprintf("[(%lu)] Mutex LOCK", req->issuer->pid); break; - - case SIMCALL_MUTEX_UNLOCK: - label = bprintf("[(%lu)] Mutex UNLOCK", req->issuer->pid); - break; case SIMCALL_MC_RANDOM: if (req->issuer->smx_host) -- 2.20.1