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
|| 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
}
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));
}
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;
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))) {