From: Brian Norris Date: Thu, 7 Mar 2013 03:35:26 +0000 (-0800) Subject: Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker-benchmarks X-Git-Tag: oopsla2013-final~27 X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=991978d306af445e74509a0ffef879505b115b94;hp=a33695544b9778b5e13039a10c2f7ba080889760;p=model-checker-benchmarks.git Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker-benchmarks --- diff --git a/Makefile b/Makefile index f97463a..326c00c 100644 --- a/Makefile +++ b/Makefile @@ -1,4 +1,4 @@ -DIRS := barrier mcs-lock mpmc-queue spsc-queue spsc-bugfix linuxrwlocks dekker-fences +DIRS := barrier mcs-lock mpmc-queue spsc-queue spsc-bugfix linuxrwlocks dekker-fences chase-lev-deque .PHONY: $(DIRS) diff --git a/chase-lev-deque/Makefile b/chase-lev-deque/Makefile new file mode 100644 index 0000000..91ff999 --- /dev/null +++ b/chase-lev-deque/Makefile @@ -0,0 +1,17 @@ +include ../benchmarks.mk + +TESTNAME = main + +HEADERS = deque.h +OBJECTS = main.o deque.o + +all: $(TESTNAME) + +$(TESTNAME): $(HEADERS) $(OBJECTS) + $(CC) -o $@ $(OBJECTS) $(CPPFLAGS) $(LDFLAGS) + +%.o: %.c + $(CC) -c -o $@ $< $(CPPFLAGS) + +clean: + rm -f $(TESTNAME) *.o diff --git a/chase-lev-deque/deque.c b/chase-lev-deque/deque.c index efa9b16..b74907f 100644 --- a/chase-lev-deque/deque.c +++ b/chase-lev-deque/deque.c @@ -1,26 +1,28 @@ #include #include +#include "deque.h" +#include -typedef struct { - atomic_size_t size; - atomic_int buffer[]; -} Array; - -typedef struct { - atomic_size_t top, bottom; - atomic_uintptr_t array; /* Atomic(Array *) */ -} Deque; +Deque * create() { + Deque * q = (Deque *) calloc(1, sizeof(Deque)); + Array * a = (Array *) calloc(1, sizeof(Array)+2*sizeof(atomic_int)); + atomic_store_explicit(&q->array, a, memory_order_relaxed); + atomic_store_explicit(&q->top, 0, memory_order_relaxed); + atomic_store_explicit(&q->bottom, 0, memory_order_relaxed); + atomic_store_explicit(&a->size, 2, memory_order_relaxed); + return q; +} int take(Deque *q) { size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed) - 1; - Array *a = atomic_load_explicit(&q->array, memory_order_relaxed); + Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed); atomic_store_explicit(&q->bottom, b, memory_order_relaxed); atomic_thread_fence(memory_order_seq_cst); size_t t = atomic_load_explicit(&q->top, memory_order_relaxed); int x; if (t <= b) { /* Non-empty queue. */ - x = atomic_load_explicit(&a->buffer[b % a->size], memory_order_relaxed); + x = atomic_load_explicit(&a->buffer[b % atomic_load_explicit(&a->size,memory_order_relaxed)], memory_order_relaxed); if (t == b) { /* Single last element in queue. */ if (!atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1, memory_order_seq_cst, memory_order_relaxed)) @@ -35,13 +37,32 @@ int take(Deque *q) { return x; } +void resize(Deque *q) { + Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed); + size_t size=atomic_load_explicit(&a->size, memory_order_relaxed); + size_t new_size=size << 1; + Array *new_a = (Array *) calloc(1, new_size * sizeof(atomic_int) + sizeof(Array)); + size_t top=atomic_load_explicit(&q->top, memory_order_relaxed); + size_t bottom=atomic_load_explicit(&q->bottom, memory_order_relaxed); + atomic_store_explicit(&new_a->size, new_size, memory_order_relaxed); + size_t i; + 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); + } + atomic_store_explicit(&q->array, new_a, memory_order_relaxed); + printf("resize\n"); +} + void push(Deque *q, int x) { size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed); size_t t = atomic_load_explicit(&q->top, memory_order_acquire); - Array *a = atomic_load_explicit(&q->array, memory_order_relaxed); - if (b - t > a->size - 1) /* Full queue. */ + 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. */ { resize(q); - atomic_store_explicit(&a->buffer[b % a->size], x, memory_order_relaxed); + //Bug in paper...should have next line... + a = (Array *) atomic_load_explicit(&q->array, 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); atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed); } @@ -53,8 +74,8 @@ int steal(Deque *q) { int x = EMPTY; if (t < b) { /* Non-empty queue. */ - Array *a = atomic_load_explicit(&q->array, memory_order_relaxed); - x = atomic_load_explicit(&a->buffer[t % a->size], memory_order_relaxed); + Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed); + x = atomic_load_explicit(&a->buffer[t % atomic_load_explicit(&a->size, memory_order_relaxed)], memory_order_relaxed); if (!atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1, memory_order_seq_cst, memory_order_relaxed)) /* Failed race. */ return ABORT; diff --git a/chase-lev-deque/deque.h b/chase-lev-deque/deque.h new file mode 100644 index 0000000..bc670e7 --- /dev/null +++ b/chase-lev-deque/deque.h @@ -0,0 +1,22 @@ +#ifndef DEQUE_H +#define DEQUE_H + +typedef struct { + atomic_size_t size; + atomic_int buffer[]; +} Array; + +typedef struct { + atomic_size_t top, bottom; + atomic_uintptr_t array; /* Atomic(Array *) */ +} Deque; + +Deque * create(); +int take(Deque *q); +void resize(Deque *q); +void push(Deque *q, int x); + +#define EMPTY 0xffffffff +#define ABORT 0xfffffffe + +#endif diff --git a/chase-lev-deque/main.c b/chase-lev-deque/main.c new file mode 100644 index 0000000..424806f --- /dev/null +++ b/chase-lev-deque/main.c @@ -0,0 +1,46 @@ +#include +#include +#include +#include +#include +#include + +#include "model-assert.h" + +#include "deque.h" + +Deque *q; +int a; +int b; +int c; + +static void task(void * param) { + a=steal(q); +} + +int user_main(int argc, char **argv) +{ + thrd_t t; + q=create(); + thrd_create(&t, task, 0); + push(q, 1); + push(q, 2); + push(q, 4); + b=take(q); + c=take(q); + thrd_join(t); + + bool correct=true; + if (a!=1 && a!=2 && a!=4 && a!= EMPTY) + correct=false; + if (b!=1 && b!=2 && b!=4 && b!= EMPTY) + correct=false; + if (c!=1 && c!=2 && c!=4 && a!= EMPTY) + correct=false; + if (a!=EMPTY && b!=EMPTY && c!=EMPTY && (a+b+c)!=7) + correct=false; + if (!correct) + printf("a=%d b=%d c=%d\n",a,b,c); + + return 0; +}