X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=datarace.h;h=627b8cc88c7016b27cc2660bdebdf4693e674c40;hb=ddea30a10d1acaef02712575c6fa4856de72cd4c;hp=33a5c26770df7deacc5ad4f14cacf9c7a3702880;hpb=20926923f6de1790fdd368d5e7fa1738abe7b9a6;p=c11tester.git diff --git a/datarace.h b/datarace.h index 33a5c267..627b8cc8 100644 --- a/datarace.h +++ b/datarace.h @@ -5,7 +5,12 @@ #ifndef DATARACE_H #include "config.h" #include -#include "clockvector.h" +#include +#include "modeltypes.h" + +/* Forward declaration */ +class ClockVector; +class ModelAction; struct ShadowTable { void * array[65536]; @@ -15,13 +20,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); +bool checkDataRaces(); +void printRace(struct DataRace *race); - +extern std::vector unrealizedraces; /** Basic encoding idea: * (void *) Either: