thread_id_t tid = int_to_id(i);
Thread *thr = get_thread(tid);
if (scheduler->is_sleep_set(thr) && thr->get_pending() == NULL) {
- thr->set_state(THREAD_RUNNING);
scheduler->next_thread(thr);
Thread::swap(&system_context, thr);
priv->current_action->set_sleep_flag();
switch (curr->get_type()) {
case THREAD_CREATE: {
- Thread *th = curr->get_thread_operand();
+ thrd_t *thrd = (thrd_t *)curr->get_location();
+ struct thread_params *params = (struct thread_params *)curr->get_value();
+ Thread *th = new Thread(thrd, params->func, params->arg);
+ add_thread(th);
th->set_creation(curr);
/* Promises can be satisfied by children */
for (unsigned int i = 0; i < promises->size(); i++) {
DBG();
Thread *old = thread_current();
set_current_action(act);
- old->set_state(THREAD_READY);
if (Thread::swap(old, &system_context) < 0) {
perror("swap threads");
exit(EXIT_FAILURE);
/**
* Takes the next step in the execution, if possible.
* @param curr The current step to take
- * @return Returns true (success) if a step was taken and false otherwise.
+ * @return Returns the next Thread to run, if any; NULL if this execution
+ * should terminate
*/
-bool ModelChecker::take_step(ModelAction *curr)
+Thread * ModelChecker::take_step(ModelAction *curr)
{
if (has_asserted())
- return false;
+ return NULL;
Thread *curr_thrd = get_thread(curr);
ASSERT(curr_thrd->get_state() == THREAD_READY);
/* Infeasible -> don't take any more steps */
if (is_infeasible())
- return false;
+ return NULL;
else if (isfeasibleprefix() && have_bug_reports()) {
set_assert();
- return false;
+ return NULL;
}
- if (params.bound != 0)
- if (priv->used_sequence_numbers > params.bound)
- return false;
+ if (params.bound != 0 && priv->used_sequence_numbers > params.bound)
+ return NULL;
if (curr_thrd->is_blocked() || curr_thrd->is_complete())
scheduler->remove_thread(curr_thrd);
std::memory_order_seq_cst, NULL, VALUE_NONE,
model_thread);
set_current_action(fixup);
- return true;
+ return model_thread;
}
/* next_thrd == NULL -> don't take any more steps */
if (!next_thrd)
- return false;
-
- next_thrd->set_state(THREAD_RUNNING);
+ return NULL;
if (next_thrd->get_pending() != NULL) {
/* restart a pending action */
set_current_action(next_thrd->get_pending());
next_thrd->set_pending(NULL);
- next_thrd->set_state(THREAD_READY);
- return true;
+ return next_thrd;
}
- /* Return false only if swap fails with an error */
- return (Thread::swap(&system_context, next_thrd) == 0);
+ return next_thrd;
}
/** Wrapper to run the user's main function, with appropriate arguments */
do {
thrd_t user_thread;
Thread *t = new Thread(&user_thread, &user_main_wrapper, NULL);
-
add_thread(t);
- /* Run user thread up to its first action */
- scheduler->next_thread(t);
- Thread::swap(&system_context, t);
-
- /* Wait for all threads to complete */
- while (take_step(priv->current_action));
+ do {
+ scheduler->next_thread(t);
+ Thread::swap(&system_context, t);
+ t = take_step(priv->current_action);
+ } while (t && !t->is_model_thread());
+ /** @TODO Re-write release sequence fixups here */
} while (next_execution());
print_stats();