X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=datarace.cc;h=bdfade358e60595d1157e94cd2fcd0b5a18d0b86;hp=293743052858c8029fb685ff246ac071f38b821e;hb=4159ba45e83f6542e3a3320e83bca9fbaf2da3ea;hpb=328a2c09c2ee06d0e1c49ccb84877fa17b436a01 diff --git a/datarace.cc b/datarace.cc index 29374305..bdfade35 100644 --- a/datarace.cc +++ b/datarace.cc @@ -1,32 +1,49 @@ #include "datarace.h" #include "model.h" -#include "threads.h" +#include "threads-model.h" #include #include #include "mymemory.h" +#include "clockvector.h" +#include "config.h" struct ShadowTable *root; std::vector unrealizedraces; +void *memory_base; +void *memory_top; + /** This function initialized the data race detector. */ void initRaceDetector() { root = (struct ShadowTable *)snapshot_calloc(sizeof(struct ShadowTable), 1); + memory_base = snapshot_calloc(sizeof(struct ShadowBaseTable)*SHADOWBASETABLES, 1); + memory_top = ((char *)memory_base) + sizeof(struct ShadowBaseTable)*SHADOWBASETABLES; +} + +void * table_calloc(size_t size) { + if ((((char *)memory_base)+size)>memory_top) { + return snapshot_calloc(size, 1); + } else { + void *tmp=memory_base; + memory_base=((char *)memory_base)+size; + return tmp; + } } /** This function looks up the entry in the shadow table corresponding to a * given address.*/ -static uint64_t * lookupAddressEntry(void * address) { +static uint64_t * lookupAddressEntry(const void * address) { struct ShadowTable *currtable=root; #if BIT48 currtable=(struct ShadowTable *) currtable->array[(((uintptr_t)address)>>32)&MASK16BIT]; if (currtable==NULL) { - currtable = (struct ShadowTable *)(root->array[(((uintptr_t)address)>>32)&MASK16BIT] = snapshot_calloc(sizeof(struct ShadowTable), 1)); + currtable = (struct ShadowTable *)(root->array[(((uintptr_t)address)>>32)&MASK16BIT] = table_calloc(sizeof(struct ShadowTable))); } #endif struct ShadowBaseTable * basetable=(struct ShadowBaseTable *) currtable->array[(((uintptr_t)address)>>16)&MASK16BIT]; if (basetable==NULL) { - basetable = (struct ShadowBaseTable *)(currtable->array[(((uintptr_t)address)>>16)&MASK16BIT] = snapshot_calloc(sizeof(struct ShadowBaseTable), 1)); + basetable = (struct ShadowBaseTable *)(currtable->array[(((uintptr_t)address)>>16)&MASK16BIT] = table_calloc(sizeof(struct ShadowBaseTable))); } return &basetable->array[((uintptr_t)address)&MASK16BIT]; } @@ -74,7 +91,7 @@ static void expandRecord(uint64_t * shadow) { } /** This function is called when we detect a data race.*/ -static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool isoldwrite, ModelAction *newaction, bool isnewwrite, void *address) { +static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool isoldwrite, ModelAction *newaction, bool isnewwrite, const void *address) { struct DataRace *race = (struct DataRace *)snapshot_malloc(sizeof(struct DataRace)); race->oldthread=oldthread; race->oldclock=oldclock; @@ -85,45 +102,57 @@ static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool is unrealizedraces.push_back(race); /* If the race is realized, bail out now. */ - if (checkDataRaces()) { - model->set_assert(); + if (checkDataRaces()) model->switch_to_master(NULL); - } } -/** This function goes through the list of unrealized data races, - * removes the impossible ones, and print the realized ones. */ - +/** + * @brief Check and report data races + * + * If the trace is feasible (a feasible prefix), clear out the list of + * unrealized data races, asserting any realized ones as execution bugs so that + * the model-checker will end the execution. + * + * @return True if any data races were realized + */ bool checkDataRaces() { if (model->isfeasibleprefix()) { + bool race_asserted = false; /* 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); - - if (unrealizedraces.size()!=0) { - /* We have an actual realized race. */ - 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 clock %u, iswrite %u\n", race->newaction->get_tid(), race->newaction->get_seq_number() , race->isnewwrite); +/** + * @brief Assert a data race + * + * Asserts a data race which is currently realized, causing the execution to + * end and stashing a message in the model-checker's bug list + * + * @param race The race to report + */ +void assert_race(struct DataRace *race) +{ + char buf[200]; + char *ptr = buf; + ptr += sprintf(ptr, "Data race detected @ address %p:\n", race->address); + ptr += sprintf(ptr, " Access 1: %5s in thread %2d @ clock %3u\n", + race->isoldwrite ? "write" : "read", + id_to_int(race->oldthread), race->oldclock); + ptr += sprintf(ptr, " Access 2: %5s in thread %2d @ clock %3u", + race->isnewwrite ? "write" : "read", + id_to_int(race->newaction->get_tid()), race->newaction->get_seq_number()); + model->assert_bug(buf); } /** This function does race detection for a write on an expanded record. */ @@ -205,7 +234,7 @@ void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock) } /** This function does race detection on a read for an expanded record. */ -void fullRaceCheckRead(thread_id_t thread, void *location, uint64_t * shadow, ClockVector *currClock) { +void fullRaceCheckRead(thread_id_t thread, const void *location, uint64_t * shadow, ClockVector *currClock) { struct RaceRecord * record=(struct RaceRecord *) (*shadow); /* Check for datarace against last write. */ @@ -263,7 +292,7 @@ void fullRaceCheckRead(thread_id_t thread, void *location, uint64_t * shadow, Cl } /** This function does race detection on a read. */ -void raceCheckRead(thread_id_t thread, void *location, ClockVector *currClock) { +void raceCheckRead(thread_id_t thread, const void *location, ClockVector *currClock) { uint64_t * shadow=lookupAddressEntry(location); uint64_t shadowval=*shadow;