From 3e520de48b5be0b0d4fa4a5f033e207b17c4496d Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Tue, 12 Feb 2013 16:54:38 -0800 Subject: [PATCH] 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. --- model.cc | 2 +- threads.cc | 8 +++++++- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/model.cc b/model.cc index d19fdf9..c832b03 100644 --- 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 9de5802..a8f282a 100644 --- 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); -- 2.34.1