projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
datarace: simplify raceCheck{Read,Write}() function interfaces
[model-checker.git]
/
datarace.cc
diff --git
a/datarace.cc
b/datarace.cc
index 5f007f36522754960db4c4588c80ee75c2a49ad5..5174c042e177a52773eee7d7668e010ed38a5e54 100644
(file)
--- a/
datarace.cc
+++ b/
datarace.cc
@@
-201,10
+201,11
@@
void fullRaceCheckWrite(thread_id_t thread, void *location, uint64_t *shadow, Cl
}
/** This function does race detection on a write. */
}
/** 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;
{
uint64_t *shadow = lookupAddressEntry(location);
uint64_t shadowval = *shadow;
+ ClockVector *currClock = model->get_cv(thread);
/* Do full record */
if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
/* Do full record */
if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
@@
-304,10
+305,11
@@
void fullRaceCheckRead(thread_id_t thread, const void *location, uint64_t *shado
}
/** This function does race detection on a read. */
}
/** 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;
{
uint64_t *shadow = lookupAddressEntry(location);
uint64_t shadowval = *shadow;
+ ClockVector *currClock = model->get_cv(thread);
/* Do full record */
if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
/* Do full record */
if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {