Add pthread functions

diff --git a/execution.cc b/execution.cc
index a98567edb9ba7b723c474405cbb5d3d75433687a..de54394c49a034aedec1465082ce316f19a21bc5 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -1527,6 +1527,40 @@ void ModelExecution::print_summary()
 
 }
 
 
 }
 

+void ModelExecution::print_tail()
+{
+       model_print("Execution trace %d:\n", get_execution_number());
+
+       sllnode<ModelAction*> *it;
+
+       model_print("------------------------------------------------------------------------------------\n");
+       model_print("#    t    Action type     MO       Location         Value               Rf  CV\n");
+       model_print("------------------------------------------------------------------------------------\n");
+
+       unsigned int hash = 0;
+
+       int length = 25;
+       int counter = 0;
+       SnapList<ModelAction *> list;
+       for (it = action_trace.end(); it != NULL; it = it->getPrev()) {
+               if (counter > length)
+                       break;
+
+               ModelAction * act = it->getVal();
+               list.push_front(act);
+               counter++;
+       }
+
+       for (it = list.begin();it != NULL;it=it->getNext()) {
+               const ModelAction *act = it->getVal();
+               if (act->get_seq_number() > 0)
+                       act->print();
+               hash = hash^(hash<<3)^(it->getVal()->hash());
+       }
+       model_print("HASH %u\n", hash);
+       model_print("------------------------------------------------------------------------------------\n");
+}
+

 /**
  * Add a Thread to the system for the first time. Should only be called once
  * per thread.
 /**
  * Add a Thread to the system for the first time. Should only be called once
  * per thread.


@@ -1577,8 +1611,12 @@ Thread * ModelExecution::get_pthread(pthread_t pid) {
        } x;
        x.p = pid;
        uint32_t thread_id = x.v;
        } x;
        x.p = pid;
        uint32_t thread_id = x.v;

+       return get_thread(thread_id);   // Temporary fix for firefox
+
+/*

        if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
        else return NULL;
        if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
        else return NULL;

+*/

 }
 
 /**
 }
 
 /**

diff --git a/execution.h b/execution.h
index 6cdaeaf17a90b156e0bf14da5be134324cc4155d..722b864723a40f8d902c5ed2920575d43b837b01 100644 (file)
--- a/execution.h
+++ b/execution.h
@@ -41,6 +41,7 @@ public:
        Thread * take_step(ModelAction *curr);
 
        void print_summary();
        Thread * take_step(ModelAction *curr);
 
        void print_summary();

+       void print_tail();

 #if SUPPORT_MOD_ORDER_DUMP
        void dumpGraph(char *filename);
 #endif
 #if SUPPORT_MOD_ORDER_DUMP
        void dumpGraph(char *filename);
 #endif

diff --git a/include/mypthread.h b/include/mypthread.h
index ff7458edf6a3acbc839b2dbc0d242caba1c2a998..4b2b615f61f9b1c0bcd0f64311e1edacd05824e1 100644 (file)
--- a/include/mypthread.h
+++ b/include/mypthread.h
@@ -16,6 +16,23 @@ struct pthread_params {
        void *arg;
 };
 
        void *arg;
 };
 

+struct pthread_attr
+{
+       /* Scheduler parameters and priority.  */
+       struct sched_param schedparam;
+       int schedpolicy;
+       /* Various flags like detachstate, scope, etc.  */
+       int flags;
+       /* Size of guard area.  */
+       size_t guardsize;
+       /* Stack handling.  */
+       void *stackaddr;
+       size_t stacksize;
+       /* Affinity map.  */
+       cpu_set_t *cpuset;
+       size_t cpusetsize;
+};
+

 extern "C" {
 int user_main(int, char**);
 }
 extern "C" {
 int user_main(int, char**);
 }

diff --git a/newfuzzer.cc b/newfuzzer.cc
index ad279770e1588267a1bdc22f3d18c3be2dceaabf..fca9da8d48896504b6aafeea2dda40060a10e1a8 100644 (file)
--- a/newfuzzer.cc
+++ b/newfuzzer.cc
@@ -33,7 +33,7 @@ void NewFuzzer::register_engine(ModelChecker *_model, ModelExecution *execution)
 
 int NewFuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set)
 {
 
 int NewFuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set)
 {

-//     return random() % rf_set->size();
+       return random() % rf_set->size();

 
        thread_id_t tid = read->get_tid();
        int thread_id = id_to_int(tid);
 
        thread_id_t tid = read->get_tid();
        int thread_id = id_to_int(tid);


@@ -344,7 +344,6 @@ Thread * NewFuzzer::selectThread(int * threadlist, int numthreads)
                wake_up_paused_threads(threadlist, &numthreads);
                //model_print("list size: %d, active t id: %d\n", numthreads, threadlist[0]);
        }
                wake_up_paused_threads(threadlist, &numthreads);
                //model_print("list size: %d, active t id: %d\n", numthreads, threadlist[0]);
        }

-

        int random_index = random() % numthreads;
        int thread = threadlist[random_index];
        thread_id_t curr_tid = int_to_id(thread);
        int random_index = random() % numthreads;
        int thread = threadlist[random_index];
        thread_id_t curr_tid = int_to_id(thread);

diff --git a/pthread.cc b/pthread.cc
index b5fb7ce964200750a108412c63041de7cea56c3d..706f1b75602ef6ae33e2876be5064dcd10ab18a3 100644 (file)
--- a/pthread.cc
+++ b/pthread.cc
@@ -162,6 +162,12 @@ int pthread_mutex_timedlock (pthread_mutex_t *__restrict p_mutex,
 }
 
 pthread_t pthread_self() {
 }
 
 pthread_t pthread_self() {

+       if (!model) {
+               snapshot_system_init(10000, 1024, 1024, 40000);
+               model = new ModelChecker();
+               model->startChecker();
+       }
+

        Thread* th = model->get_current_thread();
        return (pthread_t)th->get_id();
 }
        Thread* th = model->get_current_thread();
        return (pthread_t)th->get_id();
 }


@@ -246,3 +252,37 @@ int pthread_cond_destroy(pthread_cond_t *p_cond) {
        }
        return 0;
 }
        }
        return 0;
 }

+
+/* https://github.com/lattera/glibc/blob/master/nptl/pthread_getattr_np.c */
+int pthread_getattr_np(pthread_t t, pthread_attr_t *attr)
+{
+       ModelExecution *execution = model->get_execution();
+       Thread *th = execution->get_pthread(t);
+
+       struct pthread_attr *iattr = (struct pthread_attr *) attr;
+
+       /* The sizes are subject to alignment.  */
+       if (th != NULL) {
+#if _STACK_GROWS_DOWN
+               ASSERT(false);
+#else
+               iattr->stackaddr = (char *) th->get_stack_addr();
+#endif
+
+       } else {
+               ASSERT(false);
+       }
+
+       return 0;
+}
+
+int pthread_setname_np(pthread_t t, const char *name)
+{
+       ModelExecution *execution = model->get_execution();
+       Thread *th = execution->get_pthread(t);
+
+       if (th != NULL)
+               return 0;
+
+       return 1;
+}

diff --git a/threads-model.h b/threads-model.h
index c6078200f5911f5bf3dd78f80125b881683e1a0e..e159697d9d54ce10c3cfb1fe204352a9e0bd7435 100644 (file)
--- a/threads-model.h
+++ b/threads-model.h
@@ -101,6 +101,8 @@ public:
 
        bool is_model_thread() const { return model_thread; }
 
 
        bool is_model_thread() const { return model_thread; }
 

+       void * get_stack_addr() { return stack; }
+

        friend void thread_startup();
 #ifdef TLS
        friend void setup_context();
        friend void thread_startup();
 #ifdef TLS
        friend void setup_context();


@@ -156,6 +158,7 @@ private:
        void *arg;
        ucontext_t context;
        void *stack;
        void *arg;
        ucontext_t context;
        void *stack;

+       uint32_t stack_size;

 #ifdef TLS
        void * helper_stack;
 public:
 #ifdef TLS
        void * helper_stack;
 public: