From 8b2d7b35e955c675bbfd1f415d25b01494cc330f Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Tue, 12 Feb 2013 17:56:13 -0800 Subject: [PATCH] model: stash all pending actions immediately --- model.cc | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/model.cc b/model.cc index e21806a1..97f235c4 100644 --- a/model.cc +++ b/model.cc @@ -293,9 +293,7 @@ void ModelChecker::execute_sleep_set() for (unsigned int i = 0; i < get_num_threads(); i++) { thread_id_t tid = int_to_id(i); Thread *thr = get_thread(tid); - if (scheduler->is_sleep_set(thr) && thr->get_pending() == NULL) { - scheduler->next_thread(thr); - Thread::swap(&system_context, thr); + if (scheduler->is_sleep_set(thr) && thr->get_pending()) { thr->get_pending()->set_sleep_flag(); } } @@ -2748,8 +2746,14 @@ void ModelChecker::run() add_thread(t); do { - scheduler->next_thread(t); - Thread::swap(&system_context, t); + 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()) { + scheduler->next_thread(thr); + Thread::swap(&system_context, thr); + } + } /* Catch assertions from prior take_step or from * between-ModelAction bugs (e.g., data races) */ -- 2.34.1