add support for pthread_mutex

[c11tester.git] / execution.cc

diff --git a/execution.cc b/execution.cc
index 0fcf4e8d10b206e5a07062849e038c12915264a9..887e2efa03df0f31832ff6ee260a1a8b1ed9794d 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -17,6 +17,8 @@
 #include "threads-model.h"
 #include "bugmessage.h"
 
+#include <pthread.h>
+
 #define INITIAL_THREAD_ID      0
 
 /**
@@ -947,6 +949,22 @@ bool ModelExecution::process_thread_action(ModelAction *curr)
                thrd_t *thrd = (thrd_t *)curr->get_location();
                struct thread_params *params = (struct thread_params *)curr->get_value();
                Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
+               curr->set_thread_operand(th);
+               add_thread(th);
+               th->set_creation(curr);
+               /* Promises can be satisfied by children */
+               for (unsigned int i = 0; i < promises.size(); i++) {
+                       Promise *promise = promises[i];
+                       if (promise->thread_is_available(curr->get_tid()))
+                               promise->add_thread(th->get_id());
+               }
+               break;
+       }
+       case PTHREAD_CREATE: {
+               thrd_t *thrd = (thrd_t *)curr->get_location();
+               struct pthread_params *params = (struct pthread_params *)curr->get_value();
+               Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
+               curr->set_thread_operand(th);
                add_thread(th);
                th->set_creation(curr);
                /* Promises can be satisfied by children */
@@ -964,6 +982,14 @@ bool ModelExecution::process_thread_action(ModelAction *curr)
                updated = true; /* trigger rel-seq checks */
                break;
        }
+       case PTHREAD_JOIN: {
+               Thread *blocking = curr->get_thread_operand();
+               ModelAction *act = get_last_action(blocking->get_id());
+               synchronize(act, curr);
+               updated = true; /* trigger rel-seq checks */
+               break; // WL: to be add (modified)
+       }
+
        case THREAD_FINISH: {
                Thread *th = get_thread(curr);
                /* Wake up any joining threads */
@@ -1132,6 +1158,7 @@ bool ModelExecution::initialize_curr_action(ModelAction **curr)
  *
  * @return True if this read established synchronization
  */
+
 bool ModelExecution::read_from(ModelAction *act, const ModelAction *rf)
 {
        ASSERT(rf);
@@ -2692,7 +2719,7 @@ static void print_list(const action_list_t *list)
        action_list_t::const_iterator it;
 
        model_print("------------------------------------------------------------------------------------\n");
-       model_print("#    t    Action type     MO       Location         Value               Rf  CV\n");
+       model_print("#    t     Action type     MO       Location         Value               Rf  CV\n");
        model_print("------------------------------------------------------------------------------------\n");
 
        unsigned int hash = 0;
@@ -2891,8 +2918,12 @@ Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) cons
        }
 
        /* Follow CREATE with the created thread */
+       /* which is not needed, because model.cc takes care of this */
        if (curr->get_type() == THREAD_CREATE)
+               return curr->get_thread_operand(); 
+       if (curr->get_type() == PTHREAD_CREATE) {
                return curr->get_thread_operand();
+       }
        return NULL;
 }