Fix a bug in memcpy, implement memset, and remove model_thread

diff --git a/datarace.cc b/datarace.cc
index 13aa4655ce05bf254d66604b3f359622a5c00941..11811a1a81456cd26e118410d86a7caba9b2a60f 100644 (file)
--- a/datarace.cc
+++ b/datarace.cc
@@ -865,6 +865,9 @@ Exit:
 
 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
@@ -893,6 +896,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;
        }
 
@@ -910,10 +914,14 @@ 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
@@ -930,6 +938,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;
        }
 
@@ -939,10 +948,14 @@ 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
@@ -952,20 +965,26 @@ void raceCheckRead16(thread_id_t thread, const void *location)
        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)
 {
+       int old_flag = GET_MODEL_FLAG;
+       ENTER_MODEL_FLAG;
+
        uint64_t old_shadowval, new_shadowval;
        old_shadowval = new_shadowval = INVALIDSHADOWVAL;
 #ifdef COLLECT_STAT
        load8_count++;
 #endif
        raceCheckRead_firstIt(thread, location, &old_shadowval, &new_shadowval);
+       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)
@@ -1110,6 +1129,8 @@ Exit:
 
 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
@@ -1138,6 +1159,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;
        }
 
@@ -1155,10 +1177,14 @@ 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
@@ -1175,6 +1201,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;
        }
 
@@ -1184,10 +1211,14 @@ 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
@@ -1198,20 +1229,26 @@ void raceCheckWrite16(thread_id_t thread, const void *location)
        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)
 {
+       int old_flag = GET_MODEL_FLAG;
+       ENTER_MODEL_FLAG;
+
        uint64_t old_shadowval, new_shadowval;
        old_shadowval = new_shadowval = INVALIDSHADOWVAL;
 #ifdef COLLECT_STAT
        store8_count++;
 #endif
        raceCheckWrite_firstIt(thread, location, &old_shadowval, &new_shadowval);
+       RESTORE_MODEL_FLAG(old_flag);
 }
 
 #ifdef COLLECT_STAT

diff --git a/execution.cc b/execution.cc
index 4953718d360499b85dfa8eed8bc6d8415bc1e33a..61d33cb9b629478a4d442bebfbacd155c4383fc6 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -18,8 +18,6 @@
 #include "fuzzer.h"
 #include "newfuzzer.h"
 
-#define INITIAL_THREAD_ID       0
-
 #ifdef COLLECT_STAT
 static unsigned int atomic_load_count = 0;
 static unsigned int atomic_store_count = 0;
@@ -89,8 +87,6 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
        isfinished(false)
 {
        /* Initialize a model-checker thread, for special ModelActions */
-       model_thread = new Thread(get_next_id());
-       add_thread(model_thread);
        fuzzer->register_engine(m, this);
        scheduler->register_engine(this);
 #ifdef TLS

diff --git a/execution.h b/execution.h
index 82d629ce31a808b2cb07353d914e1ae4ecd42c91..b8bfb03580c324309c2af068d6239fed005f5eba 100644 (file)
--- a/execution.h
+++ b/execution.h
@@ -19,6 +19,8 @@
 #include <condition_variable>
 #include "classlist.h"
 
+#define INITIAL_THREAD_ID       0
+
 struct PendingFutureValue {
        PendingFutureValue(ModelAction *writer, ModelAction *reader) :
                writer(writer), reader(reader)

diff --git a/hashtable.h b/hashtable.h
index b7cac67410c287004e9861d14db91c4afc0367dd..22563a01839c4a352adf1dd5679cc7e96422eefc 100644 (file)
--- a/hashtable.h
+++ b/hashtable.h
@@ -113,7 +113,7 @@ public:
 
        /** @brief Reset the table to its initial state. */
        void reset() {
-               memset(table, 0, capacity * sizeof(struct hashlistnode<_Key, _Val>));
+               real_memset(table, 0, capacity * sizeof(struct hashlistnode<_Key, _Val>));
                if (zero) {
                        _free(zero);
                        zero = NULL;

diff --git a/model.cc b/model.cc
index 450aac5a51f2201c62d4743d94339c0cab0c2469..4b94d75a9016a2b4d0cffaab2e9e6ced32f808cc 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -59,9 +59,11 @@ void install_handler() {
 
 void createModelIfNotExist() {
        if (!model) {
+               ENTER_MODEL_FLAG;
                snapshot_system_init(100000);
                model = new ModelChecker();
                model->startChecker();
+               EXIT_MODEL_FLAG;
        }
 }
 
@@ -73,7 +75,7 @@ ModelChecker::ModelChecker() :
        history(new ModelHistory()),
        execution(new ModelExecution(this, scheduler)),
        execution_number(1),
-       curr_thread_num(1),
+       curr_thread_num(INITIAL_THREAD_ID),
        trace_analyses(),
        inspect_plugin(NULL)
 {
@@ -82,7 +84,7 @@ ModelChecker::ModelChecker() :
                                                        "Distributed under the GPLv2\n"
                                                        "Written by Weiyu Luo, Brian Norris, and Brian Demsky\n\n");
        init_memory_ops();
-       memset(&stats,0,sizeof(struct execution_stats));
+       real_memset(&stats,0,sizeof(struct execution_stats));
        init_thread = new Thread(execution->get_next_id(), (thrd_t *) model_malloc(sizeof(thrd_t)), &placeholder, NULL, NULL);
 #ifdef TLS
        init_thread->setTLS((char *)get_tls_addr());
@@ -351,11 +353,11 @@ void ModelChecker::startRunExecution(Thread *old) {
                        execution->collectActions();
                }
 
-               curr_thread_num = 1;
+               curr_thread_num = INITIAL_THREAD_ID;
                Thread *thr = getNextThread(old);
                if (thr != nullptr) {
                        scheduler->set_current_thread(thr);
-                       inside_model = 0;
+                       EXIT_MODEL_FLAG;
                        if (Thread::swap(old, thr) < 0) {
                                perror("swap threads");
                                exit(EXIT_FAILURE);
@@ -419,7 +421,7 @@ void ModelChecker::finishRunExecution(Thread *old)
        scheduler->set_current_thread(NULL);
 
        /** Reset curr_thread_num to initial value for next execution. */
-       curr_thread_num = 1;
+       curr_thread_num = INITIAL_THREAD_ID;
 
        /** If we have more executions, we won't make it past this call. */
        finish_execution(execution_number < params.maxexecutions);
@@ -454,7 +456,7 @@ uint64_t ModelChecker::switch_thread(ModelAction *act)
                delete act;
                return 0;
        }
-       inside_model = 1;
+       ENTER_MODEL_FLAG;
 
        DBG();
        Thread *old = thread_current();

diff --git a/model.h b/model.h
index 331ea18adf96b6e43bcfd8f14551209e3b6ecc6e..9e52f53752e016152bcc9d8267890472e391d1a8 100644 (file)
--- a/model.h
+++ b/model.h
@@ -18,6 +18,11 @@
 #include "classlist.h"
 #include "snapshot-interface.h"
 
+#define ENTER_MODEL_FLAG (inside_model = 1)
+#define EXIT_MODEL_FLAG (inside_model = 0)
+#define GET_MODEL_FLAG (inside_model)
+#define RESTORE_MODEL_FLAG(f) (inside_model = f)
+
 /** @brief Model checker execution stats */
 struct execution_stats {
        int num_total;  /**< @brief Total number of executions */

diff --git a/mymemory.cc b/mymemory.cc
index e82f8d2ef997f31f0d2d38871c74dd6cf17a8cbd..cda63dcc4bd7d20928bf16a089afaa318a0186b0 100644 (file)
--- a/mymemory.cc
+++ b/mymemory.cc
@@ -137,31 +137,32 @@ void init_memory_ops()
 }
 
 void * memcpy(void * dst, const void * src, size_t n) {
-       if (false && model && !inside_model) {
+       if (model && !inside_model) {
+               //model_print("memcpy intercepted\n");
                thread_id_t tid = thread_current_id();
                if (((uintptr_t)src&7) == 0 && ((uintptr_t)dst&7) == 0 && (n&7) == 0) {
                        for (uint i = 0; i < (n>>3); i++) {
-                               raceCheckRead64(tid, (void *)(((char *)src) + i));
+                               raceCheckRead64(tid, (void *)(((uint64_t *)src) + i));
                                ((volatile uint64_t *)dst)[i] = ((uint64_t *)src)[i];
-                               raceCheckWrite64(tid, (void *)(((char *)src) + i));
+                               raceCheckWrite64(tid, (void *)(((uint64_t *)dst) + i));
                        }
                } else if (((uintptr_t)src&3) == 0 && ((uintptr_t)dst&3) == 0 && (n&3) == 0) {
                        for (uint i = 0; i < (n>>2); i++) {
-                               raceCheckRead32(tid, (void *)(((char *)src) + i));
+                               raceCheckRead32(tid, (void *)(((uint32_t *)src) + i));
                                ((volatile uint32_t *)dst)[i] = ((uint32_t *)src)[i];
-                               raceCheckWrite32(tid, (void *)(((char *)src) + i));
+                               raceCheckWrite32(tid, (void *)(((uint32_t *)dst) + i));
                        }
                } else if (((uintptr_t)src&1) == 0 && ((uintptr_t)dst&1) == 0 && (n&1) == 0) {
                        for (uint i = 0; i < (n>>1); i++) {
-                               raceCheckRead16(tid, (void *)(((char *)src) + i));
+                               raceCheckRead16(tid, (void *)(((uint16_t *)src) + i));
                                ((volatile uint16_t *)dst)[i] = ((uint16_t *)src)[i];
-                               raceCheckWrite16(tid, (void *)(((char *)src) + i));
+                               raceCheckWrite16(tid, (void *)(((uint16_t *)dst) + i));
                        }
                } else {
                        for(uint i=0;i<n;i++) {
                                raceCheckRead8(tid, (void *)(((char *)src) + i));
                                ((volatile char *)dst)[i] = ((char *)src)[i];
-                               raceCheckWrite8(tid, (void *)(((char *)src) + i));
+                               raceCheckWrite8(tid, (void *)(((char *)dst) + i));
                        }
                }
        } else {
@@ -176,3 +177,47 @@ void * memcpy(void * dst, const void * src, size_t n) {
        }
        return dst;
 }
+
+void * memset(void *dst, int c, size_t n) {
+       if (model && !inside_model) {
+               thread_id_t tid = thread_current_id();
+               uint8_t cs = c&0xff;
+               if (((uintptr_t)dst&7) == 0 && (n&7) == 0) {
+                       for (uint i = 0; i < (n>>3); i++) {
+                   uint16_t cs2 = cs << 8 | cs;
+                   uint64_t cs3 = cs2 << 16 | cs2;
+                   uint64_t cs4 = cs3 << 32 | cs3;
+                               ((volatile uint64_t *)dst)[i] = cs4;
+                               raceCheckWrite64(tid, (void *)(((uint64_t *)dst) + i));
+                       }
+               } else if (((uintptr_t)dst&3) == 0 && (n&3) == 0) {
+                       for (uint i = 0; i < (n>>2); i++) {
+                   uint16_t cs2 = cs << 8 | cs;
+                   uint32_t cs3 = cs2 << 16 | cs2;
+                               ((volatile uint32_t *)dst)[i] = cs3;
+                               raceCheckWrite32(tid, (void *)(((uint32_t *)dst) + i));
+                       }
+               } else if (((uintptr_t)dst&1) == 0 && (n&1) == 0) {
+                       for (uint i = 0; i < (n>>1); i++) {
+                   uint16_t cs2 = cs << 8 | cs;
+                               ((volatile uint16_t *)dst)[i] = cs2;
+                               raceCheckWrite16(tid, (void *)(((uint16_t *)dst) + i));
+                       }
+               } else {
+                       for (uint i=0;i<n;i++) {
+                               ((volatile char *)dst)[i] = cs;
+                               raceCheckWrite8(tid, (void *)(((char *)dst) + i));
+                       }
+               }
+       } else {
+               if (((uintptr_t)real_memset) < 2) {
+                       //stuck in dynamic linker alloc cycle...
+                       for(size_t s=0;s<n;s++) {
+                               ((volatile char *)dst)[s] = (char) c;
+                       }
+                       return dst;
+               }
+               return real_memset(dst, c, n);
+       }
+       return dst;
+}

diff --git a/schedule.cc b/schedule.cc
index 74ecf406e3cff544ef195d7a48178931ba7cb8cb..93c4fc3fdc0369c79d817d4ef268f4fe0bc3ecb3 100644 (file)
--- a/schedule.cc
+++ b/schedule.cc
@@ -57,7 +57,7 @@ void Scheduler::set_enabled(Thread *t, enabled_type_t enabled_status) {
        int threadid = id_to_int(t->get_id());
        if (threadid >= enabled_len) {
                enabled_type_t *new_enabled = (enabled_type_t *)snapshot_malloc(sizeof(enabled_type_t) * (threadid + 1));
-               memset(&new_enabled[enabled_len], 0, (threadid + 1 - enabled_len) * sizeof(enabled_type_t));
+               real_memset(&new_enabled[enabled_len], 0, (threadid + 1 - enabled_len) * sizeof(enabled_type_t));
                if (enabled != NULL) {
                        real_memcpy(new_enabled, enabled, enabled_len * sizeof(enabled_type_t));
                        snapshot_free(enabled);

diff --git a/threads.cc b/threads.cc
index faa49fc5707454bb105b384d1f4482bd418fb711..024f6ea582e12381b8a76e5c8f53972f57ba48c7 100644 (file)
--- a/threads.cc
+++ b/threads.cc
@@ -419,7 +419,7 @@ Thread::Thread(thread_id_t tid) :
        last_action_val(0),
        model_thread(true)
 {
-       memset(&context, 0, sizeof(context));
+       real_memset(&context, 0, sizeof(context));
 }
 
 /**