threads: bugfix - do not call thread_current() from model-checker

thread_current() was designed for use in the user context. It is not
guaranteed to provide a reliable result in the model-checker context,
since we may perform context switches as needed, such that the "last
executed user thread" may not be the thread that we are checking at the
time.

This change is made to clear up future changes that will modify the
scheduling patterns.

diff --git a/model.cc b/model.cc
index d19fdf9d12c1d809a7e72b4d6974b65f3be674a3..c832b03710fc360ab17bcb5b3afe7a5920c1cfa6 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -216,7 +216,7 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
        if (curr != NULL) {
                /* Do not split atomic actions. */
                if (curr->is_rmwr())
-                       return thread_current();
+                       return get_thread(curr);
                else if (curr->get_type() == THREAD_CREATE)
                        return curr->get_thread_operand();
        }

diff --git a/threads.cc b/threads.cc
index 9de580297871687e4529f2a67512aa6087a9cc1b..a8f282a8b32efdb96d1d248570fc8b7574af92f7 100644 (file)
--- a/threads.cc
+++ b/threads.cc
@@ -23,7 +23,13 @@ static void stack_free(void *stack)
        snapshot_free(stack);
 }
 
-/** Return the currently executing thread. */
+/**
+ * @brief Get the current Thread
+ *
+ * Must be called from a user context
+ *
+ * @return The currently executing thread
+ */
 Thread * thread_current(void)
 {
        ASSERT(model);