Add support for converting normal writes into ModelActions after the fact

diff --git a/action.cc b/action.cc
index 0cd49cf140589149395c7745ccc7f2593c211546..c9b920c8e6299ac514290d239e4b64bbc06c7d4d 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -262,7 +262,7 @@ bool ModelAction::is_read() const
 
 bool ModelAction::is_write() const
 {
 
 bool ModelAction::is_write() const
 {

-       return type == ATOMIC_WRITE || type == ATOMIC_RMW || type == ATOMIC_INIT || type == ATOMIC_UNINIT;
+       return type == ATOMIC_WRITE || type == ATOMIC_RMW || type == ATOMIC_INIT || type == ATOMIC_UNINIT || type == NONATOMIC_WRITE;

 }
 
 bool ModelAction::could_be_write() const
 }
 
 bool ModelAction::could_be_write() const


@@ -594,9 +594,9 @@ void ModelAction::set_read_from(ModelAction *act)
 
        if (act->is_uninitialized()) {  // WL
                uint64_t val = *((uint64_t *) location);
 
        if (act->is_uninitialized()) {  // WL
                uint64_t val = *((uint64_t *) location);

-               ModelAction * act_initialized = (ModelAction *)act;
-               act_initialized->set_value(val);
-               reads_from = act_initialized;
+               ModelAction * act_uninitialized = (ModelAction *)act;
+               act_uninitialized->set_value(val);
+               reads_from = act_uninitialized;

 
 // disabled by WL, because LLVM IR is unable to detect atomic init
 /*             model->assert_bug("May read from uninitialized atomic:\n"
 
 // disabled by WL, because LLVM IR is unable to detect atomic init
 /*             model->assert_bug("May read from uninitialized atomic:\n"


@@ -650,6 +650,7 @@ const char * ModelAction::get_type_str() const
        case PTHREAD_JOIN: return "pthread join";
 
        case ATOMIC_UNINIT: return "uninitialized";
        case PTHREAD_JOIN: return "pthread join";
 
        case ATOMIC_UNINIT: return "uninitialized";

+       case NONATOMIC_WRITE: return "nonatomic write";

        case ATOMIC_READ: return "atomic read";
        case ATOMIC_WRITE: return "atomic write";
        case ATOMIC_RMW: return "atomic rmw";
        case ATOMIC_READ: return "atomic read";
        case ATOMIC_WRITE: return "atomic write";
        case ATOMIC_RMW: return "atomic rmw";

diff --git a/action.h b/action.h
index 5862485b7e54b58a70ac10e0800be70f23548c33..7c79f435cff8aba9b248fba38af5ee40b8aac84c 100644 (file)
--- a/action.h
+++ b/action.h
@@ -55,13 +55,15 @@ typedef enum action_type {
        PTHREAD_CREATE, // < A pthread creation action
        PTHREAD_JOIN,   // < A pthread join action
        ATOMIC_UNINIT,  // < Represents an uninitialized atomic
        PTHREAD_CREATE, // < A pthread creation action
        PTHREAD_JOIN,   // < A pthread join action
        ATOMIC_UNINIT,  // < Represents an uninitialized atomic

-       ATOMIC_READ,    // < An atomic read action
+       NONATOMIC_WRITE,        // < Represents a non-atomic store
+       ATOMIC_INIT,    // < Initialization of an atomic object (e.g., atomic_init())

        ATOMIC_WRITE,   // < An atomic write action
        ATOMIC_WRITE,   // < An atomic write action

+       ATOMIC_RMW,     // < The write part of an atomic RMW action
+       ATOMIC_READ,    // < An atomic read action

        ATOMIC_RMWR,    // < The read part of an atomic RMW action
        ATOMIC_RMWRCAS, // < The read part of an atomic RMW action
        ATOMIC_RMWR,    // < The read part of an atomic RMW action
        ATOMIC_RMWRCAS, // < The read part of an atomic RMW action

-       ATOMIC_RMW,     // < The write part of an atomic RMW action

        ATOMIC_RMWC,    // < Convert an atomic RMW action into a READ
        ATOMIC_RMWC,    // < Convert an atomic RMW action into a READ

-       ATOMIC_INIT,    // < Initialization of an atomic object (e.g., atomic_init())
+

        ATOMIC_FENCE,   // < A fence action
        ATOMIC_LOCK,    // < A lock action
        ATOMIC_TRYLOCK, // < A trylock action
        ATOMIC_FENCE,   // < A fence action
        ATOMIC_LOCK,    // < A lock action
        ATOMIC_TRYLOCK, // < A trylock action

diff --git a/datarace.cc b/datarace.cc
index 4a6b8d819d3c620a6bd24d070e42a00a3fc49d15..af97a20cd91d7caf965073894081aa554ca67299 100644 (file)
--- a/datarace.cc
+++ b/datarace.cc
@@ -60,6 +60,44 @@ static uint64_t * lookupAddressEntry(const void *address)
        return &basetable->array[((uintptr_t)address) & MASK16BIT];
 }
 
        return &basetable->array[((uintptr_t)address) & MASK16BIT];
 }
 

+
+bool hasNonAtomicStore(const void *address) {
+       uint64_t * shadow = lookupAddressEntry(address);
+       uint64_t shadowval = *shadow;
+       if (ISSHORTRECORD(shadowval)) {
+               //Do we have a non atomic write with a non-zero clock
+               return ((WRITEVECTOR(shadowval) != 0) && !(ATOMICMASK & shadowval));
+       } else {
+               struct RaceRecord *record = (struct RaceRecord *)shadowval;
+               return !record->isAtomic && record->writeClock != 0;
+       }
+}
+
+void setAtomicStoreFlag(const void *address) {
+       uint64_t * shadow = lookupAddressEntry(address);
+       uint64_t shadowval = *shadow;
+       if (ISSHORTRECORD(shadowval)) {
+               *shadow = shadowval | ATOMICMASK;
+       } else {
+               struct RaceRecord *record = (struct RaceRecord *)shadowval;
+               record->isAtomic = 1;
+       }
+}
+
+void getStoreThreadAndClock(const void *address, thread_id_t * thread, modelclock_t * clock) {
+       uint64_t * shadow = lookupAddressEntry(address);
+       uint64_t shadowval = *shadow;
+       if (ISSHORTRECORD(shadowval)) {
+               //Do we have a non atomic write with a non-zero clock
+               *thread = WRTHREADID(shadowval);
+               *clock = WRITEVECTOR(shadowval);
+       } else {
+               struct RaceRecord *record = (struct RaceRecord *)shadowval;
+               *thread = record->writeThread;
+               *clock = record->writeClock;
+       }
+}
+

 /**
  * Compares a current clock-vector/thread-ID pair with a clock/thread-ID pair
  * to check the potential for a data race.
 /**
  * Compares a current clock-vector/thread-ID pair with a clock/thread-ID pair
  * to check the potential for a data race.


@@ -150,11 +188,11 @@ static struct DataRace * reportDataRace(thread_id_t oldthread, modelclock_t oldc
  */
 void assert_race(struct DataRace *race)
 {
  */
 void assert_race(struct DataRace *race)
 {

-       model_print("At location: \n");
+       model_print("Race detected at location: \n");

        backtrace_symbols_fd(race->backtrace, race->numframes, model_out);
        backtrace_symbols_fd(race->backtrace, race->numframes, model_out);

-       model_print("Data race detected @ address %p:\n"
+       model_print("\nData race detected @ address %p:\n"

                                                        "    Access 1: %5s in thread %2d @ clock %3u\n"
                                                        "    Access 1: %5s in thread %2d @ clock %3u\n"

-                                                       "    Access 2: %5s in thread %2d @ clock %3u",
+                                                       "    Access 2: %5s in thread %2d @ clock %3u\n\n",

                                                        race->address,
                                                        race->isoldwrite ? "write" : "read",
                                                        id_to_int(race->oldthread),
                                                        race->address,
                                                        race->isoldwrite ? "write" : "read",
                                                        id_to_int(race->oldthread),

diff --git a/datarace.h b/datarace.h
index 67d58e7c3c12cd46387391c132c62a945b911685..c78f5a424929d89d3cedc805006f1b401790a211 100644 (file)
--- a/datarace.h
+++ b/datarace.h
@@ -48,6 +48,9 @@ void raceCheckRead(thread_id_t thread, const void *location);
 void recordWrite(thread_id_t thread, void *location);
 bool checkDataRaces();
 void assert_race(struct DataRace *race);
 void recordWrite(thread_id_t thread, void *location);
 bool checkDataRaces();
 void assert_race(struct DataRace *race);

+bool hasNonAtomicStore(const void *location);
+void setAtomicStoreFlag(const void *location);
+void getStoreThreadAndClock(const void *address, thread_id_t * thread, modelclock_t * clock);

 
 /**
  * @brief A record of information for detecting data races
 
 /**
  * @brief A record of information for detecting data races

diff --git a/execution.cc b/execution.cc
index e162a4a10f9e250c123efd6d5c9c39c601b86d17..b5f86ff006016b1cfa90dc0436c7975a2754afc6 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -253,6 +253,19 @@ bool ModelExecution::is_complete_execution() const
        return true;
 }
 
        return true;
 }
 

+ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
+       uint64_t value = *((const uint64_t *) location);
+       modelclock_t storeclock;
+       thread_id_t storethread;
+       getStoreThreadAndClock(location, &storethread, &storeclock);
+       setAtomicStoreFlag(location);
+       ModelAction * act = new ModelAction(NONATOMIC_WRITE, memory_order_relaxed, location, value, get_thread(storethread));
+       add_normal_write_to_lists(act);
+       add_write_to_lists(act);
+       w_modification_order(act);
+       return act;
+}
+

 
 /**
  * Processes a read model action.
 
 /**
  * Processes a read model action.


@@ -264,6 +277,11 @@ void ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> *
 {
        SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
        while(true) {
 {
        SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
        while(true) {

+               bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
+               if (hasnonatomicstore) {
+                       ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
+                       rf_set->push_back(nonatomicstore);
+               }

 
                int index = fuzzer->selectWrite(curr, rf_set);
                ModelAction *rf = (*rf_set)[index];
 
                int index = fuzzer->selectWrite(curr, rf_set);
                ModelAction *rf = (*rf_set)[index];


@@ -1111,6 +1129,51 @@ void ModelExecution::add_action_to_lists(ModelAction *act)
        }
 }
 
        }
 }
 

+void insertIntoActionList(action_list_t *list, ModelAction *act) {
+       action_list_t::reverse_iterator rit = list->rbegin();
+       modelclock_t next_seq = act->get_seq_number();
+       if ((*rit)->get_seq_number() == next_seq)
+               list->push_back(act);
+       else {
+               for(;rit != list->rend();rit++) {
+                       if ((*rit)->get_seq_number() == next_seq) {
+                               action_list_t::iterator it = rit.base();
+                               it++;   //get to right sequence number
+                               it++;   //get to item after it
+                               list->insert(it, act);
+                               break;
+                       }
+               }
+       }
+}
+
+/**
+ * Performs various bookkeeping operations for a normal write.  The
+ * complication is that we are typically inserting a normal write
+ * lazily, so we need to insert it into the middle of lists.
+ *
+ * @param act is the ModelAction to add.
+ */
+
+void ModelExecution::add_normal_write_to_lists(ModelAction *act)
+{
+       int tid = id_to_int(act->get_tid());
+       action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
+       insertIntoActionList(list, act);
+       insertIntoActionList(&action_trace, act);
+
+       // Update obj_thrd_map, a per location, per thread, order of actions
+       SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
+       if (tid >= (int)vec->size())
+               vec->resize(priv->next_thread_id);
+       insertIntoActionList(&(*vec)[tid],act);
+
+       // Update thrd_last_action, the last action taken by each thrad
+       if (thrd_last_action[tid]->get_seq_number() == act->get_seq_number())
+               thrd_last_action[tid] = act;
+}
+
+

 void ModelExecution::add_write_to_lists(ModelAction *write) {
        // Update seq_cst map
        if (write->is_seqcst())
 void ModelExecution::add_write_to_lists(ModelAction *write) {
        // Update seq_cst map
        if (write->is_seqcst())

diff --git a/execution.h b/execution.h
index 422430e87babd8bb5a1fee1f770b77e6f662959c..682e94b15017ef2c16d4dd0085f9a7ed99cb3644 100644 (file)
--- a/execution.h
+++ b/execution.h
@@ -118,6 +118,7 @@ private:
        bool synchronize(const ModelAction *first, ModelAction *second);
 
        void add_action_to_lists(ModelAction *act);
        bool synchronize(const ModelAction *first, ModelAction *second);
 
        void add_action_to_lists(ModelAction *act);

+       void add_normal_write_to_lists(ModelAction *act);

        void add_write_to_lists(ModelAction *act);
        ModelAction * get_last_fence_release(thread_id_t tid) const;
        ModelAction * get_last_seq_cst_write(ModelAction *curr) const;
        void add_write_to_lists(ModelAction *act);
        ModelAction * get_last_fence_release(thread_id_t tid) const;
        ModelAction * get_last_seq_cst_write(ModelAction *curr) const;


@@ -130,6 +131,7 @@ private:
        void w_modification_order(ModelAction *curr);
        ClockVector * get_hb_from_write(ModelAction *rf) const;
        ModelAction * get_uninitialized_action(ModelAction *curr) const;
        void w_modification_order(ModelAction *curr);
        ClockVector * get_hb_from_write(ModelAction *rf) const;
        ModelAction * get_uninitialized_action(ModelAction *curr) const;

+       ModelAction * convertNonAtomicStore(void*);

 
        action_list_t action_trace;
        SnapVector<Thread *> thread_map;
 
        action_list_t action_trace;
        SnapVector<Thread *> thread_map;