Get data race detector working... Commented out function call code since it crashes...
authorroot <root@dw-6.eecs.uci.edu>
Thu, 11 Jul 2019 18:39:35 +0000 (11:39 -0700)
committerroot <root@dw-6.eecs.uci.edu>
Thu, 11 Jul 2019 18:39:35 +0000 (11:39 -0700)
cmodelint.cc
librace.cc
main.cc
model.cc

index b1a8eb4..98f7f89 100644 (file)
@@ -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());
+       */
 }
index a9bb705..6413330 100644 (file)
@@ -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 a484f49..80ac52a 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());
index 1791695..6214e9b 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 */