return ++used_thread_id;
}
-void ModelChecker::add_system_thread(Thread *t)
-{
- this->system_thread = t;
-}
-
Thread * ModelChecker::schedule_next_thread()
{
Thread *t;
bool ModelChecker::next_execution()
{
num_executions++;
+ print_summary();
if ((exploring = model->get_next_backtrack()) == NULL)
return false;
model->reset_to_initial_state();
continue;
/* Conflict from the same thread is not really a conflict */
if (id == prev->get_tid())
- return NULL;
+ continue;
return prev;
}
return NULL;
DEBUG("trying to push NULL action...\n");
return;
}
+ current_action = NULL;
nextThread = advance_backtracking_state();
next->set_node(currentNode);
set_backtracking(next);
this->action_trace->push_back(next);
}
-void ModelChecker::print_trace(void)
+void ModelChecker::print_summary(void)
{
action_list_t::iterator it;
scheduler->print();
- printf("\nTrace:\n\n");
+ printf("Trace:\n\n");
for (it = action_trace->begin(); it != action_trace->end(); it++) {
DBG();
int ModelChecker::switch_to_master(ModelAction *act)
{
- Thread *old, *next;
+ Thread *old;
DBG();
old = thread_current();
set_current_action(act);
old->set_state(THREAD_READY);
- next = system_thread;
- return old->swap(next);
+ return Thread::swap(old, get_system_context());
}
ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, int value)