model: stash all pending actions immediately

diff --git a/model.cc b/model.cc
index e21806a18a82fd37c2fd3ccfdbe312929a071d99..97f235c463ce2915fb136865e3bd7a3fc0aaebbb 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) */