summary |
shortlog |
log |
commit | commitdiff |
tree
raw |
patch |
inline | side by side (from parent 1:
2568ec7)
- DPOR currently does not handle SIMCALL_MUTEX operations;
- MUTEX_TRYLOCK should be visible: depending on the interleavigns it
might succeed or fail.
+ case SIMCALL_MUTEX_TRYLOCK:
+ return TRUE;
+
case SIMCALL_MUTEX_LOCK: {
smx_mutex_t mutex = simcall_mutex_lock__get__mutex(req);
#ifdef HAVE_MC
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_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
#ifdef HAVE_MC
|| req->call == SIMCALL_MC_SNAPSHOT
|| req->call == SIMCALL_MC_COMPARE_SNAPSHOTS
+ case SIMCALL_MUTEX_TRYLOCK:
case SIMCALL_MUTEX_LOCK: {
case SIMCALL_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),
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));
s_xbt_swag_t mutex_sleeping;
mc_model_checker->process().read_bytes(&mutex_sleeping, sizeof(mutex_sleeping),
remote(mutex.sleeping));
+ case SIMCALL_MUTEX_TRYLOCK:
+ label = bprintf("[(%lu)] Mutex TRYLOCK", issuer->pid);
+ break;
+
case SIMCALL_MUTEX_LOCK:
label = bprintf("[(%lu)] Mutex LOCK", 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);
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))) {
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))) {