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
* @param msg Descriptive message for the bug (do not include newline char)
* @return True if bug is immediately-feasible
*/
-bool ModelChecker::assert_bug(const char *msg, ...)
+void ModelChecker::assert_bug(const char *msg, ...)
{
char str[800];
vsnprintf(str, sizeof(str), msg, ap);
va_end(ap);
- return execution->assert_bug(str);
+ execution->assert_bug(str);
}
/**
void ModelChecker::assert_user_bug(const char *msg)
{
/* If feasible bug, bail out now */
- if (assert_bug(msg))
- switch_to_master(NULL);
+ assert_bug(msg);
+ switch_to_master(NULL);
}
/** @brief Print bug report listing for this execution (if any bugs exist) */
void ModelChecker::record_stats()
{
stats.num_total ++;
- if (!execution->isfeasibleprefix())
- stats.num_infeasible ++;
- else if (execution->have_bug_reports())
+ if (execution->have_bug_reports())
stats.num_buggy_executions ++;
else if (execution->is_complete_execution())
stats.num_complete ++;
else {
- stats.num_redundant ++;
-
+ //All threads are sleeping
/**
* @todo We can violate this ASSERT() when fairness/sleep sets
* conflict to cause an execution to terminate, e.g. with:
void ModelChecker::print_stats() const
{
model_print("Number of complete, bug-free executions: %d\n", stats.num_complete);
- model_print("Number of redundant executions: %d\n", stats.num_redundant);
model_print("Number of buggy executions: %d\n", stats.num_buggy_executions);
- model_print("Number of infeasible executions: %d\n", stats.num_infeasible);
model_print("Total executions: %d\n", stats.num_total);
}
{
DBG();
/* Is this execution a feasible execution that's worth bug-checking? */
- bool complete = execution->isfeasibleprefix() &&
- (execution->is_complete_execution() ||
+ bool complete = (execution->is_complete_execution() ||
execution->have_bug_reports());
/* End-of-execution bug checks */
bool ModelChecker::should_terminate_execution()
{
- /* Infeasible -> don't take any more steps */
- if (execution->is_infeasible())
- return true;
- else if (execution->isfeasibleprefix() && execution->have_fatal_bug_reports()) {
+ if (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);
+ t = NULL;
+ continue; // Allow this thread to stash the next pending action
+ }
/* Consume the next action for a Thread */
ModelAction *curr = t->get_pending();