From: Peizhao Ou <peizhaoo@uci.edu>
Date: Thu, 20 Mar 2014 00:40:59 +0000 (-0700)
Subject: need to fix deque
X-Git-Url: http://demsky.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 <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 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),