#include "threads-model.h"
#include "bugmessage.h"
+#include <pthread.h>
+
#define INITIAL_THREAD_ID 0
/**
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 */
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 */
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;
}
/* 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;
}