params(params),
current_action(NULL),
diverge(NULL),
- nextThread(THREAD_ID_T_NONE),
+ nextThread(NULL),
action_trace(new action_list_t()),
thread_map(new HashTable<int, Thread *, int>()),
obj_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),
current_action = NULL;
next_thread_id = INITIAL_THREAD_ID;
used_sequence_numbers = 0;
- nextThread = 0;
+ nextThread = NULL;
next_backtrack = NULL;
failed_promise = false;
snapshotObject->backTrackBeforeStep(0);
return ++used_sequence_numbers;
}
-/**
- * Performs the "scheduling" for the model-checker. That is, it checks if the
- * model-checker has selected a "next thread to run" and returns it, if
- * available. This function should be called from the Scheduler routine, where
- * the Scheduler falls back to a default scheduling routine if needed.
- *
- * @return The next thread chosen by the model-checker. If the model-checker
- * makes no selection, retuns NULL.
- */
-Thread * ModelChecker::schedule_next_thread()
-{
- Thread *t;
- if (nextThread == THREAD_ID_T_NONE)
- return NULL;
- t = thread_map->get(id_to_int(nextThread));
-
- ASSERT(t != NULL);
-
- return t;
-}
-
/**
* Choose the next thread in the replay sequence.
*
* from the backtracking set. Otherwise, simply returns the next thread in the
* sequence that is being replayed.
*/
-thread_id_t ModelChecker::get_next_replay_thread()
+Thread * ModelChecker::get_next_replay_thread()
{
thread_id_t tid;
/* Have we completed exploring the preselected path? */
if (diverge == NULL)
- return THREAD_ID_T_NONE;
+ return NULL;
/* Else, we are trying to replay an execution */
ModelAction *next = node_stack->get_next()->get_action();
tid = next->get_tid();
}
DEBUG("*** ModelChecker chose next thread = %d ***\n", tid);
- return tid;
+ ASSERT(tid != THREAD_ID_T_NONE);
+ return thread_map->get(id_to_int(tid));
}
/**
return next;
}
-void ModelChecker::check_current_action(void)
+Thread * ModelChecker::check_current_action(ModelAction *curr)
{
- ModelAction *curr = this->current_action;
bool already_added = false;
- this->current_action = NULL;
- if (!curr) {
- DEBUG("trying to push NULL action...\n");
- return;
- }
+
+ ASSERT(curr);
if (curr->is_rmwc() || curr->is_rmw()) {
ModelAction *tmp = process_rmw(curr);
/* Assign reads_from values */
Thread *th = get_thread(curr->get_tid());
uint64_t value = VALUE_NONE;
+ bool updated = false;
if (curr->is_read()) {
const ModelAction *reads_from = curr->get_node()->get_read_from();
if (reads_from != NULL) {
value = reads_from->get_value();
/* Assign reads_from, perform release/acquire synchronization */
curr->read_from(reads_from);
- r_modification_order(curr,reads_from);
+ if (r_modification_order(curr,reads_from))
+ updated = true;
} else {
/* Read from future value */
value = curr->get_node()->get_future_value();
promises->push_back(valuepromise);
}
} else if (curr->is_write()) {
- w_modification_order(curr);
- resolve_promises(curr);
+ if (w_modification_order(curr))
+ updated = true;;
+ if (resolve_promises(curr))
+ updated = true;
}
+ if (updated)
+ resolve_release_sequences(curr->get_location());
+
th->set_return_value(value);
/* Add action to list. */
if (!already_added)
add_action_to_lists(curr);
- /** @todo Is there a better interface for setting the next thread rather
- than this field/convoluted approach? Perhaps like just returning
- it or something? */
-
- /* Do not split atomic actions. */
- if (curr->is_rmwr())
- nextThread = thread_current()->get_id();
- else
- nextThread = get_next_replay_thread();
-
Node *currnode = curr->get_node();
Node *parnode = currnode->get_parent();
next_backtrack = curr;
set_backtracking(curr);
+
+ /* Do not split atomic actions. */
+ if (curr->is_rmwr())
+ return thread_current();
+ else
+ return get_next_replay_thread();
}
/** @returns whether the current partial trace is feasible. */
curr = thread_current();
if (curr) {
if (curr->get_state() == THREAD_READY) {
- check_current_action();
+ if (current_action) {
+ nextThread = check_current_action(current_action);
+ current_action = NULL;
+ }
scheduler->add_thread(curr);
} else if (curr->get_state() == THREAD_RUNNING) {
/* Stopped while running; i.e., completed */
ASSERT(false);
}
}
- next = scheduler->next_thread();
+ next = scheduler->next_thread(nextThread);
/* Infeasible -> don't take any more steps */
if (!isfeasible())