threads/model: allocate Thread from w/in ModelChecker
authorBrian Norris <banorris@uci.edu>
Wed, 19 Dec 2012 01:46:40 +0000 (17:46 -0800)
committerBrian Norris <banorris@uci.edu>
Thu, 14 Feb 2013 20:25:04 +0000 (12:25 -0800)
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
libthreads.cc
model.cc
nodestack.cc
threads-model.h

index d5eb581..317c6a7 100644 (file)
--- 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
index adb4b2b..0a56996 100644 (file)
  */
 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)&params));
        return 0;
 }
 
index 0809652..400adc2 100644 (file)
--- 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++) {
index addf93f..b2ef73c 100644 (file)
@@ -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;
index 0236210..d4d2da2 100644 (file)
 #include <threads.h>
 #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 */