return blocking_threads;
}
-/**
- * Check if a Thread has entered a circular wait deadlock situation. This will
- * not check other threads for potential deadlock situations, and may miss
- * deadlocks involving WAIT.
- *
- * @param t The thread which may have entered a deadlock
- * @return True if this Thread entered a deadlock; false otherwise
- */
-bool ModelChecker::is_circular_wait(const Thread *t) const
-{
- for (Thread *waiting = t->waiting_on() ; waiting != NULL; waiting = waiting->waiting_on())
- if (waiting == t)
- return true;
- return false;
-}
-
/**
* Check if this is a complete execution. That is, have all thread completed
* execution (rather than exiting because sleep sets have forced a redundant
*
* If one of the following is true:
* (a) there are no pending promises
- * (b) the reader is ordered after the latest Promise creation
+ * (b) the reader and writer do not cross any promises
* Then, it is safe to pass a future value back now.
*
* Otherwise, we must save the pending future value until (a) or (b) is true
bool ModelChecker::promises_may_allow(const ModelAction *writer,
const ModelAction *reader) const
{
- return promises->empty() ||
- *(promises->back()->get_reader(0)) < *reader;
+ if (promises->empty())
+ return true;
+ for(int i=promises->size()-1;i>=0;i--) {
+ ModelAction *pr=(*promises)[i]->get_reader(0);
+ //reader is after promise...doesn't cross any promise
+ if (*reader > *pr)
+ return true;
+ //writer is after promise, reader before...bad...
+ if (*writer > *pr)
+ return false;
+ }
+ return true;
}
/**
Thread *thr = get_thread(tid);
if (!thr->is_model_thread() && !thr->is_complete() && !thr->get_pending()) {
switch_from_master(thr);
- if (is_circular_wait(thr))
+ if (thr->is_waiting_on(thr))
assert_bug("Deadlock detected");
}
}