X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=datarace.h;h=737a6d6e99a915a06d2f21d9f6a521a5ad126e03;hp=6c92203cfd4e7d7b234dffd0bc75ef62bbe60dea;hb=130a35155171503883aaf18e57f8957ce63d06e8;hpb=4fa31aac91303266f4c87a6cd5d60cbab34135db diff --git a/datarace.h b/datarace.h index 6c92203..737a6d6 100644 --- a/datarace.h +++ b/datarace.h @@ -2,14 +2,14 @@ * @brief Data race detection code. */ -#ifndef DATARACE_H +#ifndef __DATARACE_H__ +#define __DATARACE_H__ + #include "config.h" #include #include "modeltypes.h" -#include "stl-model.h" /* Forward declaration */ -class ClockVector; class ModelAction; struct ShadowTable { @@ -42,12 +42,11 @@ struct DataRace { #define MASK16BIT 0xffff void initRaceDetector(); -void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock); -void raceCheckRead(thread_id_t thread, const void *location, ClockVector *currClock); +void raceCheckWrite(thread_id_t thread, void *location); +void raceCheckRead(thread_id_t thread, const void *location); bool checkDataRaces(); void assert_race(struct DataRace *race); - -extern SnapVector unrealizedraces; +bool haveUnrealizedRaces(); /** * @brief A record of information for detecting data races @@ -91,4 +90,5 @@ struct RaceRecord { #define MAXTHREADID (THREADMASK-1) #define MAXREADVECTOR (READMASK-1) #define MAXWRITEVECTOR (WRITEMASK-1) -#endif + +#endif /* __DATARACE_H__ */