save
authorPeizhao Ou <peizhaoo@uci.edu>
Mon, 24 Mar 2014 02:07:34 +0000 (19:07 -0700)
committerPeizhao Ou <peizhaoo@uci.edu>
Mon, 24 Mar 2014 02:07:34 +0000 (19:07 -0700)
;
;

benchmark/chase-lev-deque-bugfix/deque.c
benchmark/chase-lev-deque-bugfix/deque.h
benchmark/chase-lev-deque-bugfix/main.c
benchmark/cliffc-hashtable/cliffc_hashtable.h
benchmark/mcs-lock/mcs-lock.h
benchmark/mpmc-queue/mpmc-queue.h
benchmark/ms-queue/main.c
benchmark/ms-queue/my_queue.c

index 1ebeb13..9fbc426 100644 (file)
@@ -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);
                /**
index 6bb4698..8a3e857 100644 (file)
@@ -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
index 782539e..1906f1d 100644 (file)
@@ -15,6 +15,7 @@ int c;
 
 static void task(void * param) {
        a=steal(q);
+       a=steal(q);
 }
 
 int user_main(int argc, char **argv)
index ff5d9c3..645531f 100644 (file)
@@ -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
index 4714567..a165437 100644 (file)
@@ -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();
index d482c9e..e6d5485 100644 (file)
@@ -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
index c8d160b..12cf32e 100644 (file)
@@ -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);
        }
 }
 
index 2b90fe5..0d64ed8 100644 (file)
@@ -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,