remove another field

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index c4bcaf9b1c257ec7ec8707f506d5a35c44cf8e64..9bf9764184c553bdda9a83e983734cf04325b3d6 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -28,7 +28,7 @@ ModelChecker::ModelChecker(struct model_params params) :
        exit_flag(false),
        scheduler(new Scheduler()),
        node_stack(new NodeStack()),
-       execution(new ModelExecution(this, &this->params, scheduler, node_stack)),      // L: Model thread is created inside
+       execution(new ModelExecution(this, &this->params, scheduler, node_stack)),
        execution_number(1),
        diverge(NULL),
        earliest_diverge(NULL),
@@ -95,72 +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));
-}
-
-/**
- * We need to know what the next actions of all threads in the sleep
- * set will be.  This method computes them and stores the actions at
- * the corresponding thread object's pending action.
- */
-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()) {
-                       thr->get_pending()->set_sleep_flag();
-               }
-       }
+       return scheduler->select_next_thread(node_stack->get_head());
 }
 
 /**
@@ -319,8 +259,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 +410,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
@@ -540,12 +482,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<2); // 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();