{
action_type type = act->get_type();
- switch (type) {
- case ATOMIC_READ:
- case ATOMIC_WRITE:
- case ATOMIC_RMW:
- break;
- default:
- return NULL;
- }
- /* linear search: from most recent to oldest */
- action_list_t *list = obj_map->get_safe_ptr(act->get_location());
- action_list_t::reverse_iterator rit;
- for (rit = list->rbegin(); rit != list->rend(); rit++) {
- ModelAction *prev = *rit;
- if (act->is_synchronizing(prev))
- return prev;
+ if (type==ATOMIC_READ||type==ATOMIC_WRITE||type==ATOMIC_RMW) {
+ /* linear search: from most recent to oldest */
+ action_list_t *list = obj_map->get_safe_ptr(act->get_location());
+ action_list_t::reverse_iterator rit;
+ for (rit = list->rbegin(); rit != list->rend(); rit++) {
+ ModelAction *prev = *rit;
+ if (act->is_synchronizing(prev))
+ return prev;
+ }
+ } else if (type==ATOMIC_LOCK||type==ATOMIC_TRYLOCK) {
+ /* linear search: from most recent to oldest */
+ action_list_t *list = obj_map->get_safe_ptr(act->get_location());
+ action_list_t::reverse_iterator rit;
+ for (rit = list->rbegin(); rit != list->rend(); rit++) {
+ ModelAction *prev = *rit;
+ if (prev->is_success_lock())
+ return prev;
+ }
+ } else if (type==ATOMIC_UNLOCK) {
+ /* linear search: from most recent to oldest */
+ action_list_t *list = obj_map->get_safe_ptr(act->get_location());
+ action_list_t::reverse_iterator rit;
+ for (rit = list->rbegin(); rit != list->rend(); rit++) {
+ ModelAction *prev = *rit;
+ if (prev->is_failed_trylock())
+ return prev;
+ }
}
return NULL;
}
curr = tmp;
compute_promises(curr);
} else {
- ModelAction *tmp = node_stack->explore_action(curr, NULL);
+ ModelAction *tmp = node_stack->explore_action(curr, scheduler->get_enabled());
if (tmp) {
/* Discard duplicate ModelAction; use action from NodeStack */
/* First restore type and order in case of RMW operation */
if (curr->is_rmwr())
tmp->copy_typeandorder(curr);
-
+
/* If we have diverged, we need to reset the clock vector. */
if (diverge == NULL)
tmp->create_cv(get_parent_action(tmp->get_tid()));
-
+
delete curr;
curr = tmp;
} else {
* @return Returns true (success) if a step was taken and false otherwise.
*/
bool ModelChecker::take_step() {
- Thread *curr, *next;
-
if (has_asserted())
return false;
- curr = thread_current();
+ Thread * curr = thread_current();
if (curr) {
if (curr->get_state() == THREAD_READY) {
ASSERT(priv->current_action);
priv->nextThread = check_current_action(priv->current_action);
priv->current_action = NULL;
- if (!curr->is_blocked() && !curr->is_complete())
- scheduler->add_thread(curr);
+ if (curr->is_blocked() || curr->is_complete())
+ scheduler->remove_thread(curr);
} else {
ASSERT(false);
}
}
- next = scheduler->next_thread(priv->nextThread);
+ Thread * next = scheduler->next_thread(priv->nextThread);
/* Infeasible -> don't take any more steps */
if (!isfeasible())