From 82df62c2b0805848b87bb71df5b66a4a66f8e25d Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Tue, 18 Dec 2012 17:46:40 -0800 Subject: [PATCH] threads/model: allocate Thread from w/in ModelChecker It adds scheduling difficulties if we allocate/schedule a Thread from the user-context (i.e., directly from the thrd_create() interface) because then it is not necessarily atomic. For example, if we run a thread up to its context switch for a THREAD_CREATE then switch to another thread before the THREAD_CREATE is processed, then we will already have constructed a Thread from the first thread (and prepared it for scheduling) without processing it in the ModelChecker appropriately. For instance, the following schedule might appear, causing problems: TID ACTION --- ------ ... 1 ATOMIC_READ <--- Next action is THREAD_CREATE (1) (construct Thread 3) (1) (prepare new Thread for Scheduling) 2 ATOMIC_READ 3 THREAD_START <--- Before its CREATE event?? 1 THREAD_CREATE Note that this scheduling does not yet happen, as we always execute the "lead-in" to THREAD_CREATE atomically. This may change, though. --- action.cc | 9 +++++---- libthreads.cc | 6 ++---- model.cc | 5 ++++- nodestack.cc | 6 +++++- threads-model.h | 5 +++++ 5 files changed, 21 insertions(+), 10 deletions(-) diff --git a/action.cc b/action.cc index d5eb581..317c6a7 100644 --- a/action.cc +++ b/action.cc @@ -253,10 +253,11 @@ void ModelAction::copy_typeandorder(ModelAction * act) */ Thread * ModelAction::get_thread_operand() const { - if (type == THREAD_CREATE) - /* THREAD_CREATE uses (Thread *) for location */ - return (Thread *)get_location(); - else if (type == THREAD_JOIN) + if (type == THREAD_CREATE) { + /* THREAD_CREATE stores its (Thread *) in a thrd_t::priv */ + thrd_t *thrd = (thrd_t *)get_location(); + return thrd->priv; + } else if (type == THREAD_JOIN) /* THREAD_JOIN uses (Thread *) for location */ return (Thread *)get_location(); else diff --git a/libthreads.cc b/libthreads.cc index adb4b2b..0a56996 100644 --- a/libthreads.cc +++ b/libthreads.cc @@ -10,11 +10,9 @@ */ int thrd_create(thrd_t *t, thrd_start_t start_routine, void *arg) { - Thread *thread; - thread = new Thread(t, start_routine, arg); - model->add_thread(thread); + struct thread_params params = { start_routine, arg }; /* seq_cst is just a 'don't care' parameter */ - model->switch_to_master(new ModelAction(THREAD_CREATE, std::memory_order_seq_cst, thread, VALUE_NONE)); + model->switch_to_master(new ModelAction(THREAD_CREATE, std::memory_order_seq_cst, t, (uint64_t)¶ms)); return 0; } diff --git a/model.cc b/model.cc index 0809652..400adc2 100644 --- a/model.cc +++ b/model.cc @@ -969,7 +969,10 @@ bool ModelChecker::process_thread_action(ModelAction *curr) switch (curr->get_type()) { case THREAD_CREATE: { - Thread *th = curr->get_thread_operand(); + thrd_t *thrd = (thrd_t *)curr->get_location(); + struct thread_params *params = (struct thread_params *)curr->get_value(); + Thread *th = new Thread(thrd, params->func, params->arg); + add_thread(th); th->set_creation(curr); /* Promises can be satisfied by children */ for (unsigned int i = 0; i < promises->size(); i++) { diff --git a/nodestack.cc b/nodestack.cc index addf93f..b2ef73c 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -556,7 +556,11 @@ ModelAction * NodeStack::explore_action(ModelAction *act, enabled_type_t *is_ena if (model->params.fairwindow != 0 && head_idx > (int)model->params.fairwindow) prevfairness = node_list[head_idx - model->params.fairwindow]; } - node_list.push_back(new Node(act, head, model->get_num_threads(), prevfairness)); + + int next_threads = model->get_num_threads(); + if (act->get_type() == THREAD_CREATE) + next_threads++; + node_list.push_back(new Node(act, head, next_threads, prevfairness)); total_nodes++; head_idx++; return NULL; diff --git a/threads-model.h b/threads-model.h index 0236210..d4d2da2 100644 --- a/threads-model.h +++ b/threads-model.h @@ -13,6 +13,11 @@ #include #include "modeltypes.h" +struct thread_params { + thrd_start_t func; + void *arg; +}; + /** @brief Represents the state of a user Thread */ typedef enum thread_state { /** Thread was just created and hasn't run yet */ -- 2.34.1