params(),
restart_flag(false),
scheduler(new Scheduler()),
- execution(new ModelExecution(this, scheduler)),
history(new ModelHistory()),
+ execution(new ModelExecution(this, scheduler)),
execution_number(1),
trace_analyses(),
inspect_plugin(NULL)
{
memset(&stats,0,sizeof(struct execution_stats));
- init_thread = new Thread(execution->get_next_id(), (thrd_t *) model_malloc(sizeof(thrd_t)), &user_main_wrapper, NULL, NULL); // L: user_main_wrapper passes the user program
+ init_thread = new Thread(execution->get_next_id(), (thrd_t *) model_malloc(sizeof(thrd_t)), &user_main_wrapper, NULL, NULL);
#ifdef TLS
init_thread->setTLS((char *)get_tls_addr());
#endif
/* Infeasible -> don't take any more steps */
if (execution->is_infeasible())
return true;
- else if (execution->isfeasibleprefix() && execution->have_fatal_bug_reports()) {
+ else if (execution->isfeasibleprefix() && execution->have_bug_reports()) {
execution->set_assert();
return true;
} else if (execution->isFinished()) {
for (unsigned int i = 0;i < get_num_threads();i++) {
thread_id_t tid = int_to_id(i);
Thread *thr = get_thread(tid);
- if (!thr->is_model_thread() && !thr->is_complete() && (!thr->get_pending())) {
- switch_from_master(thr); // L: context swapped, and action type of thr changed.
+ if (!thr->is_model_thread() && !thr->is_complete() && !thr->get_pending()) {
+ switch_from_master(thr);
if (thr->is_waiting_on(thr))
assert_bug("Deadlock detected (thread %u)", i);
}
t = get_next_thread();
if (!t || t->is_model_thread())
break;
+ if (t->just_woken_up()) {
+ t->set_wakeup_state(false);
+ t->set_pending(NULL);
+ continue; // Allow this thread to stash the next pending action
+ }
/* Consume the next action for a Thread */
ModelAction *curr = t->get_pending();