model: stash all pending actions immediately
authorBrian Norris <banorris@uci.edu>
Wed, 13 Feb 2013 01:56:13 +0000 (17:56 -0800)
committerBrian Norris <banorris@uci.edu>
Fri, 15 Feb 2013 22:55:02 +0000 (14:55 -0800)
model.cc

index e21806a..97f235c 100644 (file)
--- 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);
        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();
                }
        }
                        thr->get_pending()->set_sleep_flag();
                }
        }
@@ -2748,8 +2746,14 @@ void ModelChecker::run()
                add_thread(t);
 
                do {
                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) */
 
                        /* Catch assertions from prior take_step or from
                         * between-ModelAction bugs (e.g., data races) */