#include <algorithm>
#include <mutex>
#include <new>
+#include <stdarg.h>
#include "model.h"
#include "action.h"
* @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)
+bool ModelChecker::assert_bug(const char *msg, ...)
{
- priv->bugs.push_back(new bug_message(msg));
+ char str[800];
+
+ va_list ap;
+ va_start(ap, msg);
+ vsnprintf(str, sizeof(str), msg, ap);
+ va_end(ap);
+
+ priv->bugs.push_back(new bug_message(str));
if (isfeasibleprefix()) {
set_assert();
Thread *curr_thrd = get_thread(curr);
ASSERT(curr_thrd->get_state() == THREAD_READY);
- if (!check_action_enabled(curr)) {
- /* Make the execution look like we chose to run this action
- * much later, when a lock/join can succeed */
- get_thread(curr)->set_pending(curr);
- scheduler->sleep(curr_thrd);
- curr = NULL;
- } else {
- curr = check_current_action(curr);
- ASSERT(curr);
- }
+ ASSERT(check_action_enabled(curr)); /* May have side effects? */
+ curr = check_current_action(curr);
+ ASSERT(curr);
if (curr_thrd->is_blocked() || curr_thrd->is_complete())
scheduler->remove_thread(curr_thrd);
- if (curr)
- return action_select_next_thread(curr);
- return NULL;
+ return action_select_next_thread(curr);
}
/** Wrapper to run the user's main function, with appropriate arguments */
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");
+ assert_bug("Deadlock detected (thread %u)", i);
+ }
+ }
+
+ /* Don't schedule threads which should be disabled */
+ for (unsigned int i = 0; i < get_num_threads(); i++) {
+ Thread *th = get_thread(int_to_id(i));
+ ModelAction *act = th->get_pending();
+ if (act && is_enabled(th) && !check_action_enabled(act)) {
+ scheduler->sleep(th);
}
}