From: Brian Demsky Date: Thu, 6 Sep 2012 06:04:30 +0000 (-0700) Subject: working towards making datarace detection work X-Git-Tag: pldi2013~237 X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=620c53f1b91d3f9b51424ff57c652d247f6fbaac working towards making datarace detection work --- diff --git a/datarace.cc b/datarace.cc index fb9ca61..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,7 +287,7 @@ 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; } 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);