model: stash all pending actions immediately

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index d19fdf9d12c1d809a7e72b4d6974b65f3be674a3..97f235c463ce2915fb136865e3bd7a3fc0aaebbb 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -216,7 +216,7 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
        if (curr != NULL) {
                /* Do not split atomic actions. */
                if (curr->is_rmwr())
-                       return thread_current();
+                       return get_thread(curr);
                else if (curr->get_type() == THREAD_CREATE)
                        return curr->get_thread_operand();
        }
@@ -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();
                }
        }
@@ -2681,9 +2679,6 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act)
  */
 Thread * ModelChecker::take_step(ModelAction *curr)
 {
-       if (has_asserted())
-               return NULL;
-
        Thread *curr_thrd = get_thread(curr);
        ASSERT(curr_thrd->get_state() == THREAD_READY);
 
@@ -2751,8 +2746,19 @@ 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) */
+                       if (has_asserted())
+                               break;
 
                        /* Consume the next action for a Thread */
                        ModelAction *curr = t->get_pending();