for(unsigned int i=0;i<get_num_threads();i++) {
thread_id_t tid=int_to_id(i);
Thread *thr=get_thread(tid);
- if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET ) {
+ if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET &&
+ thr->get_pending() == NULL ) {
thr->set_state(THREAD_RUNNING);
scheduler->next_thread(thr);
Thread::swap(&system_context, thr);
pending_rel_seqs->size());
- if (isfinalfeasible() || (params.bound != 0 && priv->used_sequence_numbers > params.bound ) || DBG_ENABLED() )
+ if (isfinalfeasible() || (params.bound != 0 && priv->used_sequence_numbers > params.bound ) || DBG_ENABLED() ) {
+ checkDataRaces();
print_summary();
+ }
if ((diverge = get_next_backtrack()) == NULL)
return false;
break;
/* Don't backtrack into a point where the thread is disabled or sleeping. */
- if (node->get_enabled_array()[i]!=THREAD_ENABLED)
+ if (node->enabled_status(tid)!=THREAD_ENABLED)
continue;
/* Check if this has been explored already */
/** @return whether the current partial trace must be a prefix of a
* feasible trace. */
bool ModelChecker::isfeasibleprefix() {
- return promises->size() == 0 && pending_rel_seqs->size() == 0;
+ return promises->size() == 0 && pending_rel_seqs->size() == 0 && isfeasible();
}
/** @return whether the current partial trace is feasible. */
ModelAction *act=*rit;
bool foundvalue = false;
for (int j = 0; j<act->get_node()->get_read_from_size(); j++) {
- if (act->get_node()->get_read_from_at(i)==write) {
+ if (act->get_node()->get_read_from_at(j)==write) {
foundvalue = true;
break;
}
/* Iterate over all threads */
for (i = 0; i < thrd_lists->size(); i++) {
- ModelAction *write_after_read = NULL;
+ const ModelAction *write_after_read = NULL;
/* Iterate over actions in thread, starting from most recent */
action_list_t *list = &(*thrd_lists)[i];
break;
else if (act->is_write())
write_after_read = act;
+ else if (act->is_read()&&act->get_reads_from()!=NULL) {
+ write_after_read = act->get_reads_from();
+ }
}
-
- if (write_after_read && mo_graph->checkReachable(write_after_read, writer))
+
+ if (write_after_read && write_after_read!=writer && mo_graph->checkReachable(write_after_read, writer))
return false;
}
!act->same_thread(curr) &&
act->get_location() == curr->get_location() &&
promise->get_value() == curr->get_value()) {
- curr->get_node()->set_promise(i);
+ curr->get_node()->set_promise(i, act->is_rmw());
}
}
}
}
}
+void ModelChecker::check_promises_thread_disabled() {
+ for (unsigned int i = 0; i < promises->size(); i++) {
+ Promise *promise = (*promises)[i];
+ if (promise->check_promise()) {
+ failed_promise = true;
+ return;
+ }
+ }
+}
+
/** Checks promises in response to addition to modification order for threads.
* Definitions:
* pthread is the thread that performed the read that created the promise
if (promise->has_sync_thread(tid))
continue;
- if (mo_graph->checkReachable(promise->get_write(), write)) {
+ if (promise->get_write()&&mo_graph->checkReachable(promise->get_write(), write)) {
if (promise->increment_threads(tid)) {
failed_promise = true;
return;
bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) {
while(true) {
Node *prevnode=write->get_node()->get_parent();
- bool thread_sleep=prevnode->get_enabled_array()[id_to_int(curr->get_tid())]==THREAD_SLEEP_SET;
+
+ bool thread_sleep=prevnode->enabled_status(curr->get_tid())==THREAD_SLEEP_SET;
if (write->is_release()&&thread_sleep)
return true;
if (!write->is_rmw()) {