model: refactor "get next thread" code

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 43530fe12c25e2ecafa4af78cbb5eb3008b6190d..90c7ad91493bf50bd0c7859ba1d01db7d12afb09 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -39,6 +39,8 @@ ModelChecker::ModelChecker(struct model_params params) :
        priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv));
        /* First thread created will have id INITIAL_THREAD_ID */
        priv->next_thread_id = INITIAL_THREAD_ID;
+
+       lazy_sync_size = &priv->lazy_sync_size;
 }
 
 /** @brief Destructor */
@@ -96,16 +98,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;
@@ -360,21 +375,13 @@ 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
  * feasible trace. */
-
 bool ModelChecker::isfeasibleprefix() {
-       return promises->size()==0;
+       return promises->size() == 0 && *lazy_sync_size == 0;
 }
 
 /** @returns whether the current partial trace is feasible. */
@@ -565,7 +572,11 @@ bool ModelChecker::release_seq_head(const ModelAction *rf,
        if (rf->is_release())
                release_heads->push_back(rf);
        if (rf->is_rmw()) {
-               if (rf->is_acquire())
+               /* We need a RMW action that is both an acquire and release to stop */
+               /** @todo Need to be smarter here...  In the linux lock
+                * example, this will run to the beginning of the program for
+                * every acquire. */
+               if (rf->is_acquire() && rf->is_release())
                        return true; /* complete */
                return release_seq_head(rf->get_reads_from(), release_heads);
        }
@@ -665,6 +676,7 @@ void ModelChecker::get_release_seq_heads(ModelAction *act,
                std::list<ModelAction *> *list;
                list = lazy_sync_with_release->get_safe_ptr(act->get_location());
                list->push_back(act);
+               (*lazy_sync_size)++;
        }
 }
 
@@ -711,9 +723,10 @@ bool ModelChecker::resolve_release_sequences(void *location)
                                        propagate->synchronize_with(act);
                        }
                }
-               if (complete)
+               if (complete) {
                        it = list->erase(it);
-               else
+                       (*lazy_sync_size)--;
+               } else
                        it++;
        }