From: Brian Norris Date: Thu, 6 Sep 2012 23:16:51 +0000 (-0700) Subject: Merge branch 'norris' X-Git-Tag: pldi2013~235^2 X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=0accacf66b9f7bb4479205a0840f208dd8da6960;hp=33a0676006be6e35e0fa9e6bd907ca7bae5e53e2 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 f0d3dc6..5ab52fc 100644 --- a/datarace.cc +++ b/datarace.cc @@ -1,9 +1,11 @@ #include "datarace.h" +#include "model.h" #include "threads.h" #include #include struct ShadowTable *root; +std::vector 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;inewaction->get_cv(), race->newaction->get_tid(), race->oldclock, race->oldthread)) { + unrealizedraces[newloc++]=race; + } + } + if (newloc!=i) + unrealizedraces.resize(newloc); + for(i=0;iaddress); + 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 33a5c26..b2f7099 100644 --- a/datarace.h +++ b/datarace.h @@ -6,6 +6,7 @@ #include "config.h" #include #include "clockvector.h" +#include 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 unrealizedraces; /** Basic encoding idea: * (void *) Either: diff --git a/model.h b/model.h index e55863d..9eb9aa6 100644 --- 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 index 0000000..18e6ffb --- /dev/null +++ b/test/linuxrwlocks.c @@ -0,0 +1,114 @@ +#include + +#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()); +}