towards fuzzing only

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index bfb6d22f85009e61e0d4fbad5926764328a4a8fd..f277970a6166e33205a871edcc59ab7bc501daae 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -95,56 +95,12 @@ Thread * ModelChecker::get_current_thread() const
  */
 Thread * ModelChecker::get_next_thread()
 {
-       thread_id_t tid;
 
        /*
         * Have we completed exploring the preselected path? Then let the
         * scheduler decide
         */
-       if (diverge == NULL)    // W: diverge is set to NULL permanently
-               return scheduler->select_next_thread(node_stack->get_head());
-
-       /* Else, we are trying to replay an execution */
-       ModelAction *next = node_stack->get_next()->get_action();
-
-       if (next == diverge) {
-               if (earliest_diverge == NULL || *diverge < *earliest_diverge)
-                       earliest_diverge = diverge;
-
-               Node *nextnode = next->get_node();
-               Node *prevnode = nextnode->get_parent();
-               scheduler->update_sleep_set(prevnode);
-
-               /* Reached divergence point */
-               if (nextnode->increment_behaviors()) {
-                       /* Execute the same thread with a new behavior */
-                       tid = next->get_tid();
-                       node_stack->pop_restofstack(2);
-               } else {
-                       ASSERT(prevnode);
-                       /* Make a different thread execute for next step */
-                       scheduler->add_sleep(get_thread(next->get_tid()));
-                       tid = prevnode->get_next_backtrack();
-                       /* Make sure the backtracked thread isn't sleeping. */
-                       node_stack->pop_restofstack(1);
-                       if (diverge == earliest_diverge) {
-                               earliest_diverge = prevnode->get_action();
-                       }
-               }
-               /* Start the round robin scheduler from this thread id */
-               scheduler->set_scheduler_thread(tid);
-               /* The correct sleep set is in the parent node. */
-               execute_sleep_set();
-
-               DEBUG("*** Divergence point ***\n");
-
-               diverge = NULL;
-       } else {
-               tid = next->get_tid();
-       }
-       DEBUG("*** ModelChecker chose next thread = %d ***\n", id_to_int(tid));
-       ASSERT(tid != THREAD_ID_T_NONE);
-       return get_thread(id_to_int(tid));
+       return scheduler->select_next_thread(node_stack->get_head());
 }
 
 /**
@@ -319,8 +275,7 @@ bool ModelChecker::next_execution()
 // test code
        execution_number++;
        reset_to_initial_state();
-       node_stack->pop_restofstack(2);
-//     node_stack->full_reset();
+       node_stack->full_reset();
        diverge = NULL;
        return false;
 /* test
@@ -471,12 +426,15 @@ void ModelChecker::do_restart()
 /** @brief Run ModelChecker for the user program */
 void ModelChecker::run()
 {
-       bool has_next;
        int i = 0;
+       //Need to initial random number generator state to avoid resets on rollback
+       char random_state[256];
+       initstate(423121, random_state, sizeof(random_state));
        do {
                thrd_t user_thread;
                Thread *t = new Thread(execution->get_next_id(), &user_thread, &user_main_wrapper, NULL, NULL); // L: user_main_wrapper passes the user program
                execution->add_thread(t);
+               //Need to seed random number generator, otherwise its state gets reset
                do {
                        /*
                         * Stash next pending action(s) for thread(s). There
@@ -503,8 +461,6 @@ void ModelChecker::run()
                                        scheduler->sleep(th);
                                }
                        }
-                       /* Catch assertions from prior take_step or from
-                        * between-ModelAction bugs (e.g., data races) */
 
                        for (unsigned int i = 1; i < get_num_threads(); i++) {
                                Thread *th = get_thread(int_to_id(i));
@@ -512,17 +468,23 @@ void ModelChecker::run()
                                if (act && execution->is_enabled(th) && (th->get_state() != THREAD_BLOCKED) ){
                                        if (act->is_write()){
                                                std::memory_order order = act->get_mo(); 
-                                               if (order == std::memory_order_relaxed || order == std::memory_order_release) {
+                                               if (order == std::memory_order_relaxed || \
+                                                       order == std::memory_order_release) {
                                                        t = th;
                                                        break;
                                                }
-                                       } else if (act->get_type() == THREAD_CREATE || act->get_type() == THREAD_START || act->get_type() == THREAD_FINISH) {
+                                       } else if (act->get_type() == THREAD_CREATE || \
+                                                       act->get_type() == PTHREAD_CREATE || \
+                                                       act->get_type() == THREAD_START || \
+                                                       act->get_type() == THREAD_FINISH) {
                                                t = th;
                                                break;
                                        }                               
                                }
                        }
 
+                       /* Catch assertions from prior take_step or from
+                        * between-ModelAction bugs (e.g., data races) */
 
                        if (execution->has_asserted())
                                break;
@@ -536,12 +498,11 @@ void ModelChecker::run()
                        t->set_pending(NULL);
                        t = execution->take_step(curr);
                } while (!should_terminate_execution());
-
-               has_next = next_execution();
+               next_execution();
                i++;
-       } while (i<250); // while (has_next);
-
-       execution->fixup_release_sequences();
+               //restore random number generator state after rollback
+               setstate(random_state);
+       } while (i<5); // while (has_next);
 
        model_print("******* Model-checking complete: *******\n");
        print_stats();