pthread_create is working now

diff --git a/action.cc b/action.cc
index c913b74c80daa134f4e1140c1b4ffb292d2882aa..ea4921050ee541575c65f43241211935268bfa36 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -280,10 +280,16 @@ Thread * ModelAction::get_thread_operand() const
                /* 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)
+       } else if (type == PTHREAD_CREATE) {
+               // not implemented
+               return NULL;
+       } else if (type == THREAD_JOIN) {
                /* THREAD_JOIN uses (Thread *) for location */
                return (Thread *)get_location();
-       else
+       } else if (type == PTHREAD_JOIN) {
+               // WL: to be added (modified)
+               return (Thread *)get_location();
+       } else
                return NULL;
 }
 
@@ -551,6 +557,10 @@ const char * ModelAction::get_type_str() const
                case THREAD_YIELD: return "thread yield";
                case THREAD_JOIN: return "thread join";
                case THREAD_FINISH: return "thread finish";
+
+               case PTHREAD_CREATE: return "pthread create";
+               case PTHREAD_JOIN: return "pthread join";
+
                case ATOMIC_UNINIT: return "uninitialized";
                case ATOMIC_READ: return "atomic read";
                case ATOMIC_WRITE: return "atomic write";

diff --git a/execution.cc b/execution.cc
index 869833c21ccda7949c1c655bb85f62828175fa26..87e5425286e20253bce18d11f219631351b60819 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
 
 /**
@@ -957,6 +959,20 @@ bool ModelExecution::process_thread_action(ModelAction *curr)
                }
                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));
+               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 THREAD_JOIN: {
                Thread *blocking = curr->get_thread_operand();
                ModelAction *act = get_last_action(blocking->get_id());
@@ -964,6 +980,14 @@ bool ModelExecution::process_thread_action(ModelAction *curr)
                updated = true; /* trigger rel-seq checks */
                break;
        }
+       case PTHREAD_JOIN: {
+               break; // WL: to be add (modified)
+               Thread *blocking = curr->get_thread_operand();
+               ModelAction *act = get_last_action(blocking->get_id());
+               synchronize(act, curr);
+               updated = true; /* trigger rel-seq checks */
+       }
+
        case THREAD_FINISH: {
                Thread *th = get_thread(curr);
                /* Wake up any joining threads */
@@ -2892,8 +2916,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;
 }
 

diff --git a/model.cc b/model.cc
index ccc109a7be96594f395c2ccd0f6ab56cf230a88f..64bef579afd8b014ed00ad97f2178ad3685ddf67 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -503,8 +503,6 @@ void ModelChecker::run()
                                        scheduler->sleep(th);
                                }
                        }
-                       /* Catch assertions from prior take_step or from
-                        * between-ModelAction bugs (e.g., data races) */
 
                        for (unsigned int i = 1; i < get_num_threads(); i++) {
                                Thread *th = get_thread(int_to_id(i));
@@ -518,6 +516,7 @@ void ModelChecker::run()
                                                        break;
                                                }
                                        } else if (act->get_type() == THREAD_CREATE || \
+                                                       act->get_type() == PTHREAD_CREATE || \
                                                        act->get_type() == THREAD_START || \
                                                        act->get_type() == THREAD_FINISH) {
                                                t = th;
@@ -526,6 +525,8 @@ void ModelChecker::run()
                                }
                        }
 
+                       /* Catch assertions from prior take_step or from
+                        * between-ModelAction bugs (e.g., data races) */
 
                        if (execution->has_asserted())
                                break;