X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=datarace.cc;h=732d6ff748b6e77187c10f0bf5dcd6b6b834b025;hp=5ab52fc49eefa87ea1d2ad4e3c8c1a4b607f15f5;hb=caa1df880547acce2804221c8e6995170a5121eb;hpb=0accacf66b9f7bb4479205a0840f208dd8da6960 diff --git a/datarace.cc b/datarace.cc index 5ab52fc..732d6ff 100644 --- a/datarace.cc +++ b/datarace.cc @@ -1,15 +1,33 @@ #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 *) calloc(sizeof(struct ShadowTable),1); + 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 @@ -19,13 +37,13 @@ static uint64_t * lookupAddressEntry(void * address) { #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]=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]=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]; } @@ -57,14 +75,14 @@ static void expandRecord(uint64_t * shadow) { modelclock_t writeClock = WRITEVECTOR(shadowval); thread_id_t writeThread = int_to_id(WRTHREADID(shadowval)); - struct RaceRecord * record=(struct RaceRecord *)calloc(1,sizeof(struct RaceRecord)); + struct RaceRecord *record = (struct RaceRecord *)snapshot_calloc(1, sizeof(struct RaceRecord)); record->writeThread=writeThread; record->writeClock=writeClock; if (readClock!=0) { record->capacity=INITCAPACITY; - record->thread=(thread_id_t *) malloc(sizeof(thread_id_t)*record->capacity); - record->readClock=(modelclock_t *) malloc(sizeof(modelclock_t)*record->capacity); + record->thread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t)*record->capacity); + record->readClock = (modelclock_t *)snapshot_malloc(sizeof(modelclock_t)*record->capacity); record->numReads=1; record->thread[0]=readThread; record->readClock[0]=readClock; @@ -74,7 +92,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) { - struct DataRace * race=(struct DataRace *)malloc(sizeof(struct DataRace)); + struct DataRace *race = (struct DataRace *)snapshot_malloc(sizeof(struct DataRace)); race->oldthread=oldthread; race->oldclock=oldclock; race->isoldwrite=isoldwrite; @@ -82,14 +100,19 @@ static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool is race->isnewwrite=isnewwrite; race->address=address; unrealizedraces.push_back(race); - checkDataRaces(); + + /* If the race is realized, bail out now. */ + if (checkDataRaces()) { + model->set_assert(); + model->switch_to_master(NULL); + } } /** This function goes through the list of unrealized data races, * removes the impossible ones, and print the realized ones. */ -void checkDataRaces() { - if (true) { +bool checkDataRaces() { + if (model->isfeasibleprefix()) { /* Prune the non-racing unrealized dataraces */ unsigned int i,newloc=0; 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); +void printRace(struct DataRace *race) +{ + printf("Datarace detected @ address %p:\n", race->address); + printf(" Access 1: %5s in thread %2d @ clock %3u\n", + race->isoldwrite ? "write" : "read", + id_to_int(race->oldthread), race->oldclock); + printf(" Access 2: %5s in thread %2d @ clock %3u\n", + race->isnewwrite ? "write" : "read", + id_to_int(race->newaction->get_tid()), race->newaction->get_seq_number()); } /** This function does race detection for a write on an expanded record. */ @@ -232,12 +265,12 @@ void fullRaceCheckRead(thread_id_t thread, void *location, uint64_t * shadow, Cl if (copytoindex>=record->capacity) { int newCapacity=record->capacity*2; - thread_id_t *newthread=(thread_id_t *) malloc(sizeof(thread_id_t)*newCapacity); - modelclock_t * newreadClock=(modelclock_t *) malloc(sizeof(modelclock_t)*newCapacity); + thread_id_t *newthread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t)*newCapacity); + modelclock_t *newreadClock =( modelclock_t *)snapshot_malloc(sizeof(modelclock_t)*newCapacity); std::memcpy(newthread, record->thread, record->capacity*sizeof(thread_id_t)); std::memcpy(newreadClock, record->readClock, record->capacity*sizeof(modelclock_t)); - free(record->readClock); - free(record->thread); + snapshot_free(record->readClock); + snapshot_free(record->thread); record->readClock=newreadClock; record->thread=newthread; record->capacity=newCapacity;