need to fix deque

diff --git a/benchmark/chase-lev-deque-bugfix/deque.c b/benchmark/chase-lev-deque-bugfix/deque.c
index b556460bd5d6fb095c6e623a786d36c0545a641b..2cfbb76a0607a9d743e8e3235fb624ad6fd975a7 100644 (file)
--- a/benchmark/chase-lev-deque-bugfix/deque.c
+++ b/benchmark/chase-lev-deque-bugfix/deque.c
@@ -35,11 +35,7 @@ int take(Deque *q) {
        int x;
        if (t <= b) {
                /* Non-empty queue. */
-               int size = atomic_load_explicit(&a->size, memory_order_relaxed);
-               if (size == 0) 
-                       model_print("take: size == 0\n");
-               // TODO: size can be zero here!!
-               x = atomic_load_explicit(&a->buffer[b % size], memory_order_relaxed);
+               x = atomic_load_explicit(&a->buffer[b % atomic_load_explicit(&a->size,memory_order_relaxed)], memory_order_relaxed);
                /**
                        @Begin
                        @Commit_point_define_check: t != b
@@ -86,10 +82,6 @@ void resize(Deque *q) {
        atomic_store_explicit(&new_a->size, new_size, memory_order_relaxed);
        size_t i;
        for(i=top; i < bottom; i++) {
-               if (new_size == 0)
-                       model_print("resize: new_size == 0\n");
-               if (size == 0)
-                       model_print("resize: size == 0\n");
                atomic_store_explicit(&new_a->buffer[i % new_size], atomic_load_explicit(&a->buffer[i % size], memory_order_relaxed), memory_order_relaxed);
        }
        atomic_store_explicit(&q->array, new_a, memory_order_release);
@@ -110,10 +102,7 @@ void push(Deque *q, int x) {
                //Bug in paper...should have next line...
                a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
        }
-       int size = atomic_load_explicit(&a->size, memory_order_relaxed);
-       if (size == 0) 
-               model_print("push: size == 0\n");
-       atomic_store_explicit(&a->buffer[b % size], x, memory_order_relaxed);
+       atomic_store_explicit(&a->buffer[b % atomic_load_explicit(&a->size, memory_order_relaxed)], x, memory_order_relaxed);
        atomic_thread_fence(memory_order_release);
        /**
                @Begin
@@ -143,10 +132,7 @@ int steal(Deque *q) {
        if (t < b) {
                /* Non-empty queue. */
                Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_acquire);
-               int size = atomic_load_explicit(&a->size, memory_order_relaxed);
-               if (size == 0) 
-                       model_print("steal: size == 0\n");
-               x = atomic_load_explicit(&a->buffer[t % size], memory_order_relaxed);
+               x = atomic_load_explicit(&a->buffer[t % atomic_load_explicit(&a->size, memory_order_relaxed)], memory_order_relaxed);
                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 b046cc7b7cc0d11af1d578be663ff067c39ae60a..fa76d8dc4e7073e52fc72c234430e21c6d219a7c 100644 (file)
--- a/benchmark/chase-lev-deque-bugfix/deque.h
+++ b/benchmark/chase-lev-deque-bugfix/deque.h
@@ -1,11 +1,5 @@
 #ifndef DEQUE_H
 #define DEQUE_H
-#include <spec_lib.h>
-#include <stdlib.h>
-#include <cdsannotate.h>
-#include <specannotation.h>
-#include <model_memory.h>
-#include "common.h"
 
 typedef struct {
        atomic_size_t size;

diff --git a/benchmark/chase-lev-deque-bugfix/main.c b/benchmark/chase-lev-deque-bugfix/main.c
index a67be6efad20e8f81fdf029c1ffe13e8e363a29c..7fb831f3d55d08568ba8db5a986146f173e1de21 100644 (file)
--- a/benchmark/chase-lev-deque-bugfix/main.c
+++ b/benchmark/chase-lev-deque-bugfix/main.c
@@ -13,12 +13,11 @@ int a;
 int b;
 int c;
 
-static void task1(void * param) {
-       a=steal(q);
-}
+static void task(void * param) {
+       // FIXME: Add the following take() will expose an Uninitialzied Load bug...
+       //a=take(q);
 
-static void task2(void * param) {
-       a=take(q);
+       a=steal(q);
 }
 
 int user_main(int argc, char **argv)
@@ -28,17 +27,15 @@ int user_main(int argc, char **argv)
                @Entry_point
                @End
        */
-       thrd_t t1, t2;
+       thrd_t t;
        q=create();
+       thrd_create(&t, task, 0);
        push(q, 1);
        push(q, 2);
-       thrd_create(&t1, task1, 0);
-       thrd_create(&t2, task2, 0);
        push(q, 4);
        b=take(q);
        c=take(q);
-       thrd_join(t1);
-       thrd_join(t2);
+       thrd_join(t);
 
        bool correct=true;
        if (a!=1 && a!=2 && a!=4 && a!= EMPTY)
@@ -51,7 +48,7 @@ int user_main(int argc, char **argv)
                correct=false;
        if (!correct)
                printf("a=%d b=%d c=%d\n",a,b,c);
-       //MODEL_ASSERT(correct);
+       MODEL_ASSERT(correct);
 
        return 0;
 }

diff --git a/benchmark/linuxrwlocks/linuxrwlocks.c b/benchmark/linuxrwlocks/linuxrwlocks.c
index 6341c4c1fcf336474ea9008b5e84b3e083b0968f..0a1a7b203f02f6477623c5ed8f64765ca341a10a 100644 (file)
--- a/benchmark/linuxrwlocks/linuxrwlocks.c
+++ b/benchmark/linuxrwlocks/linuxrwlocks.c
@@ -61,6 +61,11 @@ typedef union {
        @Happens_before:
                # Since commit_point_set has no ID attached, A -> B means that for any B,
                # the previous A happens before B.
+               Read_Unlock -> Read_Lock
+               Read_Unlock -> Write_Lock
+               Read_Unlock -> Write_Trylock(HB_Write_Trylock_Succ)
+               Read_Unlock -> Read_Trylock(HB_Read_Trylock_Succ)
+
                Write_Unlock -> Write_Lock
                Write_Unlock -> Write_Trylock(HB_Write_Trylock_Succ)
 
@@ -202,20 +207,17 @@ static inline int read_trylock(rwlock_t *rw)
        @Interface: Write_Trylock
        @Commit_point_set:
                Write_Trylock_Succ_Point | Write_Trylock_Fail_Point
-       @Condition:
-               !writer_lock_acquired && reader_lock_cnt == 0
        @HB_condition:
                HB_Write_Trylock_Succ :: __RET__ == 1
        @Action:
-               if (__COND_SAT__)
+               if (__RET__ == 1)
                        writer_lock_acquired = true;
-       @Post_check:
-               __COND_SAT__ ? __RET__ == 1 : __RET__ == 0
        @End
 */
 static inline int write_trylock(rwlock_t *rw)
 {
        int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
+       //model_print("write_trylock: priorvalue: %d\n", priorvalue);
        /**
                @Begin
                @Potential_commit_point_define: true

diff --git a/benchmark/mcs-lock/mcs-lock.cc b/benchmark/mcs-lock/mcs-lock.cc
index ec0cc5df9d55c904d3a5cf9a677f42488371a7bb..00817ee65f6ccc6a920527b60f3db4c89c15613b 100644 (file)
--- a/benchmark/mcs-lock/mcs-lock.cc
+++ b/benchmark/mcs-lock/mcs-lock.cc
@@ -13,20 +13,24 @@ void threadA(void *arg)
 {
        mcs_mutex::guard g(mutex);
        printf("store: %d\n", 17);
-       store_32(&shared, 17);
+       //store_32(&shared, 17);
+       shared = 17;
        mutex->unlock(&g);
        mutex->lock(&g);
-       printf("load: %u\n", load_32(&shared));
+       //printf("load: %u\n", load_32(&shared));
+       printf("load: %u\n", shared);
 }
 
 void threadB(void *arg)
 {
        mcs_mutex::guard g(mutex);
-       printf("load: %u\n", load_32(&shared));
+       //printf("load: %u\n", load_32(&shared));
+       printf("load: %u\n", shared);
        mutex->unlock(&g);
        mutex->lock(&g);
        printf("store: %d\n", 17);
-       store_32(&shared, 17);
+       shared = 17;
+       //store_32(&shared, 17);
 }
 
 int user_main(int argc, char **argv)

diff --git a/benchmark/ms-queue/my_queue.c b/benchmark/ms-queue/my_queue.c
index 232e5d839347794a2056a5c0de5c7e17c6d50811..ae8d2b73d2fc221c5f9f8bc7e29c73ad1841f77e 100644 (file)
--- a/benchmark/ms-queue/my_queue.c
+++ b/benchmark/ms-queue/my_queue.c
@@ -22,14 +22,16 @@ static unsigned int new_node()
        int i;
        int t = get_thread_num();
        for (i = 0; i < MAX_FREELIST; i++) {
-               unsigned int node = load_32(&free_lists[t][i]);
+               //unsigned int node = load_32(&free_lists[t][i]);
+               unsigned int node = free_lists[t][i];
                if (node) {
-                       store_32(&free_lists[t][i], 0);
+                       //store_32(&free_lists[t][i], 0);
+                       free_lists[t][i] = 0;
                        return node;
                }
        }
        /* free_list is empty? */
-       MODEL_ASSERT(0);
+       //MODEL_ASSERT(0);
        return 0;
 }
 
@@ -40,20 +42,22 @@ static void reclaim(unsigned int node)
        int t = get_thread_num();
 
        /* Don't reclaim NULL node */
-       MODEL_ASSERT(node);
+       //MODEL_ASSERT(node);
 
        for (i = 0; i < MAX_FREELIST; i++) {
                /* Should never race with our own thread here */
-               unsigned int idx = load_32(&free_lists[t][i]);
+               //unsigned int idx = load_32(&free_lists[t][i]);
+               unsigned int idx = free_lists[t][i];
 
                /* Found empty spot in free list */
                if (idx == 0) {
-                       store_32(&free_lists[t][i], node);
+                       //store_32(&free_lists[t][i], node);
+                       free_lists[t][i] = node;
                        return;
                }
        }
        /* free list is full? */
-       MODEL_ASSERT(0);
+       //MODEL_ASSERT(0);
 }
 
 void init_queue(queue_t *q, int num_threads)
@@ -90,7 +94,8 @@ void enqueue(queue_t *q, unsigned int val)
        pointer tmp;
 
        node = new_node();
-       store_32(&q->nodes[node].value, val);
+       //store_32(&q->nodes[node].value, val);
+       q->nodes[node].value = val;
        tmp = atomic_load_explicit(&q->nodes[node].next, relaxed);
        set_ptr(&tmp, 0); // NULL
        atomic_store_explicit(&q->nodes[node].next, tmp, relaxed);
@@ -101,7 +106,7 @@ void enqueue(queue_t *q, unsigned int val)
                if (tail == atomic_load_explicit(&q->tail, relaxed)) {
 
                        /* Check for uninitialized 'next' */
-                       MODEL_ASSERT(get_ptr(next) != POISON_IDX);
+                       //MODEL_ASSERT(get_ptr(next) != POISON_IDX);
 
                        if (get_ptr(next) == 0) { // == NULL
                                pointer value = MAKE_POINTER(node, get_count(next) + 1);
@@ -151,7 +156,7 @@ unsigned int dequeue(queue_t *q)
                        if (get_ptr(head) == get_ptr(tail)) {
 
                                /* Check for uninitialized 'next' */
-                               MODEL_ASSERT(get_ptr(next) != POISON_IDX);
+                               //MODEL_ASSERT(get_ptr(next) != POISON_IDX);
 
                                if (get_ptr(next) == 0) { // NULL
                                        /**
@@ -168,7 +173,8 @@ unsigned int dequeue(queue_t *q)
                                                release, release);
                                thrd_yield();
                        } else {
-                               value = load_32(&q->nodes[get_ptr(next)].value);
+                               //value = load_32(&q->nodes[get_ptr(next)].value);
+                               value = q->nodes[get_ptr(next)].value;
                                success = atomic_compare_exchange_strong_explicit(&q->head,
                                                &head,
                                                MAKE_POINTER(get_ptr(next), get_count(head) + 1),