Add pthread functions

[c11tester.git] / execution.cc

diff --git a/execution.cc b/execution.cc
index cd3ef4b01d93ff7daf1e4b29e0fc6e521f0f716c..de54394c49a034aedec1465082ce316f19a21bc5 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -58,7 +58,10 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
        obj_map(),
        condvar_waiters_map(),
        obj_thrd_map(),
+       obj_wr_thrd_map(),
+       obj_last_sc_map(),
        mutex_map(),
+       cond_map(),
        thrd_last_action(1),
        thrd_last_fence_release(),
        priv(new struct model_snapshot_members ()),
@@ -1524,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.
@@ -1574,8 +1611,12 @@ Thread * ModelExecution::get_pthread(pthread_t pid) {
        } 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;
+*/
 }
 
 /**
@@ -1612,7 +1653,7 @@ bool ModelExecution::is_enabled(thread_id_t tid) const
 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
 {
        /* Do not split atomic RMW */
-       if (curr->is_rmwr() && !paused_by_fuzzer(curr))
+       if (curr->is_rmwr())
                return get_thread(curr);
        /* Follow CREATE with the created thread */
        /* which is not needed, because model.cc takes care of this */
@@ -1624,15 +1665,6 @@ Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) cons
        return NULL;
 }
 
-/** @param act A read atomic action */
-bool ModelExecution::paused_by_fuzzer(const ModelAction * act) const
-{
-       ASSERT(act->is_read());
-
-       // Actions paused by fuzzer have their sequence number reset to 0
-       return act->get_seq_number() == 0;
-}
-
 /**
  * Takes the next step in the execution, if possible.
  * @param curr The current step to take
@@ -1735,6 +1767,9 @@ void ModelExecution::fixupLastAct(ModelAction *act) {
 /** Compute which actions to free.  */
 
 void ModelExecution::collectActions() {
+       if (priv->used_sequence_numbers < params->traceminsize)
+               return;
+
        //Compute minimal clock vector for all live threads
        ClockVector *cvmin = computeMinimalCV();
        SnapVector<CycleNode *> * queue = new SnapVector<CycleNode *>();
@@ -1809,6 +1844,7 @@ void ModelExecution::collectActions() {
                                        if (islastact) {
                                                fixupLastAct(act);
                                        }
+
                                        delete act;
                                        continue;
                                }
@@ -1880,6 +1916,11 @@ void ModelExecution::collectActions() {
                        modelclock_t tid_clock = cvmin->getClock(act_tid);
                        if (actseq <= tid_clock) {
                                removeAction(act);
+                               // Remove reference to act from thrd_last_fence_release
+                               int thread_id = id_to_int( act->get_tid() );
+                               if (thrd_last_fence_release[thread_id] == act) {
+                                       thrd_last_fence_release[thread_id] = NULL;
+                               }
                                delete act;
                                continue;
                        }
@@ -1905,18 +1946,17 @@ void ModelExecution::collectActions() {
                                delete act;
                                continue;
                        }
+               }
 
-                       //If we don't delete the action, we should remove references to release fences
-                       const ModelAction *rel_fence =act->get_last_fence_release();
-                       if (rel_fence != NULL) {
-                               modelclock_t relfenceseq = rel_fence->get_seq_number();
-                               thread_id_t relfence_tid = rel_fence->get_tid();
-                               modelclock_t tid_clock = cvmin->getClock(relfence_tid);
-                               //Remove references to irrelevant release fences
-                               if (relfenceseq <= tid_clock)
-                                       act->set_last_fence_release(NULL);
-                       }
-
+               //If we don't delete the action, we should remove references to release fences
+               const ModelAction *rel_fence =act->get_last_fence_release();
+               if (rel_fence != NULL) {
+                       modelclock_t relfenceseq = rel_fence->get_seq_number();
+                       thread_id_t relfence_tid = rel_fence->get_tid();
+                       modelclock_t tid_clock = cvmin->getClock(relfence_tid);
+                       //Remove references to irrelevant release fences
+                       if (relfenceseq <= tid_clock)
+                               act->set_last_fence_release(NULL);
                }
        }