Merge branch 'norris'

Fixes up some THREAD_JOIN behavior, cleaning up a little bit of general model-checker structure.

diff --git a/datarace.cc b/datarace.cc
index f0d3dc619489d780ea7e9be237b2007d428a4b33..5ab52fc49eefa87ea1d2ad4e3c8c1a4b607f15f5 100644 (file)
--- a/datarace.cc
+++ b/datarace.cc
@@ -1,9 +1,11 @@
 #include "datarace.h"
+#include "model.h"
 #include "threads.h"
 #include <stdio.h>
 #include <cstring>
 
 struct ShadowTable *root;
+std::vector<struct DataRace *> unrealizedraces;
 
 /** This function initialized the data race detector. */
 void initRaceDetector() {
@@ -71,12 +73,49 @@ static void expandRecord(uint64_t * shadow) {
 }
 
 /** This function is called when we detect a data race.*/
-static void reportDataRace() {
-       printf("The reportDataRace method should report useful things about this datarace!\n");
+static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool isoldwrite, ModelAction *newaction, bool isnewwrite, void *address) {
+       struct DataRace * race=(struct DataRace *)malloc(sizeof(struct DataRace));
+       race->oldthread=oldthread;
+       race->oldclock=oldclock;
+       race->isoldwrite=isoldwrite;
+       race->newaction=newaction;
+       race->isnewwrite=isnewwrite;
+       race->address=address;
+       unrealizedraces.push_back(race);
+       checkDataRaces();
+}
+
+/** This function goes through the list of unrealized data races,
+ *     removes the impossible ones, and print the realized ones. */
+
+void checkDataRaces() {
+       if (true) {
+               /* Prune the non-racing unrealized dataraces */
+               unsigned int i,newloc=0;
+               for(i=0;i<unrealizedraces.size();i++) {
+                       struct DataRace * race=unrealizedraces[i];
+                       if (clock_may_race(race->newaction->get_cv(), race->newaction->get_tid(), race->oldclock, race->oldthread)) {
+                               unrealizedraces[newloc++]=race;
+                       }
+               }
+               if (newloc!=i)
+                       unrealizedraces.resize(newloc);
+               for(i=0;i<unrealizedraces.size();i++) {
+                       struct DataRace * race=unrealizedraces[i];
+                       printRace(race);
+               }
+       }
+}
+
+void printRace(struct DataRace * race) {
+       printf("Datarace detected\n");
+       printf("Location %p\n", race->address);
+       printf("Initial access: thread %u clock %u, iswrite %u\n",race->oldthread,race->oldclock, race->isoldwrite);
+       printf("Second access: thread %u, iswrite %u\n", race->newaction->get_tid(), race->isnewwrite);
 }
 
 /** This function does race detection for a write on an expanded record. */
-void fullRaceCheckWrite(thread_id_t thread, uint64_t * shadow, ClockVector *currClock) {
+void fullRaceCheckWrite(thread_id_t thread, void *location, uint64_t * shadow, ClockVector *currClock) {
        struct RaceRecord * record=(struct RaceRecord *) (*shadow);
 
        /* Check for datarace against last read. */
@@ -90,7 +129,7 @@ void fullRaceCheckWrite(thread_id_t thread, uint64_t * shadow, ClockVector *curr
 
                if (clock_may_race(currClock, thread, readClock, readThread)) {
                        /* We have a datarace */
-                       reportDataRace();
+                       reportDataRace(readThread, readClock, false, model->get_parent_action(thread), true, location);
                }
        }
 
@@ -101,7 +140,7 @@ void fullRaceCheckWrite(thread_id_t thread, uint64_t * shadow, ClockVector *curr
 
        if (clock_may_race(currClock, thread, writeClock, writeThread)) {
                /* We have a datarace */
-               reportDataRace();
+               reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), true, location);
        }
 
        record->numReads=0;
@@ -117,7 +156,7 @@ void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock)
 
        /* Do full record */
        if (shadowval!=0&&!ISSHORTRECORD(shadowval)) {
-               fullRaceCheckWrite(thread, shadow, currClock);
+               fullRaceCheckWrite(thread, location, shadow, currClock);
                return;
        }
 
@@ -127,7 +166,7 @@ void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock)
        /* Thread ID is too large or clock is too large. */
        if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
                expandRecord(shadow);
-               fullRaceCheckWrite(thread, shadow, currClock);
+               fullRaceCheckWrite(thread, location, shadow, currClock);
                return;
        }
 
@@ -138,7 +177,7 @@ void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock)
 
        if (clock_may_race(currClock, thread, readClock, readThread)) {
                /* We have a datarace */
-               reportDataRace();
+               reportDataRace(readThread, readClock, false, model->get_parent_action(thread), true, location);
        }
 
        /* Check for datarace against last write. */
@@ -148,13 +187,13 @@ void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock)
 
        if (clock_may_race(currClock, thread, writeClock, writeThread)) {
                /* We have a datarace */
-               reportDataRace();
+               reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), true, location);
        }
        *shadow = ENCODEOP(0, 0, threadid, ourClock);
 }
 
 /** This function does race detection on a read for an expanded record. */
-void fullRaceCheckRead(thread_id_t thread, uint64_t * shadow, ClockVector *currClock) {
+void fullRaceCheckRead(thread_id_t thread, void *location, uint64_t * shadow, ClockVector *currClock) {
        struct RaceRecord * record=(struct RaceRecord *) (*shadow);
 
        /* Check for datarace against last write. */
@@ -164,7 +203,7 @@ void fullRaceCheckRead(thread_id_t thread, uint64_t * shadow, ClockVector *currC
 
        if (clock_may_race(currClock, thread, writeClock, writeThread)) {
                /* We have a datarace */
-               reportDataRace();
+               reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), false, location);
        }
 
        /* Shorten vector when possible */
@@ -218,7 +257,7 @@ void raceCheckRead(thread_id_t thread, void *location, ClockVector *currClock) {
 
        /* Do full record */
        if (shadowval!=0&&!ISSHORTRECORD(shadowval)) {
-               fullRaceCheckRead(thread, shadow, currClock);
+               fullRaceCheckRead(thread, location, shadow, currClock);
                return;
        }
 
@@ -228,7 +267,7 @@ void raceCheckRead(thread_id_t thread, void *location, ClockVector *currClock) {
        /* Thread ID is too large or clock is too large. */
        if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
                expandRecord(shadow);
-               fullRaceCheckRead(thread, shadow, currClock);
+               fullRaceCheckRead(thread, location, shadow, currClock);
                return;
        }
 
@@ -239,7 +278,7 @@ void raceCheckRead(thread_id_t thread, void *location, ClockVector *currClock) {
 
        if (clock_may_race(currClock, thread, writeClock, writeThread)) {
                /* We have a datarace */
-               reportDataRace();
+               reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), false, location);
        }
 
        modelclock_t readClock = READVECTOR(shadowval);
@@ -248,9 +287,9 @@ void raceCheckRead(thread_id_t thread, void *location, ClockVector *currClock) {
        if (clock_may_race(currClock, thread, readClock, readThread)) {
                /* We don't subsume this read... Have to expand record. */
                expandRecord(shadow);
-               fullRaceCheckRead(thread, shadow, currClock);
+               fullRaceCheckRead(thread, location, shadow, currClock);
                return;
        }
 
-       *shadow = ENCODEOP(writeThread, writeClock, threadid, ourClock);
+       *shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock);
 }

diff --git a/datarace.h b/datarace.h
index 33a5c26770df7deacc5ad4f14cacf9c7a3702880..b2f709911ecff2274596ed11f7c5338365ee57e7 100644 (file)
--- a/datarace.h
+++ b/datarace.h
@@ -6,6 +6,7 @@
 #include "config.h"
 #include <stdint.h>
 #include "clockvector.h"
+#include <vector>
 
 struct ShadowTable {
        void * array[65536];
@@ -15,13 +16,34 @@ struct ShadowBaseTable {
        uint64_t array[65536];
 };
 
+struct DataRace {
+       /* Clock and thread associated with first action.  This won't change in
+                response to synchronization. */
+
+       thread_id_t oldthread;
+       modelclock_t oldclock;
+       /* Record whether this is a write, so we can tell the user. */
+       bool isoldwrite;
+
+       /* Model action associated with second action.  This could change as
+                a result of synchronization. */
+       ModelAction *newaction;
+       /* Record whether this is a write, so we can tell the user. */
+       bool isnewwrite;
+
+       /* Address of data race. */
+       void *address;
+};
+
 #define MASK16BIT 0xffff
 
 void initRaceDetector();
 void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock);
 void raceCheckRead(thread_id_t thread, void *location, ClockVector *currClock);
+void checkDataRaces();
+void printRace(struct DataRace *race);
 
-
+extern std::vector<struct DataRace *> unrealizedraces;
 
 /** Basic encoding idea:
  *      (void *) Either:

diff --git a/model.h b/model.h
index e55863dce74ec1ea9906b0589db7734c21c856cc..9eb9aa655c0285914c48be1414c17d4061171f64 100644 (file)
--- a/model.h
+++ b/model.h
@@ -55,6 +55,7 @@ public:
 
        int switch_to_master(ModelAction *act);
        ClockVector * get_cv(thread_id_t tid);
+       ModelAction * get_parent_action(thread_id_t tid);
        bool next_execution();
        bool isfeasible();
        bool isfinalfeasible();
@@ -96,7 +97,6 @@ private:
 
        void add_action_to_lists(ModelAction *act);
        ModelAction * get_last_action(thread_id_t tid);
-       ModelAction * get_parent_action(thread_id_t tid);
        ModelAction * get_last_seq_cst(const void *location);
        void build_reads_from_past(ModelAction *curr);
        ModelAction * process_rmw(ModelAction *curr);

diff --git a/test/linuxrwlocks.c b/test/linuxrwlocks.c
new file mode 100644 (file)
index 0000000..18e6ffb
--- /dev/null
+++ b/test/linuxrwlocks.c
@@ -0,0 +1,114 @@
+#include <stdio.h>
+
+#include "libthreads.h"
+#include "librace.h"
+#include "stdatomic.h"
+
+
+#define RW_LOCK_BIAS            0x00100000
+#define WRITE_LOCK_CMP          RW_LOCK_BIAS
+
+/** Example implementation of linux rw lock along with 2 thread test
+ *  driver... */
+
+
+typedef union {
+       atomic_int lock;
+} rwlock_t;
+
+static inline int read_can_lock(rwlock_t *lock)
+{
+       return atomic_load_explicit(&lock->lock, memory_order_relaxed) > 0;
+}
+
+static inline int write_can_lock(rwlock_t *lock)
+{
+       return atomic_load_explicit(&lock->lock, memory_order_relaxed) == RW_LOCK_BIAS;
+}
+
+static inline void read_lock(rwlock_t *rw)
+{
+       int currentvalue=atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
+       while (currentvalue<0) {
+               atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
+               do {
+                       currentvalue=atomic_load_explicit(&rw->lock, memory_order_relaxed);
+               }       while(currentvalue<=0);
+               currentvalue=atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
+       }
+}
+
+static inline void write_lock(rwlock_t *rw)
+{
+       int currentvalue=atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
+       while (currentvalue!=0) {
+               atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
+               do {
+                       currentvalue=atomic_load_explicit(&rw->lock, memory_order_relaxed);
+               }       while(currentvalue!=RW_LOCK_BIAS);
+               currentvalue=atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
+       }
+}
+
+static inline int read_trylock(rwlock_t *rw)
+{
+       int currentvalue=atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
+       if (currentvalue>=0)
+               return 1;
+       
+       atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
+       return 0;
+}
+
+static inline int write_trylock(rwlock_t *rw)
+{
+       int currentvalue=atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
+       if (currentvalue>=0)
+               return 1;
+       
+       atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
+       return 0;
+}
+
+static inline void read_unlock(rwlock_t *rw)
+{
+       atomic_fetch_add_explicit(&rw->lock, 1, memory_order_release);
+}
+
+static inline void write_unlock(rwlock_t *rw)
+{
+       atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_release);
+}
+
+rwlock_t mylock;
+int shareddata;
+
+static void a(void *obj)
+{
+       int i;
+       for(i=0;i<2;i++) {
+               if ((i%2)==0) {
+                       read_lock(&mylock);
+                       load_32(&shareddata);
+                       read_unlock(&mylock);
+               } else {
+                       write_lock(&mylock);
+                       store_32(&shareddata,(unsigned int)i);
+                       write_unlock(&mylock);
+               }
+       }
+}
+
+void user_main()
+{
+       thrd_t t1, t2;
+       atomic_init(&mylock.lock, RW_LOCK_BIAS);
+
+       printf("Thread %d: creating 2 threads\n", thrd_current());
+       thrd_create(&t1, (thrd_start_t)&a, NULL);
+       thrd_create(&t2, (thrd_start_t)&a, NULL);
+       
+       thrd_join(t1);
+       thrd_join(t2);
+       printf("Thread %d is finished\n", thrd_current());
+}