DEBUG("+++ Resetting to initial state +++\n");
node_stack->reset_execution();
- /* Print all model-checker output before rollback */
- fflush(model_out);
-
/**
* FIXME: if we utilize partial rollback, we will need to free only
* those pending actions which were NOT pending before the rollback
}
DEBUG("*** ModelChecker chose next thread = %d ***\n", id_to_int(tid));
ASSERT(tid != THREAD_ID_T_NONE);
- return thread_map->get(id_to_int(tid));
+ return get_thread(id_to_int(tid));
}
/**
Node *node = prev->get_node()->get_parent();
+ /* See Dynamic Partial Order Reduction (addendum), POPL '05 */
int low_tid, high_tid;
if (node->enabled_status(t->get_id()) == THREAD_ENABLED) {
low_tid = id_to_int(act->get_tid());
if (i >= node->get_num_threads())
break;
+ /* See Dynamic Partial Order Reduction (addendum), POPL '05 */
/* Don't backtrack into a point where the thread is disabled or sleeping. */
if (node->enabled_status(tid) != THREAD_ENABLED)
continue;
}
case THREAD_FINISH: {
Thread *th = get_thread(curr);
- while (!th->wait_list_empty()) {
- ModelAction *act = th->pop_wait_list();
- scheduler->wake(get_thread(act));
+ /* Wake up any joining threads */
+ for (unsigned int i = 0; i < get_num_threads(); i++) {
+ Thread *waiting = get_thread(int_to_id(i));
+ if (waiting->waiting_on() == th &&
+ waiting->get_pending()->is_thread_join())
+ scheduler->wake(waiting);
}
th->complete();
/* Completed thread can't satisfy promises */
*/
bool ModelChecker::check_action_enabled(ModelAction *curr) {
if (curr->is_lock()) {
- std::mutex *lock = (std::mutex *)curr->get_location();
+ std::mutex *lock = curr->get_mutex();
struct std::mutex_state *state = lock->get_state();
if (state->locked)
return false;
} else if (curr->is_thread_join()) {
- Thread *blocking = (Thread *)curr->get_location();
+ Thread *blocking = curr->get_thread_operand();
if (!blocking->is_complete()) {
- blocking->push_wait_list(curr);
thread_blocking_check_promises(blocking, get_thread(curr));
return false;
}