From e4d3739e981eb46fbfca0ff837c681e26e8a44c6 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Fri, 28 Aug 2015 11:01:45 +0200 Subject: [PATCH 1/1] [mc] Make SIMCALL_MUTEX_TRYLOCK visible and forbid usage of MUTEX operations with DPOR - DPOR currently does not handle SIMCALL_MUTEX operations; - MUTEX_TRYLOCK should be visible: depending on the interleavigns it might succeed or fail. --- src/mc/mc_base.cpp | 4 ++++ src/mc/mc_request.cpp | 16 ++++++++++++++-- src/mc/mc_safety.cpp | 3 +++ 3 files changed, 21 insertions(+), 2 deletions(-) diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp index 8c8610fe80..74c8268aaf 100644 --- a/src/mc/mc_base.cpp +++ b/src/mc/mc_base.cpp @@ -142,6 +142,9 @@ int MC_request_is_enabled(smx_simcall_t req) return FALSE; } + case SIMCALL_MUTEX_TRYLOCK: + return TRUE; + case SIMCALL_MUTEX_LOCK: { smx_mutex_t mutex = simcall_mutex_lock__get__mutex(req); #ifdef HAVE_MC @@ -179,6 +182,7 @@ 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_TRYLOCK #ifdef HAVE_MC || req->call == SIMCALL_MC_SNAPSHOT || req->call == SIMCALL_MC_COMPARE_SNAPSHOTS diff --git a/src/mc/mc_request.cpp b/src/mc/mc_request.cpp index 4503597f38..979166090a 100644 --- a/src/mc/mc_request.cpp +++ b/src/mc/mc_request.cpp @@ -401,12 +401,20 @@ char *MC_request_to_string(smx_simcall_t req, int value, e_mc_request_type_t 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)); @@ -649,6 +657,10 @@ 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", issuer->pid); break; diff --git a/src/mc/mc_safety.cpp b/src/mc/mc_safety.cpp index 2ca64ec1ae..7336489ef4 100644 --- a/src/mc/mc_safety.cpp +++ b/src/mc/mc_safety.cpp @@ -199,6 +199,9 @@ void MC_modelcheck_safety(void) while ((state = (mc_state_t) xbt_fifo_shift(mc_stack))) { if (mc_reduce_kind == e_mc_reduce_dpor) { req = MC_state_get_internal_request(state); + if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK) + xbt_die("Mutex is currently not supported with DPOR, " + "use --cfg=model-check/reduction:dpor"); const smx_process_t issuer = MC_smx_simcall_get_issuer(req); xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) { if (MC_request_depend(req, MC_state_get_internal_request(prev_state))) { -- 2.20.1