Bug fixes

diff --git a/datarace.cc b/datarace.cc
index 895e9c019e539ba8ea78840cbd0784fd30e6c2d1..4558e2ba35472b3a0e98092f698ef5db31fb2fbd 100644 (file)
--- a/datarace.cc
+++ b/datarace.cc
@@ -69,7 +69,7 @@ bool hasNonAtomicStore(const void *address) {
                return !(ATOMICMASK & shadowval);
        } else {
                if (shadowval == 0)
-                       return false;
+                       return true;
                struct RaceRecord *record = (struct RaceRecord *)shadowval;
                return !record->isAtomic;
        }
@@ -81,8 +81,10 @@ void setAtomicStoreFlag(const void *address) {
        if (ISSHORTRECORD(shadowval)) {
                *shadow = shadowval | ATOMICMASK;
        } else {
-               if (shadowval == 0)
+               if (shadowval == 0) {
+                       *shadow = ATOMICMASK | ENCODEOP(0, 0, 0, 0);
                        return;
+               }
                struct RaceRecord *record = (struct RaceRecord *)shadowval;
                record->isAtomic = 1;
        }
@@ -91,7 +93,7 @@ void setAtomicStoreFlag(const void *address) {
 void getStoreThreadAndClock(const void *address, thread_id_t * thread, modelclock_t * clock) {
        uint64_t * shadow = lookupAddressEntry(address);
        uint64_t shadowval = *shadow;
-       if (ISSHORTRECORD(shadowval)) {
+       if (ISSHORTRECORD(shadowval) || shadowval == 0) {
                //Do we have a non atomic write with a non-zero clock
                *thread = WRTHREADID(shadowval);
                *clock = WRITEVECTOR(shadowval);

diff --git a/execution.cc b/execution.cc
index d84ebbb2d6da19b0ecc1d225ed2be2658386abe5..0128f41a0515a3e1c4b8bc7f1c694abba72e0ecc 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -1219,8 +1219,9 @@ void ModelExecution::add_normal_write_to_lists(ModelAction *act)
        }
        act->setThrdMapRef(insertIntoActionList(&(*vec)[tid],act));
 
+       ModelAction * lastact = thrd_last_action[tid];
        // Update thrd_last_action, the last action taken by each thrad
-       if (thrd_last_action[tid]->get_seq_number() == act->get_seq_number())
+       if (lastact == NULL || lastact->get_seq_number() == act->get_seq_number())
                thrd_last_action[tid] = act;
 }
 
@@ -1394,46 +1395,47 @@ SnapVector<ModelAction *> *  ModelExecution::build_may_read_from(ModelAction *cu
        SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
 
        /* Iterate over all threads */
-       for (i = 0;i < thrd_lists->size();i++) {
-               /* Iterate over actions in thread, starting from most recent */
-               action_list_t *list = &(*thrd_lists)[i];
-               sllnode<ModelAction *> * rit;
-               for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
-                       ModelAction *act = rit->getVal();
-
-                       if (act == curr)
-                               continue;
+       if (thrd_lists != NULL)
+               for (i = 0;i < thrd_lists->size();i++) {
+                       /* Iterate over actions in thread, starting from most recent */
+                       action_list_t *list = &(*thrd_lists)[i];
+                       sllnode<ModelAction *> * rit;
+                       for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
+                               ModelAction *act = rit->getVal();
+
+                               if (act == curr)
+                                       continue;
 
-                       /* Don't consider more than one seq_cst write if we are a seq_cst read. */
-                       bool allow_read = true;
-
-                       if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
-                               allow_read = false;
-
-                       /* Need to check whether we will have two RMW reading from the same value */
-                       if (curr->is_rmwr()) {
-                               /* It is okay if we have a failing CAS */
-                               if (!curr->is_rmwrcas() ||
-                                               valequals(curr->get_value(), act->get_value(), curr->getSize())) {
-                                       //Need to make sure we aren't the second RMW
-                                       CycleNode * node = mo_graph->getNode_noCreate(act);
-                                       if (node != NULL && node->getRMW() != NULL) {
-                                               //we are the second RMW
-                                               allow_read = false;
+                               /* Don't consider more than one seq_cst write if we are a seq_cst read. */
+                               bool allow_read = true;
+
+                               if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
+                                       allow_read = false;
+
+                               /* Need to check whether we will have two RMW reading from the same value */
+                               if (curr->is_rmwr()) {
+                                       /* It is okay if we have a failing CAS */
+                                       if (!curr->is_rmwrcas() ||
+                                                       valequals(curr->get_value(), act->get_value(), curr->getSize())) {
+                                               //Need to make sure we aren't the second RMW
+                                               CycleNode * node = mo_graph->getNode_noCreate(act);
+                                               if (node != NULL && node->getRMW() != NULL) {
+                                                       //we are the second RMW
+                                                       allow_read = false;
+                                               }
                                        }
                                }
-                       }
 
-                       if (allow_read) {
-                               /* Only add feasible reads */
-                               rf_set->push_back(act);
-                       }
+                               if (allow_read) {
+                                       /* Only add feasible reads */
+                                       rf_set->push_back(act);
+                               }
 
-                       /* Include at most one act per-thread that "happens before" curr */
-                       if (act->happens_before(curr))
-                               break;
+                               /* Include at most one act per-thread that "happens before" curr */
+                               if (act->happens_before(curr))
+                                       break;
+                       }
                }
-       }
 
        if (DBG_ENABLED()) {
                model_print("Reached read action:\n");