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.

diff --git a/action.cc b/action.cc
index d5eb581a23d4e7ec5b7ffe3aefeff54fb263ae94..317c6a7cd87d9a94fbb695ecb95615ed5bae5613 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -253,10 +253,11 @@ void ModelAction::copy_typeandorder(ModelAction * act)
  */
 Thread * ModelAction::get_thread_operand() const
 {
  */
 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
                /* THREAD_JOIN uses (Thread *) for location */
                return (Thread *)get_location();
        else

diff --git a/libthreads.cc b/libthreads.cc
index adb4b2bfdb0c4f709999d6d2c6af6554098e9325..0a5699695f9e856f413bddec9714751a0313c99d 100644 (file)
--- a/libthreads.cc
+++ b/libthreads.cc
@@ -10,11 +10,9 @@
  */
 int thrd_create(thrd_t *t, thrd_start_t start_routine, void *arg)
 {
  */
 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 */
        /* 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;
 }
 
        return 0;
 }
 

diff --git a/model.cc b/model.cc
index 08096528bddc326b04dbe31b0772b1fcfb6458f6..400adc208047f8d2c7b4700c31bc20b650854e34 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: {
 
        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++) {
                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 addf93f67469f1cd7f96a15ffad8ec5551cb1c1b..b2ef73cac30108fab56745f89b0542a186fc6410 100644 (file)
--- 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];
        }
                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;
        total_nodes++;
        head_idx++;
        return NULL;

diff --git a/threads-model.h b/threads-model.h
index 02362100dca410b35f531ef536e2066f85315890..d4d2da29e82a7fc1c58a2a61db7ee61aac7206a5 100644 (file)
--- a/threads-model.h
+++ b/threads-model.h
@@ -13,6 +13,11 @@
 #include <threads.h>
 #include "modeltypes.h"
 
 #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 */
 /** @brief Represents the state of a user Thread */
 typedef enum thread_state {
        /** Thread was just created and hasn't run yet */