From: Peizhao Ou Date: Thu, 20 Mar 2014 00:40:59 +0000 (-0700) Subject: need to fix deque X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=1d9d47017487cb49f6c592a17667cebdd70a1da4;p=cdsspec-compiler.git need to fix deque --- diff --git a/benchmark/chase-lev-deque-bugfix/deque.c b/benchmark/chase-lev-deque-bugfix/deque.c index b556460..2cfbb76 100644 --- 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 b046cc7..fa76d8d 100644 --- 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 -#include -#include -#include -#include -#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 a67be6e..7fb831f 100644 --- 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 6341c4c..0a1a7b2 100644 --- 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 ec0cc5d..00817ee 100644 --- 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 232e5d8..ae8d2b7 100644 --- 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),