Get data race detector working... Commented out function call code since it crashes...

diff --git a/cmodelint.cc b/cmodelint.cc
index b1a8eb43d3258add2ff3d8af5f821ab566669105..98f7f89d46a44af0481b0246eb6fe307c1069796 100644 (file)
--- a/cmodelint.cc
+++ b/cmodelint.cc
@@ -363,7 +363,7 @@ void cds_atomic_thread_fence(int atomic_index, const char * position) {
 
 void cds_func_entry(const char * funcName) {
        if (!model) return;
-
+       /*
        Thread * th = thread_current();
        uint32_t func_id;
 
@@ -378,11 +378,12 @@ void cds_func_entry(const char * funcName) {
        }
 
        history->enter_function(func_id, th->get_id());
+       */
 }
 
 void cds_func_exit(const char * funcName) {
        if (!model) return;
-
+       /*
        Thread * th = thread_current();
        uint32_t func_id;
 
@@ -390,4 +391,5 @@ void cds_func_exit(const char * funcName) {
        func_id = history->getFuncMap()->get(funcName);
 
        history->exit_function(func_id, th->get_id());
+       */
 }

diff --git a/librace.cc b/librace.cc
index a9bb7052ebca835ae5fc0fd69cf212cdb410f983..64133304e31e5fc72414c4399d6719e0b410c4d3 100644 (file)
--- a/librace.cc
+++ b/librace.cc
@@ -6,6 +6,7 @@
 #include "datarace.h"
 #include "model.h"
 #include "threads-model.h"
+#include "snapshot-interface.h"
 
 void store_8(void *addr, uint8_t val)
 {
@@ -101,6 +102,8 @@ uint64_t load_64(const void *addr)
 void cds_store8(void *addr)
 {
        //DEBUG("addr = %p, val = %" PRIu8 "\n", addr, val);
+       if (!model)
+               return;
        thread_id_t tid = thread_current()->get_id();
        raceCheckWrite(tid, addr);
 }
@@ -108,6 +111,8 @@ void cds_store8(void *addr)
 void cds_store16(void *addr)
 {
        //DEBUG("addr = %p, val = %" PRIu16 "\n", addr, val);
+       if (!model)
+               return;
        thread_id_t tid = thread_current()->get_id();
        raceCheckWrite(tid, addr);
        raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 1));
@@ -116,6 +121,8 @@ void cds_store16(void *addr)
 void cds_store32(void *addr)
 {
        //DEBUG("addr = %p, val = %" PRIu32 "\n", addr, val);
+       if (!model)
+               return;
        thread_id_t tid = thread_current()->get_id();
        raceCheckWrite(tid, addr);
        raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 1));
@@ -126,6 +133,8 @@ void cds_store32(void *addr)
 void cds_store64(void *addr)
 {
        //DEBUG("addr = %p, val = %" PRIu64 "\n", addr, val);
+       if (!model)
+               return;
        thread_id_t tid = thread_current()->get_id();
        raceCheckWrite(tid, addr);
        raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 1));
@@ -137,7 +146,41 @@ void cds_store64(void *addr)
        raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 7));
 }
 
-void cds_load8(const void *addr) { load_8(addr); }
-void cds_load16(const void *addr) { load_16(addr); }
-void cds_load32(const void *addr) { load_32(addr); }
-void cds_load64(const void *addr) { load_64(addr); }
+void cds_load8(const void *addr) {
+       if (!model)
+               return;
+       thread_id_t tid = thread_current()->get_id();
+       raceCheckRead(tid, addr);
+}
+
+void cds_load16(const void *addr) {
+       if (!model)
+               return;
+       thread_id_t tid = thread_current()->get_id();
+       raceCheckRead(tid, addr);
+       raceCheckRead(tid, (const void *)(((uintptr_t)addr) + 1));
+}
+
+void cds_load32(const void *addr) {
+       if (!model)
+               return;
+       thread_id_t tid = thread_current()->get_id();
+       raceCheckRead(tid, addr);
+       raceCheckRead(tid, (const void *)(((uintptr_t)addr) + 1));
+       raceCheckRead(tid, (const void *)(((uintptr_t)addr) + 2));
+       raceCheckRead(tid, (const void *)(((uintptr_t)addr) + 3));
+}
+
+void cds_load64(const void *addr) {
+       if (!model)
+               return;
+       thread_id_t tid = thread_current()->get_id();
+       raceCheckRead(tid, addr);
+       raceCheckRead(tid, (const void *)(((uintptr_t)addr) + 1));
+       raceCheckRead(tid, (const void *)(((uintptr_t)addr) + 2));
+       raceCheckRead(tid, (const void *)(((uintptr_t)addr) + 3));
+       raceCheckRead(tid, (const void *)(((uintptr_t)addr) + 4));
+       raceCheckRead(tid, (const void *)(((uintptr_t)addr) + 5));
+       raceCheckRead(tid, (const void *)(((uintptr_t)addr) + 6));
+       raceCheckRead(tid, (const void *)(((uintptr_t)addr) + 7));
+}

diff --git a/main.cc b/main.cc
index a484f497458ee078270aa2cd52ccc2a20c551c1a..80ac52ac1995b9303d012a76ca434c00014be117 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -198,8 +198,6 @@ int main(int argc, char **argv)
        model_params *params = model->getParams();
        parse_options(params, main_argc, main_argv);
 
-       //Initialize race detector
-       initRaceDetector();
 
        snapshot_stack_init();
        install_trace_analyses(model->get_execution());

diff --git a/model.cc b/model.cc
index 1791695432cc0e7f3348e1564c06fd58c030d062..6214e9bcfcea73f4668351197820473e0ae0d923 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -45,6 +45,7 @@ ModelChecker::ModelChecker() :
        scheduler->set_current_thread(init_thread);
        execution->setParams(&params);
        param_defaults(&params);
+       initRaceDetector();
 }
 
 /** @brief Destructor */