X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=datarace.cc;h=5a1c1154c2ddca44a916fa3601fe55c119280e60;hb=HEAD;hp=0bfaaff70b0b91efefc5bff7c68cdd705428a3b7;hpb=638ad334ebfab1329faaba7c1b554e8c59af5cf6;p=c11tester.git

diff --git a/datarace.cc b/datarace.cc
index 0bfaaff7..5a1c1154 100644
--- a/datarace.cc
+++ b/datarace.cc
@@ -16,6 +16,18 @@ static void *memory_base;
 static void *memory_top;
 static RaceSet * raceset;
 
+#ifdef COLLECT_STAT
+static unsigned int store8_count = 0;
+static unsigned int store16_count = 0;
+static unsigned int store32_count = 0;
+static unsigned int store64_count = 0;
+
+static unsigned int load8_count = 0;
+static unsigned int load16_count = 0;
+static unsigned int load32_count = 0;
+static unsigned int load64_count = 0;
+#endif
+
 static const ModelExecution * get_execution()
 {
 	return model->get_execution();
@@ -43,7 +55,7 @@ void * table_calloc(size_t size)
 
 /** This function looks up the entry in the shadow table corresponding to a
  * given address.*/
-static uint64_t * lookupAddressEntry(const void *address)
+static inline uint64_t * lookupAddressEntry(const void *address)
 {
 	struct ShadowTable *currtable = root;
 #if BIT48
@@ -113,7 +125,7 @@ void getStoreThreadAndClock(const void *address, thread_id_t * thread, modelcloc
  * @param tid2 The thread ID for the potentially-racing action
  * @return true if the current clock allows a race with the event at clock2/tid2
  */
-static bool clock_may_race(ClockVector *clock1, thread_id_t tid1,
+static inline bool clock_may_race(ClockVector *clock1, thread_id_t tid1,
 													 modelclock_t clock2, thread_id_t tid2)
 {
 	return tid1 != tid2 && clock2 != 0 && clock1->getClock(tid2) <= clock2;
@@ -143,6 +155,8 @@ static void expandRecord(uint64_t *shadow)
 		ASSERT(readThread >= 0);
 		record->thread[0] = readThread;
 		record->readClock[0] = readClock;
+	} else {
+		record->thread = NULL;
 	}
 	if (shadowval & ATOMICMASK)
 		record->isAtomic = 1;
@@ -160,7 +174,6 @@ unsigned int race_hash(struct DataRace *race) {
 	return hash;
 }
 
-
 bool race_equals(struct DataRace *r1, struct DataRace *r2) {
 	if (r1->numframes != r2->numframes)
 		return false;
@@ -174,6 +187,7 @@ bool race_equals(struct DataRace *r1, struct DataRace *r2) {
 /** This function is called when we detect a data race.*/
 static struct DataRace * reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool isoldwrite, ModelAction *newaction, bool isnewwrite, const void *address)
 {
+#ifdef REPORT_DATA_RACES
 	struct DataRace *race = (struct DataRace *)model_malloc(sizeof(struct DataRace));
 	race->oldthread = oldthread;
 	race->oldclock = oldclock;
@@ -182,6 +196,9 @@ static struct DataRace * reportDataRace(thread_id_t oldthread, modelclock_t oldc
 	race->isnewwrite = isnewwrite;
 	race->address = address;
 	return race;
+#else
+	return NULL;
+#endif
 }
 
 /**
@@ -232,7 +249,6 @@ struct DataRace * fullRaceCheckWrite(thread_id_t thread, const void *location, u
 	}
 
 	/* Check for datarace against last write. */
-
 	{
 		modelclock_t writeClock = record->writeClock;
 		thread_id_t writeThread = record->writeThread;
@@ -252,74 +268,6 @@ Exit:
 	return race;
 }
 
-/** This function does race detection on a write. */
-void raceCheckWrite(thread_id_t thread, void *location)
-{
-	uint64_t *shadow = lookupAddressEntry(location);
-	uint64_t shadowval = *shadow;
-	ClockVector *currClock = get_execution()->get_cv(thread);
-	if (currClock == NULL)
-		return;
-
-	struct DataRace * race = NULL;
-	/* Do full record */
-	if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
-		race = fullRaceCheckWrite(thread, location, shadow, currClock);
-		goto Exit;
-	}
-
-	{
-		int threadid = id_to_int(thread);
-		modelclock_t ourClock = currClock->getClock(thread);
-
-		/* Thread ID is too large or clock is too large. */
-		if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
-			expandRecord(shadow);
-			race = fullRaceCheckWrite(thread, location, shadow, currClock);
-			goto Exit;
-		}
-
-
-
-		{
-			/* Check for datarace against last read. */
-			modelclock_t readClock = READVECTOR(shadowval);
-			thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
-
-			if (clock_may_race(currClock, thread, readClock, readThread)) {
-				/* We have a datarace */
-				race = reportDataRace(readThread, readClock, false, get_execution()->get_parent_action(thread), true, location);
-				goto ShadowExit;
-			}
-		}
-
-		{
-			/* Check for datarace against last write. */
-
-			modelclock_t writeClock = WRITEVECTOR(shadowval);
-			thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
-
-			if (clock_may_race(currClock, thread, writeClock, writeThread)) {
-				/* We have a datarace */
-				race = reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), true, location);
-				goto ShadowExit;
-			}
-		}
-
-ShadowExit:
-		*shadow = ENCODEOP(0, 0, threadid, ourClock);
-	}
-
-Exit:
-	if (race) {
-		race->numframes=backtrace(race->backtrace, sizeof(race->backtrace)/sizeof(void*));
-		if (raceset->add(race))
-			assert_race(race);
-		else model_free(race);
-	}
-}
-
-
 /** This function does race detection for a write on an expanded record. */
 struct DataRace * atomfullRaceCheckWrite(thread_id_t thread, const void *location, uint64_t *shadow, ClockVector *currClock)
 {
@@ -399,7 +347,6 @@ void atomraceCheckWrite(thread_id_t thread, void *location)
 
 		{
 			/* Check for datarace against last read. */
-
 			modelclock_t readClock = READVECTOR(shadowval);
 			thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
 
@@ -412,7 +359,6 @@ void atomraceCheckWrite(thread_id_t thread, void *location)
 
 		{
 			/* Check for datarace against last write. */
-
 			modelclock_t writeClock = WRITEVECTOR(shadowval);
 			thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
 
@@ -429,10 +375,14 @@ ShadowExit:
 
 Exit:
 	if (race) {
+#ifdef REPORT_DATA_RACES
 		race->numframes=backtrace(race->backtrace, sizeof(race->backtrace)/sizeof(void*));
 		if (raceset->add(race))
 			assert_race(race);
 		else model_free(race);
+#else
+		model_free(race);
+#endif
 	}
 }
 
@@ -482,7 +432,7 @@ void recordWrite(thread_id_t thread, void *location) {
 
 /** This function just updates metadata on atomic write. */
 void recordCalloc(void *location, size_t size) {
-	thread_id_t thread = thread_current()->get_id();
+	thread_id_t thread = thread_current_id();
 	for(;size != 0;size--) {
 		uint64_t *shadow = lookupAddressEntry(location);
 		uint64_t shadowval = *shadow;
@@ -508,8 +458,6 @@ void recordCalloc(void *location, size_t size) {
 	}
 }
 
-
-
 /** This function does race detection on a read for an expanded record. */
 struct DataRace * fullRaceCheckRead(thread_id_t thread, const void *location, uint64_t *shadow, ClockVector *currClock)
 {
@@ -542,16 +490,16 @@ struct DataRace * fullRaceCheckRead(thread_id_t thread, const void *location, ui
 		if (clock_may_race(currClock, thread, readClock, readThread)) {
 			/* Still need this read in vector */
 			if (copytoindex != i) {
-				ASSERT(record->thread[i] >= 0);
-				record->readClock[copytoindex] = record->readClock[i];
-				record->thread[copytoindex] = record->thread[i];
+				ASSERT(readThread >= 0);
+				record->readClock[copytoindex] = readClock;
+				record->thread[copytoindex] = readThread;
 			}
 			copytoindex++;
 		}
 	}
 
 	if (__builtin_popcount(copytoindex) <= 1) {
-		if (copytoindex == 0) {
+		if (copytoindex == 0 && record->thread == NULL) {
 			int newCapacity = INITCAPACITY;
 			record->thread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t) * newCapacity);
 			record->readClock = (modelclock_t *)snapshot_malloc(sizeof(modelclock_t) * newCapacity);
@@ -559,8 +507,8 @@ struct DataRace * fullRaceCheckRead(thread_id_t thread, const void *location, ui
 			int newCapacity = copytoindex * 2;
 			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, copytoindex * sizeof(thread_id_t));
-			std::memcpy(newreadClock, record->readClock, copytoindex * sizeof(modelclock_t));
+			real_memcpy(newthread, record->thread, copytoindex * sizeof(thread_id_t));
+			real_memcpy(newreadClock, record->readClock, copytoindex * sizeof(modelclock_t));
 			snapshot_free(record->readClock);
 			snapshot_free(record->thread);
 			record->readClock = newreadClock;
@@ -577,70 +525,6 @@ struct DataRace * fullRaceCheckRead(thread_id_t thread, const void *location, ui
 	return race;
 }
 
-/** This function does race detection on a read. */
-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);
-	if (currClock == NULL)
-		return;
-
-	struct DataRace * race = NULL;
-
-	/* Do full record */
-	if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
-		race = fullRaceCheckRead(thread, location, shadow, currClock);
-		goto Exit;
-	}
-
-	{
-		int threadid = id_to_int(thread);
-		modelclock_t ourClock = currClock->getClock(thread);
-
-		/* Thread ID is too large or clock is too large. */
-		if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
-			expandRecord(shadow);
-			race = fullRaceCheckRead(thread, location, shadow, currClock);
-			goto Exit;
-		}
-
-		/* Check for datarace against last write. */
-
-		modelclock_t writeClock = WRITEVECTOR(shadowval);
-		thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
-
-		if (clock_may_race(currClock, thread, writeClock, writeThread)) {
-			/* We have a datarace */
-			race = reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), false, location);
-			goto ShadowExit;
-		}
-
-ShadowExit:
-		{
-			modelclock_t readClock = READVECTOR(shadowval);
-			thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
-
-			if (clock_may_race(currClock, thread, readClock, readThread)) {
-				/* We don't subsume this read... Have to expand record. */
-				expandRecord(shadow);
-				fullRaceCheckRead(thread, location, shadow, currClock);
-				goto Exit;
-			}
-		}
-
-		*shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock) | (shadowval & ATOMICMASK);
-	}
-Exit:
-	if (race) {
-		race->numframes=backtrace(race->backtrace, sizeof(race->backtrace)/sizeof(void*));
-		if (raceset->add(race))
-			assert_race(race);
-		else model_free(race);
-	}
-}
-
-
 /** This function does race detection on a read for an expanded record. */
 struct DataRace * atomfullRaceCheckRead(thread_id_t thread, const void *location, uint64_t *shadow, ClockVector *currClock)
 {
@@ -682,7 +566,6 @@ void atomraceCheckRead(thread_id_t thread, const void *location)
 
 	{
 		/* Check for datarace against last write. */
-
 		modelclock_t writeClock = WRITEVECTOR(shadowval);
 		thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
 
@@ -691,15 +574,17 @@ void atomraceCheckRead(thread_id_t thread, const void *location)
 			race = reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), false, location);
 			goto Exit;
 		}
-
-
 	}
 Exit:
 	if (race) {
+#ifdef REPORT_DATA_RACES
 		race->numframes=backtrace(race->backtrace, sizeof(race->backtrace)/sizeof(void*));
 		if (raceset->add(race))
 			assert_race(race);
 		else model_free(race);
+#else
+		model_free(race);
+#endif
 	}
 }
 
@@ -732,7 +617,6 @@ static inline uint64_t * raceCheckRead_firstIt(thread_id_t thread, const void *
 		}
 
 		/* Check for datarace against last write. */
-
 		modelclock_t writeClock = WRITEVECTOR(shadowval);
 		thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
 
@@ -762,20 +646,23 @@ static inline uint64_t * raceCheckRead_firstIt(thread_id_t thread, const void *
 	}
 Exit:
 	if (race) {
+#ifdef REPORT_DATA_RACES
 		race->numframes=backtrace(race->backtrace, sizeof(race->backtrace)/sizeof(void*));
 		if (raceset->add(race))
 			assert_race(race);
 		else model_free(race);
+#else
+		model_free(race);
+#endif
 	}
 
 	return shadow;
 }
 
-static inline void raceCheckRead_otherIt(thread_id_t thread, const void * location) {
+static inline void raceCheckRead_otherIt(thread_id_t thread, const void * location)
+{
 	uint64_t *shadow = lookupAddressEntry(location);
-
 	uint64_t shadowval = *shadow;
-
 	ClockVector *currClock = get_execution()->get_cv(thread);
 	if (currClock == NULL)
 		return;
@@ -826,21 +713,27 @@ static inline void raceCheckRead_otherIt(thread_id_t thread, const void * locati
 	}
 Exit:
 	if (race) {
+#ifdef REPORT_DATA_RACES
 		race->numframes=backtrace(race->backtrace, sizeof(race->backtrace)/sizeof(void*));
 		if (raceset->add(race))
 			assert_race(race);
 		else model_free(race);
+#else
+		model_free(race);
+#endif
 	}
 }
 
-
-
 void raceCheckRead64(thread_id_t thread, const void *location)
 {
+	int old_flag = GET_MODEL_FLAG;
+	ENTER_MODEL_FLAG;
+
 	uint64_t old_shadowval, new_shadowval;
 	old_shadowval = new_shadowval = INVALIDSHADOWVAL;
-
-
+#ifdef COLLECT_STAT
+	load64_count++;
+#endif
 	uint64_t * shadow = raceCheckRead_firstIt(thread, location, &old_shadowval, &new_shadowval);
 	if (CHECKBOUNDARY(location, 7)) {
 		if (shadow[1]==old_shadowval)
@@ -864,6 +757,7 @@ void raceCheckRead64(thread_id_t thread, const void *location)
 		if (shadow[7]==old_shadowval)
 			shadow[7] = new_shadowval;
 		else goto L7;
+		RESTORE_MODEL_FLAG(old_flag);
 		return;
 	}
 
@@ -881,14 +775,19 @@ L6:
 	raceCheckRead_otherIt(thread, (const void *)(((uintptr_t)location) + 6));
 L7:
 	raceCheckRead_otherIt(thread, (const void *)(((uintptr_t)location) + 7));
+	RESTORE_MODEL_FLAG(old_flag);
 }
 
 void raceCheckRead32(thread_id_t thread, const void *location)
 {
+	int old_flag = GET_MODEL_FLAG;
+	ENTER_MODEL_FLAG;
+
 	uint64_t old_shadowval, new_shadowval;
 	old_shadowval = new_shadowval = INVALIDSHADOWVAL;
-
-
+#ifdef COLLECT_STAT
+	load32_count++;
+#endif
 	uint64_t * shadow = raceCheckRead_firstIt(thread, location, &old_shadowval, &new_shadowval);
 	if (CHECKBOUNDARY(location, 3)) {
 		if (shadow[1]==old_shadowval)
@@ -900,6 +799,7 @@ void raceCheckRead32(thread_id_t thread, const void *location)
 		if (shadow[3]==old_shadowval)
 			shadow[3] = new_shadowval;
 		else goto L3;
+		RESTORE_MODEL_FLAG(old_flag);
 		return;
 	}
 
@@ -909,31 +809,41 @@ L2:
 	raceCheckRead_otherIt(thread, (const void *)(((uintptr_t)location) + 2));
 L3:
 	raceCheckRead_otherIt(thread, (const void *)(((uintptr_t)location) + 3));
+	RESTORE_MODEL_FLAG(old_flag);
 }
 
 void raceCheckRead16(thread_id_t thread, const void *location)
 {
+	int old_flag = GET_MODEL_FLAG;
+	ENTER_MODEL_FLAG;
+
 	uint64_t old_shadowval, new_shadowval;
 	old_shadowval = new_shadowval = INVALIDSHADOWVAL;
-
-
+#ifdef COLLECT_STAT
+	load16_count++;
+#endif
 	uint64_t * shadow = raceCheckRead_firstIt(thread, location, &old_shadowval, &new_shadowval);
 	if (CHECKBOUNDARY(location, 1)) {
 		if (shadow[1]==old_shadowval) {
 			shadow[1] = new_shadowval;
+			RESTORE_MODEL_FLAG(old_flag);
 			return;
 		}
 	}
 	raceCheckRead_otherIt(thread, (const void *)(((uintptr_t)location) + 1));
+	RESTORE_MODEL_FLAG(old_flag);
 }
 
 void raceCheckRead8(thread_id_t thread, const void *location)
 {
-	uint64_t old_shadowval, new_shadowval;
-	old_shadowval = new_shadowval = INVALIDSHADOWVAL;
-
+	int old_flag = GET_MODEL_FLAG;
+	ENTER_MODEL_FLAG;
 
-	raceCheckRead_firstIt(thread, location, &old_shadowval, &new_shadowval);
+#ifdef COLLECT_STAT
+	load8_count++;
+#endif
+	raceCheckRead_otherIt(thread, location);
+	RESTORE_MODEL_FLAG(old_flag);
 }
 
 static inline uint64_t * raceCheckWrite_firstIt(thread_id_t thread, const void * location, uint64_t *old_val, uint64_t *new_val)
@@ -995,20 +905,23 @@ ShadowExit:
 
 Exit:
 	if (race) {
+#ifdef REPORT_DATA_RACES
 		race->numframes=backtrace(race->backtrace, sizeof(race->backtrace)/sizeof(void*));
 		if (raceset->add(race))
 			assert_race(race);
 		else model_free(race);
+#else
+		model_free(race);
+#endif
 	}
 
 	return shadow;
 }
 
-static inline void raceCheckWrite_otherIt(thread_id_t thread, const void * location) {
+static inline void raceCheckWrite_otherIt(thread_id_t thread, const void * location)
+{
 	uint64_t *shadow = lookupAddressEntry(location);
-
 	uint64_t shadowval = *shadow;
-
 	ClockVector *currClock = get_execution()->get_cv(thread);
 	if (currClock == NULL)
 		return;
@@ -1061,19 +974,26 @@ ShadowExit:
 
 Exit:
 	if (race) {
+#ifdef REPORT_DATA_RACES
 		race->numframes=backtrace(race->backtrace, sizeof(race->backtrace)/sizeof(void*));
 		if (raceset->add(race))
 			assert_race(race);
 		else model_free(race);
+#else
+		model_free(race);
+#endif
 	}
 }
 
 void raceCheckWrite64(thread_id_t thread, const void *location)
 {
+	int old_flag = GET_MODEL_FLAG;
+	ENTER_MODEL_FLAG;
 	uint64_t old_shadowval, new_shadowval;
 	old_shadowval = new_shadowval = INVALIDSHADOWVAL;
-
-
+#ifdef COLLECT_STAT
+	store64_count++;
+#endif
 	uint64_t * shadow = raceCheckWrite_firstIt(thread, location, &old_shadowval, &new_shadowval);
 	if (CHECKBOUNDARY(location, 7)) {
 		if (shadow[1]==old_shadowval)
@@ -1097,6 +1017,7 @@ void raceCheckWrite64(thread_id_t thread, const void *location)
 		if (shadow[7]==old_shadowval)
 			shadow[7] = new_shadowval;
 		else goto L7;
+		RESTORE_MODEL_FLAG(old_flag);
 		return;
 	}
 
@@ -1114,14 +1035,19 @@ L6:
 	raceCheckWrite_otherIt(thread, (const void *)(((uintptr_t)location) + 6));
 L7:
 	raceCheckWrite_otherIt(thread, (const void *)(((uintptr_t)location) + 7));
+	RESTORE_MODEL_FLAG(old_flag);
 }
 
 void raceCheckWrite32(thread_id_t thread, const void *location)
 {
+	int old_flag = GET_MODEL_FLAG;
+	ENTER_MODEL_FLAG;
+
 	uint64_t old_shadowval, new_shadowval;
 	old_shadowval = new_shadowval = INVALIDSHADOWVAL;
-
-
+#ifdef COLLECT_STAT
+	store32_count++;
+#endif
 	uint64_t * shadow = raceCheckWrite_firstIt(thread, location, &old_shadowval, &new_shadowval);
 	if (CHECKBOUNDARY(location, 3)) {
 		if (shadow[1]==old_shadowval)
@@ -1133,6 +1059,7 @@ void raceCheckWrite32(thread_id_t thread, const void *location)
 		if (shadow[3]==old_shadowval)
 			shadow[3] = new_shadowval;
 		else goto L3;
+		RESTORE_MODEL_FLAG(old_flag);
 		return;
 	}
 
@@ -1142,29 +1069,215 @@ L2:
 	raceCheckWrite_otherIt(thread, (const void *)(((uintptr_t)location) + 2));
 L3:
 	raceCheckWrite_otherIt(thread, (const void *)(((uintptr_t)location) + 3));
+	RESTORE_MODEL_FLAG(old_flag);
 }
 
 void raceCheckWrite16(thread_id_t thread, const void *location)
 {
+	int old_flag = GET_MODEL_FLAG;
+	ENTER_MODEL_FLAG;
+
 	uint64_t old_shadowval, new_shadowval;
 	old_shadowval = new_shadowval = INVALIDSHADOWVAL;
-
+#ifdef COLLECT_STAT
+	store16_count++;
+#endif
 
 	uint64_t * shadow = raceCheckWrite_firstIt(thread, location, &old_shadowval, &new_shadowval);
 	if (CHECKBOUNDARY(location, 1)) {
 		if (shadow[1]==old_shadowval) {
 			shadow[1] = new_shadowval;
+			RESTORE_MODEL_FLAG(old_flag);
 			return;
 		}
 	}
 	raceCheckWrite_otherIt(thread, (const void *)(((uintptr_t)location) + 1));
+	RESTORE_MODEL_FLAG(old_flag);
 }
 
 void raceCheckWrite8(thread_id_t thread, const void *location)
 {
-	uint64_t old_shadowval, new_shadowval;
-	old_shadowval = new_shadowval = INVALIDSHADOWVAL;
+	int old_flag = GET_MODEL_FLAG;
+	ENTER_MODEL_FLAG;
+
+#ifdef COLLECT_STAT
+	store8_count++;
+#endif
+	raceCheckWrite_otherIt(thread, location);
+	RESTORE_MODEL_FLAG(old_flag);
+}
+
+void raceCheckWriteMemop(thread_id_t thread, const void *location, size_t size)
+{
+	int old_flag = GET_MODEL_FLAG;
+	ENTER_MODEL_FLAG;
+
+	ClockVector *currClock = get_execution()->get_cv(thread);
+	if (currClock == NULL) {
+		RESTORE_MODEL_FLAG(old_flag);
+		return;
+	}
+
+	bool alreadyHasRace = false;
+	for (uint i = 0; i < size; i++) {
+		uint64_t *shadow = lookupAddressEntry(location);
+		uint64_t shadowval = *shadow;
+
+		struct DataRace * race = NULL;
+		/* Do full record */
+		if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
+			race = fullRaceCheckWrite(thread, location, shadow, currClock);
+			goto Exit;
+		}
+
+		{
+			int threadid = id_to_int(thread);
+			modelclock_t ourClock = currClock->getClock(thread);
 
+			/* Thread ID is too large or clock is too large. */
+			if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
+				expandRecord(shadow);
+				race = fullRaceCheckWrite(thread, location, shadow, currClock);
+				goto Exit;
+			}
+
+			{
+				/* Check for datarace against last read. */
+				modelclock_t readClock = READVECTOR(shadowval);
+				thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
+
+				if (clock_may_race(currClock, thread, readClock, readThread)) {
+					/* We have a datarace */
+					race = reportDataRace(readThread, readClock, false, get_execution()->get_parent_action(thread), true, location);
+					goto ShadowExit;
+				}
+			}
+
+			{
+				/* Check for datarace against last write. */
+				modelclock_t writeClock = WRITEVECTOR(shadowval);
+				thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
+
+				if (clock_may_race(currClock, thread, writeClock, writeThread)) {
+					/* We have a datarace */
+					race = reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), true, location);
+					goto ShadowExit;
+				}
+			}
+
+ShadowExit:
+			*shadow = ENCODEOP(0, 0, threadid, ourClock);
+		}
+
+Exit:
+		if (race) {
+#ifdef REPORT_DATA_RACES
+			if (!alreadyHasRace) {
+				alreadyHasRace = true;
+				race->numframes=backtrace(race->backtrace, sizeof(race->backtrace)/sizeof(void*));
+				if (raceset->add(race))
+					assert_race(race);
+				else model_free(race);
+			} else {
+				model_free(race);
+			}
+#else
+			model_free(race);
+#endif
+		}
+	}
+	RESTORE_MODEL_FLAG(old_flag);
+}
+
+void raceCheckReadMemop(thread_id_t thread, const void * location, size_t size)
+{
+	int old_flag = GET_MODEL_FLAG;
+	ENTER_MODEL_FLAG;
+
+	ClockVector *currClock = get_execution()->get_cv(thread);
+	if (currClock == NULL) {
+		RESTORE_MODEL_FLAG(old_flag);
+		return;
+	}
+
+	bool alreadyHasRace = false;
+	for (uint i = 0; i < size; i++) {
+		uint64_t *shadow = lookupAddressEntry(location);
+		uint64_t shadowval = *shadow;
+		struct DataRace * race = NULL;
+
+		/* Do full record */
+		if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
+			race = fullRaceCheckRead(thread, location, shadow, currClock);
+			goto Exit;
+		}
 
-	raceCheckWrite_firstIt(thread, location, &old_shadowval, &new_shadowval);
+		{
+			int threadid = id_to_int(thread);
+			modelclock_t ourClock = currClock->getClock(thread);
+
+			/* Thread ID is too large or clock is too large. */
+			if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
+				expandRecord(shadow);
+				race = fullRaceCheckRead(thread, location, shadow, currClock);
+				goto Exit;
+			}
+
+			/* Check for datarace against last write. */
+			modelclock_t writeClock = WRITEVECTOR(shadowval);
+			thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
+
+			if (clock_may_race(currClock, thread, writeClock, writeThread)) {
+				/* We have a datarace */
+				race = reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), false, location);
+			}
+
+			modelclock_t readClock = READVECTOR(shadowval);
+			thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
+
+			if (clock_may_race(currClock, thread, readClock, readThread)) {
+				/* We don't subsume this read... Have to expand record. */
+				expandRecord(shadow);
+				struct RaceRecord *record = (struct RaceRecord *) (*shadow);
+				record->thread[1] = thread;
+				record->readClock[1] = ourClock;
+				record->numReads++;
+
+				goto Exit;
+			}
+
+			*shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock) | (shadowval & ATOMICMASK);
+		}
+Exit:
+		if (race) {
+#ifdef REPORT_DATA_RACES
+			if (!alreadyHasRace) {
+				race->numframes=backtrace(race->backtrace, sizeof(race->backtrace)/sizeof(void*));
+				if (raceset->add(race))
+					assert_race(race);
+				else model_free(race);
+			} else {
+				model_free(race);
+			}
+#else
+			model_free(race);
+#endif
+		}
+	}
+	RESTORE_MODEL_FLAG(old_flag);
 }
+
+#ifdef COLLECT_STAT
+void print_normal_accesses()
+{
+	model_print("store 8  count: %u\n", store8_count);
+	model_print("store 16 count: %u\n", store16_count);
+	model_print("store 32 count: %u\n", store32_count);
+	model_print("store 64 count: %u\n", store64_count);
+
+	model_print("load  8  count: %u\n", load8_count);
+	model_print("load  16 count: %u\n", load16_count);
+	model_print("load  32 count: %u\n", load32_count);
+	model_print("load  64 count: %u\n", load64_count);
+}
+#endif