save

;
;

diff --git a/benchmark/chase-lev-deque-bugfix/deque.c b/benchmark/chase-lev-deque-bugfix/deque.c
index 1ebeb135c3cee5c456133794b2f83bcf1030419d..9fbc426101362b6787a9c45bf42f359246224f4b 100644 (file)
--- a/benchmark/chase-lev-deque-bugfix/deque.c
+++ b/benchmark/chase-lev-deque-bugfix/deque.c
@@ -24,6 +24,7 @@ int take(Deque *q) {
        size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed) - 1;
        Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
        atomic_store_explicit(&q->bottom, b, memory_order_relaxed);
+       /**** detected correctness ****/
        atomic_thread_fence(memory_order_seq_cst);
        size_t t = atomic_load_explicit(&q->top, memory_order_relaxed);
        /**
@@ -79,7 +80,7 @@ void resize(Deque *q) {
        for(i=top; i < bottom; i++) {
                atomic_store_explicit(&new_a->buffer[i % new_size], atomic_load_explicit(&a->buffer[i % size], memory_order_relaxed), memory_order_relaxed);
        }
-       /**** FIXME: detected failure ****/
+       /**** detected UL ****/
        atomic_store_explicit(&q->array, new_a, memory_order_release);
        printf("resize\n");
 }
@@ -91,7 +92,7 @@ void resize(Deque *q) {
 */
 void push(Deque *q, int x) {
        size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed);
-       /**** FIXME: detected correctness ****/
+       /**** detected correctness ****/
        size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
        Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
        if (b - t > atomic_load_explicit(&a->size, memory_order_relaxed) - 1) /* Full queue. */ {
@@ -107,6 +108,7 @@ void push(Deque *q, int x) {
                @Label: Push_Point
                @End
        */
+       /**** correctness error ****/
        atomic_thread_fence(memory_order_release);
        
        atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
@@ -121,7 +123,9 @@ void push(Deque *q, int x) {
 int steal(Deque *q) {
        //FIXME: weaken the following acquire causes no spec problem
        size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
+       //FIXME: remove the fence causes no error and fewer executions..
        atomic_thread_fence(memory_order_seq_cst);
+       /**** detected UL ****/
        size_t b = atomic_load_explicit(&q->bottom, memory_order_acquire);
        /**
                @Begin
@@ -132,6 +136,7 @@ int steal(Deque *q) {
        int x = EMPTY;
        if (t < b) {
                /* Non-empty queue. */
+               /**** detected UL ****/
                Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_acquire);
                int size = atomic_load_explicit(&a->size, memory_order_relaxed);
                x = atomic_load_explicit(&a->buffer[t % size], memory_order_relaxed);
@@ -141,7 +146,7 @@ int steal(Deque *q) {
                        @Label: Potential_Steal
                        @End
                */
-               
+               /**** detected correctness failure ****/ 
                bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1,
                        memory_order_seq_cst, memory_order_relaxed);
                /**

diff --git a/benchmark/chase-lev-deque-bugfix/deque.h b/benchmark/chase-lev-deque-bugfix/deque.h
index 6bb4698fee6480f95152f51e53bd8617c2176cdd..8a3e857a4de8b47c4133884625921c0658859f04 100644 (file)
--- a/benchmark/chase-lev-deque-bugfix/deque.h
+++ b/benchmark/chase-lev-deque-bugfix/deque.h
@@ -47,11 +47,17 @@ typedef struct {
             }
         @DefineFunc:
             call_id_t get_id(void *wrapper) {
-                return ((tag_elem_t*) wrapper)->id;
+                               tag_elem_t *res = (tag_elem_t*) wrapper;
+                               if (res == NULL) {
+                                       //model_print("wrong id here\n");
+                                       return 0;
+                               }
+                return res->id;
             }
         @DefineFunc:
             int get_data(void *wrapper) {
-                return ((tag_elem_t*) wrapper)->data;
+                               tag_elem_t *res = (tag_elem_t*) wrapper;
+                return res->data;
             }
     @Happens_before:
         Push -> Steal

diff --git a/benchmark/chase-lev-deque-bugfix/main.c b/benchmark/chase-lev-deque-bugfix/main.c
index 782539e9dd43b6ab4e427b8cb780546b8119d236..1906f1d66e4cc31857ff34bcf3bb895b2f7abb81 100644 (file)
--- a/benchmark/chase-lev-deque-bugfix/main.c
+++ b/benchmark/chase-lev-deque-bugfix/main.c
@@ -15,6 +15,7 @@ int c;
 
 static void task(void * param) {
        a=steal(q);
+       a=steal(q);
 }
 
 int user_main(int argc, char **argv)

diff --git a/benchmark/cliffc-hashtable/cliffc_hashtable.h b/benchmark/cliffc-hashtable/cliffc_hashtable.h
index ff5d9c32f793c1b2e9965e3c3d9d880729be846e..645531fbc241b16806d445233842c5d463911e5d 100644 (file)
--- a/benchmark/cliffc-hashtable/cliffc_hashtable.h
+++ b/benchmark/cliffc-hashtable/cliffc_hashtable.h
@@ -259,7 +259,7 @@ friend class CHM;
                        kvs_data *desired = (kvs_data*) NULL;
                        kvs_data *expected = (kvs_data*) newkvs; 
                        if (!_newkvs.compare_exchange_strong(desired, expected, memory_order_release,
-                                       memory_order_release)) {
+                                       memory_order_relaxed)) {
                                // Should clean the allocated area
                                delete newkvs;
                                newkvs = _newkvs.load(memory_order_acquire);
@@ -283,7 +283,7 @@ friend class CHM;
                                        copyidx = _copy_idx.load(memory_order_acquire);
                                        while (copyidx < (oldlen << 1) &&
                                                !_copy_idx.compare_exchange_strong(copyidx, copyidx +
-                                                       min_copy_work, memory_order_release, memory_order_release))
+                                                       min_copy_work, memory_order_release, memory_order_relaxed))
                                                copyidx = _copy_idx.load(memory_order_relaxed);
                                        if (!(copyidx < (oldlen << 1)))
                                                panic_start = copyidx;
@@ -332,7 +332,7 @@ friend class CHM;
                                topmap->_kvs.load(memory_order_acquire) == oldkvs) {
                                kvs_data *newkvs = _newkvs.load(memory_order_acquire);
                                topmap->_kvs.compare_exchange_strong(oldkvs, newkvs, memory_order_release,
-                                       memory_order_release);
+                                       memory_order_relaxed);
                        }
                }
        
@@ -648,7 +648,7 @@ friend class CHM;
        // inserted keys
        static inline bool CAS_key(kvs_data *kvs, int idx, void *expected, void *desired) {
                return kvs->_data[2 * idx + 2].compare_exchange_strong(expected,
-                       desired, memory_order_release, memory_order_release);
+                       desired, memory_order_release, memory_order_relaxed);
        }
 
        /**
@@ -660,7 +660,7 @@ friend class CHM;
        static inline bool CAS_val(kvs_data *kvs, int idx, void *expected, void
                *desired) {
                bool res =  kvs->_data[2 * idx + 3].compare_exchange_strong(expected,
-                       desired, memory_order_release, memory_order_release);
+                       desired, memory_order_release, memory_order_relaxed);
                /**
                        # If it is a successful put instead of a copy or any other internal
                        # operantions, expected != NULL

diff --git a/benchmark/mcs-lock/mcs-lock.h b/benchmark/mcs-lock/mcs-lock.h
index 4714567fd1a82b02839897c919a639bed22e96a9..a165437bf320388f52a934feb4c28ba51d6ca645 100644 (file)
--- a/benchmark/mcs-lock/mcs-lock.h
+++ b/benchmark/mcs-lock/mcs-lock.h
@@ -96,6 +96,7 @@ public:
                        // publish me to previous lock-holder :
                        // FIXME: detection miss, don't think it's necessary  
                        pred->next.store(me, std::mo_release );
+                       printf("lock_miss1\n");
 
                        // (*2) pred not touched any more       
 
@@ -134,6 +135,7 @@ public:
 
                // FIXME: detection miss, don't think it's necessary
                mcs_node * next = me->next.load(std::mo_acquire);
+               printf("unlock_miss2\n");
                if ( next == NULL )
                {
                        mcs_node * tail_was_me = me;
@@ -157,6 +159,7 @@ public:
                        for(;;) {
                                // FIXME: detection miss, don't think it's necessary
                                next = me->next.load(std::mo_acquire);
+                               printf("unlock_miss3\n");
                                if ( next != NULL )
                                        break;
                                thrd_yield();

diff --git a/benchmark/mpmc-queue/mpmc-queue.h b/benchmark/mpmc-queue/mpmc-queue.h
index d482c9e9790b62d430637b1ec9c222a386199b4a..e6d54855ede7d2b5f2d7f7dda7b51dfa6498b37b 100644 (file)
--- a/benchmark/mpmc-queue/mpmc-queue.h
+++ b/benchmark/mpmc-queue/mpmc-queue.h
@@ -81,8 +81,8 @@ public:
        */
        t_element * read_fetch() {
                // Try this new weaker semantics
-               //unsigned int rdwr = m_rdwr.load(mo_acquire);
-               unsigned int rdwr = m_rdwr.load(mo_relaxed);
+               unsigned int rdwr = m_rdwr.load(mo_acquire);
+               //unsigned int rdwr = m_rdwr.load(mo_relaxed);
                /**
                        @Begin
                        @Potential_commit_point_define: true
@@ -143,6 +143,7 @@ public:
                @End
        */
        void read_consume(t_element *bin) {
+               /**** FIXME: miss ****/
                m_read.fetch_add(1,mo_release);
                /**
                        @Begin
@@ -167,8 +168,8 @@ public:
        */
        t_element * write_prepare() {
                // Try weaker semantics
-               //unsigned int rdwr = m_rdwr.load(mo_acquire);
-               unsigned int rdwr = m_rdwr.load(mo_relaxed);
+               unsigned int rdwr = m_rdwr.load(mo_acquire);
+               //unsigned int rdwr = m_rdwr.load(mo_relaxed);
                /**
                        @Begin
                        @Potential_commit_point_define: true
@@ -230,6 +231,7 @@ public:
        */
        void write_publish(t_element *bin)
        {
+               /**** hb violation ****/
                m_written.fetch_add(1,mo_release);
                /**
                        @Begin

diff --git a/benchmark/ms-queue/main.c b/benchmark/ms-queue/main.c
index c8d160b8fb696e52ea6af0ac82e53d64c5123334..12cf32e32f9dcbe005010e0a9a7b25afc748259b 100644 (file)
--- a/benchmark/ms-queue/main.c
+++ b/benchmark/ms-queue/main.c
@@ -36,7 +36,9 @@ static void main_task(void *param)
        } else {
                input[1] = 37;
                enqueue(queue, input[1]);
-               output[1] = dequeue(queue);
+               //output[1] = dequeue(queue);
+               output[0] = dequeue(queue);
+               output[0] = dequeue(queue);
        }
 }
 

diff --git a/benchmark/ms-queue/my_queue.c b/benchmark/ms-queue/my_queue.c
index 2b90fe53886d8e8964ca8d86b8f787dbeb1a2a3d..0d64ed8d168f312fdccae77efe13823a603167d9 100644 (file)
--- a/benchmark/ms-queue/my_queue.c
+++ b/benchmark/ms-queue/my_queue.c
@@ -101,7 +101,7 @@ void enqueue(queue_t *q, unsigned int val)
        atomic_store_explicit(&q->nodes[node].next, tmp, relaxed);
 
        while (!success) {
-               /****FIXME: detected UL ****/
+               /**** detected UL ****/
                tail = atomic_load_explicit(&q->tail, acquire);
                /****FIXME: miss ****/
                next = atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire);
@@ -113,7 +113,7 @@ void enqueue(queue_t *q, unsigned int val)
 
                        if (get_ptr(next) == 0) { // == NULL
                                pointer value = MAKE_POINTER(node, get_count(next) + 1);
-                               /****FIXME: first release UL ****/
+                               /**** detected UL ****/
                                // Second release can be just relaxed
                                success = atomic_compare_exchange_strong_explicit(&q->nodes[get_ptr(tail)].next,
                                                &next, value, release, relaxed);
@@ -126,12 +126,12 @@ void enqueue(queue_t *q, unsigned int val)
                        }
                        if (!success) {
                                // This routine helps the other enqueue to update the tail
-                               /****FIXME: detected UL ****/
+                               /**** detected UL ****/
                                unsigned int ptr = get_ptr(atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire));
                                pointer value = MAKE_POINTER(ptr,
                                                get_count(tail) + 1);
                                /****FIXME: miss ****/
-                               // Seconde release can be just relaxed
+                               // Second release can be just relaxed
                                bool succ = false;
                                succ = atomic_compare_exchange_strong_explicit(&q->tail,
                                                &tail, value, release, relaxed);
@@ -143,7 +143,7 @@ void enqueue(queue_t *q, unsigned int val)
                        }
                }
        }
-       /****FIXME: first UL ****/
+       /**** dectected UL ****/
        // Second release can be just relaxed
        atomic_compare_exchange_strong_explicit(&q->tail,
                        &tail,
@@ -165,7 +165,7 @@ unsigned int dequeue(queue_t *q)
        pointer next;
 
        while (!success) {
-               /****FIXME: detected correctness error ****/
+               /**** detected correctness error ****/
                head = atomic_load_explicit(&q->head, acquire);
                tail = atomic_load_explicit(&q->tail, relaxed);
                /****FIXME: miss ****/
@@ -187,7 +187,7 @@ unsigned int dequeue(queue_t *q)
                                        return 0; // NULL
                                }
                                /****FIXME: miss (not reached) ****/
-                               // Seconde release can be just relaxed
+                               // Second release can be just relaxed
                                bool succ = false;
                                succ = atomic_compare_exchange_strong_explicit(&q->tail,
                                                &tail,