model: stash actions in each thread

We don't want a global 'current_action' for saving the next action to
run; we want to stash the 'current action' for each thread. So just use
the 'pending' action in each Thread.

Note that this kinda breaks sleep sets for now. We'll have to redo this.

diff --git a/model.cc b/model.cc
index f5dd7cbda419209acf023c27d340218d146ebcff..d19fdf9d12c1d809a7e72b4d6974b65f3be674a3 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -39,7 +39,6 @@ struct bug_message {
  */
 struct model_snapshot_members {
        model_snapshot_members() :
  */
 struct model_snapshot_members {
        model_snapshot_members() :

-               current_action(NULL),

                /* First thread created will have id INITIAL_THREAD_ID */
                next_thread_id(INITIAL_THREAD_ID),
                used_sequence_numbers(0),
                /* First thread created will have id INITIAL_THREAD_ID */
                next_thread_id(INITIAL_THREAD_ID),
                used_sequence_numbers(0),


@@ -59,7 +58,6 @@ struct model_snapshot_members {
                bugs.clear();
        }
 
                bugs.clear();
        }
 

-       ModelAction *current_action;

        unsigned int next_thread_id;
        modelclock_t used_sequence_numbers;
        ModelAction *next_backtrack;
        unsigned int next_thread_id;
        modelclock_t used_sequence_numbers;
        ModelAction *next_backtrack;


@@ -298,8 +296,7 @@ void ModelChecker::execute_sleep_set()
                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() == NULL) {
                        scheduler->next_thread(thr);
                        Thread::swap(&system_context, thr);

-                       priv->current_action->set_sleep_flag();
-                       thr->set_pending(priv->current_action);
+                       thr->get_pending()->set_sleep_flag();

                }
        }
 }
                }
        }
 }


@@ -1215,16 +1212,6 @@ bool ModelChecker::check_action_enabled(ModelAction *curr) {
        return true;
 }
 
        return true;
 }
 

-/**
- * Stores the ModelAction for the current thread action.  Call this
- * immediately before switching from user- to system-context to pass
- * data between them.
- * @param act The ModelAction created by the user-thread action
- */
-void ModelChecker::set_current_action(ModelAction *act) {
-       priv->current_action = act;
-}
-

 /**
  * This is the heart of the model checker routine. It performs model-checking
  * actions corresponding to a given "current action." Among other processes, it
 /**
  * This is the heart of the model checker routine. It performs model-checking
  * actions corresponding to a given "current action." Among other processes, it


@@ -2678,7 +2665,7 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act)
 {
        DBG();
        Thread *old = thread_current();
 {
        DBG();
        Thread *old = thread_current();

-       set_current_action(act);
+       old->set_pending(act);

        if (Thread::swap(old, &system_context) < 0) {
                perror("swap threads");
                exit(EXIT_FAILURE);
        if (Thread::swap(old, &system_context) < 0) {
                perror("swap threads");
                exit(EXIT_FAILURE);


@@ -2738,7 +2725,7 @@ Thread * ModelChecker::take_step(ModelAction *curr)
                ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,
                                std::memory_order_seq_cst, NULL, VALUE_NONE,
                                model_thread);
                ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,
                                std::memory_order_seq_cst, NULL, VALUE_NONE,
                                model_thread);

-               set_current_action(fixup);
+               model_thread->set_pending(fixup);

                return model_thread;
        }
 
                return model_thread;
        }
 


@@ -2746,13 +2733,6 @@ Thread * ModelChecker::take_step(ModelAction *curr)
        if (!next_thrd)
                return NULL;
 
        if (!next_thrd)
                return NULL;
 

-       if (next_thrd->get_pending() != NULL) {
-               /* restart a pending action */
-               set_current_action(next_thrd->get_pending());
-               next_thrd->set_pending(NULL);
-               return next_thrd;
-       }
-

        return next_thrd;
 }
 
        return next_thrd;
 }
 


@@ -2773,7 +2753,11 @@ void ModelChecker::run()
                do {
                        scheduler->next_thread(t);
                        Thread::swap(&system_context, t);
                do {
                        scheduler->next_thread(t);
                        Thread::swap(&system_context, t);

-                       t = take_step(priv->current_action);
+
+                       /* Consume the next action for a Thread */
+                       ModelAction *curr = t->get_pending();
+                       t->set_pending(NULL);
+                       t = take_step(curr);

                } while (t && !t->is_model_thread());
                /** @TODO Re-write release sequence fixups here */
        } while (next_execution());
                } while (t && !t->is_model_thread());
                /** @TODO Re-write release sequence fixups here */
        } while (next_execution());

diff --git a/model.h b/model.h
index cd9c3989bde935ce2ec8c67da5ddd4490a3b3e34..a5262d2b5c46e18e697cedf646cb0eb539fed3d6 100644 (file)
--- a/model.h
+++ b/model.h
@@ -148,7 +148,6 @@ private:
        modelclock_t get_next_seq_num();
 
        bool next_execution();
        modelclock_t get_next_seq_num();
 
        bool next_execution();

-       void set_current_action(ModelAction *act);

        ModelAction * check_current_action(ModelAction *curr);
        bool initialize_curr_action(ModelAction **curr);
        bool process_read(ModelAction *curr, bool second_part_of_rmw);
        ModelAction * check_current_action(ModelAction *curr);
        bool initialize_curr_action(ModelAction **curr);
        bool process_read(ModelAction *curr, bool second_part_of_rmw);