bug fixes

[c11tester.git] / execution.cc

diff --git a/execution.cc b/execution.cc
index 52af5212534d397566b1d7ac2ac90925492ce192..d5fb194f633c890698cfd91ed08571614ad3956c 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -55,7 +55,7 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler, NodeStack
        action_trace(),
        thread_map(2),  /* We'll always need at least 2 threads */
        pthread_map(0),
-       pthread_counter(0),
+       pthread_counter(1),
        obj_map(),
        condvar_waiters_map(),
        obj_thrd_map(),
@@ -279,8 +279,8 @@ void ModelExecution::process_read(ModelAction *curr, SnapVector<const ModelActio
                        get_thread(curr)->set_return_value(curr->get_return_value());
                        delete priorset;
                        if (canprune && curr->get_type() == ATOMIC_READ) {
-                         int tid = id_to_int(curr->get_tid());
-                         (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
+                               int tid = id_to_int(curr->get_tid());
+                               (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
                        }
                        return;
                }
@@ -339,6 +339,8 @@ bool ModelExecution::process_mutex(ModelAction *curr)
        }
        case ATOMIC_WAIT:
        case ATOMIC_UNLOCK: {
+               //TODO: FIX WAIT SITUATION...WAITS CAN SPURIOUSLY FAIL...TIMED WAITS SHOULD PROBABLY JUST BE THE SAME AS NORMAL WAITS...THINK ABOUT PROBABILITIES THOUGH....AS IN TIMED WAIT MUST FAIL TO GUARANTEE PROGRESS...NORMAL WAIT MAY FAIL...SO NEED NORMAL WAIT TO WORK CORRECTLY IN THE CASE IT SPURIOUSLY FAILS AND IN THE CASE IT DOESN'T...  TIMED WAITS MUST EVENMTUALLY RELEASE...
+
                /* wake up the other threads */
                for (unsigned int i = 0;i < get_num_threads();i++) {
                        Thread *t = get_thread(int_to_id(i));
@@ -776,14 +778,11 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *
 
        /* Last SC fence in the current thread */
        ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
-       ModelAction *last_sc_write = NULL;
-       if (curr->is_seqcst())
-               last_sc_write = get_last_seq_cst_write(curr);
 
        int tid = curr->get_tid();
        ModelAction *prev_same_thread = NULL;
        /* Iterate over all threads */
-       for (i = 0;i < thrd_lists->size();i++, tid = ((tid+1) == thrd_lists->size()) ? 0: tid + 1) {
+       for (i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
                /* Last SC fence in thread tid */
                ModelAction *last_sc_fence_thread_local = NULL;
                if (i != 0)
@@ -796,11 +795,11 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *
 
                //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
                if (prev_same_thread != NULL &&
-                   (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
-                   (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
-                     continue;
+                               (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
+                               (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
+                       continue;
                }
-               
+
                /* Iterate over actions in thread, starting from most recent */
                action_list_t *list = &(*thrd_lists)[tid];
                action_list_t::reverse_iterator rit;
@@ -850,12 +849,12 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *
                         * before" curr
                         */
                        if (act->happens_before(curr)) {
-                         if (i==0) {
-                           if (last_sc_fence_local == NULL ||
-                               (*last_sc_fence_local < *prev_same_thread)) {
-                             prev_same_thread = act;
-                           }
-                         }
+                               if (i==0) {
+                                       if (last_sc_fence_local == NULL ||
+                                                       (*last_sc_fence_local < *prev_same_thread)) {
+                                               prev_same_thread = act;
+                                       }
+                               }
                                if (act->is_write()) {
                                        if (mo_graph->checkReachable(rf, act))
                                                return false;
@@ -1301,7 +1300,8 @@ ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
  */
 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
 {
-       return get_parent_action(tid)->get_cv();
+       ModelAction *firstaction=get_parent_action(tid);
+       return firstaction != NULL ? firstaction->get_cv() : NULL;
 }
 
 bool valequals(uint64_t val1, uint64_t val2, int size) {