X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=datarace.cc;h=653039b3307e3ebfb195e2dc99efda36ae123a7c;hb=130a35155171503883aaf18e57f8957ce63d06e8;hp=c70d41897f4fd5c4ff9c68f3daf96d4ed6240ba6;hpb=bb39508b2f65c261a703ad38cf16f6cdd590e67d;p=model-checker.git diff --git a/datarace.cc b/datarace.cc index c70d418..653039b 100644 --- a/datarace.cc +++ b/datarace.cc @@ -6,12 +6,19 @@ #include "mymemory.h" #include "clockvector.h" #include "config.h" +#include "action.h" +#include "execution.h" +#include "stl-model.h" -struct ShadowTable *root; -std::vector unrealizedraces; -void *memory_base; -void *memory_top; +static struct ShadowTable *root; +static SnapVector *unrealizedraces; +static void *memory_base; +static void *memory_top; +static const ModelExecution * get_execution() +{ + return model->get_execution(); +} /** This function initialized the data race detector. */ void initRaceDetector() @@ -19,6 +26,7 @@ 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; + unrealizedraces = new SnapVector(); } void * table_calloc(size_t size) @@ -104,7 +112,7 @@ static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool is race->newaction = newaction; race->isnewwrite = isnewwrite; race->address = address; - unrealizedraces.push_back(race); + unrealizedraces->push_back(race); /* If the race is realized, bail out now. */ if (checkDataRaces()) @@ -122,18 +130,18 @@ static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool is */ bool checkDataRaces() { - if (model->isfeasibleprefix()) { + if (get_execution()->isfeasibleprefix()) { bool race_asserted = false; /* Prune the non-racing unrealized dataraces */ - for (unsigned i = 0; i < unrealizedraces.size(); i++) { - struct DataRace *race = unrealizedraces[i]; + for (unsigned 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)) { assert_race(race); race_asserted = true; } snapshot_free(race); } - unrealizedraces.clear(); + unrealizedraces->clear(); return race_asserted; } return false; @@ -149,16 +157,18 @@ bool checkDataRaces() */ 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", + model->assert_bug( + "Data race detected @ address %p:\n" + " Access 1: %5s in thread %2d @ clock %3u\n" + " Access 2: %5s in thread %2d @ clock %3u", + race->address, race->isoldwrite ? "write" : "read", - id_to_int(race->oldthread), race->oldclock); - ptr += sprintf(ptr, " Access 2: %5s in thread %2d @ clock %3u", + id_to_int(race->oldthread), + race->oldclock, race->isnewwrite ? "write" : "read", - id_to_int(race->newaction->get_tid()), race->newaction->get_seq_number()); - model->assert_bug(buf); + id_to_int(race->newaction->get_tid()), + race->newaction->get_seq_number() + ); } /** This function does race detection for a write on an expanded record. */ @@ -177,7 +187,7 @@ void fullRaceCheckWrite(thread_id_t thread, void *location, uint64_t *shadow, Cl if (clock_may_race(currClock, thread, readClock, readThread)) { /* We have a datarace */ - reportDataRace(readThread, readClock, false, model->get_parent_action(thread), true, location); + reportDataRace(readThread, readClock, false, get_execution()->get_parent_action(thread), true, location); } } @@ -188,7 +198,7 @@ void fullRaceCheckWrite(thread_id_t thread, void *location, uint64_t *shadow, Cl if (clock_may_race(currClock, thread, writeClock, writeThread)) { /* We have a datarace */ - reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), true, location); + reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), true, location); } record->numReads = 0; @@ -198,10 +208,11 @@ void fullRaceCheckWrite(thread_id_t thread, void *location, uint64_t *shadow, Cl } /** This function does race detection on a write. */ -void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock) +void raceCheckWrite(thread_id_t thread, void *location) { uint64_t *shadow = lookupAddressEntry(location); uint64_t shadowval = *shadow; + ClockVector *currClock = get_execution()->get_cv(thread); /* Do full record */ if (shadowval != 0 && !ISSHORTRECORD(shadowval)) { @@ -226,7 +237,7 @@ void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock) if (clock_may_race(currClock, thread, readClock, readThread)) { /* We have a datarace */ - reportDataRace(readThread, readClock, false, model->get_parent_action(thread), true, location); + reportDataRace(readThread, readClock, false, get_execution()->get_parent_action(thread), true, location); } /* Check for datarace against last write. */ @@ -236,7 +247,7 @@ void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock) if (clock_may_race(currClock, thread, writeClock, writeThread)) { /* We have a datarace */ - reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), true, location); + reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), true, location); } *shadow = ENCODEOP(0, 0, threadid, ourClock); } @@ -253,7 +264,7 @@ void fullRaceCheckRead(thread_id_t thread, const void *location, uint64_t *shado if (clock_may_race(currClock, thread, writeClock, writeThread)) { /* We have a datarace */ - reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), false, location); + reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), false, location); } /* Shorten vector when possible */ @@ -301,10 +312,11 @@ void fullRaceCheckRead(thread_id_t thread, const void *location, uint64_t *shado } /** This function does race detection on a read. */ -void raceCheckRead(thread_id_t thread, const void *location, ClockVector *currClock) +void raceCheckRead(thread_id_t thread, const void *location) { uint64_t *shadow = lookupAddressEntry(location); uint64_t shadowval = *shadow; + ClockVector *currClock = get_execution()->get_cv(thread); /* Do full record */ if (shadowval != 0 && !ISSHORTRECORD(shadowval)) { @@ -329,7 +341,7 @@ void raceCheckRead(thread_id_t thread, const void *location, ClockVector *currCl if (clock_may_race(currClock, thread, writeClock, writeThread)) { /* We have a datarace */ - reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), false, location); + reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), false, location); } modelclock_t readClock = READVECTOR(shadowval); @@ -344,3 +356,8 @@ void raceCheckRead(thread_id_t thread, const void *location, ClockVector *currCl *shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock); } + +bool haveUnrealizedRaces() +{ + return !unrealizedraces->empty(); +}