race: where possible, use "const void *" for addresses
[model-checker.git] / datarace.cc
index 293743052858c8029fb685ff246ac071f38b821e..e6bbe05c29ddb2dd83e454751cab04ff8d201233 100644 (file)
@@ -1,9 +1,10 @@
 #include "datarace.h"
 #include "model.h"
-#include "threads.h"
+#include "threads-model.h"
 #include <stdio.h>
 #include <cstring>
 #include "mymemory.h"
+#include "clockvector.h"
 
 struct ShadowTable *root;
 std::vector<struct DataRace *> unrealizedraces;
@@ -15,7 +16,7 @@ void initRaceDetector() {
 
 /** This function looks up the entry in the shadow table corresponding to a
  * given address.*/
-static uint64_t * lookupAddressEntry(void * address) {
+static uint64_t * lookupAddressEntry(const void * address) {
        struct ShadowTable *currtable=root;
 #if BIT48
        currtable=(struct ShadowTable *) currtable->array[(((uintptr_t)address)>>32)&MASK16BIT];
@@ -74,7 +75,7 @@ static void expandRecord(uint64_t * shadow) {
 }
 
 /** This function is called when we detect a data race.*/
-static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool isoldwrite, ModelAction *newaction, bool isnewwrite, void *address) {
+static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool isoldwrite, ModelAction *newaction, bool isnewwrite, const void *address) {
        struct DataRace *race = (struct DataRace *)snapshot_malloc(sizeof(struct DataRace));
        race->oldthread=oldthread;
        race->oldclock=oldclock;
@@ -119,11 +120,15 @@ bool checkDataRaces() {
        return false;
 }
 
-void printRace(struct DataRace * race) {
-       printf("Datarace detected\n");
-       printf("Location %p\n", race->address);
-       printf("Initial access: thread %u clock %u, iswrite %u\n",race->oldthread,race->oldclock, race->isoldwrite);
-       printf("Second access: thread %u clock %u, iswrite %u\n", race->newaction->get_tid(), race->newaction->get_seq_number() , race->isnewwrite);
+void printRace(struct DataRace *race)
+{
+       printf("Datarace detected @ address %p:\n", race->address);
+       printf("    Access 1: %5s in thread %2d @ clock %3u\n",
+                       race->isoldwrite ? "write" : "read",
+                       id_to_int(race->oldthread), race->oldclock);
+       printf("    Access 2: %5s in thread %2d @ clock %3u\n",
+                       race->isnewwrite ? "write" : "read",
+                       id_to_int(race->newaction->get_tid()), race->newaction->get_seq_number());
 }
 
 /** This function does race detection for a write on an expanded record. */
@@ -205,7 +210,7 @@ void raceCheckWrite(thread_id_t thread, void *location, ClockVector *currClock)
 }
 
 /** This function does race detection on a read for an expanded record. */
-void fullRaceCheckRead(thread_id_t thread, void *location, uint64_t * shadow, ClockVector *currClock) {
+void fullRaceCheckRead(thread_id_t thread, const void *location, uint64_t * shadow, ClockVector *currClock) {
        struct RaceRecord * record=(struct RaceRecord *) (*shadow);
 
        /* Check for datarace against last write. */
@@ -263,7 +268,7 @@ void fullRaceCheckRead(thread_id_t thread, void *location, uint64_t * shadow, Cl
 }
 
 /** This function does race detection on a read. */
-void raceCheckRead(thread_id_t thread, void *location, ClockVector *currClock) {
+void raceCheckRead(thread_id_t thread, const void *location, ClockVector *currClock) {
        uint64_t * shadow=lookupAddressEntry(location);
        uint64_t shadowval=*shadow;