Merge branch 'demsky'

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 6f144abab044d5d6a23880a9744e2b95ee5b3f24..3e54a001a4541b8d5acada69e76c189ff5e82b36 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -100,16 +100,29 @@ modelclock_t ModelChecker::get_next_seq_num()
 }
 
 /**
- * Choose the next thread in the replay sequence.
+ * @brief Choose the next thread to execute.
  *
- * If the replay sequence has reached the 'diverge' point, returns a thread
- * from the backtracking set. Otherwise, simply returns the next thread in the
- * sequence that is being replayed.
+ * This function chooses the next thread that should execute. It can force the
+ * adjacency of read/write portions of a RMW action, force THREAD_CREATE to be
+ * followed by a THREAD_START, or it can enforce execution replay/backtracking.
+ * The model-checker may have no preference regarding the next thread (i.e.,
+ * when exploring a new execution ordering), in which case this will return
+ * NULL.
+ * @param curr The current ModelAction. This action might guide the choice of
+ * next thread.
+ * @return The next thread to run. If the model-checker has no preference, NULL.
  */
-Thread * ModelChecker::get_next_replay_thread()
+Thread * ModelChecker::get_next_thread(ModelAction *curr)
 {
        thread_id_t tid;
 
+       /* Do not split atomic actions. */
+       if (curr->is_rmwr())
+               return thread_current();
+       /* The THREAD_CREATE action points to the created Thread */
+       else if (curr->get_type() == THREAD_CREATE)
+               return (Thread *)curr->get_location();
+
        /* Have we completed exploring the preselected path? */
        if (diverge == NULL)
                return NULL;
@@ -339,28 +352,37 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                }
        }
 
-       /* Assign 'creation' parent */
-       if (curr->get_type() == THREAD_CREATE) {
+       /* Thread specific actions */
+       switch(curr->get_type()) {
+       case THREAD_CREATE: {
                Thread *th = (Thread *)curr->get_location();
                th->set_creation(curr);
-       } else if (curr->get_type() == THREAD_JOIN) {
+               break;
+       }
+       case THREAD_JOIN: {
                Thread *wait, *join;
                wait = get_thread(curr->get_tid());
                join = (Thread *)curr->get_location();
                if (!join->is_complete())
                        scheduler->wait(wait, join);
-       } else if (curr->get_type() == THREAD_FINISH) {
+               break;
+       }
+       case THREAD_FINISH: {
                Thread *th = get_thread(curr->get_tid());
                while (!th->wait_list_empty()) {
                        Thread *wake = th->pop_wait_list();
                        scheduler->wake(wake);
                }
                th->complete();
+               break;
        }
-
-       /* Deal with new thread */
-       if (curr->get_type() == THREAD_START)
+       case THREAD_START: {
                check_promises(NULL, curr->get_cv());
+               break;
+       }
+       default:
+               break;
+       }
 
        Thread *th = get_thread(curr->get_tid());
 
@@ -399,14 +421,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 
        set_backtracking(curr);
 
-       /* Do not split atomic actions. */
-       if (curr->is_rmwr())
-               return thread_current();
-       /* The THREAD_CREATE action points to the created Thread */
-       else if (curr->get_type() == THREAD_CREATE)
-               return (Thread *)curr->get_location();
-       else
-               return get_next_replay_thread();
+       return get_next_thread(curr);
 }
 
 /** @returns whether the current partial trace must be a prefix of a