From 1e4cd56e5cf72f7cb6dddb2990183f050afc4cbc Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Mon, 26 Sep 2016 11:25:19 -0700 Subject: [PATCH] The CDSSpec checker's benchmarks --- Makefile | 7 +- barrier/.gitignore | 1 - barrier/Makefile | 11 - barrier/barrier.cc | 40 - barrier/barrier.h | 36 - benchmarks.mk | 2 +- blocking-mpmc-example/Makefile | 23 + blocking-mpmc-example/example.txt | 39 + blocking-mpmc-example/main.cc | 56 + blocking-mpmc-example/queue.cc | 49 + blocking-mpmc-example/queue.h | 36 + blocking-mpmc-example/testcase1.cc | 86 ++ blocking-mpmc-example/testcase2.cc | 88 ++ blocking-mpmc-example/testcase3.cc | 88 ++ blocking-mpmc-example/testcase4.cc | 89 ++ chase-lev-deque-bugfix/Makefile | 22 +- chase-lev-deque-bugfix/deque.c | 111 +- chase-lev-deque-bugfix/deque.h | 17 + chase-lev-deque-bugfix/main.c | 8 +- chase-lev-deque-bugfix/testcase1.c | 74 + chase-lev-deque-bugfix/testcase2.c | 56 + chase-lev-deque-bugfix/testcase3.c | 62 + chase-lev-deque-bugfix/testcase4.c | 54 + chase-lev-deque-bugfix/testcase5.c | 55 + chase-lev-deque-bugfix/testcase6.c | 55 + cliffc-hashtable/Makefile | 11 - cliffc-hashtable/NonBlockingHashMap.java | 1292 ----------------- cliffc-hashtable/cliffc_hashtable.h | 970 ------------- cliffc-hashtable/main.cc | 104 -- concurrent-hashmap/Makefile | 27 +- concurrent-hashmap/hashmap.cc | 125 ++ concurrent-hashmap/hashmap.h | 247 +--- concurrent-hashmap/main.cc | 60 +- concurrent-hashmap/note.txt | 7 + concurrent-hashmap/result1.txt | 9 - concurrent-hashmap/result2.txt | 11 - concurrent-hashmap/testcase1.cc | 53 +- concurrent-hashmap/testcase2.cc | 57 +- concurrent-hashmap/testcase3.cc | 81 -- count-lines.sh | 32 + dekker-fences/.gitignore | 1 - dekker-fences/Makefile | 11 - dekker-fences/dekker-fences.cc | 91 -- elimination-backoff/stack.c | 95 -- elimination-backoff/stack.h | 16 - generate.sh | 9 + include/unrelacy.h | 11 +- linuxrwlocks/Makefile | 22 +- linuxrwlocks/linuxrwlocks.c | 125 +- linuxrwlocks/linuxrwlocks.h | 34 + linuxrwlocks/main.c | 45 + linuxrwlocks/testcase1.c | 72 + linuxrwlocks/testcase2.c | 54 + linuxrwlocks/testcase3.c | 55 + mcs-lock/Makefile | 22 +- mcs-lock/main.cc | 47 + mcs-lock/mcs-lock.cc | 117 +- mcs-lock/mcs-lock.h | 82 +- mcs-lock/testcase.cc | 47 + mpmc-queue/Makefile | 29 +- mpmc-queue/main.cc | 60 + mpmc-queue/mpmc-queue.cc | 200 ++- mpmc-queue/mpmc-queue.h | 85 +- mpmc-queue/testcase1.cc | 58 + mpmc-queue/testcase2.cc | 69 + ms-queue-loose/Makefile | 23 + ms-queue-loose/main.c | 86 ++ ms-queue/my_queue.c => ms-queue-loose/queue.c | 68 +- .../my_stack.h => ms-queue-loose/queue.h | 24 +- ms-queue-loose/testcase1.c | 92 ++ ms-queue-loose/testcase2.c | 101 ++ ms-queue-loose/testcase3.c | 100 ++ ms-queue-loose/testcase4.c | 90 ++ ms-queue/.gitignore | 9 +- ms-queue/Makefile | 24 +- ms-queue/main.c | 35 +- ms-queue/queue.c | 207 +++ ms-queue/{my_queue.h => queue.h} | 12 +- ms-queue/testcase1.c | 92 ++ ms-queue/testcase2.c | 101 ++ ms-queue/testcase3.c | 100 ++ ms-queue/testcase4.c | 90 ++ read-copy-update/Makefile | 23 + read-copy-update/main.cc | 42 + read-copy-update/rcu.cc | 42 + read-copy-update/rcu.h | 25 + read-copy-update/testcase.cc | 42 + seqlock/Makefile | 21 +- seqlock/main.cc | 33 + seqlock/seqlock.c | 75 - seqlock/seqlock.cc | 85 ++ seqlock/seqlock.h | 25 + seqlock/testcase1.cc | 33 + seqlock/testcase2.cc | 33 + spsc-bugfix/Makefile | 30 +- spsc-bugfix/eventcount.h | 5 + .../spsc-queue.cc => spsc-bugfix/main.cc | 22 +- spsc-bugfix/queue.cc | 62 + spsc-bugfix/queue.h | 56 +- spsc-bugfix/{ => relacy}/eventcount-relacy.h | 0 spsc-bugfix/{ => relacy}/queue-relacy.h | 0 spsc-bugfix/{ => relacy}/spsc-relacy.cc | 0 spsc-bugfix/{spsc-queue.cc => testcase1.cc} | 22 +- spsc-queue/.gitignore | 2 - spsc-queue/Makefile | 23 - spsc-queue/eventcount-relacy.h | 64 - spsc-queue/eventcount.h | 69 - spsc-queue/queue-relacy.h | 74 - spsc-queue/queue.h | 77 - spsc-queue/spsc-relacy.cc | 27 - ticket-lock/Makefile | 23 + ticket-lock/lock.c | 48 + ticket-lock/lock.h | 19 + ticket-lock/main.c | 39 + ticket-lock/testcase1.c | 39 + treiber-stack/Makefile | 10 - treiber-stack/main.c | 89 -- treiber-stack/my_stack.c | 123 -- 118 files changed, 4082 insertions(+), 4282 deletions(-) delete mode 100644 barrier/.gitignore delete mode 100644 barrier/Makefile delete mode 100644 barrier/barrier.cc delete mode 100644 barrier/barrier.h create mode 100644 blocking-mpmc-example/Makefile create mode 100644 blocking-mpmc-example/example.txt create mode 100644 blocking-mpmc-example/main.cc create mode 100644 blocking-mpmc-example/queue.cc create mode 100644 blocking-mpmc-example/queue.h create mode 100644 blocking-mpmc-example/testcase1.cc create mode 100644 blocking-mpmc-example/testcase2.cc create mode 100644 blocking-mpmc-example/testcase3.cc create mode 100644 blocking-mpmc-example/testcase4.cc create mode 100644 chase-lev-deque-bugfix/testcase1.c create mode 100644 chase-lev-deque-bugfix/testcase2.c create mode 100644 chase-lev-deque-bugfix/testcase3.c create mode 100644 chase-lev-deque-bugfix/testcase4.c create mode 100644 chase-lev-deque-bugfix/testcase5.c create mode 100644 chase-lev-deque-bugfix/testcase6.c delete mode 100644 cliffc-hashtable/Makefile delete mode 100644 cliffc-hashtable/NonBlockingHashMap.java delete mode 100644 cliffc-hashtable/cliffc_hashtable.h delete mode 100644 cliffc-hashtable/main.cc create mode 100644 concurrent-hashmap/hashmap.cc delete mode 100644 concurrent-hashmap/result1.txt delete mode 100644 concurrent-hashmap/result2.txt delete mode 100644 concurrent-hashmap/testcase3.cc create mode 100755 count-lines.sh delete mode 100644 dekker-fences/.gitignore delete mode 100644 dekker-fences/Makefile delete mode 100644 dekker-fences/dekker-fences.cc delete mode 100644 elimination-backoff/stack.c delete mode 100644 elimination-backoff/stack.h create mode 100755 generate.sh create mode 100644 linuxrwlocks/linuxrwlocks.h create mode 100644 linuxrwlocks/main.c create mode 100644 linuxrwlocks/testcase1.c create mode 100644 linuxrwlocks/testcase2.c create mode 100644 linuxrwlocks/testcase3.c create mode 100644 mcs-lock/main.cc create mode 100644 mcs-lock/testcase.cc create mode 100644 mpmc-queue/main.cc create mode 100644 mpmc-queue/testcase1.cc create mode 100644 mpmc-queue/testcase2.cc create mode 100644 ms-queue-loose/Makefile create mode 100644 ms-queue-loose/main.c rename ms-queue/my_queue.c => ms-queue-loose/queue.c (60%) rename treiber-stack/my_stack.h => ms-queue-loose/queue.h (71%) create mode 100644 ms-queue-loose/testcase1.c create mode 100644 ms-queue-loose/testcase2.c create mode 100644 ms-queue-loose/testcase3.c create mode 100644 ms-queue-loose/testcase4.c create mode 100644 ms-queue/queue.c rename ms-queue/{my_queue.h => queue.h} (80%) create mode 100644 ms-queue/testcase1.c create mode 100644 ms-queue/testcase2.c create mode 100644 ms-queue/testcase3.c create mode 100644 ms-queue/testcase4.c create mode 100644 read-copy-update/Makefile create mode 100644 read-copy-update/main.cc create mode 100644 read-copy-update/rcu.cc create mode 100644 read-copy-update/rcu.h create mode 100644 read-copy-update/testcase.cc create mode 100644 seqlock/main.cc delete mode 100644 seqlock/seqlock.c create mode 100644 seqlock/seqlock.cc create mode 100644 seqlock/seqlock.h create mode 100644 seqlock/testcase1.cc create mode 100644 seqlock/testcase2.cc rename spsc-queue/spsc-queue.cc => spsc-bugfix/main.cc (66%) create mode 100644 spsc-bugfix/queue.cc rename spsc-bugfix/{ => relacy}/eventcount-relacy.h (100%) rename spsc-bugfix/{ => relacy}/queue-relacy.h (100%) rename spsc-bugfix/{ => relacy}/spsc-relacy.cc (100%) rename spsc-bugfix/{spsc-queue.cc => testcase1.cc} (66%) delete mode 100644 spsc-queue/.gitignore delete mode 100644 spsc-queue/Makefile delete mode 100644 spsc-queue/eventcount-relacy.h delete mode 100644 spsc-queue/eventcount.h delete mode 100644 spsc-queue/queue-relacy.h delete mode 100644 spsc-queue/queue.h delete mode 100644 spsc-queue/spsc-relacy.cc create mode 100644 ticket-lock/Makefile create mode 100644 ticket-lock/lock.c create mode 100644 ticket-lock/lock.h create mode 100644 ticket-lock/main.c create mode 100644 ticket-lock/testcase1.c delete mode 100644 treiber-stack/Makefile delete mode 100644 treiber-stack/main.c delete mode 100644 treiber-stack/my_stack.c diff --git a/Makefile b/Makefile index 003ac10..7471656 100644 --- a/Makefile +++ b/Makefile @@ -1,6 +1,7 @@ -DIRS := barrier mcs-lock mpmc-queue spsc-queue spsc-bugfix linuxrwlocks \ - dekker-fences chase-lev-deque ms-queue chase-lev-deque-bugfix seqlock \ - treiber-stack cliffc-hashtable concurrent-hashmap +DIRS := register-acqrel register-relaxed ms-queue linuxrwlocks mcs-lock \ + chase-lev-deque-bugfix treiber-stack ticket-lock seqlock read-copy-update \ + concurrent-hashmap spsc-bugfix mpmc-queue barrier \ + chase-lev-deque-bugfix-loose ms-queue-loose blocking-mpmc-example .PHONY: $(DIRS) diff --git a/barrier/.gitignore b/barrier/.gitignore deleted file mode 100644 index dc2a8be..0000000 --- a/barrier/.gitignore +++ /dev/null @@ -1 +0,0 @@ -/barrier diff --git a/barrier/Makefile b/barrier/Makefile deleted file mode 100644 index 22df223..0000000 --- a/barrier/Makefile +++ /dev/null @@ -1,11 +0,0 @@ -include ../benchmarks.mk - -TESTNAME = barrier - -all: $(TESTNAME) - -$(TESTNAME): $(TESTNAME).cc $(TESTNAME).h - $(CXX) -o $@ $< $(CXXFLAGS) $(LDFLAGS) - -clean: - rm -f $(TESTNAME) *.o diff --git a/barrier/barrier.cc b/barrier/barrier.cc deleted file mode 100644 index 5c99f65..0000000 --- a/barrier/barrier.cc +++ /dev/null @@ -1,40 +0,0 @@ -#include -#include - -#include "barrier.h" - -#include "librace.h" - -spinning_barrier *barr; -int var = 0; - -void threadA(void *arg) -{ - store_32(&var, 1); - barr->wait(); -} - -void threadB(void *arg) -{ - barr->wait(); - printf("var = %d\n", load_32(&var)); -} - -#define NUMREADERS 1 -int user_main(int argc, char **argv) -{ - thrd_t A, B[NUMREADERS]; - int i; - - barr = new spinning_barrier(NUMREADERS + 1); - - thrd_create(&A, &threadA, NULL); - for (i = 0; i < NUMREADERS; i++) - thrd_create(&B[i], &threadB, NULL); - - for (i = 0; i < NUMREADERS; i++) - thrd_join(B[i]); - thrd_join(A); - - return 0; -} diff --git a/barrier/barrier.h b/barrier/barrier.h deleted file mode 100644 index dd5d39c..0000000 --- a/barrier/barrier.h +++ /dev/null @@ -1,36 +0,0 @@ -#include - -class spinning_barrier { - public: - spinning_barrier (unsigned int n) : n_ (n) { - nwait_ = 0; - step_ = 0; - } - - bool wait() { - unsigned int step = step_.load (); - - if (nwait_.fetch_add (1) == n_ - 1) { - /* OK, last thread to come. */ - nwait_.store (0); // XXX: maybe can use relaxed ordering here ?? - step_.fetch_add (1); - return true; - } else { - /* Run in circles and scream like a little girl. */ - while (step_.load () == step) - thrd_yield(); - return false; - } - } - - protected: - /* Number of synchronized threads. */ - const unsigned int n_; - - /* Number of threads currently spinning. */ - std::atomic nwait_; - - /* Number of barrier syncronizations completed so far, - * * it's OK to wrap. */ - std::atomic step_; -}; diff --git a/benchmarks.mk b/benchmarks.mk index 7f82f92..aa5329d 100644 --- a/benchmarks.mk +++ b/benchmarks.mk @@ -12,7 +12,7 @@ BASE = ../.. INCLUDE = -I$(BASE)/include -I../include # C preprocessor flags -CPPFLAGS += $(INCLUDE) -g +CPPFLAGS += $(INCLUDE) # C++ compiler flags CXXFLAGS += $(CPPFLAGS) diff --git a/blocking-mpmc-example/Makefile b/blocking-mpmc-example/Makefile new file mode 100644 index 0000000..8dd491a --- /dev/null +++ b/blocking-mpmc-example/Makefile @@ -0,0 +1,23 @@ +include ../benchmarks.mk + +BENCH := queue + +BENCH_BINARY := $(BENCH).o + +TESTS := main testcase1 testcase2 testcase3 testcase4 + +all: $(TESTS) + ../generate.sh $(notdir $(shell pwd)) + +%.o : %.c + $(CXX) -c -fPIC -MMD -MF .$@.d -o $@ $< $(CXXFLAGS) $(LDFLAGS) + +$(TESTS): % : %.o $(BENCH_BINARY) + $(CXX) -o $@ $^ $(CXXFLAGS) $(LDFLAGS) + +-include .*.d + +clean: + rm -rf $(TESTS) *.o .*.d *.dSYM + +.PHONY: clean all diff --git a/blocking-mpmc-example/example.txt b/blocking-mpmc-example/example.txt new file mode 100644 index 0000000..dd9a83c --- /dev/null +++ b/blocking-mpmc-example/example.txt @@ -0,0 +1,39 @@ +class Queue { +/** @DeclareState: IntList *q; +@Commutativity:enq<->deq(true) +@Commutativity:deq<->deq(!M1->RET||!M2->RET) */ +public: atomic tail, head; +Queue() { tail = head = new Node(); } +/** @Transition: STATE(q)->push_back(val); */ +void Queue::enq(unsigned int val) { + Node *n = new Node(val); + while(true) { + Node *t = tail.load(acquire); + Node *next = t->next.load(relaxed); + if(next) continue; + if(t->next.CAS(next, n, relaxed)) { + /** @OPDefine: true */ + tail.store(n, release); + return; + } + } +} +/**@PreCondition: +return RET ? !STATE(q)->empty() + && STATE(q)->front() == RET : true; +@Transition: if (RET) { + if (STATE(q)->empty()) return false; + STATE(q)->pop_front(); +} */ +unsigned int Queue::deq() { + while(true) { + Node *h = head.load(acquire); + Node *t = tail.load(acquire); + Node *next = h->next.load(relaxed); + /** @OPClearDefine: true */ + if(h == t) return 0; + if(head.CAS(h, next, release)) + return next->data; + } +} +}; diff --git a/blocking-mpmc-example/main.cc b/blocking-mpmc-example/main.cc new file mode 100644 index 0000000..9b3a6af --- /dev/null +++ b/blocking-mpmc-example/main.cc @@ -0,0 +1,56 @@ +#include +#include +#include +#include "queue.h" + +static int procs = 3; +Queue *q; + +int idx1, idx2; +unsigned int a, b; + + +atomic_int x[3]; + +static void main_task(void *param) +{ + unsigned int val; + int pid = *((int *)param); + if (pid % 3 == 0) { + enq(q, 2); + } else if (pid % 3 == 1) { + deq(q); + } else if (pid % 3 == 2) { + deq(q); + } +} + +int user_main(int argc, char **argv) +{ + int i; + int *param; + + atomic_init(&x[1], 0); + atomic_init(&x[2], 0); + + /** @Entry */ + q = new Queue; + + int num_threads = 3; + + param = new int[num_threads]; + thrd_t *threads = new thrd_t[num_threads]; + + for (i = 0; i < num_threads; i++) { + param[i] = i; + thrd_create(&threads[i], main_task, ¶m[i]); + } + for (i = 0; i < num_threads; i++) + thrd_join(threads[i]); + + delete param; + delete threads; + delete q; + + return 0; +} diff --git a/blocking-mpmc-example/queue.cc b/blocking-mpmc-example/queue.cc new file mode 100644 index 0000000..f86547b --- /dev/null +++ b/blocking-mpmc-example/queue.cc @@ -0,0 +1,49 @@ +#include "queue.h" + +// Make them C-callable interfaces + +/** @DeclareState: IntList *q; +@Commutativity: enq <-> deq (true) +@Commutativity: deq <-> deq (M1->C_RET!=-1||M2->C_RET!=-1) */ + +void Queue::enq(int val) { + Node *n = new Node(val); + while(true) { + Node *t = tail.load(acquire); + Node *next = t->next.load(relaxed); + if(next) continue; + if(t->next.CAS(next, n, relaxed)) { + /** @OPDefine: true */ + tail.store(n, release); + return; + } + } +} +int Queue::deq() { + while(true) { + Node *h = head.load(acquire); + Node *t = tail.load(acquire); + Node *next = h->next.load(relaxed); + /** @OPClearDefine: true */ + if(h == t) return -1; + if(head.CAS(h, next, release)) + return next->data; + } +} + +/** @Transition: STATE(q)->push_back(val); */ +void enq(Queue *q, int val) { + q->enq(val); +} + +/** @Transition: +S_RET = STATE(q)->empty() ? -1 : STATE(q)->front(); +if (S_RET != -1) + STATE(q)->pop_front(); +@PostCondition: + return C_RET == -1 ? true : C_RET == S_RET; +@JustifyingPostcondition: if (C_RET == -1) + return S_RET == -1; */ +int deq(Queue *q) { + return q->deq(); +} diff --git a/blocking-mpmc-example/queue.h b/blocking-mpmc-example/queue.h new file mode 100644 index 0000000..e7d1515 --- /dev/null +++ b/blocking-mpmc-example/queue.h @@ -0,0 +1,36 @@ +#ifndef _QUEUE_H +#define _QUEUE_H +#include +#include "unrelacy.h" + +#define CAS compare_exchange_strong +using namespace std; + +typedef struct Node { + int data; + atomic next; + + Node() { + data = 0; + next.store(NULL, relaxed); + } + + Node(int d) { + data = d; + next.store(NULL, relaxed); + } +} Node; + +class Queue { +public: atomic tail, head; +Queue() { tail = head = new Node(); } +void enq(int val); +int deq(); +}; + +// Make them C-callable interfaces +void enq(Queue *q, int val); + +int deq(Queue *s); + +#endif diff --git a/blocking-mpmc-example/testcase1.cc b/blocking-mpmc-example/testcase1.cc new file mode 100644 index 0000000..3851988 --- /dev/null +++ b/blocking-mpmc-example/testcase1.cc @@ -0,0 +1,86 @@ +#include +#include +#include + +#include "queue.h" +#include "model-assert.h" + +static Queue *queue; +static thrd_t *threads; +static unsigned int *input; +static unsigned int *output; +static int num_threads; + +int get_thread_num() +{ + thrd_t curr = thrd_current(); + int i; + for (i = 0; i < num_threads; i++) + if (curr.priv == threads[i].priv) + return i; + MODEL_ASSERT(0); + return -1; +} + +bool succ1, succ2; +atomic_int x[3]; +int idx1, idx2; +unsigned int reclaimNode; + +static int procs = 2; +static void main_task(void *param) +{ + unsigned int val; + int pid = *((int *)param); + if (pid % procs == 0) { + enq(queue, 1); + } else if (pid % procs == 1) { + succ1 = deq(queue); + } +} + +int user_main(int argc, char **argv) +{ + int i; + int *param; + unsigned int in_sum = 0, out_sum = 0; + + /** @Entry */ + queue = new Queue; + MODEL_ASSERT(queue); + + num_threads = procs; + threads = (thrd_t*) malloc(num_threads * sizeof(thrd_t)); + param = (int*) malloc(num_threads * sizeof(*param)); + input = (unsigned int *) calloc(num_threads, sizeof(*input)); + output = (unsigned int *) calloc(num_threads, sizeof(*output)); + + atomic_init(&x[0], 0); + atomic_init(&x[1], 0); + atomic_init(&x[2], 0); + queue = new Queue; + for (i = 0; i < num_threads; i++) { + param[i] = i; + thrd_create(&threads[i], main_task, ¶m[i]); + } + for (i = 0; i < num_threads; i++) + thrd_join(threads[i]); +/* + for (i = 0; i < num_threads; i++) { + in_sum += input[i]; + out_sum += output[i]; + } + for (i = 0; i < num_threads; i++) + printf("input[%d] = %u\n", i, input[i]); + for (i = 0; i < num_threads; i++) + printf("output[%d] = %u\n", i, output[i]); + if (succ1 && succ2) + MODEL_ASSERT(in_sum == out_sum); + else + MODEL_ASSERT (false); +*/ + free(param); + free(threads); + + return 0; +} diff --git a/blocking-mpmc-example/testcase2.cc b/blocking-mpmc-example/testcase2.cc new file mode 100644 index 0000000..1e66c2e --- /dev/null +++ b/blocking-mpmc-example/testcase2.cc @@ -0,0 +1,88 @@ +#include +#include +#include + +#include "queue.h" +#include "model-assert.h" + +static Queue *queue; +static thrd_t *threads; +static unsigned int *input; +static unsigned int *output; +static int num_threads; + +int get_thread_num() +{ + thrd_t curr = thrd_current(); + int i; + for (i = 0; i < num_threads; i++) + if (curr.priv == threads[i].priv) + return i; + MODEL_ASSERT(0); + return -1; +} + +bool succ1, succ2; +atomic_int x[3]; +int idx1, idx2; +unsigned int reclaimNode; + +static int procs = 3; +static void main_task(void *param) +{ + unsigned int val; + int pid = *((int *)param); + if (pid % procs == 0) { + enq(queue, 1); + } else if (pid % procs == 1) { + enq(queue, 2); + } else if (pid % procs == 2) { + succ1 = deq(queue); + } +} + +int user_main(int argc, char **argv) +{ + int i; + int *param; + unsigned int in_sum = 0, out_sum = 0; + + /** @Entry */ + queue = new Queue; + MODEL_ASSERT(queue); + + num_threads = procs; + threads = (thrd_t*) malloc(num_threads * sizeof(thrd_t)); + param = (int*) malloc(num_threads * sizeof(*param)); + input = (unsigned int *) calloc(num_threads, sizeof(*input)); + output = (unsigned int *) calloc(num_threads, sizeof(*output)); + + atomic_init(&x[0], 0); + atomic_init(&x[1], 0); + atomic_init(&x[2], 0); + queue = new Queue; + for (i = 0; i < num_threads; i++) { + param[i] = i; + thrd_create(&threads[i], main_task, ¶m[i]); + } + for (i = 0; i < num_threads; i++) + thrd_join(threads[i]); +/* + for (i = 0; i < num_threads; i++) { + in_sum += input[i]; + out_sum += output[i]; + } + for (i = 0; i < num_threads; i++) + printf("input[%d] = %u\n", i, input[i]); + for (i = 0; i < num_threads; i++) + printf("output[%d] = %u\n", i, output[i]); + if (succ1 && succ2) + MODEL_ASSERT(in_sum == out_sum); + else + MODEL_ASSERT (false); +*/ + free(param); + free(threads); + + return 0; +} diff --git a/blocking-mpmc-example/testcase3.cc b/blocking-mpmc-example/testcase3.cc new file mode 100644 index 0000000..5a2bbbe --- /dev/null +++ b/blocking-mpmc-example/testcase3.cc @@ -0,0 +1,88 @@ +#include +#include +#include + +#include "queue.h" +#include "model-assert.h" + +static Queue *queue; +static thrd_t *threads; +static unsigned int *input; +static unsigned int *output; +static int num_threads; + +int get_thread_num() +{ + thrd_t curr = thrd_current(); + int i; + for (i = 0; i < num_threads; i++) + if (curr.priv == threads[i].priv) + return i; + MODEL_ASSERT(0); + return -1; +} + +bool succ1, succ2; +atomic_int x[3]; +int idx1, idx2; +unsigned int reclaimNode; + +static int procs = 2; +static void main_task(void *param) +{ + unsigned int val; + int pid = *((int *)param); + if (pid % procs == 0) { + enq(queue, 1); + succ1 = deq(queue); + } else if (pid % procs == 1) { + enq(queue, 2); + succ2 = deq(queue); + } +} + +int user_main(int argc, char **argv) +{ + int i; + int *param; + unsigned int in_sum = 0, out_sum = 0; + + /** @Entry */ + queue = new Queue; + MODEL_ASSERT(queue); + + num_threads = procs; + threads = (thrd_t*) malloc(num_threads * sizeof(thrd_t)); + param = (int*) malloc(num_threads * sizeof(*param)); + input = (unsigned int *) calloc(num_threads, sizeof(*input)); + output = (unsigned int *) calloc(num_threads, sizeof(*output)); + + atomic_init(&x[0], 0); + atomic_init(&x[1], 0); + atomic_init(&x[2], 0); + queue = new Queue; + for (i = 0; i < num_threads; i++) { + param[i] = i; + thrd_create(&threads[i], main_task, ¶m[i]); + } + for (i = 0; i < num_threads; i++) + thrd_join(threads[i]); +/* + for (i = 0; i < num_threads; i++) { + in_sum += input[i]; + out_sum += output[i]; + } + for (i = 0; i < num_threads; i++) + printf("input[%d] = %u\n", i, input[i]); + for (i = 0; i < num_threads; i++) + printf("output[%d] = %u\n", i, output[i]); + if (succ1 && succ2) + MODEL_ASSERT(in_sum == out_sum); + else + MODEL_ASSERT (false); +*/ + free(param); + free(threads); + + return 0; +} diff --git a/blocking-mpmc-example/testcase4.cc b/blocking-mpmc-example/testcase4.cc new file mode 100644 index 0000000..fbb0cea --- /dev/null +++ b/blocking-mpmc-example/testcase4.cc @@ -0,0 +1,89 @@ +#include +#include +#include + +#include "queue.h" +#include "model-assert.h" + +static Queue *queue; +static thrd_t *threads; +static unsigned int *input; +static unsigned int *output; +static int num_threads; + +int get_thread_num() +{ + thrd_t curr = thrd_current(); + int i; + for (i = 0; i < num_threads; i++) + if (curr.priv == threads[i].priv) + return i; + //MODEL_ASSERT(0); + return -1; +} + +bool succ1, succ2; +atomic_int x[3]; +int idx1, idx2, idx3; +unsigned int reclaimNode; + +static int procs = 2; +static void main_task(void *param) +{ + unsigned int val; + int pid = *((int *)param); + if (pid % procs == 0) { + enq(queue, 1); + succ1 = deq(queue); + enq(queue, 2); + } else if (pid % procs == 1) { + enq(queue, 2); + succ2 = deq(queue); + } +} + +int user_main(int argc, char **argv) +{ + int i; + int *param; + unsigned int in_sum = 0, out_sum = 0; + + /** @Entry */ + queue = new Queue; + MODEL_ASSERT(queue); + + num_threads = procs; + threads = (thrd_t*) malloc(num_threads * sizeof(thrd_t)); + param = (int*) malloc(num_threads * sizeof(*param)); + input = (unsigned int *) calloc(num_threads, sizeof(*input)); + output = (unsigned int *) calloc(num_threads, sizeof(*output)); + + atomic_init(&x[0], 0); + atomic_init(&x[1], 0); + atomic_init(&x[2], 0); + queue = new Queue; + for (i = 0; i < num_threads; i++) { + param[i] = i; + thrd_create(&threads[i], main_task, ¶m[i]); + } + for (i = 0; i < num_threads; i++) + thrd_join(threads[i]); +/* + for (i = 0; i < num_threads; i++) { + in_sum += input[i]; + out_sum += output[i]; + } + for (i = 0; i < num_threads; i++) + printf("input[%d] = %u\n", i, input[i]); + for (i = 0; i < num_threads; i++) + printf("output[%d] = %u\n", i, output[i]); + if (succ1 && succ2) + MODEL_ASSERT(in_sum == out_sum); + else + MODEL_ASSERT (false); +*/ + free(param); + free(threads); + + return 0; +} diff --git a/chase-lev-deque-bugfix/Makefile b/chase-lev-deque-bugfix/Makefile index 91ff999..dca2e81 100644 --- a/chase-lev-deque-bugfix/Makefile +++ b/chase-lev-deque-bugfix/Makefile @@ -1,17 +1,23 @@ include ../benchmarks.mk -TESTNAME = main +BENCH := deque -HEADERS = deque.h -OBJECTS = main.o deque.o +BENCH_BINARY := $(BENCH).o -all: $(TESTNAME) +TESTS := main testcase1 testcase2 testcase3 testcase4 testcase5 testcase6 -$(TESTNAME): $(HEADERS) $(OBJECTS) - $(CC) -o $@ $(OBJECTS) $(CPPFLAGS) $(LDFLAGS) +all: $(TESTS) + ../generate.sh $(notdir $(shell pwd)) %.o: %.c - $(CC) -c -o $@ $< $(CPPFLAGS) + $(CC) -c -fPIC -MMD -MF .$@.d -o $@ $< $(CFLAGS) $(LDFLAGS) + +$(TESTS): %: %.o $(BENCH_BINARY) + $(CC) -o $@ $^ $(CFLAGS) $(LDFLAGS) + +-include .*.d clean: - rm -f $(TESTNAME) *.o + rm -rf $(TESTS) *.o .*.d *.dSYM + +.PHONY: clean all diff --git a/chase-lev-deque-bugfix/deque.c b/chase-lev-deque-bugfix/deque.c index 6328446..b851e51 100644 --- a/chase-lev-deque-bugfix/deque.c +++ b/chase-lev-deque-bugfix/deque.c @@ -1,9 +1,27 @@ -#include -#include #include "deque.h" #include #include +/** @Define: + bool succ(int res) { return res != EMPTY && res != ABORT; } + bool fail(int res) { return !succ(res); } */ + +/** @DeclareState: IntList *deque; + @Initial: deque = new IntList; + @Commutativity: push <-> push (true) + @Commutativity: push <-> take (true) + @Commutativity: take <-> take (true) */ + +Deque * create_size(int size) { + Deque * q = (Deque *) calloc(1, sizeof(Deque)); + Array * a = (Array *) calloc(1, sizeof(Array)+size*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, size, memory_order_relaxed); + return q; +} + Deque * create() { Deque * q = (Deque *) calloc(1, sizeof(Deque)); Array * a = (Array *) calloc(1, sizeof(Array)+2*sizeof(atomic_int)); @@ -14,27 +32,72 @@ Deque * create() { return q; } +/** + Note: + 1. The expected way to use the deque is that we have a main thread where we + call push() and take(); and then we have other stealing threads that only + call steal(). + 2. Bottom stores the index that push() is ready to update on; Top stores the + index that steal() is ready to read from. + 3. take() greedly decreases the bottom, and then later check whether it is + going to take the last element; If so, it will race with the corresponding + stealing threads. + XXX: + 4. In this implementation, there are two places where we update the Top: a) + take() racing the last element and steal() consumes an element. We need to + have seq_cst for all the updates because we need to have a total SC order + between them such that the SC fences in take() and steal() can prevent the + load of Top right after the fence in take() will read the update-to-date + value. + 5. Note that the steal() really can bail any time since it never retries!!! + +*/ + + +/** @PreCondition: return succ(C_RET) ? !STATE(deque)->empty() && + STATE(deque)->back() == C_RET : true; + @JustifyingPrecondition: if (!succ(C_RET) && !STATE(deque)->empty()) { + // Make sure there are concurrent stealers who take those items + ForEach (item, STATE(deque)) + if (!HasItem(CONCURRENT, Guard(EQ(NAME, "steal") && C_RET(steal) == item))) + return false; + } + @Transition: if (succ(C_RET)) { + if (STATE(deque)->empty()) return false; + STATE(deque)->pop_back(); + } */ int take(Deque *q) { + // take() greedly decrease the Bottom, then check later 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 (testcase2) **********/ 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 % atomic_load_explicit(&a->size,memory_order_relaxed)], memory_order_relaxed); + int sz = atomic_load_explicit(&a->size,memory_order_relaxed); + // Reads the buffer value before racing + x = atomic_load_explicit(&a->buffer[b % sz], 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)) + // FIXME: This might not be necessary!!! We don't know yet + if (!atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1, + memory_order_relaxed, memory_order_relaxed)) { /* Failed race. */ x = EMPTY; + } + // Restore the Bottom atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed); } } else { /* Empty queue. */ x = EMPTY; + // Restore the Bottom atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed); } + // Make sure we have one ordering point (push <-> take) when it's empty + /** @OPClearDefine: true */ return x; } @@ -47,39 +110,73 @@ void resize(Deque *q) { 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; + + // XXX: Initialize the whole new array to turn off the CDSChecker UL error + // Check if CDSSpec checker can catch this bug + /* + for(i=0; i < new_size; i++) { + atomic_store_explicit(&new_a->buffer[i % new_size], atomic_load_explicit(&a->buffer[i % size], memory_order_relaxed), memory_order_relaxed); + } + */ + 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); } + + /********** Detected UL **********/ atomic_store_explicit(&q->array, new_a, memory_order_release); printf("resize\n"); } +/** @Transition: STATE(deque)->push_back(x); */ void push(Deque *q, int x) { size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed); + /********** Detected Correctness (testcase1 -x1000) **********/ 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. */ { resize(q); + /********** Also Detected (testcase1) **********/ //Bug in paper...should have next line... a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed); } + // Update the buffer (this is the ordering point) atomic_store_explicit(&a->buffer[b % atomic_load_explicit(&a->size, memory_order_relaxed)], x, memory_order_relaxed); + /** @OPDefine: true */ + /********** Detected UL (testcase1) **********/ atomic_thread_fence(memory_order_release); atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed); } +/** @PreCondition: return succ(C_RET) ? !STATE(deque)->empty() && + STATE(deque)->front() == C_RET : true; + @Transition: if (succ(C_RET)) { + if (STATE(deque)->empty()) return false; + STATE(deque)->pop_front(); + } */ int steal(Deque *q) { - size_t t = atomic_load_explicit(&q->top, memory_order_acquire); + // XXX: The following load should be just relaxed (cause it's followed by an + // SC fence (discussed in AutoMO) + size_t t = atomic_load_explicit(&q->top, memory_order_relaxed); + /********** Detected Correctness (testcase2) **********/ atomic_thread_fence(memory_order_seq_cst); + /********** Detected UL (testcase1 -x100) **********/ size_t b = atomic_load_explicit(&q->bottom, memory_order_acquire); int x = EMPTY; if (t < b) { /* Non-empty queue. */ + /********** Detected UL (testcase1 -x100) **********/ Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_acquire); - 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)) + int sz = atomic_load_explicit(&a->size, memory_order_relaxed); + x = atomic_load_explicit(&a->buffer[t % sz], memory_order_relaxed); + /********** Detected Correctness (testcase1 -x1000) **********/ + bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1, + memory_order_seq_cst, memory_order_relaxed); + /** @OPDefine: true */ + if (!succ) { /* Failed race. */ return ABORT; + } } return x; } diff --git a/chase-lev-deque-bugfix/deque.h b/chase-lev-deque-bugfix/deque.h index f474355..b61f8c7 100644 --- a/chase-lev-deque-bugfix/deque.h +++ b/chase-lev-deque-bugfix/deque.h @@ -1,6 +1,9 @@ #ifndef DEQUE_H #define DEQUE_H +#include +#include + typedef struct { atomic_size_t size; atomic_int buffer[]; @@ -11,6 +14,7 @@ typedef struct { atomic_uintptr_t array; /* Atomic(Array *) */ } Deque; +Deque * create_size(int size); Deque * create(); int take(Deque *q); void resize(Deque *q); @@ -20,4 +24,17 @@ int steal(Deque *q); #define EMPTY 0xffffffff #define ABORT 0xfffffffe +/** @Define: +#ifdef __cplusplus +extern "C" { +#endif + +bool succ(int res); +bool fail(int res); + +#ifdef __cplusplus +}; +#endif +*/ + #endif diff --git a/chase-lev-deque-bugfix/main.c b/chase-lev-deque-bugfix/main.c index f2e8dca..792f08b 100644 --- a/chase-lev-deque-bugfix/main.c +++ b/chase-lev-deque-bugfix/main.c @@ -19,16 +19,17 @@ static void task(void * param) { int user_main(int argc, char **argv) { + /** @Entry */ thrd_t t; q=create(); thrd_create(&t, task, 0); push(q, 1); push(q, 2); - push(q, 4); + push(q, 3); b=take(q); c=take(q); thrd_join(t); - +/* bool correct=true; if (a!=1 && a!=2 && a!=4 && a!= EMPTY) correct=false; @@ -40,7 +41,8 @@ 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/chase-lev-deque-bugfix/testcase1.c b/chase-lev-deque-bugfix/testcase1.c new file mode 100644 index 0000000..246d96b --- /dev/null +++ b/chase-lev-deque-bugfix/testcase1.c @@ -0,0 +1,74 @@ +#include +#include +#include +#include +#include + +#include "model-assert.h" + +#include "deque.h" + +Deque *q; +int a; +int b; +int c; +int x; + +static void task(void * param) { + a=steal(q); + if (a == ABORT) { + printf("Steal NULL\n"); + } else { + printf("Steal %d\n", a); + } + + x=steal(q); + if (x == ABORT) { + printf("Steal NULL\n"); + } else { + printf("Steal %d\n", x); + } +} + +int user_main(int argc, char **argv) +{ + /** @Entry */ + thrd_t t; + q=create(); + thrd_create(&t, task, 0); + push(q, 1); + printf("Push 1\n"); + push(q, 2); + printf("Push 2\n"); + push(q, 4); + printf("Push 4\n"); + b=take(q); + if (b == EMPTY) { + printf("Take NULL\n"); + } else { + printf("Take %d\n", b); + } + c=take(q); + if (c == EMPTY) { + printf("Take NULL\n"); + } else { + printf("Take %d\n", c); + } + 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); + */ + //MODEL_ASSERT(correct); + + return 0; +} diff --git a/chase-lev-deque-bugfix/testcase2.c b/chase-lev-deque-bugfix/testcase2.c new file mode 100644 index 0000000..fa5fbf8 --- /dev/null +++ b/chase-lev-deque-bugfix/testcase2.c @@ -0,0 +1,56 @@ +#include +#include +#include +#include +#include + +#include "model-assert.h" + +#include "deque.h" + +Deque *q; +int a; +int b; +int c; + +/** Making CAS in steal() (w39) SC */ + +static void task(void * param) { + b=steal(q); + c=steal(q); + printf("steal: b=%d, c=%d\n", b, c); +} + +int user_main(int argc, char **argv) +{ + thrd_t t1, t2; + q=create_size(16); + /** @Entry */ + + push(q, 1); + thrd_create(&t1, task, 0); + push(q, 2); + a=take(q); + printf("take: a=%d\n", a); + thrd_join(t1); + + int d =take(q); + bool correct= b == 1 && c == 2 && a == 2 ; + //MODEL_ASSERT(!correct); +/* + 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); + MODEL_ASSERT(correct); + */ + + return 0; +} diff --git a/chase-lev-deque-bugfix/testcase3.c b/chase-lev-deque-bugfix/testcase3.c new file mode 100644 index 0000000..15cbd4e --- /dev/null +++ b/chase-lev-deque-bugfix/testcase3.c @@ -0,0 +1,62 @@ +#include +#include +#include +#include +#include + +#include "model-assert.h" + +#include "deque.h" + +Deque *q; +int a; +int b; +int c; + +/** Making CAS in steal() (w39) SC */ + +static void task1(void * param) { + b=steal(q); + printf("steal: b=%d\n", b); +} + +static void task2(void * param) { + c=steal(q); + printf("steal: c=%d\n", c); +} + +int user_main(int argc, char **argv) +{ + thrd_t t1, t2; + q=create(); + /** @Entry */ + + push(q, 1); + thrd_create(&t1, task1, 0); + thrd_create(&t2, task2, 0); + push(q, 2); + a=take(q); + printf("take: a=%d\n", a); + thrd_join(t1); + thrd_join(t2); + + int d =take(q); + bool correct= b == 1 && c == 2 && a == 2 ; + MODEL_ASSERT(!correct); +/* + 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); + MODEL_ASSERT(correct); + */ + + return 0; +} diff --git a/chase-lev-deque-bugfix/testcase4.c b/chase-lev-deque-bugfix/testcase4.c new file mode 100644 index 0000000..060c5f8 --- /dev/null +++ b/chase-lev-deque-bugfix/testcase4.c @@ -0,0 +1,54 @@ +#include +#include +#include +#include +#include + +#include "model-assert.h" + +#include "deque.h" + +Deque *q; +int a; +int b; +int c; + +/** Making CAS in steal() (w39) SC */ + +static void task(void * param) { + b=steal(q); + printf("steal: b=%d\n", b); +} + +int user_main(int argc, char **argv) +{ + thrd_t t1, t2; + q=create(); + /** @Entry */ + + push(q, 1); + thrd_create(&t1, task, 0); + a=take(q); + printf("take: a=%d\n", a); + thrd_join(t1); + + int d =take(q); + bool correct= b == 1 && c == 2 && a == 2 ; + MODEL_ASSERT(!correct); +/* + 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); + MODEL_ASSERT(correct); + */ + + return 0; +} diff --git a/chase-lev-deque-bugfix/testcase5.c b/chase-lev-deque-bugfix/testcase5.c new file mode 100644 index 0000000..f9552a7 --- /dev/null +++ b/chase-lev-deque-bugfix/testcase5.c @@ -0,0 +1,55 @@ +#include +#include +#include +#include +#include + +#include "model-assert.h" + +#include "deque.h" + +Deque *q; +int a; +int b; +int c; + +/** Making CAS in steal() (w39) SC */ + +static void task(void * param) { + steal(q); + steal(q); +} + +int user_main(int argc, char **argv) +{ + thrd_t t1, t2; + q=create(); + /** @Entry */ + + push(q, 1); + push(q, 2); + thrd_create(&t1, task, 0); + a=take(q); + printf("take: a=%d\n", a); + thrd_join(t1); + + int d =take(q); + bool correct= b == 1 && c == 2 && a == 2 ; + MODEL_ASSERT(!correct); +/* + 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); + MODEL_ASSERT(correct); + */ + + return 0; +} diff --git a/chase-lev-deque-bugfix/testcase6.c b/chase-lev-deque-bugfix/testcase6.c new file mode 100644 index 0000000..e2b3451 --- /dev/null +++ b/chase-lev-deque-bugfix/testcase6.c @@ -0,0 +1,55 @@ +#include +#include +#include +#include +#include + +#include "model-assert.h" + +#include "deque.h" + +Deque *q; +int a; +int b; +int c; + +/** Making CAS in steal() (w39) SC */ + +static void task(void * param) { + steal(q); +} + +int user_main(int argc, char **argv) +{ + thrd_t t1, t2; + q=create(); + /** @Entry */ + + push(q, 1); + push(q, 2); + thrd_create(&t1, task, 0); + take(q); + take(q); + printf("take: a=%d\n", a); + thrd_join(t1); + + int d =take(q); + bool correct= b == 1 && c == 2 && a == 2 ; + MODEL_ASSERT(!correct); +/* + 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); + MODEL_ASSERT(correct); + */ + + return 0; +} diff --git a/cliffc-hashtable/Makefile b/cliffc-hashtable/Makefile deleted file mode 100644 index f1e5227..0000000 --- a/cliffc-hashtable/Makefile +++ /dev/null @@ -1,11 +0,0 @@ -include ../benchmarks.mk - -TESTS := table - -all: $(TESTS) - -table: main.cc - $(CXX) -o $@ $^ $(SPEC_OBJ) $(CXXFLAGS) -std=c++0x $(LDFLAGS) - -clean: - rm -f *.o *.d $(TESTS) diff --git a/cliffc-hashtable/NonBlockingHashMap.java b/cliffc-hashtable/NonBlockingHashMap.java deleted file mode 100644 index 5995e48..0000000 --- a/cliffc-hashtable/NonBlockingHashMap.java +++ /dev/null @@ -1,1292 +0,0 @@ -/* - * Written by Cliff Click and released to the public domain, as explained at - * http://creativecommons.org/licenses/publicdomain - */ - -package org.cliffc.high_scale_lib; -import java.io.IOException; -import java.io.Serializable; -import java.lang.reflect.Field; -import java.util.*; -import java.util.concurrent.ConcurrentMap; -import java.util.concurrent.atomic.*; -import sun.misc.Unsafe; - -/** - * A lock-free alternate implementation of {@link java.util.concurrent.ConcurrentHashMap} - * with better scaling properties and generally lower costs to mutate the Map. - * It provides identical correctness properties as ConcurrentHashMap. All - * operations are non-blocking and multi-thread safe, including all update - * operations. {@link NonBlockingHashMap} scales substatially better than - * {@link java.util.concurrent.ConcurrentHashMap} for high update rates, even with a - * large concurrency factor. Scaling is linear up to 768 CPUs on a 768-CPU - * Azul box, even with 100% updates or 100% reads or any fraction in-between. - * Linear scaling up to all cpus has been observed on a 32-way Sun US2 box, - * 32-way Sun Niagra box, 8-way Intel box and a 4-way Power box. - * - * This class obeys the same functional specification as {@link - * java.util.Hashtable}, and includes versions of methods corresponding to - * each method of Hashtable. However, even though all operations are - * thread-safe, operations do not entail locking and there is - * not any support for locking the entire table in a way that - * prevents all access. This class is fully interoperable with - * Hashtable in programs that rely on its thread safety but not on - * its synchronization details. - * - *

Operations (including put) generally do not block, so may - * overlap with other update operations (including other puts and - * removes). Retrievals reflect the results of the most recently - * completed update operations holding upon their onset. For - * aggregate operations such as putAll, concurrent retrievals may - * reflect insertion or removal of only some entries. Similarly, Iterators - * and Enumerations return elements reflecting the state of the hash table at - * some point at or since the creation of the iterator/enumeration. They do - * not throw {@link ConcurrentModificationException}. However, - * iterators are designed to be used by only one thread at a time. - * - *

Very full tables, or tables with high reprobe rates may trigger an - * internal resize operation to move into a larger table. Resizing is not - * terribly expensive, but it is not free either; during resize operations - * table throughput may drop somewhat. All threads that visit the table - * during a resize will 'help' the resizing but will still be allowed to - * complete their operation before the resize is finished (i.e., a simple - * 'get' operation on a million-entry table undergoing resizing will not need - * to block until the entire million entries are copied). - * - *

This class and its views and iterators implement all of the - * optional methods of the {@link Map} and {@link Iterator} - * interfaces. - * - *

Like {@link Hashtable} but unlike {@link HashMap}, this class - * does not allow null to be used as a key or value. - * - * - * @since 1.5 - * @author Cliff Click - * @param the type of keys maintained by this map - * @param the type of mapped values - * - * @version 1.1.2 - * @author Prashant Deva - moved hash() function out of get_impl() so it is - * not calculated multiple times. - */ - -public class NonBlockingHashMap - extends AbstractMap - implements ConcurrentMap, Cloneable, Serializable { - - private static final long serialVersionUID = 1234123412341234123L; - - private static final int REPROBE_LIMIT=10; // Too many reprobes then force a table-resize - - // --- Bits to allow Unsafe access to arrays - private static final Unsafe _unsafe = UtilUnsafe.getUnsafe(); - private static final int _Obase = _unsafe.arrayBaseOffset(Object[].class); - private static final int _Oscale = _unsafe.arrayIndexScale(Object[].class); - private static long rawIndex(final Object[] ary, final int idx) { - assert idx >= 0 && idx < ary.length; - return _Obase + idx * _Oscale; - } - - // --- Setup to use Unsafe - private static final long _kvs_offset; - static { // - Field f = null; - try { f = NonBlockingHashMap.class.getDeclaredField("_kvs"); } - catch( java.lang.NoSuchFieldException e ) { throw new RuntimeException(e); } - _kvs_offset = _unsafe.objectFieldOffset(f); - } - private final boolean CAS_kvs( final Object[] oldkvs, final Object[] newkvs ) { - return _unsafe.compareAndSwapObject(this, _kvs_offset, oldkvs, newkvs ); - } - - // --- Adding a 'prime' bit onto Values via wrapping with a junk wrapper class - private static final class Prime { - final Object _V; - Prime( Object V ) { _V = V; } - static Object unbox( Object V ) { return V instanceof Prime ? ((Prime)V)._V : V; } - } - - // --- hash ---------------------------------------------------------------- - // Helper function to spread lousy hashCodes - private static final int hash(final Object key) { - int h = key.hashCode(); // The real hashCode call - // Spread bits to regularize both segment and index locations, - // using variant of single-word Wang/Jenkins hash. - h += (h << 15) ^ 0xffffcd7d; - h ^= (h >>> 10); - h += (h << 3); - h ^= (h >>> 6); - h += (h << 2) + (h << 14); - return h ^ (h >>> 16); - } - - // --- The Hash Table -------------------- - // Slot 0 is always used for a 'CHM' entry below to hold the interesting - // bits of the hash table. Slot 1 holds full hashes as an array of ints. - // Slots {2,3}, {4,5}, etc hold {Key,Value} pairs. The entire hash table - // can be atomically replaced by CASing the _kvs field. - // - // Why is CHM buried inside the _kvs Object array, instead of the other way - // around? The CHM info is used during resize events and updates, but not - // during standard 'get' operations. I assume 'get' is much more frequent - // than 'put'. 'get' can skip the extra indirection of skipping through the - // CHM to reach the _kvs array. - private transient Object[] _kvs; - private static final CHM chm (Object[] kvs) { return (CHM )kvs[0]; } - private static final int[] hashes(Object[] kvs) { return (int[])kvs[1]; } - // Number of K,V pairs in the table - private static final int len(Object[] kvs) { return (kvs.length-2)>>1; } - - // Time since last resize - private transient long _last_resize_milli; - - // --- Minimum table size ---------------- - // Pick size 8 K/V pairs, which turns into (8*2+2)*4+12 = 84 bytes on a - // standard 32-bit HotSpot, and (8*2+2)*8+12 = 156 bytes on 64-bit Azul. - private static final int MIN_SIZE_LOG=3; // - private static final int MIN_SIZE=(1<>2); - } - - // --- NonBlockingHashMap -------------------------------------------------- - // Constructors - - /** Create a new NonBlockingHashMap with default minimum size (currently set - * to 8 K/V pairs or roughly 84 bytes on a standard 32-bit JVM). */ - public NonBlockingHashMap( ) { this(MIN_SIZE); } - - /** Create a new NonBlockingHashMap with initial room for the given number of - * elements, thus avoiding internal resizing operations to reach an - * appropriate size. Large numbers here when used with a small count of - * elements will sacrifice space for a small amount of time gained. The - * initial size will be rounded up internally to the next larger power of 2. */ - public NonBlockingHashMap( final int initial_sz ) { initialize(initial_sz); } - private final void initialize( int initial_sz ) { - if( initial_sz < 0 ) throw new IllegalArgumentException(); - int i; // Convert to next largest power-of-2 - if( initial_sz > 1024*1024 ) initial_sz = 1024*1024; - for( i=MIN_SIZE_LOG; (1<size() == 0. - * @return size() == 0 */ - @Override - public boolean isEmpty ( ) { return size() == 0; } - - /** Tests if the key in the table using the equals method. - * @return true if the key is in the table using the equals method - * @throws NullPointerException if the specified key is null */ - @Override - public boolean containsKey( Object key ) { return get(key) != null; } - - /** Legacy method testing if some key maps into the specified value in this - * table. This method is identical in functionality to {@link - * #containsValue}, and exists solely to ensure full compatibility with - * class {@link java.util.Hashtable}, which supported this method prior to - * introduction of the Java Collections framework. - * @param val a value to search for - * @return true if this map maps one or more keys to the specified value - * @throws NullPointerException if the specified value is null */ - public boolean contains ( Object val ) { return containsValue(val); } - - /** Maps the specified key to the specified value in the table. Neither key - * nor value can be null. - *

The value can be retrieved by calling {@link #get} with a key that is - * equal to the original key. - * @param key key with which the specified value is to be associated - * @param val value to be associated with the specified key - * @return the previous value associated with key, or - * null if there was no mapping for key - * @throws NullPointerException if the specified key or value is null */ - @Override - public TypeV put ( TypeK key, TypeV val ) { return putIfMatch( key, val, NO_MATCH_OLD); } - - /** Atomically, do a {@link #put} if-and-only-if the key is not mapped. - * Useful to ensure that only a single mapping for the key exists, even if - * many threads are trying to create the mapping in parallel. - * @return the previous value associated with the specified key, - * or null if there was no mapping for the key - * @throws NullPointerException if the specified key or value is null */ - public TypeV putIfAbsent( TypeK key, TypeV val ) { return putIfMatch( key, val, TOMBSTONE ); } - - /** Removes the key (and its corresponding value) from this map. - * This method does nothing if the key is not in the map. - * @return the previous value associated with key, or - * null if there was no mapping for key - * @throws NullPointerException if the specified key is null */ - @Override - public TypeV remove ( Object key ) { return putIfMatch( key,TOMBSTONE, NO_MATCH_OLD); } - - /** Atomically do a {@link #remove(Object)} if-and-only-if the key is mapped - * to a value which is equals to the given value. - * @throws NullPointerException if the specified key or value is null */ - public boolean remove ( Object key,Object val ) { return putIfMatch( key,TOMBSTONE, val ) == val; } - - /** Atomically do a put(key,val) if-and-only-if the key is - * mapped to some value already. - * @throws NullPointerException if the specified key or value is null */ - public TypeV replace ( TypeK key, TypeV val ) { return putIfMatch( key, val,MATCH_ANY ); } - - /** Atomically do a put(key,newValue) if-and-only-if the key is - * mapped a value which is equals to oldValue. - * @throws NullPointerException if the specified key or value is null */ - public boolean replace ( TypeK key, TypeV oldValue, TypeV newValue ) { - return putIfMatch( key, newValue, oldValue ) == oldValue; - } - - private final TypeV putIfMatch( Object key, Object newVal, Object oldVal ) { - if (oldVal == null || newVal == null) throw new NullPointerException(); - final Object res = putIfMatch( this, _kvs, key, newVal, oldVal ); - assert !(res instanceof Prime); - assert res != null; - return res == TOMBSTONE ? null : (TypeV)res; - } - - - /** Copies all of the mappings from the specified map to this one, replacing - * any existing mappings. - * @param m mappings to be stored in this map */ - @Override - public void putAll(Map m) { - for (Map.Entry e : m.entrySet()) - put(e.getKey(), e.getValue()); - } - - /** Removes all of the mappings from this map. */ - @Override - public void clear() { // Smack a new empty table down - Object[] newkvs = new NonBlockingHashMap(MIN_SIZE)._kvs; - while( !CAS_kvs(_kvs,newkvs) ) // Spin until the clear works - ; - } - - /** Returns true if this Map maps one or more keys to the specified - * value. Note: This method requires a full internal traversal of the - * hash table and is much slower than {@link #containsKey}. - * @param val value whose presence in this map is to be tested - * @return true if this map maps one or more keys to the specified value - * @throws NullPointerException if the specified value is null */ - @Override - public boolean containsValue( final Object val ) { - if( val == null ) throw new NullPointerException(); - for( TypeV V : values() ) - if( V == val || V.equals(val) ) - return true; - return false; - } - - // This function is supposed to do something for Hashtable, and the JCK - // tests hang until it gets called... by somebody ... for some reason, - // any reason.... - protected void rehash() { - } - - /** - * Creates a shallow copy of this hashtable. All the structure of the - * hashtable itself is copied, but the keys and values are not cloned. - * This is a relatively expensive operation. - * - * @return a clone of the hashtable. - */ - @Override - public Object clone() { - try { - // Must clone, to get the class right; NBHM might have been - // extended so it would be wrong to just make a new NBHM. - NonBlockingHashMap t = (NonBlockingHashMap) super.clone(); - // But I don't have an atomic clone operation - the underlying _kvs - // structure is undergoing rapid change. If I just clone the _kvs - // field, the CHM in _kvs[0] won't be in sync. - // - // Wipe out the cloned array (it was shallow anyways). - t.clear(); - // Now copy sanely - for( TypeK K : keySet() ) { - final TypeV V = get(K); // Do an official 'get' - t.put(K,V); - } - return t; - } catch (CloneNotSupportedException e) { - // this shouldn't happen, since we are Cloneable - throw new InternalError(); - } - } - - /** - * Returns a string representation of this map. The string representation - * consists of a list of key-value mappings in the order returned by the - * map's entrySet view's iterator, enclosed in braces - * ("{}"). Adjacent mappings are separated by the characters - * ", " (comma and space). Each key-value mapping is rendered as - * the key followed by an equals sign ("=") followed by the - * associated value. Keys and values are converted to strings as by - * {@link String#valueOf(Object)}. - * - * @return a string representation of this map - */ - @Override - public String toString() { - Iterator> i = entrySet().iterator(); - if( !i.hasNext()) - return "{}"; - - StringBuilder sb = new StringBuilder(); - sb.append('{'); - for (;;) { - Entry e = i.next(); - TypeK key = e.getKey(); - TypeV value = e.getValue(); - sb.append(key == this ? "(this Map)" : key); - sb.append('='); - sb.append(value == this ? "(this Map)" : value); - if( !i.hasNext()) - return sb.append('}').toString(); - sb.append(", "); - } - } - - // --- keyeq --------------------------------------------------------------- - // Check for key equality. Try direct pointer compare first, then see if - // the hashes are unequal (fast negative test) and finally do the full-on - // 'equals' v-call. - private static boolean keyeq( Object K, Object key, int[] hashes, int hash, int fullhash ) { - return - K==key || // Either keys match exactly OR - // hash exists and matches? hash can be zero during the install of a - // new key/value pair. - ((hashes[hash] == 0 || hashes[hash] == fullhash) && - // Do not call the users' "equals()" call with a Tombstone, as this can - // surprise poorly written "equals()" calls that throw exceptions - // instead of simply returning false. - K != TOMBSTONE && // Do not call users' equals call with a Tombstone - // Do the match the hard way - with the users' key being the loop- - // invariant "this" pointer. I could have flipped the order of - // operands (since equals is commutative), but I'm making mega-morphic - // v-calls in a reprobing loop and nailing down the 'this' argument - // gives both the JIT and the hardware a chance to prefetch the call target. - key.equals(K)); // Finally do the hard match - } - - // --- get ----------------------------------------------------------------- - /** Returns the value to which the specified key is mapped, or {@code null} - * if this map contains no mapping for the key. - *

More formally, if this map contains a mapping from a key {@code k} to - * a value {@code v} such that {@code key.equals(k)}, then this method - * returns {@code v}; otherwise it returns {@code null}. (There can be at - * most one such mapping.) - * @throws NullPointerException if the specified key is null */ - // Never returns a Prime nor a Tombstone. - @Override - public TypeV get( Object key ) { - final int fullhash= hash (key); // throws NullPointerException if key is null - final Object V = get_impl(this,_kvs,key,fullhash); - assert !(V instanceof Prime); // Never return a Prime - return (TypeV)V; - } - - private static final Object get_impl( final NonBlockingHashMap topmap, final Object[] kvs, final Object key, final int fullhash ) { - final int len = len (kvs); // Count of key/value pairs, reads kvs.length - final CHM chm = chm (kvs); // The CHM, for a volatile read below; reads slot 0 of kvs - final int[] hashes=hashes(kvs); // The memoized hashes; reads slot 1 of kvs - - int idx = fullhash & (len-1); // First key hash - - // Main spin/reprobe loop, looking for a Key hit - int reprobe_cnt=0; - while( true ) { - // Probe table. Each read of 'val' probably misses in cache in a big - // table; hopefully the read of 'key' then hits in cache. - final Object K = key(kvs,idx); // Get key before volatile read, could be null - final Object V = val(kvs,idx); // Get value before volatile read, could be null or Tombstone or Prime - if( K == null ) return null; // A clear miss - - // We need a volatile-read here to preserve happens-before semantics on - // newly inserted Keys. If the Key body was written just before inserting - // into the table a Key-compare here might read the uninitalized Key body. - // Annoyingly this means we have to volatile-read before EACH key compare. - // . - // We also need a volatile-read between reading a newly inserted Value - // and returning the Value (so the user might end up reading the stale - // Value contents). Same problem as with keys - and the one volatile - // read covers both. - final Object[] newkvs = chm._newkvs; // VOLATILE READ before key compare - - // Key-compare - if( keyeq(K,key,hashes,idx,fullhash) ) { - // Key hit! Check for no table-copy-in-progress - if( !(V instanceof Prime) ) // No copy? - return (V == TOMBSTONE) ? null : V; // Return the value - // Key hit - but slot is (possibly partially) copied to the new table. - // Finish the copy & retry in the new table. - return get_impl(topmap,chm.copy_slot_and_check(topmap,kvs,idx,key),key,fullhash); // Retry in the new table - } - // get and put must have the same key lookup logic! But only 'put' - // needs to force a table-resize for a too-long key-reprobe sequence. - // Check for too-many-reprobes on get - and flip to the new table. - // ???? Why a TOMBSTONE key means no more keys in this table - // because a TOMBSTONE key should be null before - if( ++reprobe_cnt >= reprobe_limit(len) || // too many probes - key == TOMBSTONE ) // found a TOMBSTONE key, means no more keys in this table - return newkvs == null ? null : get_impl(topmap,topmap.help_copy(newkvs),key,fullhash); // Retry in the new table - - idx = (idx+1)&(len-1); // Reprobe by 1! (could now prefetch) - } - } - - // --- putIfMatch --------------------------------------------------------- - // Put, Remove, PutIfAbsent, etc. Return the old value. If the returned - // value is equal to expVal (or expVal is NO_MATCH_OLD) then the put can be - // assumed to work (although might have been immediately overwritten). Only - // the path through copy_slot passes in an expected value of null, and - // putIfMatch only returns a null if passed in an expected null. - private static final Object putIfMatch( final NonBlockingHashMap topmap, final Object[] kvs, final Object key, final Object putval, final Object expVal ) { - assert putval != null; - assert !(putval instanceof Prime); - assert !(expVal instanceof Prime); - final int fullhash = hash (key); // throws NullPointerException if key null - final int len = len (kvs); // Count of key/value pairs, reads kvs.length - final CHM chm = chm (kvs); // Reads kvs[0] - final int[] hashes = hashes(kvs); // Reads kvs[1], read before kvs[0] - int idx = fullhash & (len-1); - - // --- - // Key-Claim stanza: spin till we can claim a Key (or force a resizing). - int reprobe_cnt=0; - Object K=null, V=null; - Object[] newkvs=null; - while( true ) { // Spin till we get a Key slot - V = val(kvs,idx); // Get old value (before volatile read below!) - K = key(kvs,idx); // Get current key - if( K == null ) { // Slot is free? - // Found an empty Key slot - which means this Key has never been in - // this table. No need to put a Tombstone - the Key is not here! - if( putval == TOMBSTONE ) return putval; // Not-now & never-been in this table - // Claim the null key-slot - if( CAS_key(kvs,idx, null, key ) ) { // Claim slot for Key - chm._slots.add(1); // Raise key-slots-used count - hashes[idx] = fullhash; // Memoize fullhash - break; // Got it! - } - // CAS to claim the key-slot failed. - // - // This re-read of the Key points out an annoying short-coming of Java - // CAS. Most hardware CAS's report back the existing value - so that - // if you fail you have a *witness* - the value which caused the CAS - // to fail. The Java API turns this into a boolean destroying the - // witness. Re-reading does not recover the witness because another - // thread can write over the memory after the CAS. Hence we can be in - // the unfortunate situation of having a CAS fail *for cause* but - // having that cause removed by a later store. This turns a - // non-spurious-failure CAS (such as Azul has) into one that can - // apparently spuriously fail - and we avoid apparent spurious failure - // by not allowing Keys to ever change. - K = key(kvs,idx); // CAS failed, get updated value - assert K != null; // If keys[idx] is null, CAS shoulda worked - } - // Key slot was not null, there exists a Key here - - // We need a volatile-read here to preserve happens-before semantics on - // newly inserted Keys. If the Key body was written just before inserting - // into the table a Key-compare here might read the uninitalized Key body. - // Annoyingly this means we have to volatile-read before EACH key compare. - newkvs = chm._newkvs; // VOLATILE READ before key compare - - if( keyeq(K,key,hashes,idx,fullhash) ) - break; // Got it! - - // get and put must have the same key lookup logic! Lest 'get' give - // up looking too soon. - //topmap._reprobes.add(1); - if( ++reprobe_cnt >= reprobe_limit(len) || // too many probes or - key == TOMBSTONE ) { // found a TOMBSTONE key, means no more keys - // We simply must have a new table to do a 'put'. At this point a - // 'get' will also go to the new table (if any). We do not need - // to claim a key slot (indeed, we cannot find a free one to claim!). - newkvs = chm.resize(topmap,kvs); - if( expVal != null ) topmap.help_copy(newkvs); // help along an existing copy - return putIfMatch(topmap,newkvs,key,putval,expVal); - } - - idx = (idx+1)&(len-1); // Reprobe! - } // End of spinning till we get a Key slot - - // --- - // Found the proper Key slot, now update the matching Value slot. We - // never put a null, so Value slots monotonically move from null to - // not-null (deleted Values use Tombstone). Thus if 'V' is null we - // fail this fast cutout and fall into the check for table-full. - if( putval == V ) return V; // Fast cutout for no-change - - // See if we want to move to a new table (to avoid high average re-probe - // counts). We only check on the initial set of a Value from null to - // not-null (i.e., once per key-insert). Of course we got a 'free' check - // of newkvs once per key-compare (not really free, but paid-for by the - // time we get here). - if( newkvs == null && // New table-copy already spotted? - // Once per fresh key-insert check the hard way - ((V == null && chm.tableFull(reprobe_cnt,len)) || - // Or we found a Prime, but the JMM allowed reordering such that we - // did not spot the new table (very rare race here: the writing - // thread did a CAS of _newkvs then a store of a Prime. This thread - // reads the Prime, then reads _newkvs - but the read of Prime was so - // delayed (or the read of _newkvs was so accelerated) that they - // swapped and we still read a null _newkvs. The resize call below - // will do a CAS on _newkvs forcing the read. - V instanceof Prime) ) - newkvs = chm.resize(topmap,kvs); // Force the new table copy to start - // See if we are moving to a new table. - // If so, copy our slot and retry in the new table. - if( newkvs != null ) - return putIfMatch(topmap,chm.copy_slot_and_check(topmap,kvs,idx,expVal),key,putval,expVal); - - // --- - // We are finally prepared to update the existing table - while( true ) { - assert !(V instanceof Prime); - - // Must match old, and we do not? Then bail out now. Note that either V - // or expVal might be TOMBSTONE. Also V can be null, if we've never - // inserted a value before. expVal can be null if we are called from - // copy_slot. - - if( expVal != NO_MATCH_OLD && // Do we care about expected-Value at all? - V != expVal && // No instant match already? - (expVal != MATCH_ANY || V == TOMBSTONE || V == null) && - !(V==null && expVal == TOMBSTONE) && // Match on null/TOMBSTONE combo - (expVal == null || !expVal.equals(V)) ) // Expensive equals check at the last - return V; // Do not update! - - // Actually change the Value in the Key,Value pair - if( CAS_val(kvs, idx, V, putval ) ) { - // CAS succeeded - we did the update! - // Both normal put's and table-copy calls putIfMatch, but table-copy - // does not (effectively) increase the number of live k/v pairs. - if( expVal != null ) { - // Adjust sizes - a striped counter - if( (V == null || V == TOMBSTONE) && putval != TOMBSTONE ) chm._size.add( 1); - if( !(V == null || V == TOMBSTONE) && putval == TOMBSTONE ) chm._size.add(-1); - } - return (V==null && expVal!=null) ? TOMBSTONE : V; - } - // Else CAS failed - V = val(kvs,idx); // Get new value - // If a Prime'd value got installed, we need to re-run the put on the - // new table. Otherwise we lost the CAS to another racing put. - // Simply retry from the start. - if( V instanceof Prime ) - return putIfMatch(topmap,chm.copy_slot_and_check(topmap,kvs,idx,expVal),key,putval,expVal); - } - } - - // --- help_copy --------------------------------------------------------- - // Help along an existing resize operation. This is just a fast cut-out - // wrapper, to encourage inlining for the fast no-copy-in-progress case. We - // always help the top-most table copy, even if there are nested table - // copies in progress. - private final Object[] help_copy( Object[] helper ) { - // Read the top-level KVS only once. We'll try to help this copy along, - // even if it gets promoted out from under us (i.e., the copy completes - // and another KVS becomes the top-level copy). - Object[] topkvs = _kvs; - CHM topchm = chm(topkvs); - if( topchm._newkvs == null ) return helper; // No copy in-progress - topchm.help_copy_impl(this,topkvs,false); - return helper; - } - - - // --- CHM ----------------------------------------------------------------- - // The control structure for the NonBlockingHashMap - private static final class CHM { - // Size in active K,V pairs - private final Counter _size; - public int size () { return (int)_size.get(); } - - // --- - // These next 2 fields are used in the resizing heuristics, to judge when - // it is time to resize or copy the table. Slots is a count of used-up - // key slots, and when it nears a large fraction of the table we probably - // end up reprobing too much. Last-resize-milli is the time since the - // last resize; if we are running back-to-back resizes without growing - // (because there are only a few live keys but many slots full of dead - // keys) then we need a larger table to cut down on the churn. - - // Count of used slots, to tell when table is full of dead unusable slots - private final Counter _slots; - public int slots() { return (int)_slots.get(); } - - // --- - // New mappings, used during resizing. - // The 'new KVs' array - created during a resize operation. This - // represents the new table being copied from the old one. It's the - // volatile variable that is read as we cross from one table to the next, - // to get the required memory orderings. It monotonically transits from - // null to set (once). - volatile Object[] _newkvs; - private final AtomicReferenceFieldUpdater _newkvsUpdater = - AtomicReferenceFieldUpdater.newUpdater(CHM.class,Object[].class, "_newkvs"); - // Set the _next field if we can. - boolean CAS_newkvs( Object[] newkvs ) { - while( _newkvs == null ) - if( _newkvsUpdater.compareAndSet(this,null,newkvs) ) - return true; - return false; - } - // Sometimes many threads race to create a new very large table. Only 1 - // wins the race, but the losers all allocate a junk large table with - // hefty allocation costs. Attempt to control the overkill here by - // throttling attempts to create a new table. I cannot really block here - // (lest I lose the non-blocking property) but late-arriving threads can - // give the initial resizing thread a little time to allocate the initial - // new table. The Right Long Term Fix here is to use array-lets and - // incrementally create the new very large array. In C I'd make the array - // with malloc (which would mmap under the hood) which would only eat - // virtual-address and not real memory - and after Somebody wins then we - // could in parallel initialize the array. Java does not allow - // un-initialized array creation (especially of ref arrays!). - volatile long _resizers; // count of threads attempting an initial resize - private static final AtomicLongFieldUpdater _resizerUpdater = - AtomicLongFieldUpdater.newUpdater(CHM.class, "_resizers"); - - // --- - // Simple constructor - CHM( Counter size ) { - _size = size; - _slots= new Counter(); - } - - // --- tableFull --------------------------------------------------------- - // Heuristic to decide if this table is too full, and we should start a - // new table. Note that if a 'get' call has reprobed too many times and - // decided the table must be full, then always the estimate_sum must be - // high and we must report the table is full. If we do not, then we might - // end up deciding that the table is not full and inserting into the - // current table, while a 'get' has decided the same key cannot be in this - // table because of too many reprobes. The invariant is: - // slots.estimate_sum >= max_reprobe_cnt >= reprobe_limit(len) - private final boolean tableFull( int reprobe_cnt, int len ) { - return - // Do the cheap check first: we allow some number of reprobes always - reprobe_cnt >= REPROBE_LIMIT && - // More expensive check: see if the table is > 1/4 full. - _slots.estimate_get() >= reprobe_limit(len); - } - - // --- resize ------------------------------------------------------------ - // Resizing after too many probes. "How Big???" heuristics are here. - // Callers will (not this routine) will 'help_copy' any in-progress copy. - // Since this routine has a fast cutout for copy-already-started, callers - // MUST 'help_copy' lest we have a path which forever runs through - // 'resize' only to discover a copy-in-progress which never progresses. - private final Object[] resize( NonBlockingHashMap topmap, Object[] kvs) { - assert chm(kvs) == this; - - // Check for resize already in progress, probably triggered by another thread - Object[] newkvs = _newkvs; // VOLATILE READ - if( newkvs != null ) // See if resize is already in progress - return newkvs; // Use the new table already - - // No copy in-progress, so start one. First up: compute new table size. - int oldlen = len(kvs); // Old count of K,V pairs allowed - int sz = size(); // Get current table count of active K,V pairs - int newsz = sz; // First size estimate - - // Heuristic to determine new size. We expect plenty of dead-slots-with-keys - // and we need some decent padding to avoid endless reprobing. - if( sz >= (oldlen>>2) ) { // If we are >25% full of keys then... - newsz = oldlen<<1; // Double size - if( sz >= (oldlen>>1) ) // If we are >50% full of keys then... - newsz = oldlen<<2; // Double double size - } - // This heuristic in the next 2 lines leads to a much denser table - // with a higher reprobe rate - //if( sz >= (oldlen>>1) ) // If we are >50% full of keys then... - // newsz = oldlen<<1; // Double size - - // Last (re)size operation was very recent? Then double again; slows - // down resize operations for tables subject to a high key churn rate. - long tm = System.currentTimeMillis(); - long q=0; - if( newsz <= oldlen && // New table would shrink or hold steady? - tm <= topmap._last_resize_milli+10000 && // Recent resize (less than 1 sec ago) - (q=_slots.estimate_get()) >= (sz<<1) ) // 1/2 of keys are dead? - newsz = oldlen<<1; // Double the existing size - - // Do not shrink, ever - if( newsz < oldlen ) newsz = oldlen; - - // Convert to power-of-2 - int log2; - for( log2=MIN_SIZE_LOG; (1<>20/*megs*/; - if( r >= 2 && megs > 0 ) { // Already 2 guys trying; wait and see - newkvs = _newkvs; // Between dorking around, another thread did it - if( newkvs != null ) // See if resize is already in progress - return newkvs; // Use the new table already - // TODO - use a wait with timeout, so we'll wakeup as soon as the new table - // is ready, or after the timeout in any case. - //synchronized( this ) { wait(8*megs); } // Timeout - we always wakeup - // For now, sleep a tad and see if the 2 guys already trying to make - // the table actually get around to making it happen. - try { Thread.sleep(8*megs); } catch( Exception e ) { } - } - // Last check, since the 'new' below is expensive and there is a chance - // that another thread slipped in a new thread while we ran the heuristic. - newkvs = _newkvs; - if( newkvs != null ) // See if resize is already in progress - return newkvs; // Use the new table already - - // Double size for K,V pairs, add 1 for CHM - newkvs = new Object[((1< _copyIdxUpdater = - AtomicLongFieldUpdater.newUpdater(CHM.class, "_copyIdx"); - - // Work-done reporting. Used to efficiently signal when we can move to - // the new table. From 0 to len(oldkvs) refers to copying from the old - // table to the new. - volatile long _copyDone= 0; - static private final AtomicLongFieldUpdater _copyDoneUpdater = - AtomicLongFieldUpdater.newUpdater(CHM.class, "_copyDone"); - - // --- help_copy_impl ---------------------------------------------------- - // Help along an existing resize operation. We hope its the top-level - // copy (it was when we started) but this CHM might have been promoted out - // of the top position. - private final void help_copy_impl( NonBlockingHashMap topmap, Object[] oldkvs, boolean copy_all ) { - assert chm(oldkvs) == this; - Object[] newkvs = _newkvs; - assert newkvs != null; // Already checked by caller - int oldlen = len(oldkvs); // Total amount to copy - final int MIN_COPY_WORK = Math.min(oldlen,1024); // Limit per-thread work - - // --- - int panic_start = -1; - int copyidx=-9999; // Fool javac to think it's initialized - while( _copyDone < oldlen ) { // Still needing to copy? - // Carve out a chunk of work. The counter wraps around so every - // thread eventually tries to copy every slot repeatedly. - - // We "panic" if we have tried TWICE to copy every slot - and it still - // has not happened. i.e., twice some thread somewhere claimed they - // would copy 'slot X' (by bumping _copyIdx) but they never claimed to - // have finished (by bumping _copyDone). Our choices become limited: - // we can wait for the work-claimers to finish (and become a blocking - // algorithm) or do the copy work ourselves. Tiny tables with huge - // thread counts trying to copy the table often 'panic'. - if( panic_start == -1 ) { // No panic? - copyidx = (int)_copyIdx; - while( copyidx < (oldlen<<1) && // 'panic' check - !_copyIdxUpdater.compareAndSet(this,copyidx,copyidx+MIN_COPY_WORK) ) - copyidx = (int)_copyIdx; // Re-read - if( !(copyidx < (oldlen<<1)) ) // Panic! - panic_start = copyidx; // Record where we started to panic-copy - } - - // We now know what to copy. Try to copy. - int workdone = 0; - for( int i=0; i 0 ) // Report work-done occasionally - copy_check_and_promote( topmap, oldkvs, workdone );// See if we can promote - //for( int i=0; i 0 ) { - while( !_copyDoneUpdater.compareAndSet(this,copyDone,copyDone+workdone) ) { - copyDone = _copyDone; // Reload, retry - assert (copyDone+workdone) <= oldlen; - } - //if( (10*copyDone/oldlen) != (10*(copyDone+workdone)/oldlen) ) - //System.out.print(" "+(copyDone+workdone)*100/oldlen+"%"+"_"+(_copyIdx*100/oldlen)+"%"); - } - - // Check for copy being ALL done, and promote. Note that we might have - // nested in-progress copies and manage to finish a nested copy before - // finishing the top-level copy. We only promote top-level copies. - if( copyDone+workdone == oldlen && // Ready to promote this table? - topmap._kvs == oldkvs && // Looking at the top-level table? - // Attempt to promote - topmap.CAS_kvs(oldkvs,_newkvs) ) { - topmap._last_resize_milli = System.currentTimeMillis(); // Record resize time for next check - //long nano = System.nanoTime(); - //System.out.println(" "+nano+" Promote table to "+len(_newkvs)); - //if( System.out != null ) System.out.print("]"); - } - } - // --- copy_slot --------------------------------------------------------- - // Copy one K/V pair from oldkvs[i] to newkvs. Returns true if we can - // confirm that the new table guaranteed has a value for this old-table - // slot. We need an accurate confirmed-copy count so that we know when we - // can promote (if we promote the new table too soon, other threads may - // 'miss' on values not-yet-copied from the old table). We don't allow - // any direct updates on the new table, unless they first happened to the - // old table - so that any transition in the new table from null to - // not-null must have been from a copy_slot (or other old-table overwrite) - // and not from a thread directly writing in the new table. Thus we can - // count null-to-not-null transitions in the new table. - private boolean copy_slot( NonBlockingHashMap topmap, int idx, Object[] oldkvs, Object[] newkvs ) { - // Blindly set the key slot from null to TOMBSTONE, to eagerly stop - // fresh put's from inserting new values in the old table when the old - // table is mid-resize. We don't need to act on the results here, - // because our correctness stems from box'ing the Value field. Slamming - // the Key field is a minor speed optimization. - Object key; - while( (key=key(oldkvs,idx)) == null ) - CAS_key(oldkvs,idx, null, TOMBSTONE); - - // --- - // Prevent new values from appearing in the old table. - // Box what we see in the old table, to prevent further updates. - Object oldval = val(oldkvs,idx); // Read OLD table - while( !(oldval instanceof Prime) ) { - final Prime box = (oldval == null || oldval == TOMBSTONE) ? TOMBPRIME : new Prime(oldval); - if( CAS_val(oldkvs,idx,oldval,box) ) { // CAS down a box'd version of oldval - // If we made the Value slot hold a TOMBPRIME, then we both - // prevented further updates here but also the (absent) - // oldval is vaccuously available in the new table. We - // return with true here: any thread looking for a value for - // this key can correctly go straight to the new table and - // skip looking in the old table. - if( box == TOMBPRIME ) - return true; - // Otherwise we boxed something, but it still needs to be - // copied into the new table. - oldval = box; // Record updated oldval - break; // Break loop; oldval is now boxed by us - } - oldval = val(oldkvs,idx); // Else try, try again - } - if( oldval == TOMBPRIME ) return false; // Copy already complete here! - - // --- - // Copy the value into the new table, but only if we overwrite a null. - // If another value is already in the new table, then somebody else - // wrote something there and that write is happens-after any value that - // appears in the old table. If putIfMatch does not find a null in the - // new table - somebody else should have recorded the null-not_null - // transition in this copy. - Object old_unboxed = ((Prime)oldval)._V; - assert old_unboxed != TOMBSTONE; - boolean copied_into_new = (putIfMatch(topmap, newkvs, key, old_unboxed, null) == null); - - // --- - // Finally, now that any old value is exposed in the new table, we can - // forever hide the old-table value by slapping a TOMBPRIME down. This - // will stop other threads from uselessly attempting to copy this slot - // (i.e., it's a speed optimization not a correctness issue). - while( !CAS_val(oldkvs,idx,oldval,TOMBPRIME) ) - oldval = val(oldkvs,idx); - - return copied_into_new; - } // end copy_slot - } // End of CHM - - - // --- Snapshot ------------------------------------------------------------ - // The main class for iterating over the NBHM. It "snapshots" a clean - // view of the K/V array. - private class SnapshotV implements Iterator, Enumeration { - final Object[] _sskvs; - public SnapshotV() { - while( true ) { // Verify no table-copy-in-progress - Object[] topkvs = _kvs; - CHM topchm = chm(topkvs); - if( topchm._newkvs == null ) { // No table-copy-in-progress - // The "linearization point" for the iteration. Every key in this - // table will be visited, but keys added later might be skipped or - // even be added to a following table (also not iterated over). - _sskvs = topkvs; - break; - } - // Table copy in-progress - so we cannot get a clean iteration. We - // must help finish the table copy before we can start iterating. - topchm.help_copy_impl(NonBlockingHashMap.this,topkvs,true); - } - // Warm-up the iterator - next(); - } - int length() { return len(_sskvs); } - Object key(int idx) { return NonBlockingHashMap.key(_sskvs,idx); } - private int _idx; // Varies from 0-keys.length - private Object _nextK, _prevK; // Last 2 keys found - private TypeV _nextV, _prevV; // Last 2 values found - public boolean hasNext() { return _nextV != null; } - public TypeV next() { - // 'next' actually knows what the next value will be - it had to - // figure that out last go-around lest 'hasNext' report true and - // some other thread deleted the last value. Instead, 'next' - // spends all its effort finding the key that comes after the - // 'next' key. - if( _idx != 0 && _nextV == null ) throw new NoSuchElementException(); - _prevK = _nextK; // This will become the previous key - _prevV = _nextV; // This will become the previous value - _nextV = null; // We have no more next-key - // Attempt to set <_nextK,_nextV> to the next K,V pair. - // _nextV is the trigger: stop searching when it is != null - while( _idx elements() { return new SnapshotV(); } - - // --- values -------------------------------------------------------------- - /** Returns a {@link Collection} view of the values contained in this map. - * The collection is backed by the map, so changes to the map are reflected - * in the collection, and vice-versa. The collection supports element - * removal, which removes the corresponding mapping from this map, via the - * Iterator.remove, Collection.remove, - * removeAll, retainAll, and clear operations. - * It does not support the add or addAll operations. - * - *

The view's iterator is a "weakly consistent" iterator that - * will never throw {@link ConcurrentModificationException}, and guarantees - * to traverse elements as they existed upon construction of the iterator, - * and may (but is not guaranteed to) reflect any modifications subsequent - * to construction. */ - @Override - public Collection values() { - return new AbstractCollection() { - @Override public void clear ( ) { NonBlockingHashMap.this.clear ( ); } - @Override public int size ( ) { return NonBlockingHashMap.this.size ( ); } - @Override public boolean contains( Object v ) { return NonBlockingHashMap.this.containsValue(v); } - @Override public Iterator iterator() { return new SnapshotV(); } - }; - } - - // --- keySet -------------------------------------------------------------- - private class SnapshotK implements Iterator, Enumeration { - final SnapshotV _ss; - public SnapshotK() { _ss = new SnapshotV(); } - public void remove() { _ss.remove(); } - public TypeK next() { _ss.next(); return (TypeK)_ss._prevK; } - public boolean hasNext() { return _ss.hasNext(); } - public TypeK nextElement() { return next(); } - public boolean hasMoreElements() { return hasNext(); } - } - - /** Returns an enumeration of the keys in this table. - * @return an enumeration of the keys in this table - * @see #keySet() */ - public Enumeration keys() { return new SnapshotK(); } - - /** Returns a {@link Set} view of the keys contained in this map. The set - * is backed by the map, so changes to the map are reflected in the set, - * and vice-versa. The set supports element removal, which removes the - * corresponding mapping from this map, via the Iterator.remove, - * Set.remove, removeAll, retainAll, and - * clear operations. It does not support the add or - * addAll operations. - * - *

The view's iterator is a "weakly consistent" iterator that - * will never throw {@link ConcurrentModificationException}, and guarantees - * to traverse elements as they existed upon construction of the iterator, - * and may (but is not guaranteed to) reflect any modifications subsequent - * to construction. */ - @Override - public Set keySet() { - return new AbstractSet () { - @Override public void clear ( ) { NonBlockingHashMap.this.clear ( ); } - @Override public int size ( ) { return NonBlockingHashMap.this.size ( ); } - @Override public boolean contains( Object k ) { return NonBlockingHashMap.this.containsKey(k); } - @Override public boolean remove ( Object k ) { return NonBlockingHashMap.this.remove (k) != null; } - @Override public Iterator iterator() { return new SnapshotK(); } - }; - } - - - // --- entrySet ------------------------------------------------------------ - // Warning: Each call to 'next' in this iterator constructs a new NBHMEntry. - private class NBHMEntry extends AbstractEntry { - NBHMEntry( final TypeK k, final TypeV v ) { super(k,v); } - public TypeV setValue(final TypeV val) { - if( val == null ) throw new NullPointerException(); - _val = val; - return put(_key, val); - } - } - - private class SnapshotE implements Iterator> { - final SnapshotV _ss; - public SnapshotE() { _ss = new SnapshotV(); } - public void remove() { _ss.remove(); } - public Map.Entry next() { _ss.next(); return new NBHMEntry((TypeK)_ss._prevK,_ss._prevV); } - public boolean hasNext() { return _ss.hasNext(); } - } - - /** Returns a {@link Set} view of the mappings contained in this map. The - * set is backed by the map, so changes to the map are reflected in the - * set, and vice-versa. The set supports element removal, which removes - * the corresponding mapping from the map, via the - * Iterator.remove, Set.remove, removeAll, - * retainAll, and clear operations. It does not support - * the add or addAll operations. - * - *

The view's iterator is a "weakly consistent" iterator - * that will never throw {@link ConcurrentModificationException}, - * and guarantees to traverse elements as they existed upon - * construction of the iterator, and may (but is not guaranteed to) - * reflect any modifications subsequent to construction. - * - *

Warning: the iterator associated with this Set - * requires the creation of {@link java.util.Map.Entry} objects with each - * iteration. The {@link NonBlockingHashMap} does not normally create or - * using {@link java.util.Map.Entry} objects so they will be created soley - * to support this iteration. Iterating using {@link #keySet} or {@link - * #values} will be more efficient. - */ - @Override - public Set> entrySet() { - return new AbstractSet>() { - @Override public void clear ( ) { NonBlockingHashMap.this.clear( ); } - @Override public int size ( ) { return NonBlockingHashMap.this.size ( ); } - @Override public boolean remove( final Object o ) { - if( !(o instanceof Map.Entry)) return false; - final Map.Entry e = (Map.Entry)o; - return NonBlockingHashMap.this.remove(e.getKey(), e.getValue()); - } - @Override public boolean contains(final Object o) { - if( !(o instanceof Map.Entry)) return false; - final Map.Entry e = (Map.Entry)o; - TypeV v = get(e.getKey()); - return v.equals(e.getValue()); - } - @Override public Iterator> iterator() { return new SnapshotE(); } - }; - } - - // --- writeObject ------------------------------------------------------- - // Write a NBHM to a stream - private void writeObject(java.io.ObjectOutputStream s) throws IOException { - s.defaultWriteObject(); // Nothing to write - for( Object K : keySet() ) { - final Object V = get(K); // Do an official 'get' - s.writeObject(K); // Write the pair - s.writeObject(V); - } - s.writeObject(null); // Sentinel to indicate end-of-data - s.writeObject(null); - } - - // --- readObject -------------------------------------------------------- - // Read a CHM from a stream - private void readObject(java.io.ObjectInputStream s) throws IOException, ClassNotFoundException { - s.defaultReadObject(); // Read nothing - initialize(MIN_SIZE); - for(;;) { - final TypeK K = (TypeK) s.readObject(); - final TypeV V = (TypeV) s.readObject(); - if( K == null ) break; - put(K,V); // Insert with an offical put - } - } - -} // End NonBlockingHashMap class diff --git a/cliffc-hashtable/cliffc_hashtable.h b/cliffc-hashtable/cliffc_hashtable.h deleted file mode 100644 index 876a89b..0000000 --- a/cliffc-hashtable/cliffc_hashtable.h +++ /dev/null @@ -1,970 +0,0 @@ -#ifndef CLIFFC_HASHTABLE_H -#define CLIFFC_HASHTABLE_H - -#include -#include "stdio.h" -//#include -#ifdef STANDALONE -#include -#define MODEL_ASSERT assert -#else -#include -#endif -#include - -using namespace std; - -/** - This header file declares and defines a simplified version of Cliff Click's - NonblockingHashMap. It contains all the necessary structrues and main - functions. In simplified_cliffc_hashtable.cc file, it has the definition for - the static fields. -*/ - -template -class cliffc_hashtable; - -/** - Corresponding the the Object[] array in Cliff Click's Java implementation. - It keeps the first two slots for CHM (Hashtable control unit) and the hash - records (an array of hash used for fast negative key-equality check). -*/ -struct kvs_data { - int _size; - atomic *_data; - - kvs_data(int sz) { - _size = sz; - int real_size = sz * 2 + 2; - _data = new atomic[real_size]; - // The control block should be initialized in resize() - // Init the hash record array - int *hashes = new int[_size]; - int i; - for (i = 0; i < _size; i++) { - hashes[i] = 0; - } - // Init the data to Null slot - for (i = 2; i < real_size; i++) { - _data[i].store(NULL, memory_order_relaxed); - } - _data[1].store(hashes, memory_order_relaxed); - } - - ~kvs_data() { - int *hashes = (int*) _data[1].load(memory_order_relaxed); - delete hashes; - delete[] _data; - } -}; - -struct slot { - bool _prime; - void *_ptr; - - slot(bool prime, void *ptr) { - _prime = prime; - _ptr = ptr; - } -}; - - -/** - TypeK must have defined function "int hashCode()" which return the hash - code for the its object, and "int equals(TypeK anotherKey)" which is - used to judge equality. - TypeK and TypeV should define their own copy constructor. -*/ -/** - @Begin - @Class_begin - @End -*/ -template -class cliffc_hashtable { - /** - # The synchronization we have for the hashtable gives us the property of - # serializability, so we should have a sequential hashtable when we check the - # correctness. The key thing is to identify all the commit point. - - @Begin - @Options: - LANG = CPP; - CLASS = cliffc_hashtable; - @Global_define: - @DeclareVar: - spec_table *map; - spec_table *id_map; - id_tag_t *tag; - @InitVar: - map = new_spec_table_default(equals_key); - id_map = new_spec_table_default(equals_id); - tag = new_id_tag(); - - @DefineFunc: - bool equals_key(void *ptr1, void *ptr2) { - TypeK *key1 = (TypeK*) ptr1, - *key2 = (TypeK*) ptr2; - if (key1 == NULL || key2 == NULL) - return false; - return key1->equals(key2); - } - - @DefineFunc: - bool equals_val(void *ptr1, void *ptr2) { - if (ptr1 == ptr2) - return true; - TypeV *val1 = (TypeV*) ptr1, - *val2 = (TypeV*) ptr2; - if (val1 == NULL || val2 == NULL) - return false; - return val1->equals(val2); - } - - @DefineFunc: - bool equals_id(void *ptr1, void *ptr2) { - id_tag_t *id1 = (id_tag_t*) ptr1, - *id2 = (id_tag_t*) ptr2; - if (id1 == NULL || id2 == NULL) - return false; - return (*id1).tag == (*id2).tag; - } - - @DefineFunc: - # Update the tag for the current key slot if the corresponding tag - # is NULL, otherwise just return that tag. It will update the next - # available tag too if it requires a new tag for that key slot. - call_id_t getKeyTag(TypeK *key) { - if (!spec_table_contains(id_map, key)) { - call_id_t cur_id = current(tag); - spec_table_put(id_map, key, (void*) cur_id); - next(tag); - return cur_id; - } else { - call_id_t res = (call_id_t) spec_table_get(id_map, key); - return res; - } - } - @Happens_before: - Put->Get - Put->Put - @End - */ - -friend class CHM; - /** - The control structure for the hashtable - */ - private: - class CHM { - friend class cliffc_hashtable; - private: - atomic _newkvs; - - // Size of active K,V pairs - atomic_int _size; - - // Count of used slots - atomic_int _slots; - - // The next part of the table to copy - atomic_int _copy_idx; - - // Work-done reporting - atomic_int _copy_done; - - public: - CHM(int size) { - _newkvs.store(NULL, memory_order_relaxed); - _size.store(size, memory_order_relaxed); - _slots.store(0, memory_order_relaxed); - - _copy_idx.store(0, memory_order_relaxed); - _copy_done.store(0, memory_order_relaxed); - } - - ~CHM() {} - - private: - - // Heuristic to decide if the table is too full - bool table_full(int reprobe_cnt, int len) { - return - reprobe_cnt >= REPROBE_LIMIT && - _slots.load(memory_order_relaxed) >= reprobe_limit(len); - } - - kvs_data* resize(cliffc_hashtable *topmap, kvs_data *kvs) { - //model_print("resizing...\n"); - /**** FIXME: miss ****/ - kvs_data *newkvs = _newkvs.load(memory_order_acquire); - if (newkvs != NULL) - return newkvs; - - // No copy in-progress, start one; Only double the table size - int oldlen = kvs->_size; - int sz = _size.load(memory_order_relaxed); - int newsz = sz; - - // Just follow Cliff Click's heuristic to decide the new size - if (sz >= (oldlen >> 2)) { // If we are 25% full - newsz = oldlen << 1; // Double size - if (sz >= (oldlen >> 1)) - newsz = oldlen << 2; // Double double size - } - - // We do not record the record timestamp - if (newsz <= oldlen) newsz = oldlen << 1; - // Do not shrink ever - if (newsz < oldlen) newsz = oldlen; - - // Last check cause the 'new' below is expensive - /**** FIXME: miss ****/ - newkvs = _newkvs.load(memory_order_acquire); - //model_print("hey1\n"); - if (newkvs != NULL) return newkvs; - - newkvs = new kvs_data(newsz); - void *chm = (void*) new CHM(sz); - //model_print("hey2\n"); - newkvs->_data[0].store(chm, memory_order_relaxed); - - kvs_data *cur_newkvs; - // Another check after the slow allocation - /**** FIXME: miss ****/ - if ((cur_newkvs = _newkvs.load(memory_order_acquire)) != NULL) - return cur_newkvs; - // CAS the _newkvs to the allocated table - kvs_data *desired = (kvs_data*) NULL; - kvs_data *expected = (kvs_data*) newkvs; - /**** FIXME: miss ****/ - //model_print("release in resize!\n"); - if (!_newkvs.compare_exchange_strong(desired, expected, memory_order_release, - memory_order_relaxed)) { - // Should clean the allocated area - delete newkvs; - /**** FIXME: miss ****/ - newkvs = _newkvs.load(memory_order_acquire); - } - return newkvs; - } - - void help_copy_impl(cliffc_hashtable *topmap, kvs_data *oldkvs, - bool copy_all) { - MODEL_ASSERT (get_chm(oldkvs) == this); - /**** FIXME: miss ****/ - kvs_data *newkvs = _newkvs.load(memory_order_acquire); - int oldlen = oldkvs->_size; - int min_copy_work = oldlen > 1024 ? 1024 : oldlen; - - // Just follow Cliff Click's code here - int panic_start = -1; - int copyidx; - while (_copy_done.load(memory_order_relaxed) < oldlen) { - copyidx = _copy_idx.load(memory_order_relaxed); - if (panic_start == -1) { // No painc - copyidx = _copy_idx.load(memory_order_relaxed); - while (copyidx < (oldlen << 1) && - !_copy_idx.compare_exchange_strong(copyidx, copyidx + - min_copy_work, memory_order_relaxed, memory_order_relaxed)) - copyidx = _copy_idx.load(memory_order_relaxed); - if (!(copyidx < (oldlen << 1))) - panic_start = copyidx; - } - - // Now copy the chunk of work we claimed - int workdone = 0; - for (int i = 0; i < min_copy_work; i++) - if (copy_slot(topmap, (copyidx + i) & (oldlen - 1), oldkvs, - newkvs)) - workdone++; - if (workdone > 0) - copy_check_and_promote(topmap, oldkvs, workdone); - - copyidx += min_copy_work; - if (!copy_all && panic_start == -1) - return; // We are done with the work we claim - } - copy_check_and_promote(topmap, oldkvs, 0); // See if we can promote - } - - kvs_data* copy_slot_and_check(cliffc_hashtable *topmap, kvs_data - *oldkvs, int idx, void *should_help) { - /**** FIXME: miss ****/ - kvs_data *newkvs = _newkvs.load(memory_order_acquire); - // We're only here cause the caller saw a Prime - if (copy_slot(topmap, idx, oldkvs, newkvs)) - copy_check_and_promote(topmap, oldkvs, 1); // Record the slot copied - return (should_help == NULL) ? newkvs : topmap->help_copy(newkvs); - } - - void copy_check_and_promote(cliffc_hashtable *topmap, kvs_data* - oldkvs, int workdone) { - int oldlen = oldkvs->_size; - int copyDone = _copy_done.load(memory_order_relaxed); - if (workdone > 0) { - while (true) { - copyDone = _copy_done.load(memory_order_relaxed); - if (_copy_done.compare_exchange_weak(copyDone, copyDone + - workdone, memory_order_relaxed, memory_order_relaxed)) - break; - } - } - - // Promote the new table to the current table - if (copyDone + workdone == oldlen && - topmap->_kvs.load(memory_order_relaxed) == oldkvs) { - /**** FIXME: miss ****/ - kvs_data *newkvs = _newkvs.load(memory_order_acquire); - /**** CDSChecker error ****/ - topmap->_kvs.compare_exchange_strong(oldkvs, newkvs, memory_order_release, - memory_order_relaxed); - } - } - - bool copy_slot(cliffc_hashtable *topmap, int idx, kvs_data *oldkvs, - kvs_data *newkvs) { - slot *key_slot; - while ((key_slot = key(oldkvs, idx)) == NULL) - CAS_key(oldkvs, idx, NULL, TOMBSTONE); - - // First CAS old to Prime - slot *oldval = val(oldkvs, idx); - while (!is_prime(oldval)) { - slot *box = (oldval == NULL || oldval == TOMBSTONE) - ? TOMBPRIME : new slot(true, oldval->_ptr); - if (CAS_val(oldkvs, idx, oldval, box)) { - if (box == TOMBPRIME) - return 1; // Copy done - // Otherwise we CAS'd the box - oldval = box; // Record updated oldval - break; - } - oldval = val(oldkvs, idx); // Else re-try - } - - if (oldval == TOMBPRIME) return false; // Copy already completed here - - slot *old_unboxed = new slot(false, oldval->_ptr); - int copied_into_new = (putIfMatch(topmap, newkvs, key_slot, old_unboxed, - NULL) == NULL); - - // Old value is exposed in the new table - while (!CAS_val(oldkvs, idx, oldval, TOMBPRIME)) - oldval = val(oldkvs, idx); - - return copied_into_new; - } - }; - - - - private: - static const int Default_Init_Size = 4; // Intial table size - - static slot* const MATCH_ANY; - static slot* const NO_MATCH_OLD; - - static slot* const TOMBPRIME; - static slot* const TOMBSTONE; - - static const int REPROBE_LIMIT = 10; // Forces a table-resize - - atomic _kvs; - - public: - cliffc_hashtable() { - // Should initialize the CHM for the construction of the table - // For other CHM in kvs_data, they should be initialzed in resize() - // because the size is determined dynamically - /** - @Begin - @Entry_point - @End - */ - kvs_data *kvs = new kvs_data(Default_Init_Size); - void *chm = (void*) new CHM(0); - kvs->_data[0].store(chm, memory_order_relaxed); - _kvs.store(kvs, memory_order_relaxed); - } - - cliffc_hashtable(int init_size) { - // Should initialize the CHM for the construction of the table - // For other CHM in kvs_data, they should be initialzed in resize() - // because the size is determined dynamically - - /** - @Begin - @Entry_point - @End - */ - kvs_data *kvs = new kvs_data(init_size); - void *chm = (void*) new CHM(0); - kvs->_data[0].store(chm, memory_order_relaxed); - _kvs.store(kvs, memory_order_relaxed); - } - - /** - @Begin - @Interface: Get - //@Commit_point_set: Get_Point1 | Get_Point2 | Get_ReadKVS | Get_ReadNewKVS | Get_Clear - @Commit_point_set: Get_Point1 | Get_Point2 | Get_Clear - //@Commit_point_set: Get_Point1 | Get_Point2 | Get_Point3 - @ID: getKeyTag(key) - @Action: - TypeV *_Old_Val = (TypeV*) spec_table_get(map, key); - //bool passed = equals_val(_Old_Val, __RET__); - bool passed = false; - if (!passed) { - int old = _Old_Val == NULL ? 0 : _Old_Val->_val; - int ret = __RET__ == NULL ? 0 : __RET__->_val; - //model_print("Get: key: %d, _Old_Val: %d, RET: %d\n", - //key->_val, old, ret); - } - @Post_check: - //__RET__ == NULL ? true : equals_val(_Old_Val, __RET__) - equals_val(_Old_Val, __RET__) - @End - */ - TypeV* get(TypeK *key) { - slot *key_slot = new slot(false, key); - int fullhash = hash(key_slot); - /**** CDSChecker error ****/ - kvs_data *kvs = _kvs.load(memory_order_acquire); - /** - //@Begin - @Commit_point_define_check: true - @Label: Get_ReadKVS - @End - */ - slot *V = get_impl(this, kvs, key_slot, fullhash); - if (V == NULL) return NULL; - MODEL_ASSERT (!is_prime(V)); - return (TypeV*) V->_ptr; - } - - /** - @Begin - @Interface: Put - //@Commit_point_set: Put_Point | Put_ReadKVS | Put_ReadNewKVS | Put_WriteKey - @Commit_point_set: Put_Point | Put_WriteKey - @ID: getKeyTag(key) - @Action: - # Remember this old value at checking point - TypeV *_Old_Val = (TypeV*) spec_table_get(map, key); - spec_table_put(map, key, val); - //bool passed = equals_val(__RET__, _Old_Val); - bool passed = false; - if (!passed) { - int old = _Old_Val == NULL ? 0 : _Old_Val->_val; - int ret = __RET__ == NULL ? 0 : __RET__->_val; - //model_print("Put: key: %d, val: %d, _Old_Val: %d, RET: %d\n", - // key->_val, val->_val, old, ret); - } - @Post_check: - equals_val(__RET__, _Old_Val) - @End - */ - TypeV* put(TypeK *key, TypeV *val) { - return putIfMatch(key, val, NO_MATCH_OLD); - } - - /** -// @Begin - @Interface: PutIfAbsent - @Commit_point_set: - Write_Success_Point | PutIfAbsent_Fail_Point - @Condition: !spec_table_contains(map, key) - @HB_condition: - COND_PutIfAbsentSucc :: __RET__ == NULL - @ID: getKeyTag(key) - @Action: - void *_Old_Val = spec_table_get(map, key); - if (__COND_SAT__) - spec_table_put(map, key, value); - @Post_check: - __COND_SAT__ ? __RET__ == NULL : equals_val(_Old_Val, __RET__) - @End - */ - TypeV* putIfAbsent(TypeK *key, TypeV *value) { - return putIfMatch(key, val, TOMBSTONE); - } - - /** -// @Begin - @Interface: RemoveAny - @Commit_point_set: Write_Success_Point - @ID: getKeyTag(key) - @Action: - void *_Old_Val = spec_table_get(map, key); - spec_table_put(map, key, NULL); - @Post_check: - equals_val(__RET__, _Old_Val) - @End - */ - TypeV* remove(TypeK *key) { - return putIfMatch(key, TOMBSTONE, NO_MATCH_OLD); - } - - /** -// @Begin - @Interface: RemoveIfMatch - @Commit_point_set: - Write_Success_Point | RemoveIfMatch_Fail_Point - @Condition: - equals_val(spec_table_get(map, key), val) - @HB_condition: - COND_RemoveIfMatchSucc :: __RET__ == true - @ID: getKeyTag(key) - @Action: - if (__COND_SAT__) - spec_table_put(map, key, NULL); - @Post_check: - __COND_SAT__ ? __RET__ : !__RET__ - @End - */ - bool remove(TypeK *key, TypeV *val) { - slot *val_slot = val == NULL ? NULL : new slot(false, val); - return putIfMatch(key, TOMBSTONE, val) == val; - - } - - /** -// @Begin - @Interface: ReplaceAny - @Commit_point_set: - Write_Success_Point - @ID: getKeyTag(key) - @Action: - void *_Old_Val = spec_table_get(map, key); - @Post_check: - equals_val(__RET__, _Old_Val) - @End - */ - TypeV* replace(TypeK *key, TypeV *val) { - return putIfMatch(key, val, MATCH_ANY); - } - - /** -// @Begin - @Interface: ReplaceIfMatch - @Commit_point_set: - Write_Success_Point | ReplaceIfMatch_Fail_Point - @Condition: - equals_val(spec_table_get(map, key), oldval) - @HB_condition: - COND_ReplaceIfMatchSucc :: __RET__ == true - @ID: getKeyTag(key) - @Action: - if (__COND_SAT__) - spec_table_put(map, key, newval); - @Post_check: - __COND_SAT__ ? __RET__ : !__RET__ - @End - */ - bool replace(TypeK *key, TypeV *oldval, TypeV *newval) { - return putIfMatch(key, newval, oldval) == oldval; - } - - private: - static CHM* get_chm(kvs_data* kvs) { - CHM *res = (CHM*) kvs->_data[0].load(memory_order_relaxed); - return res; - } - - static int* get_hashes(kvs_data *kvs) { - return (int *) kvs->_data[1].load(memory_order_relaxed); - } - - // Preserve happens-before semantics on newly inserted keys - static inline slot* key(kvs_data *kvs, int idx) { - MODEL_ASSERT (idx >= 0 && idx < kvs->_size); - // Corresponding to the volatile read in get_impl() and putIfMatch in - // Cliff Click's Java implementation - slot *res = (slot*) kvs->_data[idx * 2 + 2].load(memory_order_relaxed); - /** - @Begin - # This is a complicated potential commit point since many many functions are - # calling val(). - @Potential_commit_point_define: true - @Label: Read_Key_Point - @End - */ - return res; - } - - /** - The atomic operation in val() function is a "potential" commit point, - which means in some case it is a real commit point while it is not for - some other cases. This so happens because the val() function is such a - fundamental function that many internal operation will call. Our - strategy is that we label any potential commit points and check if they - really are the commit points later. - */ - // Preserve happens-before semantics on newly inserted values - static inline slot* val(kvs_data *kvs, int idx) { - MODEL_ASSERT (idx >= 0 && idx < kvs->_size); - // Corresponding to the volatile read in get_impl() and putIfMatch in - // Cliff Click's Java implementation - /**** CDSChecker error & hb violation ****/ - slot *res = (slot*) kvs->_data[idx * 2 + 3].load(memory_order_acquire); - /** - @Begin - # This is a complicated potential commit point since many many functions are - # calling val(). - @Potential_commit_point_define: true - @Label: Read_Val_Point - @End - */ - return res; - - - } - - static int hash(slot *key_slot) { - MODEL_ASSERT(key_slot != NULL && key_slot->_ptr != NULL); - TypeK* key = (TypeK*) key_slot->_ptr; - int h = key->hashCode(); - // Spread bits according to Cliff Click's code - h += (h << 15) ^ 0xffffcd7d; - h ^= (h >> 10); - h += (h << 3); - h ^= (h >> 6); - h += (h << 2) + (h << 14); - return h ^ (h >> 16); - } - - // Heuristic to decide if reprobed too many times. - // Be careful here: Running over the limit on a 'get' acts as a 'miss'; on a - // put it triggers a table resize. Several places MUST have exact agreement. - static int reprobe_limit(int len) { - return REPROBE_LIMIT + (len >> 2); - } - - static inline bool is_prime(slot *val) { - return (val != NULL) && val->_prime; - } - - // Check for key equality. Try direct pointer comparison first (fast - // negative teset) and then the full 'equals' call - static bool keyeq(slot *K, slot *key_slot, int *hashes, int hash, - int fullhash) { - // Caller should've checked this. - MODEL_ASSERT (K != NULL); - TypeK* key_ptr = (TypeK*) key_slot->_ptr; - return - K == key_slot || - ((hashes[hash] == 0 || hashes[hash] == fullhash) && - K != TOMBSTONE && - key_ptr->equals(K->_ptr)); - } - - static bool valeq(slot *val_slot1, slot *val_slot2) { - MODEL_ASSERT (val_slot1 != NULL); - TypeK* ptr1 = (TypeV*) val_slot1->_ptr; - if (val_slot2 == NULL || ptr1 == NULL) return false; - return ptr1->equals(val_slot2->_ptr); - } - - // Together with key() preserve the happens-before relationship on newly - // inserted keys - static inline bool CAS_key(kvs_data *kvs, int idx, void *expected, void *desired) { - bool res = kvs->_data[2 * idx + 2].compare_exchange_strong(expected, - desired, memory_order_relaxed, memory_order_relaxed); - /** - # If it is a successful put instead of a copy or any other internal - # operantions, expected != NULL - @Begin - @Potential_commit_point_define: res - @Label: Write_Key_Point - @End - */ - return res; - } - - /** - Same as the val() function, we only label the CAS operation as the - potential commit point. - */ - // Together with val() preserve the happens-before relationship on newly - // inserted values - static inline bool CAS_val(kvs_data *kvs, int idx, void *expected, void - *desired) { - /**** CDSChecker error & HB violation ****/ - bool res = kvs->_data[2 * idx + 3].compare_exchange_strong(expected, - desired, memory_order_acq_rel, memory_order_relaxed); - /** - # If it is a successful put instead of a copy or any other internal - # operantions, expected != NULL - @Begin - @Potential_commit_point_define: res - @Label: Write_Val_Point - @End - */ - return res; - } - - slot* get_impl(cliffc_hashtable *topmap, kvs_data *kvs, slot* key_slot, int - fullhash) { - int len = kvs->_size; - CHM *chm = get_chm(kvs); - int *hashes = get_hashes(kvs); - - int idx = fullhash & (len - 1); - int reprobe_cnt = 0; - while (true) { - slot *K = key(kvs, idx); - /** - @Begin - @Commit_point_define: K == NULL - @Potential_commit_point_label: Read_Key_Point - @Label: Get_Point1 - @End - */ - slot *V = val(kvs, idx); - - if (K == NULL) { - //model_print("Key is null\n"); - return NULL; // A miss - } - - if (keyeq(K, key_slot, hashes, idx, fullhash)) { - // Key hit! Check if table-resize in progress - if (!is_prime(V)) { - /** - @Begin - @Commit_point_clear: true - @Label: Get_Clear - @End - */ - - /** - @Begin - @Commit_point_define: true - @Potential_commit_point_label: Read_Val_Point - @Label: Get_Point2 - @End - */ - return (V == TOMBSTONE) ? NULL : V; // Return this value - } - // Otherwise, finish the copy & retry in the new table - return get_impl(topmap, chm->copy_slot_and_check(topmap, kvs, - idx, key_slot), key_slot, fullhash); - } - - if (++reprobe_cnt >= REPROBE_LIMIT || - key_slot == TOMBSTONE) { - // Retry in new table - // Atomic read can be here - /**** FIXME: miss ****/ - kvs_data *newkvs = chm->_newkvs.load(memory_order_acquire); - /** - //@Begin - @Commit_point_define_check: true - @Label: Get_ReadNewKVS - @End - */ - return newkvs == NULL ? NULL : get_impl(topmap, - topmap->help_copy(newkvs), key_slot, fullhash); - } - - idx = (idx + 1) & (len - 1); // Reprobe by 1 - } - } - - // A wrapper of the essential function putIfMatch() - TypeV* putIfMatch(TypeK *key, TypeV *value, slot *old_val) { - // TODO: Should throw an exception rather return NULL - if (old_val == NULL) { - return NULL; - } - slot *key_slot = new slot(false, key); - - slot *value_slot = new slot(false, value); - /**** FIXME: miss ****/ - kvs_data *kvs = _kvs.load(memory_order_acquire); - /** - //@Begin - @Commit_point_define_check: true - @Label: Put_ReadKVS - @End - */ - slot *res = putIfMatch(this, kvs, key_slot, value_slot, old_val); - // Only when copy_slot() call putIfMatch() will it return NULL - MODEL_ASSERT (res != NULL); - MODEL_ASSERT (!is_prime(res)); - return res == TOMBSTONE ? NULL : (TypeV*) res->_ptr; - } - - /** - Put, Remove, PutIfAbsent, etc will call this function. Return the old - value. If the returned value is equals to the expVal (or expVal is - NO_MATCH_OLD), then this function puts the val_slot to the table 'kvs'. - Only copy_slot will pass a NULL expVal, and putIfMatch only returns a - NULL if passed a NULL expVal. - */ - static slot* putIfMatch(cliffc_hashtable *topmap, kvs_data *kvs, slot - *key_slot, slot *val_slot, slot *expVal) { - MODEL_ASSERT (val_slot != NULL); - MODEL_ASSERT (!is_prime(val_slot)); - MODEL_ASSERT (!is_prime(expVal)); - - int fullhash = hash(key_slot); - int len = kvs->_size; - CHM *chm = get_chm(kvs); - int *hashes = get_hashes(kvs); - int idx = fullhash & (len - 1); - - // Claim a key slot - int reprobe_cnt = 0; - slot *K; - slot *V; - kvs_data *newkvs; - - while (true) { // Spin till we get a key slot - K = key(kvs, idx); - V = val(kvs, idx); - if (K == NULL) { // Get a free slot - if (val_slot == TOMBSTONE) return val_slot; - // Claim the null key-slot - if (CAS_key(kvs, idx, NULL, key_slot)) { - /** - @Begin - @Commit_point_define: true - @Potential_commit_point_label: Write_Key_Point - @Label: Put_WriteKey - @End - */ - chm->_slots.fetch_add(1, memory_order_relaxed); // Inc key-slots-used count - hashes[idx] = fullhash; // Memorize full hash - break; - } - K = key(kvs, idx); // CAS failed, get updated value - MODEL_ASSERT (K != NULL); - } - - // Key slot not null, there exists a Key here - if (keyeq(K, key_slot, hashes, idx, fullhash)) - break; // Got it - - // Notice that the logic here should be consistent with that of get. - // The first predicate means too many reprobes means nothing in the - // old table. - if (++reprobe_cnt >= reprobe_limit(len) || - K == TOMBSTONE) { // Found a Tombstone key, no more keys - newkvs = chm->resize(topmap, kvs); - //model_print("resize1\n"); - // Help along an existing copy - if (expVal != NULL) topmap->help_copy(newkvs); - return putIfMatch(topmap, newkvs, key_slot, val_slot, expVal); - } - - idx = (idx + 1) & (len - 1); // Reprobe - } // End of spinning till we get a Key slot - - if (val_slot == V) return V; // Fast cutout for no-change - - // Here it tries to resize cause it doesn't want other threads to stop - // its progress (eagerly try to resize soon) - /**** FIXME: miss ****/ - newkvs = chm->_newkvs.load(memory_order_acquire); - /** - //@Begin - @Commit_point_define_check: true - @Label: Put_ReadNewKVS - @End - */ - if (newkvs == NULL && - ((V == NULL && chm->table_full(reprobe_cnt, len)) || is_prime(V))) { - //model_print("resize2\n"); - newkvs = chm->resize(topmap, kvs); // Force the copy to start - } - - // Finish the copy and then put it in the new table - if (newkvs != NULL) - return putIfMatch(topmap, chm->copy_slot_and_check(topmap, kvs, idx, - expVal), key_slot, val_slot, expVal); - - // Decided to update the existing table - while (true) { - MODEL_ASSERT (!is_prime(V)); - - if (expVal != NO_MATCH_OLD && - V != expVal && - (expVal != MATCH_ANY || V == TOMBSTONE || V == NULL) && - !(V == NULL && expVal == TOMBSTONE) && - (expVal == NULL || !valeq(expVal, V))) { - /** - //@Begin - @Commit_point_define: expVal == TOMBSTONE - @Potential_commit_point_label: Read_Val_Point - @Label: PutIfAbsent_Fail_Point - # This is a check for the PutIfAbsent() when the value - # is not absent - @End - */ - /** - //@Begin - @Commit_point_define: expVal != NULL && val_slot == TOMBSTONE - @Potential_commit_point_label: Read_Val_Point - @Label: RemoveIfMatch_Fail_Point - @End - */ - /** - //@Begin - @Commit_point_define: expVal != NULL && !valeq(expVal, V) - @Potential_commit_point_label: Read_Val_Point - @Label: ReplaceIfMatch_Fail_Point - @End - */ - return V; // Do not update! - } - - if (CAS_val(kvs, idx, V, val_slot)) { - /** - @Begin - # The only point where a successful put happens - @Commit_point_define: true - @Potential_commit_point_label: Write_Val_Point - @Label: Put_Point - @End - */ - if (expVal != NULL) { // Not called by a table-copy - // CAS succeeded, should adjust size - // Both normal put's and table-copy calls putIfMatch, but - // table-copy does not increase the number of live K/V pairs - if ((V == NULL || V == TOMBSTONE) && - val_slot != TOMBSTONE) - chm->_size.fetch_add(1, memory_order_relaxed); - if (!(V == NULL || V == TOMBSTONE) && - val_slot == TOMBSTONE) - chm->_size.fetch_add(-1, memory_order_relaxed); - } - return (V == NULL && expVal != NULL) ? TOMBSTONE : V; - } - // Else CAS failed - V = val(kvs, idx); - if (is_prime(V)) - return putIfMatch(topmap, chm->copy_slot_and_check(topmap, kvs, - idx, expVal), key_slot, val_slot, expVal); - } - } - - // Help along an existing table-resize. This is a fast cut-out wrapper. - kvs_data* help_copy(kvs_data *helper) { - /**** FIXME: miss ****/ - kvs_data *topkvs = _kvs.load(memory_order_acquire); - CHM *topchm = get_chm(topkvs); - // No cpy in progress - if (topchm->_newkvs.load(memory_order_relaxed) == NULL) return helper; - topchm->help_copy_impl(this, topkvs, false); - return helper; - } -}; -/** - @Begin - @Class_end - @End -*/ - -#endif diff --git a/cliffc-hashtable/main.cc b/cliffc-hashtable/main.cc deleted file mode 100644 index b29f765..0000000 --- a/cliffc-hashtable/main.cc +++ /dev/null @@ -1,104 +0,0 @@ -#include -#include "cliffc_hashtable.h" - -using namespace std; - -template -slot* const cliffc_hashtable::MATCH_ANY = new slot(false, NULL); - -template -slot* const cliffc_hashtable::NO_MATCH_OLD = new slot(false, NULL); - -template -slot* const cliffc_hashtable::TOMBPRIME = new slot(true, NULL); - -template -slot* const cliffc_hashtable::TOMBSTONE = new slot(false, NULL); - - -class IntWrapper { - private: - public: - int _val; - - IntWrapper(int val) : _val(val) {} - - IntWrapper() : _val(0) {} - - IntWrapper(IntWrapper& copy) : _val(copy._val) {} - - int get() { - return _val; - } - - int hashCode() { - return _val; - } - - bool operator==(const IntWrapper& rhs) { - return false; - } - - bool equals(const void *another) { - if (another == NULL) - return false; - IntWrapper *ptr = - (IntWrapper*) another; - return ptr->_val == _val; - } -}; - -cliffc_hashtable *table; -IntWrapper *val1, *val2; -IntWrapper *k0, *k1, *k2, *k3, *k4, *k5; -IntWrapper *v0, *v1, *v2, *v3, *v4, *v5; - -void threadA(void *arg) { - IntWrapper *Res; - int res; - Res = table->put(k3, v3); - res = Res == NULL ? 0 : Res->_val; - printf("Put1: key_%d, val_%d, res_%d\n", k3->_val, v3->_val, res); - - Res = table->get(k2); - res = Res == NULL ? 0 : Res->_val; - printf("Get2: key_%d, res_%d\n", k2->_val, res); -} - -void threadB(void *arg) { - IntWrapper *Res; - int res; - Res = table->put(k2, v2); - res = Res == NULL ? 0 : Res->_val; - printf("Put3: key_%d, val_%d, res_%d\n", k2->_val, v2->_val, res); - - Res = table->get(k3); - res = Res == NULL ? 0 : Res->_val; - printf("Get4: key_%d, res_%d\n", k3->_val, res); -} - -int user_main(int argc, char *argv[]) { - thrd_t t1, t2; - table = new cliffc_hashtable(32); - k1 = new IntWrapper(3); - k2 = new IntWrapper(5); - k3 = new IntWrapper(11); - k4 = new IntWrapper(7); - k5 = new IntWrapper(13); - - v0 = new IntWrapper(2048); - v1 = new IntWrapper(1024); - v2 = new IntWrapper(47); - v3 = new IntWrapper(73); - v4 = new IntWrapper(81); - v5 = new IntWrapper(99); - - thrd_create(&t1, threadA, NULL); - thrd_create(&t2, threadB, NULL); - thrd_join(t1); - thrd_join(t2); - - return 0; -} - - diff --git a/concurrent-hashmap/Makefile b/concurrent-hashmap/Makefile index 645b54a..e39d893 100644 --- a/concurrent-hashmap/Makefile +++ b/concurrent-hashmap/Makefile @@ -1,28 +1,23 @@ include ../benchmarks.mk BENCH := hashmap -NORMAL_TESTS := testcase1 testcase2 testcase3 -WILDCARD_TESTS := $(patsubst %, %_wildcard, $(NORMAL_TESTS)) +BENCH_BINARY := $(BENCH).o -#TESTS := $(NORMAL_TESTS) $(WILDCARD_TESTS) -TESTS := $(NORMAL_TESTS) +TESTS := main testcase1 testcase2 all: $(TESTS) + ../generate.sh $(notdir $(shell pwd)) -$(WILDCARD_TESTS): CXXFLAGS += -DWILDCARD +%.o : %.cc + $(CXX) -c -fPIC -MMD -MF .$@.d -o $@ $< $(CXXFLAGS) $(LDFLAGS) -$(BENCH).o : $(BENCH).h - $(CXX) -o $@ $< $(CXXFLAGS) -c $(LDFLAGS) +$(TESTS): % : %.o $(BENCH_BINARY) + $(CXX) -o $@ $^ $(CXXFLAGS) $(LDFLAGS) -$(BENCH)_wildcard.o : $(BENCH)_wildcard.h - $(CXX) -o $@ $< $(CXXFLAGS) -c $(LDFLAGS) - -$(WILDCARD_TESTS): %_wildcard : %.cc $(BENCH)_wildcard.o - $(CXX) -o $@ $< $(CXXFLAGS) $(LDFLAGS) - -$(NORMAL_TESTS): % : %.cc $(BENCH).o - $(CXX) -o $@ $< $(CXXFLAGS) $(LDFLAGS) +-include .*.d clean: - rm -f *.o *.d $(TESTS) + rm -rf $(TESTS) *.o .*.d *.dSYM + +.PHONY: clean all diff --git a/concurrent-hashmap/hashmap.cc b/concurrent-hashmap/hashmap.cc new file mode 100644 index 0000000..9b0ede6 --- /dev/null +++ b/concurrent-hashmap/hashmap.cc @@ -0,0 +1,125 @@ +#include "unrelacy.h" +#include "hashmap.h" + +/** @DeclareState: IntMap *map; */ + +int HashMap::get(int key) { + MODEL_ASSERT (key); + int hash = hashKey(key); + + // Try first without locking... + atomic *tab = table; + int index = hash & (capacity - 1); + atomic *first = &tab[index]; + Entry *e; + int res = 0; + + // Should be a load acquire + // This load action here makes it problematic for the SC analysis, what + // we need to do is as follows: if the get() method ever acquires the + // lock, we ignore this operation for the SC analysis, and otherwise we + // take it into consideration + + /********** Detected UL (testcase2) **********/ + Entry *firstPtr = first->load(mo_acquire); + + e = firstPtr; + while (e != NULL) { + if (e->hash == hash && eq(key, e->key)) { + /********** Detected Correctness (testcase1) **********/ + res = e->value.load(mo_seqcst); + /** @OPClearDefine: res != 0 */ + if (res != 0) + return res; + else + break; + } + // Loading the next entry, this can be relaxed because the + // synchronization has been established by the load of head + e = e->next.load(mo_relaxed); + } + + // Recheck under synch if key apparently not there or interference + Segment *seg = segments[hash & SEGMENT_MASK]; + seg->lock(); // Critical region begins + /** @OPClearDefine: true */ + // Not considering resize now, so ignore the reload of table... + + // Synchronized by locking, no need to be load acquire + Entry *newFirstPtr = first->load(mo_relaxed); + if (e != NULL || firstPtr != newFirstPtr) { + e = newFirstPtr; + while (e != NULL) { + if (e->hash == hash && eq(key, e->key)) { + // Protected by lock, no need to be SC + res = e->value.load(mo_relaxed); + seg->unlock(); // Critical region ends + return res; + } + // Synchronized by locking + e = e->next.load(mo_relaxed); + } + } + seg->unlock(); // Critical region ends + return 0; +} + +int HashMap::put(int key, int value) { + // Don't allow NULL key or value + MODEL_ASSERT (key && value); + + int hash = hashKey(key); + Segment *seg = segments[hash & SEGMENT_MASK]; + atomic *tab; + + seg->lock(); // Critical region begins + tab = table; + int index = hash & (capacity - 1); + + atomic *first = &tab[index]; + Entry *e; + int oldValue = 0; + + // The written of the entry is synchronized by locking + Entry *firstPtr = first->load(mo_relaxed); + e = firstPtr; + while (e != NULL) { + if (e->hash == hash && eq(key, e->key)) { + // FIXME: This could be a relaxed (because locking synchronize + // with the previous put())?? no need to be acquire + oldValue = e->value.load(relaxed); + /********** Detected Correctness (testcase1) **********/ + e->value.store(value, mo_seqcst); + /** @OPClearDefine: true */ + seg->unlock(); // Don't forget to unlock before return + return oldValue; + } + // Synchronized by locking + e = e->next.load(mo_relaxed); + } + + // Add to front of list + Entry *newEntry = new Entry(); + newEntry->hash = hash; + newEntry->key = key; + newEntry->value.store(value, relaxed); + /** @OPClearDefine: true */ + newEntry->next.store(firstPtr, relaxed); + /********** Detected UL (testcase2) **********/ + // Publish the newEntry to others + first->store(newEntry, mo_release); + seg->unlock(); // Critical region ends + return 0; +} + +/** @PreCondition: return STATE(map)->get(key) == C_RET; */ +int get(HashMap *map, int key) { + return map->get(key); +} + +/** @PreCondition: return STATE(map)->get(key) == C_RET; + @Transition: STATE(map)->put(key, value); */ +int put(HashMap *map, int key, int value) { + return map->put(key, value); +} + diff --git a/concurrent-hashmap/hashmap.h b/concurrent-hashmap/hashmap.h index f4deb8f..da8dbc3 100644 --- a/concurrent-hashmap/hashmap.h +++ b/concurrent-hashmap/hashmap.h @@ -2,82 +2,27 @@ #define _HASHMAP_H #include -#include "stdio.h" -//#include -#include #include +#include "unrelacy.h" -//#include "sc_annotation.h" - -#define relaxed memory_order_relaxed -#define release memory_order_release -#define acquire memory_order_acquire -#define acq_rel memory_order_acq_rel -#define seq_cst memory_order_seq_cst - -using namespace std; - -/** - For the sake of simplicity, we do not use template but some toy structs to - represent the Key and Value. -*/ -struct Key { - // Probably represent the coordinate (x, y, z) - int x; - int y; - int z; - - int hashCode() { - return x + 31 * y + 31 * 31 * z; - } - - bool equals(Key *other) { - if (!other) - return false; - return x == other->x && y == other->y && z == other->z; - } - - Key(int x, int y, int z) : - x(x), - y(y), - z(z) - { - - } -}; - -struct Value { - // Probably represent the speed vector (vX, vY, vZ) - int vX; - int vY; - int vZ; - - Value(int vX, int vY, int vZ) : - vX(vX), - vY(vY), - vZ(vZ) - { - - } - - bool equals(Value *other) { - if (!other) - return false; - return vX == other->vX && vY == other->vY && vZ == other->vZ; - } -}; +using std::atomic; +using std::atomic_int; +using std::mutex; class Entry { public: - Key *key; - atomic value; + int key; + atomic_int value; int hash; atomic next; - Entry(int h, Key *k, Value *v, Entry *n) { + Entry() { } + + Entry(int h, int k, int v, Entry *n) { this->hash = h; this->key = k; this->value.store(v, relaxed); + /** OPClearDefine: true */ this->next.store(n, relaxed); } }; @@ -129,172 +74,28 @@ class HashMap { } } - int hashKey(Key *x) { - int h = x->hashCode(); + int hashKey(int x) { + //int h = x->hashCode(); + int h = x; // Use logical right shift unsigned int tmp = (unsigned int) h; - return ((h << 7) - h + (tmp >> 9) + (tmp >> 17)); + //return ((h << 7) - h + (tmp >> 9) + (tmp >> 17)); + return x; } - bool eq(Key *x, Key *y) { - return x == y || x->equals(y); + bool eq(int x, int y) { + //return x == y || x->equals(y); + return x == y; } - Value* get(Key *key) { - //MODEL_ASSERT (key); - int hash = hashKey(key); - - // Try first without locking... - atomic *tab = table; - int index = hash & (capacity - 1); - atomic *first = &tab[index]; - Entry *e; - Value *res = NULL; - - // Should be a load acquire - // This load action here makes it problematic for the SC analysis, what - // we need to do is as follows: if the get() method ever acquires the - // lock, we ignore this operation for the SC analysis, and otherwise we - // take it into consideration - - //SC_BEGIN(); - Entry *firstPtr = first->load(acquire); - //SC_END(); + int get(int key); - e = firstPtr; - while (e != NULL) { - if (e->hash == hash && eq(key, e->key)) { - res = e->value.load(seq_cst); - if (res != NULL) - return res; - else - break; - } - // Loading the next entry, this can be relaxed because the - // synchronization has been established by the load of head - e = e->next.load(relaxed); - } - - // Recheck under synch if key apparently not there or interference - Segment *seg = segments[hash & SEGMENT_MASK]; - seg->lock(); // Critical region begins - // Not considering resize now, so ignore the reload of table... + int put(int key, int value); - // Synchronized by locking, no need to be load acquire - Entry *newFirstPtr = first->load(relaxed); - if (e != NULL || firstPtr != newFirstPtr) { - e = newFirstPtr; - while (e != NULL) { - if (e->hash == hash && eq(key, e->key)) { - // Protected by lock, no need to be SC - res = e->value.load(relaxed); - seg->unlock(); // Critical region ends - return res; - } - // Synchronized by locking - e = e->next.load(relaxed); - } - } - seg->unlock(); // Critical region ends - return NULL; - } - - Value* put(Key *key, Value *value) { - // Don't allow NULL key or value - //MODEL_ASSERT (key && value); - - int hash = hashKey(key); - Segment *seg = segments[hash & SEGMENT_MASK]; - atomic *tab; - - seg->lock(); // Critical region begins - tab = table; - int index = hash & (capacity - 1); - - atomic *first = &tab[index]; - Entry *e; - Value *oldValue = NULL; - - // The written of the entry is synchronized by locking - Entry *firstPtr = first->load(relaxed); - e = firstPtr; - while (e != NULL) { - if (e->hash == hash && eq(key, e->key)) { - // FIXME: This could be a relaxed (because locking synchronize - // with the previous put())?? no need to be acquire - oldValue = e->value.load(relaxed); - e->value.store(value, seq_cst); - seg->unlock(); // Don't forget to unlock before return - return oldValue; - } - // Synchronized by locking - e = e->next.load(relaxed); - } - - // Add to front of list - Entry *newEntry = new Entry(hash, key, value, firstPtr); - // Publish the newEntry to others - first->store(newEntry, release); - seg->unlock(); // Critical region ends - return NULL; - } - - Value* remove(Key *key, Value *value) { - //MODEL_ASSERT (key); - int hash = hashKey(key); - Segment *seg = segments[hash & SEGMENT_MASK]; - atomic *tab; - - seg->lock(); // Critical region begins - tab = table; - int index = hash & (capacity - 1); - - atomic *first = &tab[index]; - Entry *e; - Value *oldValue = NULL; - - // The written of the entry is synchronized by locking - Entry *firstPtr = first->load(relaxed); - e = firstPtr; - - while (true) { - if (e != NULL) { - seg->unlock(); // Don't forget to unlock - return NULL; - } - if (e->hash == hash && eq(key, e->key)) - break; - // Synchronized by locking - e = e->next.load(relaxed); - } - - // FIXME: This could be a relaxed (because locking synchronize - // with the previous put())?? No need to be acquire - oldValue = e->value.load(relaxed); - // If the value parameter is NULL, we will remove the entry anyway - if (value != NULL && value->equals(oldValue)) { - seg->unlock(); - return NULL; - } - - // Force the get() to grab the lock and retry - e->value.store(NULL, relaxed); - - // The strategy to remove the entry is to keep the entries after the - // removed one and copy the ones before it - Entry *head = e->next.load(relaxed); - Entry *p; - p = first->load(relaxed); - while (p != e) { - head = new Entry(p->hash, p->key, p->value.load(relaxed), head); - p = p->next.load(relaxed); - } - - // Publish the new head to readers - first->store(head, release); - seg->unlock(); // Critical region ends - return oldValue; - } }; +/** C Interface */ +int get(HashMap *map, int key); +int put(HashMap *map, int key, int value); + #endif diff --git a/concurrent-hashmap/main.cc b/concurrent-hashmap/main.cc index 084230e..de15cf9 100644 --- a/concurrent-hashmap/main.cc +++ b/concurrent-hashmap/main.cc @@ -1,69 +1,31 @@ -#include #include #include "hashmap.h" HashMap *table; +/** Making w4 & w11 seq_cst */ -void printKey(Key *key) { - if (key) - printf("pos = (%d, %d, %d)\n", key->x, key->y, key->z); - else - printf("pos = NULL\n"); -} - -void printValue(Value *value) { - if (value) - printf("velocity = (%d, %d, %d)\n", value->vX, value->vY, value->vZ); - else - printf("velocity = NULL\n"); -} - -// Key(3, 2, 6) & Key(1, 3, 3) are hashed to the same slot -> 4 -// Key(1, 1, 1) & Key(3, 2, 2) are hashed to the same slot -> 0 -// Key(2, 4, 1) & Key(3, 4, 2) are hashed to the same slot -> 3 -// Key(3, 4, 5) & Key(1, 4, 3) are hashed to the same slot -> 5 - +int k1 = 1; +int k2 = 3; +int v1 = 10; +int v2 = 30; void threadA(void *arg) { - Key *k1 = new Key(3, 2, 6); - Key *k2 = new Key(1, 1, 1); - Value *v1 = new Value(10, 10, 10); - Value *r1 = table->put(k1, v1); - //printValue(r1); - Value *r2 = table->get(k2); - //printf("Thrd A:\n"); - printValue(r2); + int r1 = put(table, k1, v1); + int r2 = get(table, k2); } void threadB(void *arg) { - Key *k1 = new Key(3, 2, 6); - Key *k2 = new Key(1, 1, 1); - Value *v2 = new Value(30, 40, 50); - Value *r3 = table->put(k2, v2); - //printValue(r3); - Value *r4 = table->get(k1); - printf("Thrd B:\n"); - printValue(r4); + int r3 = put(table, k2, v2); + int r4 = get(table, k1); } int user_main(int argc, char *argv[]) { + thrd_t t1, t2; - - Key *k1 = new Key(1, 3, 3); - Key *k1_prime = new Key(3, 2, 6); - Key *k2 = new Key(3, 2, 2); - Key *k2_prime = new Key(1, 1, 1); - Value *v1 = new Value(111, 111, 111); - Value *v2 = new Value(222, 222, 222); - + /** @Entry */ table = new HashMap; - printf("Key1: %d\n", table->hashKey(k1) % table->capacity); - printf("Key1': %d\n", table->hashKey(k1_prime) % table->capacity); - printf("Key2: %d\n", table->hashKey(k2) % table->capacity); - printf("Key2': %d\n", table->hashKey(k2_prime) % table->capacity); - thrd_create(&t1, threadA, NULL); thrd_create(&t2, threadB, NULL); thrd_join(t1); diff --git a/concurrent-hashmap/note.txt b/concurrent-hashmap/note.txt index 0056dcd..f080a48 100644 --- a/concurrent-hashmap/note.txt +++ b/concurrent-hashmap/note.txt @@ -8,3 +8,10 @@ get(k2); // b get(k1); // d When b and d both read the old head of the list (and they later grab the lock, making it the interface SC), it's non-SC because neither reads the updated value. + +Run testcase1 to make the store and load of value slot to be seq_cst. + +Then run testcase2 with "-o annotation" to get store and load of key slot to be +release/acquire. + +0m0.015s + 0m0.000 = 0m0.015s diff --git a/concurrent-hashmap/result1.txt b/concurrent-hashmap/result1.txt deleted file mode 100644 index 2425b57..0000000 --- a/concurrent-hashmap/result1.txt +++ /dev/null @@ -1,9 +0,0 @@ -Result 0: -wildcard 1 -> memory_order_relaxed -wildcard 2 -> memory_order_relaxed -wildcard 3 -> memory_order_acquire -wildcard 4 -> memory_order_relaxed -wildcard 6 -> memory_order_relaxed -wildcard 7 -> memory_order_relaxed -wildcard 9 -> memory_order_relaxed -wildcard 13 -> memory_order_release diff --git a/concurrent-hashmap/result2.txt b/concurrent-hashmap/result2.txt deleted file mode 100644 index c09db09..0000000 --- a/concurrent-hashmap/result2.txt +++ /dev/null @@ -1,11 +0,0 @@ -Result 0: -wildcard 1 -> memory_order_relaxed -wildcard 2 -> memory_order_relaxed -wildcard 3 -> memory_order_acquire -wildcard 4 -> memory_order_seq_cst -wildcard 6 -> memory_order_relaxed -wildcard 7 -> memory_order_relaxed -wildcard 9 -> memory_order_relaxed -wildcard 10 -> memory_order_relaxed -wildcard 11 -> memory_order_seq_cst -wildcard 13 -> memory_order_release diff --git a/concurrent-hashmap/testcase1.cc b/concurrent-hashmap/testcase1.cc index 939e250..4b7077b 100644 --- a/concurrent-hashmap/testcase1.cc +++ b/concurrent-hashmap/testcase1.cc @@ -1,58 +1,33 @@ #include -#ifdef WILDCARD -#include "hashmap_wildcard.h" -#else #include "hashmap.h" -#endif HashMap *table; -void printKey(Key *key) { - if (key) - printf("pos = (%d, %d, %d)\n", key->x, key->y, key->z); - else - printf("pos = NULL\n"); -} - -void printValue(Value *value) { - if (value) - printf("velocity = (%d, %d, %d)\n", value->vX, value->vY, value->vZ); - else - printf("velocity = NULL\n"); -} - -// Key(3, 2, 6) & Key(1, 3, 3) are hashed to the same slot -> 4 -// Key(1, 1, 1) & Key(3, 2, 2) are hashed to the same slot -> 0 -// Key(2, 4, 1) & Key(3, 4, 2) are hashed to the same slot -> 3 -// Key(3, 4, 5) & Key(1, 4, 3) are hashed to the same slot -> 5 - +int k1 = 1; +int k2 = 3; +int v1 = 10; +int v2 = 30; void threadA(void *arg) { - Key *k1 = new Key(3, 2, 6); - Key *k2 = new Key(1, 1, 1); - Value *v1 = new Value(10, 10, 10); - Value *r1 = table->put(k1, v1); - //printValue(r1); - Value *r2 = table->get(k2); - //printf("Thrd A:\n"); - printValue(r2); + int r1 = put(table, k1, v1); + int r2 = get(table, k2); + printf("r2=%d\n", r2); } void threadB(void *arg) { - Key *k1 = new Key(3, 2, 6); - Key *k2 = new Key(1, 1, 1); - Value *v2 = new Value(30, 40, 50); - Value *r3 = table->put(k2, v2); - //printValue(r3); - Value *r4 = table->get(k1); - printf("Thrd B:\n"); - printValue(r4); + int r3 = put(table, k2, v2); + int r4 = get(table, k1); + printf("r4=%d\n", r4); } int user_main(int argc, char *argv[]) { + thrd_t t1, t2; + /** @Entry */ table = new HashMap; + put(table, k1, 1); + put(table, k2, 1); thrd_create(&t1, threadA, NULL); thrd_create(&t2, threadB, NULL); diff --git a/concurrent-hashmap/testcase2.cc b/concurrent-hashmap/testcase2.cc index 17f79d8..802df3e 100644 --- a/concurrent-hashmap/testcase2.cc +++ b/concurrent-hashmap/testcase2.cc @@ -1,65 +1,32 @@ #include - -#ifdef WILDCARD -#include "hashmap_wildcard.h" -#else #include "hashmap.h" -#endif HashMap *table; -void printKey(Key *key) { - if (key) - printf("pos = (%d, %d, %d)\n", key->x, key->y, key->z); - else - printf("pos = NULL\n"); -} - -void printValue(Value *value) { - if (value) - printf("velocity = (%d, %d, %d)\n", value->vX, value->vY, value->vZ); - else - printf("velocity = NULL\n"); -} - -// Key(3, 2, 6) & Key(1, 3, 3) are hashed to the same slot -> 4 -// Key(1, 1, 1) & Key(3, 2, 2) are hashed to the same slot -> 0 -// Key(2, 4, 1) & Key(3, 4, 2) are hashed to the same slot -> 3 -// Key(3, 4, 5) & Key(1, 4, 3) are hashed to the same slot -> 5 +/** Making w4 & w11 seq_cst */ +int k1 = 1; +int k2 = 3; +int v1 = 10; +int v2 = 30; void threadA(void *arg) { - Key *k1 = new Key(3, 2, 6); - Key *k2 = new Key(1, 1, 1); - Value *v1 = new Value(10, 10, 10); - Value *r1 = table->put(k1, v1); - //printValue(r1); - Value *r2 = table->get(k2); - //printf("Thrd A:\n"); - printValue(r2); + int r1 = put(table, k1, v1); + int r2 = get(table, k2); + printf("r2=%d\n", r2); } void threadB(void *arg) { - Key *k1 = new Key(3, 2, 6); - Key *k2 = new Key(1, 1, 1); - Value *v2 = new Value(30, 40, 50); - Value *r3 = table->put(k2, v2); - //printValue(r3); - Value *r4 = table->get(k1); - printf("Thrd B:\n"); - printValue(r4); + int r3 = put(table, k2, v2); + int r4 = get(table, k1); + printf("r4=%d\n", r4); } int user_main(int argc, char *argv[]) { - Key *k1 = new Key(3, 2, 6); - Key *k2 = new Key(1, 1, 1); - Value *v1 = new Value(111, 111, 111); - Value *v2 = new Value(222, 222, 222); thrd_t t1, t2; + /** @Entry */ table = new HashMap; - table->put(k1, v1); - table->put(k2, v2); thrd_create(&t1, threadA, NULL); thrd_create(&t2, threadB, NULL); diff --git a/concurrent-hashmap/testcase3.cc b/concurrent-hashmap/testcase3.cc deleted file mode 100644 index 5b54a16..0000000 --- a/concurrent-hashmap/testcase3.cc +++ /dev/null @@ -1,81 +0,0 @@ -#include - -#ifdef WILDCARD -#include "hashmap_wildcard.h" -#else -#include "hashmap.h" -#endif - -HashMap *table; - -void printKey(Key *key) { - if (key) - printf("pos = (%d, %d, %d)\n", key->x, key->y, key->z); - else - printf("pos = NULL\n"); -} - -void printValue(Value *value) { - if (value) - printf("velocity = (%d, %d, %d)\n", value->vX, value->vY, value->vZ); - else - printf("velocity = NULL\n"); -} - -// Key(3, 2, 6) & Key(1, 3, 3) are hashed to the same slot -> 4 -// Key(1, 1, 1) & Key(3, 2, 2) are hashed to the same slot -> 0 -// Key(2, 4, 1) & Key(3, 4, 2) are hashed to the same slot -> 3 -// Key(3, 4, 5) & Key(1, 4, 3) & Key(1, 1, 6) are hashed to the same slot -> 5 -// Key(2, 4, 8) & Key(1, 3, 8) -> 9 -// Key(1, 4, 8) -> 10 -// Key(1, 3, 7) -> 8 -// Key(1, 2, 7) -> 7 -// Key(1, 2, 6) -> 6 - -void threadA(void *arg) { - Key *k1 = new Key(3, 4, 5); - Key *k2 = new Key(1, 4, 3); - Key *k3 = new Key(1, 1, 6); - Value *v2 = new Value(10, 10, 10); - Value *r1 = table->put(k2, v2); - //printValue(r1); - Value *r2 = table->get(k3); - printf("k1 -> %d:\n", table->hashKey(k1) % table->capacity); - printf("k2 -> %d:\n", table->hashKey(k2) % table->capacity); - printf("k3 -> %d:\n", table->hashKey(k3) % table->capacity); - //printValue(r2); -} - -void threadB(void *arg) { - Key *k1 = new Key(3, 4, 5); - Key *k2 = new Key(1, 4, 3); - Key *k3 = new Key(1, 1, 6); - Value *v3 = new Value(30, 40, 50); - Value *r3 = table->put(k3, v3); - //printValue(r3); - //Value *r4 = table->get(k1); - //printf("Thrd B:\n"); - //printValue(r4); -} - -int user_main(int argc, char *argv[]) { - Key *k1 = new Key(3, 4, 5); - Key *k2 = new Key(1, 4, 3); - Key *k3 = new Key(1, 1, 6); - //Key *k2 = new Key(1, 3, 3); - Value *v1 = new Value(111, 111, 111); - //Value *v2 = new Value(222, 222, 222); - thrd_t t1, t2; - table = new HashMap; - table->put(k1, v1); - //table->put(k2, v2); - - thrd_create(&t1, threadA, NULL); - thrd_create(&t2, threadB, NULL); - thrd_join(t1); - thrd_join(t2); - - return 0; -} - - diff --git a/count-lines.sh b/count-lines.sh new file mode 100755 index 0000000..8e4081a --- /dev/null +++ b/count-lines.sh @@ -0,0 +1,32 @@ +#!/bin/bash +# + +Files=( + mcs-lock/mcs-lock.h mcs-lock/mcs-lock.cc + linuxrwlocks/linuxrwlocks.h linuxrwlocks/linuxrwlocks.c + concurrent-hashmap/hashmap.h concurrent-hashmap/hashmap.cc + read-copy-update/rcu.h read-copy-update/rcu.cc + seqlock/seqlock.h seqlock/seqlock.cc + ticket-lock/lock.h ticket-lock/lock.c + spsc-bugfix/eventcount.h spsc-bugfix/queue.h spsc-bugfix/queue.cc + mpmc-queue/mpmc-queue.h mpmc-queue/mpmc-queue.cc + chase-lev-deque-bugfix/deque.h chase-lev-deque-bugfix/deque.c + ms-queue/queue.h ms-queue/queue.c +) + +MainFiles=( + linuxrwlocks/main.c + concurrent-hashmap/main.cc + read-copy-update/main.cc + seqlock/main.cc + ticket-lock/main.cc + spsc-bugfix/main.cc + mcs-lock/main.cc + mpmc-queue/main.cc + chase-lev-deque-bugfix/main.c + ms-queue/main.c +) + +echo "cloc ${Files[*]}" + +cloc ${Files[*]} ${MainFiles[*]} diff --git a/dekker-fences/.gitignore b/dekker-fences/.gitignore deleted file mode 100644 index 560aebf..0000000 --- a/dekker-fences/.gitignore +++ /dev/null @@ -1 +0,0 @@ -/dekker-fences diff --git a/dekker-fences/Makefile b/dekker-fences/Makefile deleted file mode 100644 index ffbb77a..0000000 --- a/dekker-fences/Makefile +++ /dev/null @@ -1,11 +0,0 @@ -include ../benchmarks.mk - -TESTNAME = dekker-fences - -all: $(TESTNAME) - -$(TESTNAME): $(TESTNAME).cc - $(CXX) -o $@ $< $(CXXFLAGS) $(LDFLAGS) - -clean: - rm -f $(TESTNAME) *.o diff --git a/dekker-fences/dekker-fences.cc b/dekker-fences/dekker-fences.cc deleted file mode 100644 index eb38d5c..0000000 --- a/dekker-fences/dekker-fences.cc +++ /dev/null @@ -1,91 +0,0 @@ -/* - * Dekker's critical section algorithm, implemented with fences. - * - * URL: - * http://www.justsoftwaresolutions.co.uk/threading/ - */ - -#include -#include - -#include "librace.h" - -std::atomic flag0, flag1; -std::atomic turn; - -uint32_t var = 0; - -void p0(void *arg) -{ - flag0.store(true,std::memory_order_relaxed); - std::atomic_thread_fence(std::memory_order_seq_cst); - - while (flag1.load(std::memory_order_relaxed)) - { - if (turn.load(std::memory_order_relaxed) != 0) - { - flag0.store(false,std::memory_order_relaxed); - while (turn.load(std::memory_order_relaxed) != 0) - { - thrd_yield(); - } - flag0.store(true,std::memory_order_relaxed); - std::atomic_thread_fence(std::memory_order_seq_cst); - } else - thrd_yield(); - } - std::atomic_thread_fence(std::memory_order_acquire); - - // critical section - store_32(&var, 1); - - turn.store(1,std::memory_order_relaxed); - std::atomic_thread_fence(std::memory_order_release); - flag0.store(false,std::memory_order_relaxed); -} - -void p1(void *arg) -{ - flag1.store(true,std::memory_order_relaxed); - std::atomic_thread_fence(std::memory_order_seq_cst); - - while (flag0.load(std::memory_order_relaxed)) - { - if (turn.load(std::memory_order_relaxed) != 1) - { - flag1.store(false,std::memory_order_relaxed); - while (turn.load(std::memory_order_relaxed) != 1) - { - thrd_yield(); - } - flag1.store(true,std::memory_order_relaxed); - std::atomic_thread_fence(std::memory_order_seq_cst); - } else - thrd_yield(); - } - std::atomic_thread_fence(std::memory_order_acquire); - - // critical section - store_32(&var, 2); - - turn.store(0,std::memory_order_relaxed); - std::atomic_thread_fence(std::memory_order_release); - flag1.store(false,std::memory_order_relaxed); -} - -int user_main(int argc, char **argv) -{ - thrd_t a, b; - - flag0 = false; - flag1 = false; - turn = 0; - - thrd_create(&a, p0, NULL); - thrd_create(&b, p1, NULL); - - thrd_join(a); - thrd_join(b); - - return 0; -} diff --git a/elimination-backoff/stack.c b/elimination-backoff/stack.c deleted file mode 100644 index cc4e84e..0000000 --- a/elimination-backoff/stack.c +++ /dev/null @@ -1,95 +0,0 @@ -#include "stack.h" - -Simple_Stack S; -void **location; -int *collision; - -void StackOp (ThreadInfo * pInfo) { - if (TryPerformStackOp (p) == FALSE) - LesOP (p); - return; -} - -void LesOP (ThreadInfo * p) { - while (1) { - location[mypid] = p; - pos = GetPosition (p); - him = collision[pos]; - while (!CAS (&collision[pos], him, mypid)) - him = collision[pos]; - if (him != EMPTY) { - q = location[him]; - if (q != NULL && q->id == him && q->op != p->op) { - if (CAS (&location[mypid], p, NULL)) { - if (TryCollision (p, q) == TRUE) - return; - else - goto stack; - } else { - FinishCollision (p); - return; - } - } - delay (p->spin); - if (!CAS (&location[mypid], p, NULL)) { - FinishCollision (p); - return; - } - stack: - if (TryPerformStackOp (p) == TRUE) - return; - } - } -} - -bool TryPerformStackOp (ThreadInfo * p) { - Cell *phead, *pnext; - if (p->op == PUSH) { - phead = S.ptop; - p->cell.pnext = phead; - if (CAS (&S.ptop, phead, &p->cell)) - return TRUE; - else - return FALSE; - } - if (p->op == POP) { - phead = S.ptop; - if (phead == NULL) { - p->cell = EMPTY; - return TRUE; - } - pnext = phead->pnext; - if (CAS (&S.ptop, phead, pnext)) { - p->cell = *phead; - return TRUE; - } else { - p->cell = EMPTY; - return FALSE; - } - } -} - -void FinishCollision (ProcessInfo * p) { - if (p->op == POP) { - p->pcell = location[mypid]->pcell; - location[mypid] = NULL; - } -} - -void TryCollision (ThreadInfo * p, ThreadInfo * q) { - if (p->op == PUSH) { - if (CAS (&location[him], q, p)) - return TRUE; - else - return FALSE; - } - if (p->op == POP) { - if (CAS (&location[him], q, NULL)) { - p->cell = q->cell; - location[mypid] = NULL; - return TRUE; - } - else - return FALSE; - } -} diff --git a/elimination-backoff/stack.h b/elimination-backoff/stack.h deleted file mode 100644 index 1a0cfd6..0000000 --- a/elimination-backoff/stack.h +++ /dev/null @@ -1,16 +0,0 @@ -struct Cell { - Cell *pnext; - void *pdata; -}; - -struct ThreadInfo { - unsigned int id; - char op; - Cell cell; - int spin; -}; - -struct Simple_Stack { - Cell *ptop; -}; - diff --git a/generate.sh b/generate.sh new file mode 100755 index 0000000..e8cbdb3 --- /dev/null +++ b/generate.sh @@ -0,0 +1,9 @@ +#!/bin/bash + +SpecCompiler=$HOME/spec-checker-compiler + +ClassPath=$SpecCompiler/classes + +Class=edu/uci/eecs/codeGenerator/CodeGenerator + +java -cp $ClassPath $Class $1 diff --git a/include/unrelacy.h b/include/unrelacy.h index 729d76f..c6369e0 100644 --- a/include/unrelacy.h +++ b/include/unrelacy.h @@ -11,19 +11,26 @@ #include #define $ - +#ifndef ASSRT #define ASSERT(expr) MODEL_ASSERT(expr) +#endif #define RL_ASSERT(expr) MODEL_ASSERT(expr) #define RL_NEW new #define RL_DELETE(expr) delete expr -#define mo_seqcst memory_order_relaxed +#define mo_seqcst memory_order_seq_cst #define mo_release memory_order_release #define mo_acquire memory_order_acquire #define mo_acq_rel memory_order_acq_rel #define mo_relaxed memory_order_relaxed +#define seq_cst memory_order_seq_cst +#define release memory_order_release +#define acquire memory_order_acquire +#define acq_rel memory_order_acq_rel +#define relaxed memory_order_relaxed + namespace rl { /* This 'useless' struct is declared just so we can use partial template diff --git a/linuxrwlocks/Makefile b/linuxrwlocks/Makefile index 90dafcf..e5a38d2 100644 --- a/linuxrwlocks/Makefile +++ b/linuxrwlocks/Makefile @@ -1,11 +1,23 @@ include ../benchmarks.mk -TESTNAME = linuxrwlocks +BENCH := linuxrwlocks -all: $(TESTNAME) +BENCH_BINARY := $(BENCH).o -$(TESTNAME): $(TESTNAME).c - $(CC) -o $@ $< $(CFLAGS) $(LDFLAGS) +TESTS := main testcase1 testcase2 testcase3 + +all: $(TESTS) + ../generate.sh $(notdir $(shell pwd)) + +%.o : %.c + $(CC) -c -fPIC -MMD -MF .$@.d -o $@ $< $(CFLAGS) $(LDFLAGS) + +$(TESTS): % : %.o $(BENCH_BINARY) + $(CC) -o $@ $^ $(CFLAGS) $(LDFLAGS) + +-include .*.d clean: - rm -f $(TESTNAME) *.o + rm -rf $(TESTS) *.o .*.d *.dSYM + +.PHONY: clean all diff --git a/linuxrwlocks/linuxrwlocks.c b/linuxrwlocks/linuxrwlocks.c index be3550e..408f35b 100644 --- a/linuxrwlocks/linuxrwlocks.c +++ b/linuxrwlocks/linuxrwlocks.c @@ -3,110 +3,131 @@ #include #include "librace.h" - -#define RW_LOCK_BIAS 0x00100000 -#define WRITE_LOCK_CMP RW_LOCK_BIAS +#include "linuxrwlocks.h" /** Example implementation of linux rw lock along with 2 thread test * driver... */ -typedef union { - atomic_int lock; -} rwlock_t; - -static inline int read_can_lock(rwlock_t *lock) +/** + Properties to check: + 1. At most 1 thread can acquire the write lock, and at the same time, no + other threads can acquire any lock (including read/write lock). + 2. At most RW_LOCK_BIAS threads can successfully acquire the read lock. + 3. A read_unlock release 1 read lock, and a write_unlock release the write + lock. They can not release a lock that they don't acquire. + ### + 4. Read_lock and write_lock can not be grabbed at the same time. + 5. Happpens-before relationship should be checked and guaranteed, which + should be as the following: + a. read_unlock hb-> write_lock + b. write_unlock hb-> write_lock + c. write_unlock hb-> read_lock +*/ + +/** + Interesting point for locks: + a. If the users unlock() before any lock(), then the model checker will fail. + For this case, we can not say that the data structure is buggy, how can we + tell them from a real data structure bug??? + b. We should specify that for a specific thread, successful locks and + unlocks should always come in pairs. We could make this check as an + auxiliary check since it is an extra rule for how the interfaces should called. +*/ + +/** @DeclareState: bool writerLockAcquired; + int readerLockCnt; */ + +int read_can_lock(rwlock_t *lock) { return atomic_load_explicit(&lock->lock, memory_order_relaxed) > 0; } -static inline int write_can_lock(rwlock_t *lock) +int write_can_lock(rwlock_t *lock) { return atomic_load_explicit(&lock->lock, memory_order_relaxed) == RW_LOCK_BIAS; } -static inline void read_lock(rwlock_t *rw) + +/** @PreCondition: return !STATE(writerLockAcquired); +@Transition: STATE(readerLockCnt)++; */ +void read_lock(rwlock_t *rw) { + + /********** Detected Correctness (testcase1) **********/ int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire); + /** @OPDefine: priorvalue > 0 */ while (priorvalue <= 0) { atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed); while (atomic_load_explicit(&rw->lock, memory_order_relaxed) <= 0) { thrd_yield(); } + /********** Detected Correctness (testcase1) **********/ priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire); + /** @OPDefine: priorvalue > 0 */ } } -static inline void write_lock(rwlock_t *rw) + +/** @PreCondition: return !STATE(writerLockAcquired) && STATE(readerLockCnt) == 0; +@Transition: STATE(writerLockAcquired) = true; */ +void write_lock(rwlock_t *rw) { + /********** Detected Correctness (testcase1) **********/ int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire); + /** @OPDefine: priorvalue == RW_LOCK_BIAS */ while (priorvalue != RW_LOCK_BIAS) { atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed); while (atomic_load_explicit(&rw->lock, memory_order_relaxed) != RW_LOCK_BIAS) { thrd_yield(); } + /********** Detected Correctness (testcase1) **********/ priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire); + /** @OPDefine: priorvalue == RW_LOCK_BIAS */ } } -static inline int read_trylock(rwlock_t *rw) +/** @PreCondition: return !C_RET || !STATE(writerLockAcquired); +@Transition: if (C_RET) STATE(readerLockCnt)++; */ +int read_trylock(rwlock_t *rw) { + /********** Detected Correctness (testcase2) **********/ int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire); - if (priorvalue > 0) + /** @OPDefine: true */ + if (priorvalue > 0) { return 1; - + } atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed); return 0; } -static inline int write_trylock(rwlock_t *rw) +/** @PreCondition: return !C_RET || !STATE(writerLockAcquired) && STATE(readerLockCnt) == 0; +@Transition: if (C_RET) STATE(writerLockAcquired) = true; */ +int write_trylock(rwlock_t *rw) { + /********** Detected Correctness (testcase2) **********/ int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire); - if (priorvalue == RW_LOCK_BIAS) + /** @OPDefine: true */ + if (priorvalue == RW_LOCK_BIAS) { return 1; - + } atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed); return 0; } -static inline void read_unlock(rwlock_t *rw) +/** @PreCondition: return STATE(readerLockCnt) > 0 && !STATE(writerLockAcquired); +@Transition: STATE(readerLockCnt)--; */ +void read_unlock(rwlock_t *rw) { + /********** Detected Correctness (testcase1) **********/ atomic_fetch_add_explicit(&rw->lock, 1, memory_order_release); + /** @OPDefine: true */ } -static inline void write_unlock(rwlock_t *rw) +/** @PreCondition: return STATE(readerLockCnt) == 0 && STATE(writerLockAcquired); +@Transition: STATE(writerLockAcquired) = false; */ +void write_unlock(rwlock_t *rw) { + /********** Detected Correctness (testcase1) **********/ atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_release); -} - -rwlock_t mylock; -int shareddata; - -static void a(void *obj) -{ - int i; - for(i = 0; i < 2; i++) { - if ((i % 2) == 0) { - read_lock(&mylock); - load_32(&shareddata); - read_unlock(&mylock); - } else { - write_lock(&mylock); - store_32(&shareddata,(unsigned int)i); - write_unlock(&mylock); - } - } -} - -int user_main(int argc, char **argv) -{ - thrd_t t1, t2; - atomic_init(&mylock.lock, RW_LOCK_BIAS); - - thrd_create(&t1, (thrd_start_t)&a, NULL); - thrd_create(&t2, (thrd_start_t)&a, NULL); - - thrd_join(t1); - thrd_join(t2); - - return 0; + /** @OPDefine: true */ } diff --git a/linuxrwlocks/linuxrwlocks.h b/linuxrwlocks/linuxrwlocks.h new file mode 100644 index 0000000..d417832 --- /dev/null +++ b/linuxrwlocks/linuxrwlocks.h @@ -0,0 +1,34 @@ +#ifndef _LINUXRWLOCKS_H +#define _LINUXRWLOCKS_H + +#include +#include +#include + +#include "librace.h" + +#define RW_LOCK_BIAS 0x00100000 +#define WRITE_LOCK_CMP RW_LOCK_BIAS + +typedef union { + atomic_int lock; +} rwlock_t; + + +int read_can_lock(rwlock_t *lock); + +int write_can_lock(rwlock_t *lock); + +void read_lock(rwlock_t *rw); + +void write_lock(rwlock_t *rw); + +int read_trylock(rwlock_t *rw); + +int write_trylock(rwlock_t *rw); + +void read_unlock(rwlock_t *rw); + +void write_unlock(rwlock_t *rw); + +#endif diff --git a/linuxrwlocks/main.c b/linuxrwlocks/main.c new file mode 100644 index 0000000..a81aa9c --- /dev/null +++ b/linuxrwlocks/main.c @@ -0,0 +1,45 @@ +#include +#include +#include + +#include "librace.h" +#include "linuxrwlocks.h" + +rwlock_t mylock; +int shareddata; + +atomic_int x, y; + +static void a(void *obj) +{ + int i; + for(i = 0; i < 2; i++) { + if ((i % 2) == 0) { + read_lock(&mylock); + load_32(&shareddata); + read_unlock(&mylock); + } else { + write_lock(&mylock); + store_32(&shareddata,(unsigned int)i); + write_unlock(&mylock); + } + } +} + + +int user_main(int argc, char **argv) +{ + thrd_t t1, t2; + atomic_init(&mylock.lock, RW_LOCK_BIAS); + atomic_init(&x, 0); + atomic_init(&y, 0); + + /** @Entry */ + thrd_create(&t1, (thrd_start_t)&a, NULL); + thrd_create(&t2, (thrd_start_t)&a, NULL); + + thrd_join(t1); + thrd_join(t2); + + return 0; +} diff --git a/linuxrwlocks/testcase1.c b/linuxrwlocks/testcase1.c new file mode 100644 index 0000000..8051cdc --- /dev/null +++ b/linuxrwlocks/testcase1.c @@ -0,0 +1,72 @@ +#include +#include +#include + +#include "librace.h" +#include "linuxrwlocks.h" + +rwlock_t mylock; +int shareddata; + +atomic_int x, y; + +static void a(void *obj) +{ + write_lock(&mylock); + //atomic_store_explicit(&x, 17, memory_order_relaxed); + write_unlock(&mylock); + +/* + + if (!write_can_lock(&mylock)) + return; + + if (write_trylock(&mylock)) { + atomic_store_explicit(&x, 17, memory_order_relaxed); + write_unlock(&mylock); + } +*/ +} + +static void b(void *obj) +{ + //if (write_trylock(&mylock)) { + //atomic_store_explicit(&x, 16, memory_order_relaxed); + // write_unlock(&mylock); + //} + + read_lock(&mylock); + //atomic_load_explicit(&x, memory_order_relaxed); + read_unlock(&mylock); + +/* + if (write_trylock(&mylock)) { + atomic_store_explicit(&x, 16, memory_order_relaxed); + write_unlock(&mylock); + } + + if (!read_can_lock(&mylock)) + return; + if (read_trylock(&mylock)) { + atomic_load_explicit(&x, memory_order_relaxed); + read_unlock(&mylock); + } +*/ +} + +int user_main(int argc, char **argv) +{ + thrd_t t1, t2; + atomic_init(&mylock.lock, RW_LOCK_BIAS); + atomic_init(&x, 0); + atomic_init(&y, 0); + + /** @Entry */ + thrd_create(&t1, (thrd_start_t)&a, NULL); + thrd_create(&t2, (thrd_start_t)&b, NULL); + + thrd_join(t1); + thrd_join(t2); + + return 0; +} diff --git a/linuxrwlocks/testcase2.c b/linuxrwlocks/testcase2.c new file mode 100644 index 0000000..77adbbb --- /dev/null +++ b/linuxrwlocks/testcase2.c @@ -0,0 +1,54 @@ +#include +#include +#include + +#include "librace.h" +#include "linuxrwlocks.h" + +rwlock_t mylock; +int shareddata; + +atomic_int x, y; + +static void a(void *obj) +{ + if (!write_can_lock(&mylock)) + return; + + if (write_trylock(&mylock)) { + // atomic_store_explicit(&x, 17, memory_order_relaxed); + write_unlock(&mylock); + } +} + +static void b(void *obj) +{ + if (write_trylock(&mylock)) { + //atomic_store_explicit(&x, 16, memory_order_relaxed); + write_unlock(&mylock); + } + + if (!read_can_lock(&mylock)) + return; + if (read_trylock(&mylock)) { + // atomic_load_explicit(&x, memory_order_relaxed); + read_unlock(&mylock); + } +} + +int user_main(int argc, char **argv) +{ + thrd_t t1, t2; + atomic_init(&mylock.lock, RW_LOCK_BIAS); + atomic_init(&x, 0); + atomic_init(&y, 0); + + /** @Entry */ + thrd_create(&t1, (thrd_start_t)&a, NULL); + thrd_create(&t2, (thrd_start_t)&b, NULL); + + thrd_join(t1); + thrd_join(t2); + + return 0; +} diff --git a/linuxrwlocks/testcase3.c b/linuxrwlocks/testcase3.c new file mode 100644 index 0000000..a6633f4 --- /dev/null +++ b/linuxrwlocks/testcase3.c @@ -0,0 +1,55 @@ +#include +#include +#include + +#include "librace.h" +#include "linuxrwlocks.h" + +rwlock_t mylock; +int shareddata; + +atomic_int x, y; + +static void a(void *obj) +{ + write_lock(&mylock); + atomic_store_explicit(&x, 17, memory_order_relaxed); + write_unlock(&mylock); + + if (!read_can_lock(&mylock)) + return; + if (read_trylock(&mylock)) { + atomic_load_explicit(&x, memory_order_relaxed); + read_unlock(&mylock); + } +} + +static void b(void *obj) +{ + + if (write_trylock(&mylock)) { + atomic_store_explicit(&x, 16, memory_order_relaxed); + write_unlock(&mylock); + } + + read_lock(&mylock); + atomic_load_explicit(&x, memory_order_relaxed); + read_unlock(&mylock); +} + +int user_main(int argc, char **argv) +{ + thrd_t t1, t2; + /** @Entry */ + atomic_init(&mylock.lock, RW_LOCK_BIAS); + atomic_init(&x, 0); + atomic_init(&y, 0); + + thrd_create(&t1, (thrd_start_t)&a, NULL); + thrd_create(&t2, (thrd_start_t)&b, NULL); + + thrd_join(t1); + thrd_join(t2); + + return 0; +} diff --git a/mcs-lock/Makefile b/mcs-lock/Makefile index 5a311b3..b74cd3c 100644 --- a/mcs-lock/Makefile +++ b/mcs-lock/Makefile @@ -1,11 +1,23 @@ include ../benchmarks.mk -TESTNAME = mcs-lock +BENCH := mcs-lock -all: $(TESTNAME) +BENCH_BINARY := $(BENCH).o -$(TESTNAME): $(TESTNAME).cc $(TESTNAME).h - $(CXX) -o $@ $< $(CXXFLAGS) $(LDFLAGS) +TESTS := main testcase + +all: $(TESTS) + ../generate.sh $(notdir $(shell pwd)) + +%.o : %.cc + $(CXX) -c -fPIC -MMD -MF .$@.d -o $@ $< $(CXXFLAGS) $(LDFLAGS) + +$(TESTS): % : %.o $(BENCH_BINARY) + $(CXX) -o $@ $^ $(CXXFLAGS) $(LDFLAGS) + +-include .*.d clean: - rm -f $(TESTNAME) *.o + rm -rf $(TESTS) *.o .*.d *.dSYM + +.PHONY: clean all diff --git a/mcs-lock/main.cc b/mcs-lock/main.cc new file mode 100644 index 0000000..052dd5b --- /dev/null +++ b/mcs-lock/main.cc @@ -0,0 +1,47 @@ +#include +#include + +#include "mcs-lock.h" + +/* For data race instrumentation */ +#include "librace.h" + +struct mcs_mutex *mutex; +static uint32_t shared; + +void threadA(void *arg) +{ + mcs_mutex::guard g(mutex); + //printf("store: %d\n", 17); + //store_32(&shared, 17); + mcs_unlock(mutex, &g); + //mutex->unlock(&g); + mcs_lock(mutex, &g); + //mutex->lock(&g); + //printf("load: %u\n", load_32(&shared)); +} + +void threadB(void *arg) +{ + mcs_mutex::guard g(mutex); + //printf("load: %u\n", load_32(&shared)); + mcs_unlock(mutex, &g); + //mutex->unlock(&g); + mcs_lock(mutex, &g); + //mutex->lock(&g); + //printf("store: %d\n", 17); + //store_32(&shared, 17); +} + +int user_main(int argc, char **argv) +{ + thrd_t A, B; + + mutex = new mcs_mutex(); + /** @Entry */ + thrd_create(&A, &threadA, NULL); + thrd_create(&B, &threadB, NULL); + thrd_join(A); + thrd_join(B); + return 0; +} diff --git a/mcs-lock/mcs-lock.cc b/mcs-lock/mcs-lock.cc index ec0cc5d..a6e8725 100644 --- a/mcs-lock/mcs-lock.cc +++ b/mcs-lock/mcs-lock.cc @@ -1,43 +1,96 @@ -#include -#include - #include "mcs-lock.h" -/* For data race instrumentation */ -#include "librace.h" +void mcs_mutex::lock(guard * I) { + mcs_node * me = &(I->m_node); + + // set up my node : + // not published yet so relaxed : + me->next.store(NULL, std::mo_relaxed ); + me->gate.store(1, std::mo_relaxed ); + + /********** Detected Correctness **********/ + /** Run this in the -Y mode to expose the HB bug */ + // publish my node as the new tail : + mcs_node * pred = m_tail.exchange(me, std::mo_acq_rel); + /** @OPDefine: pred == NULL */ + if ( pred != NULL ) { + // (*1) race here + // unlock of pred can see me in the tail before I fill next -struct mcs_mutex *mutex; -static uint32_t shared; + // FIXME: detection miss, execution never ends + // If this is relaxed, the store 0 to gate will be read before and + // that lock will never ends. + // publish me to previous lock-holder : + pred->next.store(me, std::mo_release ); -void threadA(void *arg) -{ - mcs_mutex::guard g(mutex); - printf("store: %d\n", 17); - store_32(&shared, 17); - mutex->unlock(&g); - mutex->lock(&g); - printf("load: %u\n", load_32(&shared)); + // (*2) pred not touched any more + + // now this is the spin - + // wait on predecessor setting my flag - + rl::linear_backoff bo; + /********** Detected Correctness *********/ + /** Run this in the -Y mode to expose the HB bug */ + while ( me->gate.load(std::mo_acquire) ) { + thrd_yield(); + } + /** @OPDefine: true */ + } } -void threadB(void *arg) -{ - mcs_mutex::guard g(mutex); - printf("load: %u\n", load_32(&shared)); - mutex->unlock(&g); - mutex->lock(&g); - printf("store: %d\n", 17); - store_32(&shared, 17); +void mcs_mutex::unlock(guard * I) { + mcs_node * me = &(I->m_node); + + // FIXME: detection miss, execution never ends + mcs_node * next = me->next.load(std::mo_acquire); + if ( next == NULL ) + { + mcs_node * tail_was_me = me; + /********** Detected Correctness **********/ + /** Run this in the -Y mode to expose the HB bug */ + if ( m_tail.compare_exchange_strong( + tail_was_me,NULL,std::mo_acq_rel) ) { + // got null in tail, mutex is unlocked + /** @OPDefine: true */ + return; + } + + // (*1) catch the race : + rl::linear_backoff bo; + for(;;) { + // FIXME: detection miss, execution never ends + next = me->next.load(std::mo_acquire); + if ( next != NULL ) + break; + thrd_yield(); + } + } + + // (*2) - store to next must be done, + // so no locker can be viewing my node any more + + /********** Detected Correctness **********/ + /** Run this in the -Y mode to expose the HB bug */ + // let next guy in : + next->gate.store( 0, std::mo_release); + /** @OPDefine: true */ } -int user_main(int argc, char **argv) -{ - thrd_t A, B; +// C-callable interface + +/** @DeclareState: bool lock; + @Initial: lock = false; */ - mutex = new mcs_mutex(); - thrd_create(&A, &threadA, NULL); - thrd_create(&B, &threadB, NULL); - thrd_join(A); - thrd_join(B); - return 0; +/** @PreCondition: return STATE(lock) == false; +@Transition: STATE(lock) = true; */ +void mcs_lock(mcs_mutex *mutex, CGuard guard) { + mcs_mutex::guard *myGuard = (mcs_mutex::guard*) guard; + mutex->lock(myGuard); +} + +/** @PreCondition: return STATE(lock) == true; +@Transition: STATE(lock) = false; */ +void mcs_unlock(mcs_mutex *mutex, CGuard guard) { + mcs_mutex::guard *myGuard = (mcs_mutex::guard*) guard; + mutex->unlock(myGuard); } diff --git a/mcs-lock/mcs-lock.h b/mcs-lock/mcs-lock.h index 4b808f7..012d04c 100644 --- a/mcs-lock/mcs-lock.h +++ b/mcs-lock/mcs-lock.h @@ -1,8 +1,16 @@ // mcs on stack +#ifndef _MCS_LOCK_H +#define _MCS_LOCK_H + #include +#include #include +// Forward declaration +struct mcs_node; +struct mcs_mutex; + struct mcs_node { std::atomic next; std::atomic gate; @@ -13,6 +21,12 @@ struct mcs_node { } }; +// C-callable interface +typedef void *CGuard; +void mcs_lock(mcs_mutex *mutex, CGuard guard); + +void mcs_unlock(mcs_mutex *mutex, CGuard guard); + struct mcs_mutex { public: // tail is null when lock is not held @@ -22,72 +36,22 @@ public: m_tail.store( NULL ); } ~mcs_mutex() { - ASSERT( m_tail.load() == NULL ); + RL_ASSERT( m_tail.load() == NULL ); } class guard { public: mcs_mutex * m_t; mcs_node m_node; // node held on the stack - - guard(mcs_mutex * t) : m_t(t) { t->lock(this); } - ~guard() { m_t->unlock(this); } + + // Call the wrapper (instrument every lock/unlock) + guard(mcs_mutex * t) : m_t(t) { mcs_lock(t, this); } + ~guard() { mcs_unlock(m_t, this); } }; - void lock(guard * I) { - mcs_node * me = &(I->m_node); - - // set up my node : - // not published yet so relaxed : - me->next.store(NULL, std::mo_relaxed ); - me->gate.store(1, std::mo_relaxed ); - - // publish my node as the new tail : - mcs_node * pred = m_tail.exchange(me, std::mo_acq_rel); - if ( pred != NULL ) { - // (*1) race here - // unlock of pred can see me in the tail before I fill next - - // publish me to previous lock-holder : - pred->next.store(me, std::mo_release ); - - // (*2) pred not touched any more + void lock(guard * I); - // now this is the spin - - // wait on predecessor setting my flag - - rl::linear_backoff bo; - while ( me->gate.load(std::mo_acquire) ) { - thrd_yield(); - } - } - } - - void unlock(guard * I) { - mcs_node * me = &(I->m_node); - - mcs_node * next = me->next.load(std::mo_acquire); - if ( next == NULL ) - { - mcs_node * tail_was_me = me; - if ( m_tail.compare_exchange_strong( tail_was_me,NULL,std::mo_acq_rel) ) { - // got null in tail, mutex is unlocked - return; - } - - // (*1) catch the race : - rl::linear_backoff bo; - for(;;) { - next = me->next.load(std::mo_acquire); - if ( next != NULL ) - break; - thrd_yield(); - } - } - - // (*2) - store to next must be done, - // so no locker can be viewing my node any more - - // let next guy in : - next->gate.store( 0, std::mo_release ); - } + void unlock(guard * I); }; + +#endif diff --git a/mcs-lock/testcase.cc b/mcs-lock/testcase.cc new file mode 100644 index 0000000..052dd5b --- /dev/null +++ b/mcs-lock/testcase.cc @@ -0,0 +1,47 @@ +#include +#include + +#include "mcs-lock.h" + +/* For data race instrumentation */ +#include "librace.h" + +struct mcs_mutex *mutex; +static uint32_t shared; + +void threadA(void *arg) +{ + mcs_mutex::guard g(mutex); + //printf("store: %d\n", 17); + //store_32(&shared, 17); + mcs_unlock(mutex, &g); + //mutex->unlock(&g); + mcs_lock(mutex, &g); + //mutex->lock(&g); + //printf("load: %u\n", load_32(&shared)); +} + +void threadB(void *arg) +{ + mcs_mutex::guard g(mutex); + //printf("load: %u\n", load_32(&shared)); + mcs_unlock(mutex, &g); + //mutex->unlock(&g); + mcs_lock(mutex, &g); + //mutex->lock(&g); + //printf("store: %d\n", 17); + //store_32(&shared, 17); +} + +int user_main(int argc, char **argv) +{ + thrd_t A, B; + + mutex = new mcs_mutex(); + /** @Entry */ + thrd_create(&A, &threadA, NULL); + thrd_create(&B, &threadB, NULL); + thrd_join(A); + thrd_join(B); + return 0; +} diff --git a/mpmc-queue/Makefile b/mpmc-queue/Makefile index 8d9ad1e..0d14989 100644 --- a/mpmc-queue/Makefile +++ b/mpmc-queue/Makefile @@ -1,22 +1,23 @@ include ../benchmarks.mk -TESTNAME = mpmc-queue -TESTS = mpmc-queue mpmc-1r2w mpmc-2r1w mpmc-queue-rdwr -TESTS += mpmc-queue-noinit mpmc-1r2w-noinit mpmc-2r1w-noinit mpmc-rdwr-noinit +BENCH := mpmc-queue + +BENCH_BINARY := $(BENCH).o + +TESTS := main testcase1 testcase2 all: $(TESTS) + ../generate.sh $(notdir $(shell pwd)) -mpmc-queue: CPPFLAGS += -DCONFIG_MPMC_READERS=2 -DCONFIG_MPMC_WRITERS=2 -mpmc-queue-rdwr: CPPFLAGS += -DCONFIG_MPMC_READERS=0 -DCONFIG_MPMC_WRITERS=0 -DCONFIG_MPMC_RDWR=2 -mpmc-1r2w: CPPFLAGS += -DCONFIG_MPMC_READERS=1 -DCONFIG_MPMC_WRITERS=2 -mpmc-2r1w: CPPFLAGS += -DCONFIG_MPMC_READERS=2 -DCONFIG_MPMC_WRITERS=1 -mpmc-queue-noinit: CPPFLAGS += -DCONFIG_MPMC_READERS=2 -DCONFIG_MPMC_WRITERS=2 -DCONFIG_MPMC_NO_INITIAL_ELEMENT -mpmc-1r2w-noinit: CPPFLAGS += -DCONFIG_MPMC_READERS=1 -DCONFIG_MPMC_WRITERS=2 -DCONFIG_MPMC_NO_INITIAL_ELEMENT -mpmc-2r1w-noinit: CPPFLAGS += -DCONFIG_MPMC_READERS=2 -DCONFIG_MPMC_WRITERS=1 -DCONFIG_MPMC_NO_INITIAL_ELEMENT -mpmc-rdwr-noinit: CPPFLAGS += -DCONFIG_MPMC_READERS=0 -DCONFIG_MPMC_WRITERS=0 -DCONFIG_MPMC_RDWR=2 -DCONFIG_MPMC_NO_INITIAL_ELEMENT +%.o : %.cc + $(CXX) -c -fPIC -MMD -MF .$@.d -o $@ $< $(CXXFLAGS) $(LDFLAGS) -$(TESTS): $(TESTNAME).cc $(TESTNAME).h - $(CXX) -o $@ $< $(CXXFLAGS) $(LDFLAGS) +$(TESTS): % : %.o $(BENCH_BINARY) + $(CXX) -o $@ $^ $(CXXFLAGS) $(LDFLAGS) + +-include .*.d clean: - rm -f $(TESTS) *.o + rm -rf $(TESTS) *.o .*.d *.dSYM + +.PHONY: clean all diff --git a/mpmc-queue/main.cc b/mpmc-queue/main.cc new file mode 100644 index 0000000..8aa3b76 --- /dev/null +++ b/mpmc-queue/main.cc @@ -0,0 +1,60 @@ +#include +#include +#include + +#include "mpmc-queue.h" + +atomic_int x; + +void threadA(struct mpmc_boundq_1_alt *queue) +{ + int32_t *bin = write_prepare(queue); + //store_32(bin, 1); + write_publish(queue, bin); +} + +void threadB(struct mpmc_boundq_1_alt *queue) +{ + int32_t *bin; + if ((bin = read_fetch(queue)) != NULL) { + //printf("Read: %d\n", load_32(bin)); + read_consume(queue, bin); + } +} + +void threadC(struct mpmc_boundq_1_alt *queue) +{ + int32_t *bin = write_prepare(queue); + //store_32(bin, 1); + write_publish(queue, bin); + + while ((bin = read_fetch(queue)) != NULL) { + //printf("Read: %d\n", load_32(bin)); + read_consume(queue, bin); + } +} + + +int user_main(int argc, char **argv) +{ + mpmc_boundq_1_alt *queue = createMPMC(16); + thrd_t t1, t2; + /** @Entry */ + /* + int32_t *bin = write_prepare(queue); + store_32(bin, 1); + write_publish(queue, bin); + */ + printf("Start threads\n"); + + thrd_create(&t1, (thrd_start_t)&threadC, queue); + thrd_create(&t2, (thrd_start_t)&threadC, queue); + + thrd_join(t1); + thrd_join(t2); + + printf("Threads complete\n"); + + //destroyMPMC(queue); + return 0; +} diff --git a/mpmc-queue/mpmc-queue.cc b/mpmc-queue/mpmc-queue.cc index 7de14d5..0b6999e 100644 --- a/mpmc-queue/mpmc-queue.cc +++ b/mpmc-queue/mpmc-queue.cc @@ -1,140 +1,120 @@ -#include -#include -#include -#include -#include +#include +#include "mpmc-queue.h" -#include +template +t_element * mpmc_boundq_1_alt::read_fetch() { + // FIXME: We can have a relaxed for sure here since the next CAS + // will fix the problem + unsigned int rdwr = m_rdwr.load(mo_acquire); + unsigned int rd,wr; + for(;;) { + rd = (rdwr>>16) & 0xFFFF; + wr = rdwr & 0xFFFF; -#include "mpmc-queue.h" + if ( wr == rd ) // empty + return NULL; -void threadA(struct mpmc_boundq_1_alt *queue) -{ - int32_t *bin = queue->write_prepare(); - store_32(bin, 1); - queue->write_publish(); -} + if ( m_rdwr.compare_exchange_weak(rdwr,rdwr+(1<<16),mo_acq_rel) ) + break; + else + thrd_yield(); + } -void threadB(struct mpmc_boundq_1_alt *queue) -{ - int32_t *bin; - while ((bin = queue->read_fetch()) != NULL) { - printf("Read: %d\n", load_32(bin)); - queue->read_consume(); + // (*1) + rl::backoff bo; + /********** Detected Admissibility (testcase1) **********/ + while ( (m_written.load(mo_acquire) & 0xFFFF) != wr ) { + thrd_yield(); } -} + /** @OPDefine: true */ -void threadC(struct mpmc_boundq_1_alt *queue) -{ - int32_t *bin = queue->write_prepare(); - store_32(bin, 1); - queue->write_publish(); + t_element * p = & ( m_array[ rd % t_size ] ); - while ((bin = queue->read_fetch()) != NULL) { - printf("Read: %d\n", load_32(bin)); - queue->read_consume(); - } + return p; } -#define MAXREADERS 3 -#define MAXWRITERS 3 -#define MAXRDWR 3 -#ifdef CONFIG_MPMC_READERS -#define DEFAULT_READERS (CONFIG_MPMC_READERS) -#else -#define DEFAULT_READERS 2 -#endif - -#ifdef CONFIG_MPMC_WRITERS -#define DEFAULT_WRITERS (CONFIG_MPMC_WRITERS) -#else -#define DEFAULT_WRITERS 2 -#endif +template +void mpmc_boundq_1_alt::read_consume(t_element *bin) { + /********** Detected Admissibility (testcase2) **********/ + // run with -Y + m_read.fetch_add(1,mo_release); + /** @OPDefine: true */ +} -#ifdef CONFIG_MPMC_RDWR -#define DEFAULT_RDWR (CONFIG_MPMC_RDWR) -#else -#define DEFAULT_RDWR 0 -#endif -int readers = DEFAULT_READERS, writers = DEFAULT_WRITERS, rdwr = DEFAULT_RDWR; +template +t_element * mpmc_boundq_1_alt::write_prepare() { + // FIXME: We can have a relaxed for sure here since the next CAS + // will fix the problem + unsigned int rdwr = m_rdwr.load(mo_acquire); + unsigned int rd,wr; + for(;;) { + rd = (rdwr>>16) & 0xFFFF; + wr = rdwr & 0xFFFF; -void print_usage() -{ - printf("Error: use the following options\n" - " -r Choose number of reader threads\n" - " -w Choose number of writer threads\n"); - exit(EXIT_FAILURE); -} + if ( wr == ((rd + t_size)&0xFFFF) ) // full + return NULL; -void process_params(int argc, char **argv) -{ - const char *shortopts = "hr:w:"; - int opt; - bool error = false; - - while (!error && (opt = getopt(argc, argv, shortopts)) != -1) { - switch (opt) { - case 'h': - print_usage(); - break; - case 'r': - readers = atoi(optarg); - break; - case 'w': - writers = atoi(optarg); + if ( m_rdwr.compare_exchange_weak(rdwr,(rd<<16) | ((wr+1)&0xFFFF),mo_acq_rel) ) break; - default: /* '?' */ - error = true; - break; - } + else + thrd_yield(); + } + + // (*1) + rl::backoff bo; + /********** Detected Admissibility (testcase2) **********/ + // run with -Y + while ( (m_read.load(mo_acquire) & 0xFFFF) != rd ) { + thrd_yield(); } + /** @OPDefine: true */ - if (writers < 1 || writers > MAXWRITERS) - error = true; - if (readers < 1 || readers > MAXREADERS) - error = true; + t_element * p = & ( m_array[ wr % t_size ] ); - if (error) - print_usage(); + return p; } -int user_main(int argc, char **argv) +template +void mpmc_boundq_1_alt::write_publish(t_element *bin) { - struct mpmc_boundq_1_alt queue; - thrd_t A[MAXWRITERS], B[MAXREADERS], C[MAXRDWR]; + /********** Detected Admissibility (testcase1) **********/ + m_written.fetch_add(1,mo_release); + /** @OPDefine: true */ +} - /* Note: optarg() / optind is broken in model-checker - workaround is - * to just copy&paste this test a few times */ - //process_params(argc, argv); - printf("%d reader(s), %d writer(s)\n", readers, writers); +/** @DeclareState: + @Commutativity: write_prepare <-> write_publish (M1->C_RET == M2->bin) + @Commutativity: write_publish <-> read_fetch (M1->bin == M2->C_RET) + @Commutativity: read_fetch <-> read_consume (M1->C_RET == M2->bin) + @Commutativity: read_consume <-> write_prepare (M1->bin == M2->C_RET) */ -#ifndef CONFIG_MPMC_NO_INITIAL_ELEMENT - printf("Adding initial element\n"); - int32_t *bin = queue.write_prepare(); - store_32(bin, 17); - queue.write_publish(); -#endif - printf("Start threads\n"); +mpmc_boundq_1_alt* createMPMC(int size) { + return new mpmc_boundq_1_alt(size); +} - for (int i = 0; i < writers; i++) - thrd_create(&A[i], (thrd_start_t)&threadA, &queue); - for (int i = 0; i < readers; i++) - thrd_create(&B[i], (thrd_start_t)&threadB, &queue); +void destroyMPMC(mpmc_boundq_1_alt *q) { + delete q; +} - for (int i = 0; i < rdwr; i++) - thrd_create(&C[i], (thrd_start_t)&threadC, &queue); +/** @PreCondition: */ +int32_t * read_fetch(mpmc_boundq_1_alt *q) { + return q->read_fetch(); +} - for (int i = 0; i < writers; i++) - thrd_join(A[i]); - for (int i = 0; i < readers; i++) - thrd_join(B[i]); - for (int i = 0; i < rdwr; i++) - thrd_join(C[i]); +/** @PreCondition: */ +void read_consume(mpmc_boundq_1_alt *q, int32_t *bin) { + q->read_consume(bin); +} - printf("Threads complete\n"); +/** @PreCondition: */ +int32_t * write_prepare(mpmc_boundq_1_alt *q) { + return q->write_prepare(); +} - return 0; +/** @PreCondition: */ +void write_publish(mpmc_boundq_1_alt *q, int32_t *bin) { + q->write_publish(bin); } diff --git a/mpmc-queue/mpmc-queue.h b/mpmc-queue/mpmc-queue.h index 47af8ea..cee5471 100644 --- a/mpmc-queue/mpmc-queue.h +++ b/mpmc-queue/mpmc-queue.h @@ -1,13 +1,17 @@ +#ifndef _MPMC_QUEUE_H +#define _MPMC_QUEUE_H + #include #include -template +template struct mpmc_boundq_1_alt { private: - + // buffer capacity + size_t t_size; // elements should generally be cache-line-size padded : - t_element m_array[t_size]; + t_element *m_array; // rdwr counts the reads & writes that have started atomic m_rdwr; @@ -17,8 +21,10 @@ private: public: - mpmc_boundq_1_alt() + mpmc_boundq_1_alt(int size) { + t_size = size; + m_array = new t_element[size]; m_rdwr = 0; m_read = 0; m_written = 0; @@ -26,72 +32,25 @@ public: //----------------------------------------------------- - t_element * read_fetch() { - unsigned int rdwr = m_rdwr.load(mo_acquire); - unsigned int rd,wr; - for(;;) { - rd = (rdwr>>16) & 0xFFFF; - wr = rdwr & 0xFFFF; - - if ( wr == rd ) // empty - return NULL; - - if ( m_rdwr.compare_exchange_weak(rdwr,rdwr+(1<<16),mo_acq_rel) ) - break; - else - thrd_yield(); - } - - // (*1) - rl::backoff bo; - while ( (m_written.load(mo_acquire) & 0xFFFF) != wr ) { - thrd_yield(); - } - - t_element * p = & ( m_array[ rd % t_size ] ); - - return p; - } - - void read_consume() { - m_read.fetch_add(1,mo_release); - } + t_element * read_fetch(); - //----------------------------------------------------- + void read_consume(t_element *bin); - t_element * write_prepare() { - unsigned int rdwr = m_rdwr.load(mo_acquire); - unsigned int rd,wr; - for(;;) { - rd = (rdwr>>16) & 0xFFFF; - wr = rdwr & 0xFFFF; + t_element * write_prepare(); - if ( wr == ((rd + t_size)&0xFFFF) ) // full - return NULL; + void write_publish(t_element *bin); +}; - if ( m_rdwr.compare_exchange_weak(rdwr,(rd<<16) | ((wr+1)&0xFFFF),mo_acq_rel) ) - break; - else - thrd_yield(); - } +mpmc_boundq_1_alt* createMPMC(int size); - // (*1) - rl::backoff bo; - while ( (m_read.load(mo_acquire) & 0xFFFF) != rd ) { - thrd_yield(); - } +void destroyMPMC(mpmc_boundq_1_alt *q); - t_element * p = & ( m_array[ wr % t_size ] ); +int32_t * read_fetch(mpmc_boundq_1_alt *q); - return p; - } +void read_consume(mpmc_boundq_1_alt *q, int32_t *bin); - void write_publish() - { - m_written.fetch_add(1,mo_release); - } - - //----------------------------------------------------- +int32_t * write_prepare(mpmc_boundq_1_alt *q); +void write_publish(mpmc_boundq_1_alt *q, int32_t *bin); -}; +#endif diff --git a/mpmc-queue/testcase1.cc b/mpmc-queue/testcase1.cc new file mode 100644 index 0000000..5310bee --- /dev/null +++ b/mpmc-queue/testcase1.cc @@ -0,0 +1,58 @@ +#include +#include +#include + +#include "mpmc-queue.h" + +atomic_int x; + +void threadA(struct mpmc_boundq_1_alt *queue) +{ + int32_t *bin = write_prepare(queue); + //store_32(bin, 1); + write_publish(queue, bin); +} + +void threadB(struct mpmc_boundq_1_alt *queue) +{ + int32_t *bin; + if ((bin = read_fetch(queue)) != NULL) { + //printf("Read: %d\n", load_32(bin)); + read_consume(queue, bin); + } +} + +void threadC(struct mpmc_boundq_1_alt *queue) +{ + int32_t *bin = write_prepare(queue); + //store_32(bin, 1); + write_publish(queue, bin); + + while ((bin = read_fetch(queue)) != NULL) { + //printf("Read: %d\n", load_32(bin)); + read_consume(queue, bin); + } +} + + +int user_main(int argc, char **argv) +{ + mpmc_boundq_1_alt *queue = createMPMC(2); + thrd_t A, B, C; + /** @Entry */ + x.store(0); + printf("Start threads\n"); + + thrd_create(&A, (thrd_start_t)&threadA, queue); + thrd_create(&B, (thrd_start_t)&threadB, queue); + //thrd_create(&C, (thrd_start_t)&threadC, queue); + + thrd_join(A); + thrd_join(B); + //thrd_join(C); + + printf("Threads complete\n"); + + destroyMPMC(queue); + return 0; +} diff --git a/mpmc-queue/testcase2.cc b/mpmc-queue/testcase2.cc new file mode 100644 index 0000000..3f63f80 --- /dev/null +++ b/mpmc-queue/testcase2.cc @@ -0,0 +1,69 @@ +#include +#include +#include + +#include "mpmc-queue.h" + +atomic_int x; + +void threadA(struct mpmc_boundq_1_alt *queue) +{ + int32_t *bin = write_prepare(queue); + if (bin) { + //printf("Thread A: bin=%d", bin); + //store_32(bin, 1); + write_publish(queue, bin); + } +} + +void threadB(struct mpmc_boundq_1_alt *queue) +{ + int32_t *bin; + if ((bin = read_fetch(queue)) != NULL) { + //printf("Read: %d\n", load_32(bin)); + read_consume(queue, bin); + } +} + +void threadC(struct mpmc_boundq_1_alt *queue) +{ + int32_t *bin = write_prepare(queue); + if (bin) { + //store_32(bin, 1); + write_publish(queue, bin); + } + + while ((bin = read_fetch(queue)) != NULL) { + //printf("Read: %d\n", load_32(bin)); + read_consume(queue, bin); + } +} + + +int user_main(int argc, char **argv) +{ + mpmc_boundq_1_alt *queue = createMPMC(2); + thrd_t A, B, C; + /** @Entry */ + + // A queue of capacity 2, 2 writes happened very early + int32_t *bin = write_prepare(queue); + write_publish(queue, bin); + bin = write_prepare(queue); + write_publish(queue, bin); + + printf("Start threads\n"); + + thrd_create(&A, (thrd_start_t)&threadA, queue); + thrd_create(&B, (thrd_start_t)&threadB, queue); + //thrd_create(&C, (thrd_start_t)&threadC, queue); + + thrd_join(A); + thrd_join(B); + //thrd_join(C); + + printf("Threads complete\n"); + + destroyMPMC(queue); + return 0; +} diff --git a/ms-queue-loose/Makefile b/ms-queue-loose/Makefile new file mode 100644 index 0000000..a50ca70 --- /dev/null +++ b/ms-queue-loose/Makefile @@ -0,0 +1,23 @@ +include ../benchmarks.mk + +BENCH := queue + +BENCH_BINARY := $(BENCH).o + +TESTS := main testcase1 testcase2 testcase3 testcase4 + +all: $(TESTS) + ../generate.sh $(notdir $(shell pwd)) + +%.o : %.c + $(CC) -c -fPIC -MMD -MF .$@.d -o $@ $< $(CFLAGS) $(LDFLAGS) + +$(TESTS): % : %.o $(BENCH_BINARY) + $(CC) -o $@ $^ $(CFLAGS) $(LDFLAGS) + +-include .*.d + +clean: + rm -rf $(TESTS) *.o .*.d *.dSYM + +.PHONY: clean all diff --git a/ms-queue-loose/main.c b/ms-queue-loose/main.c new file mode 100644 index 0000000..a148ad4 --- /dev/null +++ b/ms-queue-loose/main.c @@ -0,0 +1,86 @@ +#include +#include +#include + +#include "queue.h" +#include "model-assert.h" + +static queue_t *queue; +static thrd_t *threads; +static unsigned int *input; +static unsigned int *output; +static int num_threads; + +int get_thread_num() +{ + thrd_t curr = thrd_current(); + int i; + for (i = 0; i < num_threads; i++) + if (curr.priv == threads[i].priv) + return i; + MODEL_ASSERT(0); + return -1; +} + +bool succ1, succ2; +atomic_int x[3]; +unsigned int idx1, idx2; +unsigned int reclaimNode; + +static int procs = 2; +static void main_task(void *param) +{ + unsigned int val; + int pid = *((int *)param); + if (pid % 2 == 0) { + enqueue(queue, 0, 0); + succ1 = dequeue(queue, &idx1, &reclaimNode); + } else { + enqueue(queue, 1, 0); + succ2 = dequeue(queue, &idx2, &reclaimNode); + } +} + +int user_main(int argc, char **argv) +{ + int i; + int *param; + unsigned int in_sum = 0, out_sum = 0; + + /** @Entry */ + queue = (queue_t*) calloc(1, sizeof(*queue)); + MODEL_ASSERT(queue); + + num_threads = procs; + threads = (thrd_t*) malloc(num_threads * sizeof(thrd_t)); + param = (int*) malloc(num_threads * sizeof(*param)); + input = (unsigned int *) calloc(num_threads, sizeof(*input)); + output = (unsigned int *) calloc(num_threads, sizeof(*output)); + + init_queue(queue, num_threads); + for (i = 0; i < num_threads; i++) { + param[i] = i; + thrd_create(&threads[i], main_task, ¶m[i]); + } + for (i = 0; i < num_threads; i++) + thrd_join(threads[i]); +/* + for (i = 0; i < num_threads; i++) { + in_sum += input[i]; + out_sum += output[i]; + } + for (i = 0; i < num_threads; i++) + printf("input[%d] = %u\n", i, input[i]); + for (i = 0; i < num_threads; i++) + printf("output[%d] = %u\n", i, output[i]); + if (succ1 && succ2) + MODEL_ASSERT(in_sum == out_sum); + else + MODEL_ASSERT (false); +*/ + free(param); + free(threads); + free(queue); + + return 0; +} diff --git a/ms-queue/my_queue.c b/ms-queue-loose/queue.c similarity index 60% rename from ms-queue/my_queue.c rename to ms-queue-loose/queue.c index 6c0ccd4..4ac901e 100644 --- a/ms-queue/my_queue.c +++ b/ms-queue-loose/queue.c @@ -3,7 +3,7 @@ #include "librace.h" #include "model-assert.h" -#include "my_queue.h" +#include "queue.h" #define relaxed memory_order_relaxed #define release memory_order_release @@ -22,9 +22,11 @@ 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; } } @@ -33,6 +35,13 @@ static unsigned int new_node() return 0; } +/* Simulate the fact that when a node got recycled, it will get assigned to the + * same queue or for other usage */ +void simulateRecycledNodeUpdate(queue_t *q, unsigned int node) { + atomic_store_explicit(&q->nodes[node].next, -1, memory_order_release); +} + + /* Place this node index back on this thread's free list */ static void reclaim(unsigned int node) { @@ -40,20 +49,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) @@ -62,7 +73,7 @@ void init_queue(queue_t *q, int num_threads) /* Initialize each thread's free list with INITIAL_FREE pointers */ /* The actual nodes are initialized with poison indexes */ - free_lists = malloc(num_threads * sizeof(*free_lists)); + free_lists = ( unsigned int (*)[MAX_FREELIST] ) malloc(num_threads * sizeof(*free_lists)); for (i = 0; i < num_threads; i++) { for (j = 0; j < INITIAL_FREE; j++) { free_lists[i][j] = 2 + i * MAX_FREELIST + j; @@ -76,7 +87,12 @@ void init_queue(queue_t *q, int num_threads) atomic_init(&q->nodes[1].next, MAKE_POINTER(0, 0)); } -void enqueue(queue_t *q, unsigned int val) +/** @DeclareState: IntList *q; +@Commutativity: enqueue <-> dequeue (true) +@Commutativity: dequeue <-> dequeue (!M1->RET || !M2->RET) */ + +/** @Transition: STATE(q)->push_back(val); */ +void enqueue(queue_t *q, unsigned int val, int n) { int success = 0; unsigned int node; @@ -85,28 +101,36 @@ 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); + // This is a found bug in AutoMO, and testcase4 can reveal this known bug + atomic_store_explicit(&q->nodes[node].next, tmp, release); while (!success) { + /********** Detected UL **********/ tail = atomic_load_explicit(&q->tail, acquire); + /********** Detected Admissibility (testcase4) **********/ next = atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire); 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); + /********** Detected Correctness (testcase1) **********/ success = atomic_compare_exchange_strong_explicit(&q->nodes[get_ptr(tail)].next, &next, value, release, release); + /** @OPClearDefine: success */ } if (!success) { + /********** 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); + /********** Detected Correctness (testcase2) **********/ atomic_compare_exchange_strong_explicit(&q->tail, &tail, value, release, release); @@ -114,13 +138,19 @@ void enqueue(queue_t *q, unsigned int val) } } } + /********** Detected Corrctness (testcase1) **********/ atomic_compare_exchange_strong_explicit(&q->tail, &tail, MAKE_POINTER(node, get_count(tail) + 1), release, release); } -bool dequeue(queue_t *q, unsigned int *retVal) +/** @Transition: if (RET) { + if (STATE(q)->empty()) return false; + STATE(q)->pop_front(); +} +@PreCondition: return RET ? !STATE(q)->empty() && STATE(q)->front() == *retVal : true; */ +bool dequeue(queue_t *q, unsigned int *retVal, unsigned int *reclaimNode) { int success = 0; pointer head; @@ -128,9 +158,13 @@ bool dequeue(queue_t *q, unsigned int *retVal) pointer next; while (!success) { + /********** Dectected Admissibility (testcase3) **********/ head = atomic_load_explicit(&q->head, acquire); - tail = atomic_load_explicit(&q->tail, relaxed); + /********** Detected KNOWN BUG **********/ + tail = atomic_load_explicit(&q->tail, acquire); + /********** Detected Correctness (testcase1) **********/ next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, acquire); + /** @OPClearDefine: true */ if (atomic_load_explicit(&q->head, relaxed) == head) { if (get_ptr(head) == get_ptr(tail)) { @@ -140,13 +174,16 @@ bool dequeue(queue_t *q, unsigned int *retVal) if (get_ptr(next) == 0) { // NULL return false; // NULL } + /********** Detected UL **********/ atomic_compare_exchange_strong_explicit(&q->tail, &tail, MAKE_POINTER(get_ptr(next), get_count(tail) + 1), release, release); thrd_yield(); } else { - *retVal = load_32(&q->nodes[get_ptr(next)].value); + //*retVal = load_32(&q->nodes[get_ptr(next)].value); + *retVal = q->nodes[get_ptr(next)].value; + /********** Detected Admissibility (testcase3) **********/ success = atomic_compare_exchange_strong_explicit(&q->head, &head, MAKE_POINTER(get_ptr(next), get_count(head) + 1), @@ -156,6 +193,7 @@ bool dequeue(queue_t *q, unsigned int *retVal) } } } + *reclaimNode = get_ptr(head); reclaim(get_ptr(head)); return true; } diff --git a/treiber-stack/my_stack.h b/ms-queue-loose/queue.h similarity index 71% rename from treiber-stack/my_stack.h rename to ms-queue-loose/queue.h index ebb8baa..c15838a 100644 --- a/treiber-stack/my_stack.h +++ b/ms-queue-loose/queue.h @@ -1,8 +1,7 @@ -#include +#ifndef _QUEUE_H +#define _QUEUE_H -#define release memory_order_release -#define acquire memory_order_acquire -#define relaxed memory_order_relaxed +#include #define MAX_NODES 0xf @@ -21,15 +20,18 @@ static inline unsigned int get_ptr(pointer p) { return p & PTR_MASK; } typedef struct node { unsigned int value; pointer_t next; - } node_t; typedef struct { - pointer_t top; - node_t nodes[MAX_NODES + 1]; -} mystack_t; + pointer_t head; + pointer_t tail; + node_t nodes[MAX_NODES + 2]; +} queue_t; + +void init_queue(queue_t *q, int num_threads); +void enqueue(queue_t *q, unsigned int val, int n); +bool dequeue(queue_t *q, unsigned int *retVal, unsigned int *reclaimedNode); -void init_stack(mystack_t *s, int num_threads); -void push(mystack_t *s, unsigned int val); -unsigned int pop(mystack_t *s); int get_thread_num(); + +#endif diff --git a/ms-queue-loose/testcase1.c b/ms-queue-loose/testcase1.c new file mode 100644 index 0000000..9edf77a --- /dev/null +++ b/ms-queue-loose/testcase1.c @@ -0,0 +1,92 @@ +#include +#include +#include + +#include "queue.h" +#include "model-assert.h" + +static queue_t *queue; +static thrd_t *threads; +static unsigned int *input; +static unsigned int *output; +static int num_threads; + +int get_thread_num() +{ + thrd_t curr = thrd_current(); + int i; + for (i = 0; i < num_threads; i++) + if (curr.priv == threads[i].priv) + return i; + MODEL_ASSERT(0); + return -1; +} + +bool succ1, succ2; +atomic_int x[3]; +unsigned int idx1, idx2; +unsigned int reclaimNode; + +static int procs = 2; +static void main_task(void *param) +{ + unsigned int val; + int pid = *((int *)param); + if (pid % procs == 0) { + //atomic_store_explicit(&x[0], 1, memory_order_relaxed); + enqueue(queue, 0, 0); + } else if (pid % procs == 1) { + //atomic_store_explicit(&x[1], 1, memory_order_relaxed); + succ1 = dequeue(queue, &idx1, &reclaimNode); + if (succ1) { + //atomic_load_explicit(&x[idx1], memory_order_relaxed); + } + } +} + +int user_main(int argc, char **argv) +{ + int i; + int *param; + unsigned int in_sum = 0, out_sum = 0; + + /** @Entry */ + queue = (queue_t*) calloc(1, sizeof(*queue)); + MODEL_ASSERT(queue); + + num_threads = procs; + threads = (thrd_t*) malloc(num_threads * sizeof(thrd_t)); + param = (int*) malloc(num_threads * sizeof(*param)); + input = (unsigned int *) calloc(num_threads, sizeof(*input)); + output = (unsigned int *) calloc(num_threads, sizeof(*output)); + + atomic_init(&x[0], 0); + atomic_init(&x[1], 0); + atomic_init(&x[2], 0); + init_queue(queue, num_threads); + for (i = 0; i < num_threads; i++) { + param[i] = i; + thrd_create(&threads[i], main_task, ¶m[i]); + } + for (i = 0; i < num_threads; i++) + thrd_join(threads[i]); +/* + for (i = 0; i < num_threads; i++) { + in_sum += input[i]; + out_sum += output[i]; + } + for (i = 0; i < num_threads; i++) + printf("input[%d] = %u\n", i, input[i]); + for (i = 0; i < num_threads; i++) + printf("output[%d] = %u\n", i, output[i]); + if (succ1 && succ2) + MODEL_ASSERT(in_sum == out_sum); + else + MODEL_ASSERT (false); +*/ + free(param); + free(threads); + free(queue); + + return 0; +} diff --git a/ms-queue-loose/testcase2.c b/ms-queue-loose/testcase2.c new file mode 100644 index 0000000..20e79c4 --- /dev/null +++ b/ms-queue-loose/testcase2.c @@ -0,0 +1,101 @@ +#include +#include +#include + +#include "queue.h" +#include "model-assert.h" + +static queue_t *queue; +static thrd_t *threads; +static unsigned int *input; +static unsigned int *output; +static int num_threads; + +int get_thread_num() +{ + thrd_t curr = thrd_current(); + int i; + for (i = 0; i < num_threads; i++) + if (curr.priv == threads[i].priv) + return i; + MODEL_ASSERT(0); + return -1; +} + +bool succ1, succ2; +atomic_int x[3]; +unsigned int idx1, idx2; +unsigned int reclaimNode; + +static int procs = 4; +static void main_task(void *param) +{ + unsigned int val; + int pid = *((int *)param); + if (pid % 4 == 0) { + //atomic_store_explicit(&x[0], 1, memory_order_relaxed); + enqueue(queue, 0, 0); + } else if (pid % 4 == 1) { + //atomic_store_explicit(&x[1], 1, memory_order_relaxed); + enqueue(queue, 1, 0); + } else if (pid % 4 == 2) { + succ1 = dequeue(queue, &idx1, &reclaimNode); + if (succ1) { + //atomic_load_explicit(&x[idx1], memory_order_relaxed); + } + } else if (pid % 4 == 3) { + /* + succ2 = dequeue(queue, &idx2, &reclaimNode); + if (succ2) { + atomic_load_explicit(&x[idx2], memory_order_relaxed); + } + */ + } +} + +int user_main(int argc, char **argv) +{ + int i; + int *param; + unsigned int in_sum = 0, out_sum = 0; + + /** @Entry */ + queue = (queue_t*) calloc(1, sizeof(*queue)); + MODEL_ASSERT(queue); + + num_threads = procs; + threads = (thrd_t*) malloc(num_threads * sizeof(thrd_t)); + param = (int*) malloc(num_threads * sizeof(*param)); + input = (unsigned int *) calloc(num_threads, sizeof(*input)); + output = (unsigned int *) calloc(num_threads, sizeof(*output)); + + atomic_init(&x[0], 0); + atomic_init(&x[1], 0); + atomic_init(&x[2], 0); + init_queue(queue, num_threads); + for (i = 0; i < num_threads; i++) { + param[i] = i; + thrd_create(&threads[i], main_task, ¶m[i]); + } + for (i = 0; i < num_threads; i++) + thrd_join(threads[i]); +/* + for (i = 0; i < num_threads; i++) { + in_sum += input[i]; + out_sum += output[i]; + } + for (i = 0; i < num_threads; i++) + printf("input[%d] = %u\n", i, input[i]); + for (i = 0; i < num_threads; i++) + printf("output[%d] = %u\n", i, output[i]); + if (succ1 && succ2) + MODEL_ASSERT(in_sum == out_sum); + else + MODEL_ASSERT (false); +*/ + free(param); + free(threads); + free(queue); + + return 0; +} diff --git a/ms-queue-loose/testcase3.c b/ms-queue-loose/testcase3.c new file mode 100644 index 0000000..80e0f0d --- /dev/null +++ b/ms-queue-loose/testcase3.c @@ -0,0 +1,100 @@ +#include +#include +#include + +#include "queue.h" +#include "model-assert.h" + +static queue_t *queue; +static thrd_t *threads; +static unsigned int *input; +static unsigned int *output; +static int num_threads; + +int get_thread_num() +{ + thrd_t curr = thrd_current(); + int i; + for (i = 0; i < num_threads; i++) + if (curr.priv == threads[i].priv) + return i; + MODEL_ASSERT(0); + return -1; +} + +bool succ1, succ2; +atomic_int x[3]; +unsigned int idx1, idx2; +unsigned int reclaimNode; + +static int procs = 2; +static void main_task(void *param) +{ + unsigned int val; + int pid = *((int *)param); + if (pid % procs == 0) { + //atomic_store_explicit(&x[0], 1, memory_order_relaxed); + enqueue(queue, 1, 0); + printf("T2 enqueue %d\n", 1); + succ1 = dequeue(queue, &idx1, &reclaimNode); + if (succ1) + printf("T2 dequeue %d\n", idx1); + else + printf("T2 dequeue NULL\n"); + } else if (pid % procs == 1) { + enqueue(queue, 2, 0); + printf("T3 enqueue %d\n", 2); + succ2 = dequeue(queue, &idx2, &reclaimNode); + if (succ2) + printf("T3 dequeue %d\n", idx2); + else + printf("T2 dequeue NULL\n"); + } +} + +int user_main(int argc, char **argv) +{ + int i; + int *param; + unsigned int in_sum = 0, out_sum = 0; + + /** @Entry */ + queue = (queue_t*) calloc(1, sizeof(*queue)); + MODEL_ASSERT(queue); + + num_threads = procs; + threads = (thrd_t*) malloc(num_threads * sizeof(thrd_t)); + param = (int*) malloc(num_threads * sizeof(*param)); + input = (unsigned int *) calloc(num_threads, sizeof(*input)); + output = (unsigned int *) calloc(num_threads, sizeof(*output)); + + atomic_init(&x[0], 0); + atomic_init(&x[1], 0); + atomic_init(&x[2], 0); + init_queue(queue, num_threads); + for (i = 0; i < num_threads; i++) { + param[i] = i; + thrd_create(&threads[i], main_task, ¶m[i]); + } + for (i = 0; i < num_threads; i++) + thrd_join(threads[i]); +/* + for (i = 0; i < num_threads; i++) { + in_sum += input[i]; + out_sum += output[i]; + } + for (i = 0; i < num_threads; i++) + printf("input[%d] = %u\n", i, input[i]); + for (i = 0; i < num_threads; i++) + printf("output[%d] = %u\n", i, output[i]); + if (succ1 && succ2) + MODEL_ASSERT(in_sum == out_sum); + else + MODEL_ASSERT (false); +*/ + free(param); + free(threads); + free(queue); + + return 0; +} diff --git a/ms-queue-loose/testcase4.c b/ms-queue-loose/testcase4.c new file mode 100644 index 0000000..1e1d151 --- /dev/null +++ b/ms-queue-loose/testcase4.c @@ -0,0 +1,90 @@ +#include +#include +#include + +#include "queue.h" +#include "model-assert.h" + +static queue_t *queue; +static thrd_t *threads; +static unsigned int *input; +static unsigned int *output; +static int num_threads; + +int get_thread_num() +{ + thrd_t curr = thrd_current(); + int i; + for (i = 0; i < num_threads; i++) + if (curr.priv == threads[i].priv) + return i; + //MODEL_ASSERT(0); + return -1; +} + +bool succ1, succ2; +atomic_int x[3]; +unsigned int idx1, idx2, idx3; +unsigned int reclaimNode; + +static int procs = 2; +static void main_task(void *param) +{ + unsigned int val; + int pid = *((int *)param); + if (pid % procs == 0) { + enqueue(queue, 1, 0); + succ1 = dequeue(queue, &idx1, &reclaimNode); + enqueue(queue, 2, 0); + } else if (pid % procs == 1) { + enqueue(queue, 2, 2); + succ2 = dequeue(queue, &idx2, &reclaimNode); + } +} + +int user_main(int argc, char **argv) +{ + int i; + int *param; + unsigned int in_sum = 0, out_sum = 0; + + /** @Entry */ + queue = (queue_t*) calloc(1, sizeof(*queue)); + MODEL_ASSERT(queue); + + num_threads = procs; + threads = (thrd_t*) malloc(num_threads * sizeof(thrd_t)); + param = (int*) malloc(num_threads * sizeof(*param)); + input = (unsigned int *) calloc(num_threads, sizeof(*input)); + output = (unsigned int *) calloc(num_threads, sizeof(*output)); + + atomic_init(&x[0], 0); + atomic_init(&x[1], 0); + atomic_init(&x[2], 0); + init_queue(queue, num_threads); + for (i = 0; i < num_threads; i++) { + param[i] = i; + thrd_create(&threads[i], main_task, ¶m[i]); + } + for (i = 0; i < num_threads; i++) + thrd_join(threads[i]); +/* + for (i = 0; i < num_threads; i++) { + in_sum += input[i]; + out_sum += output[i]; + } + for (i = 0; i < num_threads; i++) + printf("input[%d] = %u\n", i, input[i]); + for (i = 0; i < num_threads; i++) + printf("output[%d] = %u\n", i, output[i]); + if (succ1 && succ2) + MODEL_ASSERT(in_sum == out_sum); + else + MODEL_ASSERT (false); +*/ + free(param); + free(threads); + free(queue); + + return 0; +} diff --git a/ms-queue/.gitignore b/ms-queue/.gitignore index 95811e0..71e596d 100644 --- a/ms-queue/.gitignore +++ b/ms-queue/.gitignore @@ -1 +1,8 @@ -/main +main +testcase1 +testcase2 +testcase3 +testcase4 +*.dSYM/ +*.o +.*.d diff --git a/ms-queue/Makefile b/ms-queue/Makefile index da3a0e4..a50ca70 100644 --- a/ms-queue/Makefile +++ b/ms-queue/Makefile @@ -1,17 +1,23 @@ include ../benchmarks.mk -TESTNAME = main +BENCH := queue -HEADERS = my_queue.h -OBJECTS = main.o my_queue.o +BENCH_BINARY := $(BENCH).o -all: $(TESTNAME) +TESTS := main testcase1 testcase2 testcase3 testcase4 -$(TESTNAME): $(HEADERS) $(OBJECTS) - $(CC) -o $@ $(OBJECTS) $(CFLAGS) $(LDFLAGS) +all: $(TESTS) + ../generate.sh $(notdir $(shell pwd)) -%.o: %.c - $(CC) -c -o $@ $< $(CFLAGS) +%.o : %.c + $(CC) -c -fPIC -MMD -MF .$@.d -o $@ $< $(CFLAGS) $(LDFLAGS) + +$(TESTS): % : %.o $(BENCH_BINARY) + $(CC) -o $@ $^ $(CFLAGS) $(LDFLAGS) + +-include .*.d clean: - rm -f $(TESTNAME) *.o + rm -rf $(TESTS) *.o .*.d *.dSYM + +.PHONY: clean all diff --git a/ms-queue/main.c b/ms-queue/main.c index e464138..a148ad4 100644 --- a/ms-queue/main.c +++ b/ms-queue/main.c @@ -2,10 +2,9 @@ #include #include -#include "my_queue.h" +#include "queue.h" #include "model-assert.h" -static int procs = 2; static queue_t *queue; static thrd_t *threads; static unsigned int *input; @@ -24,20 +23,21 @@ int get_thread_num() } bool succ1, succ2; +atomic_int x[3]; +unsigned int idx1, idx2; +unsigned int reclaimNode; +static int procs = 2; static void main_task(void *param) { unsigned int val; int pid = *((int *)param); - if (!pid) { - input[0] = 17; - enqueue(queue, input[0]); - succ1 = dequeue(queue, &output[0]); - //printf("Dequeue: %d\n", output[0]); + if (pid % 2 == 0) { + enqueue(queue, 0, 0); + succ1 = dequeue(queue, &idx1, &reclaimNode); } else { - input[1] = 37; - enqueue(queue, input[1]); - succ2 = dequeue(queue, &output[1]); + enqueue(queue, 1, 0); + succ2 = dequeue(queue, &idx2, &reclaimNode); } } @@ -47,14 +47,15 @@ int user_main(int argc, char **argv) int *param; unsigned int in_sum = 0, out_sum = 0; - queue = calloc(1, sizeof(*queue)); + /** @Entry */ + queue = (queue_t*) calloc(1, sizeof(*queue)); MODEL_ASSERT(queue); num_threads = procs; - threads = malloc(num_threads * sizeof(thrd_t)); - param = malloc(num_threads * sizeof(*param)); - input = calloc(num_threads, sizeof(*input)); - output = calloc(num_threads, sizeof(*output)); + threads = (thrd_t*) malloc(num_threads * sizeof(thrd_t)); + param = (int*) malloc(num_threads * sizeof(*param)); + input = (unsigned int *) calloc(num_threads, sizeof(*input)); + output = (unsigned int *) calloc(num_threads, sizeof(*output)); init_queue(queue, num_threads); for (i = 0; i < num_threads; i++) { @@ -63,7 +64,7 @@ int user_main(int argc, char **argv) } for (i = 0; i < num_threads; i++) thrd_join(threads[i]); - +/* for (i = 0; i < num_threads; i++) { in_sum += input[i]; out_sum += output[i]; @@ -76,7 +77,7 @@ int user_main(int argc, char **argv) MODEL_ASSERT(in_sum == out_sum); else MODEL_ASSERT (false); - +*/ free(param); free(threads); free(queue); diff --git a/ms-queue/queue.c b/ms-queue/queue.c new file mode 100644 index 0000000..8a0f4eb --- /dev/null +++ b/ms-queue/queue.c @@ -0,0 +1,207 @@ +#include +#include +#include "librace.h" +#include "model-assert.h" + +#include "queue.h" + +#define relaxed memory_order_relaxed +#define release memory_order_release +#define acquire memory_order_acquire + +#define MAX_FREELIST 4 /* Each thread can own up to MAX_FREELIST free nodes */ +#define INITIAL_FREE 2 /* Each thread starts with INITIAL_FREE free nodes */ + +#define POISON_IDX 0x666 + +static unsigned int (*free_lists)[MAX_FREELIST]; + +/* Search this thread's free list for a "new" node */ +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 = free_lists[t][i]; + if (node) { + //store_32(&free_lists[t][i], 0); + free_lists[t][i] = 0; + return node; + } + } + /* free_list is empty? */ + MODEL_ASSERT(0); + return 0; +} + +/* Simulate the fact that when a node got recycled, it will get assigned to the + * same queue or for other usage */ +void simulateRecycledNodeUpdate(queue_t *q, unsigned int node) { + atomic_store_explicit(&q->nodes[node].next, -1, memory_order_release); +} + + +/* Place this node index back on this thread's free list */ +static void reclaim(unsigned int node) +{ + int i; + int t = get_thread_num(); + + /* Don't reclaim NULL 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 = free_lists[t][i]; + + /* Found empty spot in free list */ + if (idx == 0) { + //store_32(&free_lists[t][i], node); + free_lists[t][i] = node; + return; + } + } + /* free list is full? */ + //MODEL_ASSERT(0); +} + +void init_queue(queue_t *q, int num_threads) +{ + int i, j; + + /* Initialize each thread's free list with INITIAL_FREE pointers */ + /* The actual nodes are initialized with poison indexes */ + free_lists = ( unsigned int (*)[MAX_FREELIST] ) malloc(num_threads * sizeof(*free_lists)); + for (i = 0; i < num_threads; i++) { + for (j = 0; j < INITIAL_FREE; j++) { + free_lists[i][j] = 2 + i * MAX_FREELIST + j; + atomic_init(&q->nodes[free_lists[i][j]].next, MAKE_POINTER(POISON_IDX, 0)); + } + } + + /* initialize queue */ + atomic_init(&q->head, MAKE_POINTER(1, 0)); + atomic_init(&q->tail, MAKE_POINTER(1, 0)); + atomic_init(&q->nodes[1].next, MAKE_POINTER(0, 0)); +} + +/** @DeclareState: IntList *q; +@Initial: q = new IntList; +@Print: + model_print("\tSTATE(q): "); + printContainer(q); + model_print("\n"); */ + +/** @Transition: STATE(q)->push_back(val); +@Print: model_print("\tENQ #%d: val=%d\n", ID, val); */ +void enqueue(queue_t *q, unsigned int val, int n) +{ + int success = 0; + unsigned int node; + pointer tail; + pointer next; + pointer tmp; + + node = new_node(); + //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 + // This is a found bug in AutoMO, and testcase4 can reveal this known bug + /********** Detected KNOWN BUG (testcase4) **********/ + atomic_store_explicit(&q->nodes[node].next, tmp, release); + + while (!success) { + /********** Detected UL **********/ + tail = atomic_load_explicit(&q->tail, acquire); + /********** Detected Correctness (testcase4) **********/ + next = atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire); + if (tail == atomic_load_explicit(&q->tail, relaxed)) { + + /* Check for uninitialized 'next' */ + //MODEL_ASSERT(get_ptr(next) != POISON_IDX); + + if (get_ptr(next) == 0) { // == NULL + pointer value = MAKE_POINTER(node, get_count(next) + 1); + /********** Detected Correctness (testcase1) **********/ + success = atomic_compare_exchange_strong_explicit(&q->nodes[get_ptr(tail)].next, + &next, value, release, release); + /** @OPClearDefine: success */ + } + if (!success) { + /********** 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); + /********** Detected Correctness (testcase2) **********/ + atomic_compare_exchange_strong_explicit(&q->tail, + &tail, value, + release, release); + thrd_yield(); + } + } + } + /********** Detected Corrctness (testcase1) **********/ + atomic_compare_exchange_strong_explicit(&q->tail, + &tail, + MAKE_POINTER(node, get_count(tail) + 1), + release, release); +} + +/** @Transition: S_RET = STATE(q)->empty() ? 0 : STATE(q)->front(); +if (S_RET) STATE(q)->pop_front(); +@JustifyingPostcondition: if (!C_RET) + return S_RET == C_RET; +@PostCondition: return C_RET ? *retVal == S_RET : true; +@Print: model_print("\tDEQ #%d: C_RET=%d && *retVal=%d && S_RET=%d\n", ID, + C_RET, *retVal, S_RET); +*/ +int dequeue(queue_t *q, unsigned int *retVal, unsigned int *reclaimNode) +{ + int success = 0; + pointer head; + pointer tail; + pointer next; + + while (!success) { + /********** Dectected Correctness (testcase3) **********/ + head = atomic_load_explicit(&q->head, acquire); + /********** Detected KNOWN BUG (testcase2) **********/ + tail = atomic_load_explicit(&q->tail, acquire); + /********** Detected Correctness (testcase1) **********/ + next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, acquire); + /** @OPClearDefine: true */ + if (atomic_load_explicit(&q->head, relaxed) == head) { + if (get_ptr(head) == get_ptr(tail)) { + + /* Check for uninitialized 'next' */ + MODEL_ASSERT(get_ptr(next) != POISON_IDX); + + if (get_ptr(next) == 0) { // NULL + return false; // NULL + } + /********** Detected UL **********/ + atomic_compare_exchange_strong_explicit(&q->tail, + &tail, + MAKE_POINTER(get_ptr(next), get_count(tail) + 1), + release, release); + thrd_yield(); + } else { + //*retVal = load_32(&q->nodes[get_ptr(next)].value); + *retVal = q->nodes[get_ptr(next)].value; + /********** Detected Correctness (testcase3) **********/ + success = atomic_compare_exchange_strong_explicit(&q->head, + &head, + MAKE_POINTER(get_ptr(next), get_count(head) + 1), + release, release); + if (!success) + thrd_yield(); + } + } + } + *reclaimNode = get_ptr(head); + reclaim(get_ptr(head)); + return true; +} diff --git a/ms-queue/my_queue.h b/ms-queue/queue.h similarity index 80% rename from ms-queue/my_queue.h rename to ms-queue/queue.h index edaf3dd..f6d12d2 100644 --- a/ms-queue/my_queue.h +++ b/ms-queue/queue.h @@ -1,3 +1,6 @@ +#ifndef _QUEUE_H +#define _QUEUE_H + #include #define MAX_NODES 0xf @@ -22,10 +25,13 @@ typedef struct node { typedef struct { pointer_t head; pointer_t tail; - node_t nodes[MAX_NODES + 1]; + node_t nodes[MAX_NODES + 2]; } queue_t; void init_queue(queue_t *q, int num_threads); -void enqueue(queue_t *q, unsigned int val); -bool dequeue(queue_t *q, unsigned int *retVal); +void enqueue(queue_t *q, unsigned int val, int n); +int dequeue(queue_t *q, unsigned int *retVal, unsigned int *reclaimedNode); + int get_thread_num(); + +#endif diff --git a/ms-queue/testcase1.c b/ms-queue/testcase1.c new file mode 100644 index 0000000..9edf77a --- /dev/null +++ b/ms-queue/testcase1.c @@ -0,0 +1,92 @@ +#include +#include +#include + +#include "queue.h" +#include "model-assert.h" + +static queue_t *queue; +static thrd_t *threads; +static unsigned int *input; +static unsigned int *output; +static int num_threads; + +int get_thread_num() +{ + thrd_t curr = thrd_current(); + int i; + for (i = 0; i < num_threads; i++) + if (curr.priv == threads[i].priv) + return i; + MODEL_ASSERT(0); + return -1; +} + +bool succ1, succ2; +atomic_int x[3]; +unsigned int idx1, idx2; +unsigned int reclaimNode; + +static int procs = 2; +static void main_task(void *param) +{ + unsigned int val; + int pid = *((int *)param); + if (pid % procs == 0) { + //atomic_store_explicit(&x[0], 1, memory_order_relaxed); + enqueue(queue, 0, 0); + } else if (pid % procs == 1) { + //atomic_store_explicit(&x[1], 1, memory_order_relaxed); + succ1 = dequeue(queue, &idx1, &reclaimNode); + if (succ1) { + //atomic_load_explicit(&x[idx1], memory_order_relaxed); + } + } +} + +int user_main(int argc, char **argv) +{ + int i; + int *param; + unsigned int in_sum = 0, out_sum = 0; + + /** @Entry */ + queue = (queue_t*) calloc(1, sizeof(*queue)); + MODEL_ASSERT(queue); + + num_threads = procs; + threads = (thrd_t*) malloc(num_threads * sizeof(thrd_t)); + param = (int*) malloc(num_threads * sizeof(*param)); + input = (unsigned int *) calloc(num_threads, sizeof(*input)); + output = (unsigned int *) calloc(num_threads, sizeof(*output)); + + atomic_init(&x[0], 0); + atomic_init(&x[1], 0); + atomic_init(&x[2], 0); + init_queue(queue, num_threads); + for (i = 0; i < num_threads; i++) { + param[i] = i; + thrd_create(&threads[i], main_task, ¶m[i]); + } + for (i = 0; i < num_threads; i++) + thrd_join(threads[i]); +/* + for (i = 0; i < num_threads; i++) { + in_sum += input[i]; + out_sum += output[i]; + } + for (i = 0; i < num_threads; i++) + printf("input[%d] = %u\n", i, input[i]); + for (i = 0; i < num_threads; i++) + printf("output[%d] = %u\n", i, output[i]); + if (succ1 && succ2) + MODEL_ASSERT(in_sum == out_sum); + else + MODEL_ASSERT (false); +*/ + free(param); + free(threads); + free(queue); + + return 0; +} diff --git a/ms-queue/testcase2.c b/ms-queue/testcase2.c new file mode 100644 index 0000000..20e79c4 --- /dev/null +++ b/ms-queue/testcase2.c @@ -0,0 +1,101 @@ +#include +#include +#include + +#include "queue.h" +#include "model-assert.h" + +static queue_t *queue; +static thrd_t *threads; +static unsigned int *input; +static unsigned int *output; +static int num_threads; + +int get_thread_num() +{ + thrd_t curr = thrd_current(); + int i; + for (i = 0; i < num_threads; i++) + if (curr.priv == threads[i].priv) + return i; + MODEL_ASSERT(0); + return -1; +} + +bool succ1, succ2; +atomic_int x[3]; +unsigned int idx1, idx2; +unsigned int reclaimNode; + +static int procs = 4; +static void main_task(void *param) +{ + unsigned int val; + int pid = *((int *)param); + if (pid % 4 == 0) { + //atomic_store_explicit(&x[0], 1, memory_order_relaxed); + enqueue(queue, 0, 0); + } else if (pid % 4 == 1) { + //atomic_store_explicit(&x[1], 1, memory_order_relaxed); + enqueue(queue, 1, 0); + } else if (pid % 4 == 2) { + succ1 = dequeue(queue, &idx1, &reclaimNode); + if (succ1) { + //atomic_load_explicit(&x[idx1], memory_order_relaxed); + } + } else if (pid % 4 == 3) { + /* + succ2 = dequeue(queue, &idx2, &reclaimNode); + if (succ2) { + atomic_load_explicit(&x[idx2], memory_order_relaxed); + } + */ + } +} + +int user_main(int argc, char **argv) +{ + int i; + int *param; + unsigned int in_sum = 0, out_sum = 0; + + /** @Entry */ + queue = (queue_t*) calloc(1, sizeof(*queue)); + MODEL_ASSERT(queue); + + num_threads = procs; + threads = (thrd_t*) malloc(num_threads * sizeof(thrd_t)); + param = (int*) malloc(num_threads * sizeof(*param)); + input = (unsigned int *) calloc(num_threads, sizeof(*input)); + output = (unsigned int *) calloc(num_threads, sizeof(*output)); + + atomic_init(&x[0], 0); + atomic_init(&x[1], 0); + atomic_init(&x[2], 0); + init_queue(queue, num_threads); + for (i = 0; i < num_threads; i++) { + param[i] = i; + thrd_create(&threads[i], main_task, ¶m[i]); + } + for (i = 0; i < num_threads; i++) + thrd_join(threads[i]); +/* + for (i = 0; i < num_threads; i++) { + in_sum += input[i]; + out_sum += output[i]; + } + for (i = 0; i < num_threads; i++) + printf("input[%d] = %u\n", i, input[i]); + for (i = 0; i < num_threads; i++) + printf("output[%d] = %u\n", i, output[i]); + if (succ1 && succ2) + MODEL_ASSERT(in_sum == out_sum); + else + MODEL_ASSERT (false); +*/ + free(param); + free(threads); + free(queue); + + return 0; +} diff --git a/ms-queue/testcase3.c b/ms-queue/testcase3.c new file mode 100644 index 0000000..80e0f0d --- /dev/null +++ b/ms-queue/testcase3.c @@ -0,0 +1,100 @@ +#include +#include +#include + +#include "queue.h" +#include "model-assert.h" + +static queue_t *queue; +static thrd_t *threads; +static unsigned int *input; +static unsigned int *output; +static int num_threads; + +int get_thread_num() +{ + thrd_t curr = thrd_current(); + int i; + for (i = 0; i < num_threads; i++) + if (curr.priv == threads[i].priv) + return i; + MODEL_ASSERT(0); + return -1; +} + +bool succ1, succ2; +atomic_int x[3]; +unsigned int idx1, idx2; +unsigned int reclaimNode; + +static int procs = 2; +static void main_task(void *param) +{ + unsigned int val; + int pid = *((int *)param); + if (pid % procs == 0) { + //atomic_store_explicit(&x[0], 1, memory_order_relaxed); + enqueue(queue, 1, 0); + printf("T2 enqueue %d\n", 1); + succ1 = dequeue(queue, &idx1, &reclaimNode); + if (succ1) + printf("T2 dequeue %d\n", idx1); + else + printf("T2 dequeue NULL\n"); + } else if (pid % procs == 1) { + enqueue(queue, 2, 0); + printf("T3 enqueue %d\n", 2); + succ2 = dequeue(queue, &idx2, &reclaimNode); + if (succ2) + printf("T3 dequeue %d\n", idx2); + else + printf("T2 dequeue NULL\n"); + } +} + +int user_main(int argc, char **argv) +{ + int i; + int *param; + unsigned int in_sum = 0, out_sum = 0; + + /** @Entry */ + queue = (queue_t*) calloc(1, sizeof(*queue)); + MODEL_ASSERT(queue); + + num_threads = procs; + threads = (thrd_t*) malloc(num_threads * sizeof(thrd_t)); + param = (int*) malloc(num_threads * sizeof(*param)); + input = (unsigned int *) calloc(num_threads, sizeof(*input)); + output = (unsigned int *) calloc(num_threads, sizeof(*output)); + + atomic_init(&x[0], 0); + atomic_init(&x[1], 0); + atomic_init(&x[2], 0); + init_queue(queue, num_threads); + for (i = 0; i < num_threads; i++) { + param[i] = i; + thrd_create(&threads[i], main_task, ¶m[i]); + } + for (i = 0; i < num_threads; i++) + thrd_join(threads[i]); +/* + for (i = 0; i < num_threads; i++) { + in_sum += input[i]; + out_sum += output[i]; + } + for (i = 0; i < num_threads; i++) + printf("input[%d] = %u\n", i, input[i]); + for (i = 0; i < num_threads; i++) + printf("output[%d] = %u\n", i, output[i]); + if (succ1 && succ2) + MODEL_ASSERT(in_sum == out_sum); + else + MODEL_ASSERT (false); +*/ + free(param); + free(threads); + free(queue); + + return 0; +} diff --git a/ms-queue/testcase4.c b/ms-queue/testcase4.c new file mode 100644 index 0000000..1e1d151 --- /dev/null +++ b/ms-queue/testcase4.c @@ -0,0 +1,90 @@ +#include +#include +#include + +#include "queue.h" +#include "model-assert.h" + +static queue_t *queue; +static thrd_t *threads; +static unsigned int *input; +static unsigned int *output; +static int num_threads; + +int get_thread_num() +{ + thrd_t curr = thrd_current(); + int i; + for (i = 0; i < num_threads; i++) + if (curr.priv == threads[i].priv) + return i; + //MODEL_ASSERT(0); + return -1; +} + +bool succ1, succ2; +atomic_int x[3]; +unsigned int idx1, idx2, idx3; +unsigned int reclaimNode; + +static int procs = 2; +static void main_task(void *param) +{ + unsigned int val; + int pid = *((int *)param); + if (pid % procs == 0) { + enqueue(queue, 1, 0); + succ1 = dequeue(queue, &idx1, &reclaimNode); + enqueue(queue, 2, 0); + } else if (pid % procs == 1) { + enqueue(queue, 2, 2); + succ2 = dequeue(queue, &idx2, &reclaimNode); + } +} + +int user_main(int argc, char **argv) +{ + int i; + int *param; + unsigned int in_sum = 0, out_sum = 0; + + /** @Entry */ + queue = (queue_t*) calloc(1, sizeof(*queue)); + MODEL_ASSERT(queue); + + num_threads = procs; + threads = (thrd_t*) malloc(num_threads * sizeof(thrd_t)); + param = (int*) malloc(num_threads * sizeof(*param)); + input = (unsigned int *) calloc(num_threads, sizeof(*input)); + output = (unsigned int *) calloc(num_threads, sizeof(*output)); + + atomic_init(&x[0], 0); + atomic_init(&x[1], 0); + atomic_init(&x[2], 0); + init_queue(queue, num_threads); + for (i = 0; i < num_threads; i++) { + param[i] = i; + thrd_create(&threads[i], main_task, ¶m[i]); + } + for (i = 0; i < num_threads; i++) + thrd_join(threads[i]); +/* + for (i = 0; i < num_threads; i++) { + in_sum += input[i]; + out_sum += output[i]; + } + for (i = 0; i < num_threads; i++) + printf("input[%d] = %u\n", i, input[i]); + for (i = 0; i < num_threads; i++) + printf("output[%d] = %u\n", i, output[i]); + if (succ1 && succ2) + MODEL_ASSERT(in_sum == out_sum); + else + MODEL_ASSERT (false); +*/ + free(param); + free(threads); + free(queue); + + return 0; +} diff --git a/read-copy-update/Makefile b/read-copy-update/Makefile new file mode 100644 index 0000000..2c49cc8 --- /dev/null +++ b/read-copy-update/Makefile @@ -0,0 +1,23 @@ +include ../benchmarks.mk + +BENCH := rcu + +BENCH_BINARY := $(BENCH).o + +TESTS := main testcase + +all: $(TESTS) + ../generate.sh $(notdir $(shell pwd)) + +%.o : %.cc + $(CXX) -c -fPIC -MMD -MF .$@.d -o $@ $< $(CXXFLAGS) $(LDFLAGS) + +$(TESTS): % : %.o $(BENCH_BINARY) + $(CXX) -o $@ $^ $(CXXFLAGS) $(LDFLAGS) + +-include .*.d + +clean: + rm -rf $(TESTS) *.o .*.d *.dSYM + +.PHONY: clean all diff --git a/read-copy-update/main.cc b/read-copy-update/main.cc new file mode 100644 index 0000000..49c52e2 --- /dev/null +++ b/read-copy-update/main.cc @@ -0,0 +1,42 @@ +#include +#include "rcu.h" + +void threadA(void *arg) { + write(1, 0); +} + +void threadB(void *arg) { + write(0, 2); +} + +void threadC(void *arg) { + write(2, 2); +} + +void threadD(void *arg) { + int *d1 = new int; + int *d2 = new int; + read(d1, d2); + printf("ThreadD: d1=%d, d2=%d\n", *d1, *d2); +} + +int user_main(int argc, char **argv) { + thrd_t t1, t2, t3, t4; + /** @Entry */ + Data *dataInit = new Data; + dataInit->data1 = 0; + dataInit->data2 = 0; + atomic_init(&dataPtr, dataInit); + + thrd_create(&t1, threadA, NULL); + thrd_create(&t2, threadB, NULL); + //thrd_create(&t3, threadC, NULL); + thrd_create(&t4, threadD, NULL); + + thrd_join(t1); + thrd_join(t2); + //thrd_join(t3); + thrd_join(t4); + + return 0; +} diff --git a/read-copy-update/rcu.cc b/read-copy-update/rcu.cc new file mode 100644 index 0000000..52a82db --- /dev/null +++ b/read-copy-update/rcu.cc @@ -0,0 +1,42 @@ +#include "rcu.h" + +/** + This is an example about how to specify the correctness of the + read-copy-update synchronization mechanism. +*/ + +atomic dataPtr; + +/** @DeclareState: int data1; + int data2; */ + +/** @JustifyingPrecondition: return STATE(data1) == *data1 && STATE(data2) == *data2; */ +void read(int *data1, int *data2) { + /********** Detected Correctness **********/ + Data *res = dataPtr.load(memory_order_acquire); + /** @OPDefine: true */ + *data1 = res->data1; + *data2 = res->data2; + //load_32(&res->data1); +} + +static void inc(Data *newPtr, Data *prev, int d1, int d2) { + newPtr->data1 = prev->data1 + d1; + newPtr->data2 = prev->data2 + d2; +} + +/** @Transition: STATE(data1) += data1; + STATE(data2) += data2; */ +void write(int data1, int data2) { + bool succ = false; + Data *tmp = new Data; + do { + /********** Detected Correctness **********/ + Data *prev = dataPtr.load(memory_order_acquire); + inc(tmp, prev, data1, data2); + /********** Detected Correctness **********/ + succ = dataPtr.compare_exchange_strong(prev, tmp, + memory_order_release, memory_order_relaxed); + /** @OPClearDefine: succ */ + } while (!succ); +} diff --git a/read-copy-update/rcu.h b/read-copy-update/rcu.h new file mode 100644 index 0000000..f40edf4 --- /dev/null +++ b/read-copy-update/rcu.h @@ -0,0 +1,25 @@ +#ifndef _RCU_H +#define _RCU_H + +#include +#include +#include +#include +#include + +#include "librace.h" + +struct Data { + /** Declare atomic just to expose them to CDSChecker */ + int data1; + int data2; +}; + + +extern atomic dataPtr; + +void read(int *data1, int *data2); + +void write(int data1, int data2); + +#endif diff --git a/read-copy-update/testcase.cc b/read-copy-update/testcase.cc new file mode 100644 index 0000000..49c52e2 --- /dev/null +++ b/read-copy-update/testcase.cc @@ -0,0 +1,42 @@ +#include +#include "rcu.h" + +void threadA(void *arg) { + write(1, 0); +} + +void threadB(void *arg) { + write(0, 2); +} + +void threadC(void *arg) { + write(2, 2); +} + +void threadD(void *arg) { + int *d1 = new int; + int *d2 = new int; + read(d1, d2); + printf("ThreadD: d1=%d, d2=%d\n", *d1, *d2); +} + +int user_main(int argc, char **argv) { + thrd_t t1, t2, t3, t4; + /** @Entry */ + Data *dataInit = new Data; + dataInit->data1 = 0; + dataInit->data2 = 0; + atomic_init(&dataPtr, dataInit); + + thrd_create(&t1, threadA, NULL); + thrd_create(&t2, threadB, NULL); + //thrd_create(&t3, threadC, NULL); + thrd_create(&t4, threadD, NULL); + + thrd_join(t1); + thrd_join(t2); + //thrd_join(t3); + thrd_join(t4); + + return 0; +} diff --git a/seqlock/Makefile b/seqlock/Makefile index 98375f9..75cd83f 100644 --- a/seqlock/Makefile +++ b/seqlock/Makefile @@ -1,9 +1,22 @@ include ../benchmarks.mk -all: seqlock +BENCH := seqlock +BENCH_BINARY := $(BENCH).o -seqlock: seqlock.c - $(CXX) -o $@ $< $(CXXFLAGS) $(LDFLAGS) +TESTS := main testcase1 testcase2 + +all: $(TESTS) + ../generate.sh $(notdir $(shell pwd)) + +%.o : %.cc + $(CXX) -c -fPIC -MMD -MF .$@.d -o $@ $< $(CXXFLAGS) $(LDFLAGS) + +$(TESTS): % : %.o $(BENCH_BINARY) + $(CXX) -o $@ $^ $(CXXFLAGS) $(LDFLAGS) + +-include .*.d clean: - rm -f seqlock + rm -rf $(TESTS) *.o .*.d *.dSYM + +.PHONY: clean all diff --git a/seqlock/main.cc b/seqlock/main.cc new file mode 100644 index 0000000..df5594f --- /dev/null +++ b/seqlock/main.cc @@ -0,0 +1,33 @@ +#include +#include "seqlock.h" + +seqlock *lock; + +static void a(void *obj) { + write(lock, 1, 2); +} + +static void b(void *obj) { + write(lock, 3, 4); +} + +static void c(void *obj) { + int *data1 = new int; + int *data2 = new int; + read(lock, data1, data2); +} + +int user_main(int argc, char **argv) { + thrd_t t1, t2, t3; + /** @Entry */ + lock = new seqlock; + + thrd_create(&t1, (thrd_start_t)&a, NULL); + //thrd_create(&t2, (thrd_start_t)&b, NULL); + thrd_create(&t3, (thrd_start_t)&c, NULL); + + thrd_join(t1); + //thrd_join(t2); + thrd_join(t3); + return 0; +} diff --git a/seqlock/seqlock.c b/seqlock/seqlock.c deleted file mode 100644 index 3762374..0000000 --- a/seqlock/seqlock.c +++ /dev/null @@ -1,75 +0,0 @@ -#include -#include - -typedef struct seqlock { - // Sequence for reader consistency check - atomic_int _seq; - // It needs to be atomic to avoid data races - atomic_int _data; - - seqlock() { - atomic_init(&_seq, 0); - atomic_init(&_data, 0); - } - - int read() { - while (true) { - int old_seq = _seq.load(memory_order_acquire); // acquire - if (old_seq % 2 == 1) continue; - - int res = _data.load(memory_order_acquire); // acquire - if (_seq.load(memory_order_relaxed) == old_seq) { // relaxed - return res; - } - } - } - - void write(int new_data) { - while (true) { - // This might be a relaxed too - int old_seq = _seq.load(memory_order_acquire); // acquire - if (old_seq % 2 == 1) - continue; // Retry - - // Should be relaxed!!! - if (_seq.compare_exchange_strong(old_seq, old_seq + 1, - memory_order_relaxed, memory_order_relaxed)) // relaxed - break; - } - - // Update the data - _data.store(new_data, memory_order_release); // release - - _seq.fetch_add(1, memory_order_release); // release - } - -} seqlock_t; - - -seqlock_t *lock; - -static void a(void *obj) { - lock->write(3); -} - -static void b(void *obj) { - lock->write(2); -} - -static void c(void *obj) { - int r1 = lock->read(); -} - -int user_main(int argc, char **argv) { - thrd_t t1, t2, t3, t4; - lock = new seqlock_t(); - - thrd_create(&t1, (thrd_start_t)&a, NULL); - thrd_create(&t2, (thrd_start_t)&b, NULL); - thrd_create(&t3, (thrd_start_t)&c, NULL); - - thrd_join(t1); - thrd_join(t2); - thrd_join(t3); - return 0; -} diff --git a/seqlock/seqlock.cc b/seqlock/seqlock.cc new file mode 100644 index 0000000..16298bd --- /dev/null +++ b/seqlock/seqlock.cc @@ -0,0 +1,85 @@ +#include +#include +#include "seqlock.h" + +seqlock::seqlock() { + atomic_init(&_seq, 0); + atomic_init(&_data1, 0); + atomic_init(&_data2, 0); +} + +/** @DeclareState: int data1; + int data2; */ + +void seqlock::read(int *data1, int *data2) { + while (true) { + // XXX: This cannot be detected unless when we only have a single data + // varaible since that becomes a plain load/store. However, when we have + // multiple data pieces, we will detect the inconsitency of the data. + /********** Detected Correctness (testcase1) **********/ + int old_seq = _seq.load(memory_order_acquire); // acquire + if (old_seq % 2 == 1) { + thrd_yield(); + continue; + } + + // Acquire ensures that the second _seq reads an update-to-date value + /********** Detected Correctness (testcase1) **********/ + *data1 = _data1.load(memory_order_relaxed); + *data2 = _data2.load(memory_order_relaxed); + /** @OPClearDefine: true */ + /********** Detected Correctness (testcase1) **********/ + atomic_thread_fence(memory_order_acquire); + if (_seq.load(memory_order_relaxed) == old_seq) { // relaxed + thrd_yield(); + return; + } + } +} + + +void seqlock::write(int data1, int data2) { + while (true) { + // #1: either here or #2 must be acquire + /********** Detected Correctness (testcase2 with -y -x1000) **********/ + int old_seq = _seq.load(memory_order_acquire); // acquire + if (old_seq % 2 == 1) { + thrd_yield(); + continue; // Retry + } + + // #2 + if (_seq.compare_exchange_strong(old_seq, old_seq + 1, + memory_order_relaxed, memory_order_relaxed)) { + thrd_yield(); + break; + } + } + + // XXX: Update the data. It needs to be release since this version use + // relaxed CAS in write(). When the first load of _seq reads the realaxed + // CAS update, it does not form synchronization, thus requiring the data to + // be acq/rel. The data in practice can be pointers to objects. + /********** Detected Correctness (testcase1) **********/ + atomic_thread_fence(memory_order_release); + _data1.store(data1, memory_order_relaxed); + _data2.store(data2, memory_order_relaxed); + /** @OPDefine: true */ + + /********** Detected Admissibility (testcase1) **********/ + _seq.fetch_add(1, memory_order_release); // release +} + +/** C Interface */ + +/** @Transition: STATE(data1) = data1; + STATE(data2) = data2; */ +void write(seqlock *lock, int data1, int data2) { + lock->write(data1, data2); +} + + +/** @JustifyingPrecondition: return STATE(data1) == *data1 && STATE(data2) == *data2; */ +void read(seqlock *lock, int *data1, int *data2) { + lock->read(data1, data2); +} diff --git a/seqlock/seqlock.h b/seqlock/seqlock.h new file mode 100644 index 0000000..1102251 --- /dev/null +++ b/seqlock/seqlock.h @@ -0,0 +1,25 @@ +#ifndef _SEQLOCK_H +#define _SEQLOCK_H + +#include + +class seqlock { + public: + // Sequence for reader consistency check + atomic_int _seq; + // It needs to be atomic to avoid data races + atomic_int _data1; + atomic_int _data2; + + seqlock(); + + void read(int *data1, int *data2); + + void write(int data1, int data2); +}; + +/** C Interface */ +void write(seqlock *lock, int data1, int data2); +void read(seqlock *lock, int *data1, int *data2); + +#endif diff --git a/seqlock/testcase1.cc b/seqlock/testcase1.cc new file mode 100644 index 0000000..df5594f --- /dev/null +++ b/seqlock/testcase1.cc @@ -0,0 +1,33 @@ +#include +#include "seqlock.h" + +seqlock *lock; + +static void a(void *obj) { + write(lock, 1, 2); +} + +static void b(void *obj) { + write(lock, 3, 4); +} + +static void c(void *obj) { + int *data1 = new int; + int *data2 = new int; + read(lock, data1, data2); +} + +int user_main(int argc, char **argv) { + thrd_t t1, t2, t3; + /** @Entry */ + lock = new seqlock; + + thrd_create(&t1, (thrd_start_t)&a, NULL); + //thrd_create(&t2, (thrd_start_t)&b, NULL); + thrd_create(&t3, (thrd_start_t)&c, NULL); + + thrd_join(t1); + //thrd_join(t2); + thrd_join(t3); + return 0; +} diff --git a/seqlock/testcase2.cc b/seqlock/testcase2.cc new file mode 100644 index 0000000..6c99e6d --- /dev/null +++ b/seqlock/testcase2.cc @@ -0,0 +1,33 @@ +#include +#include "seqlock.h" + +seqlock *lock; + +static void a(void *obj) { + write(lock, 1, 2); +} + +static void b(void *obj) { + write(lock, 3, 4); +} + +static void c(void *obj) { + int *data1 = new int; + int *data2 = new int; + read(lock, data1, data2); +} + +int user_main(int argc, char **argv) { + thrd_t t1, t2, t3; + /** @Entry */ + lock = new seqlock; + + thrd_create(&t1, (thrd_start_t)&a, NULL); + thrd_create(&t2, (thrd_start_t)&b, NULL); + thrd_create(&t3, (thrd_start_t)&c, NULL); + + thrd_join(t1); + thrd_join(t2); + thrd_join(t3); + return 0; +} diff --git a/spsc-bugfix/Makefile b/spsc-bugfix/Makefile index 33b9d01..9a72c95 100644 --- a/spsc-bugfix/Makefile +++ b/spsc-bugfix/Makefile @@ -1,23 +1,23 @@ include ../benchmarks.mk -TESTNAME = spsc-queue -RELACYNAME = spsc-relacy +BENCH := queue -all: $(TESTNAME) +BENCH_BINARY := $(BENCH).o -$(TESTNAME): $(TESTNAME).cc queue.h eventcount.h - $(CXX) -o $@ $< $(CXXFLAGS) $(LDFLAGS) +TESTS := main testcase1 -relacy: $(RELACYNAME) +all: $(TESTS) + ../generate.sh $(notdir $(shell pwd)) -$(RELACYNAME): spsc-relacy.cc queue-relacy.h eventcount-relacy.h -ifdef RELACYPATH - $(CXX) -o $(RELACYNAME) spsc-relacy.cc -I$(RELACYPATH) -Wno-deprecated -else - @echo "Please define RELACYPATH" - @echo " e.g., make RELACYPATH=/path-to-relacy" - @exit 1 -endif +%.o : %.cc + $(CXX) -c -fPIC -MMD -MF .$@.d -o $@ $< $(CXXFLAGS) $(LDFLAGS) + +$(TESTS): % : %.o $(BENCH_BINARY) + $(CXX) -o $@ $^ $(CXXFLAGS) $(LDFLAGS) + +-include .*.d clean: - rm -f $(TESTNAME) $(RELACYNAME) *.o + rm -rf $(TESTS) *.o .*.d *.dSYM + +.PHONY: clean all diff --git a/spsc-bugfix/eventcount.h b/spsc-bugfix/eventcount.h index aec3e8c..ea7458f 100644 --- a/spsc-bugfix/eventcount.h +++ b/spsc-bugfix/eventcount.h @@ -1,3 +1,6 @@ +#ifndef _EVENTCOUNT_H_ +#define _EVENTCOUNT_H_ + #include #include #include @@ -67,3 +70,5 @@ private: } } }; + +#endif diff --git a/spsc-queue/spsc-queue.cc b/spsc-bugfix/main.cc similarity index 66% rename from spsc-queue/spsc-queue.cc rename to spsc-bugfix/main.cc index f8528a8..5dcb4ea 100644 --- a/spsc-queue/spsc-queue.cc +++ b/spsc-bugfix/main.cc @@ -4,23 +4,23 @@ spsc_queue *q; - void thread(unsigned thread_index) +void thread(unsigned thread_index) +{ + if (0 == thread_index) + { + enqueue(q, 11); + } + else { - if (0 == thread_index) - { - q->enqueue(11); - } - else - { - int d = q->dequeue(); - RL_ASSERT(11 == d); - } + int d = dequeue(q); + //RL_ASSERT(11 == d); } +} int user_main(int argc, char **argv) { thrd_t A, B; - + /** @Entry */ q = new spsc_queue(); thrd_create(&A, (thrd_start_t)&thread, (void *)0); diff --git a/spsc-bugfix/queue.cc b/spsc-bugfix/queue.cc new file mode 100644 index 0000000..85903d0 --- /dev/null +++ b/spsc-bugfix/queue.cc @@ -0,0 +1,62 @@ +#include "queue.h" + +template +void spsc_queue::enqueue(T data) +{ + node* n = new node (data); + /********** Detected Correctness **********/ + //head($)->next.store(n, std::memory_order_release); + head->next.store(n, std::memory_order_release); + /** @OPDefine: true */ + head = n; + ec.signal(); +} + + +template +T spsc_queue::dequeue() +{ + T data = try_dequeue(); + while (0 == data) + { + int cmp = ec.get(); + data = try_dequeue(); + if (data) + break; + ec.wait(cmp); + data = try_dequeue(); + if (data) + break; + } + return data; +} + +template +T spsc_queue::try_dequeue() +{ + //node* t = tail($); + node* t = tail; + /********** Detected Correctness **********/ + node* n = t->next.load(std::memory_order_acquire); + /** @OPClearDefine: true */ + if (0 == n) + return 0; + //T data = n->data($); + T data = n->data; + delete (t); + tail = n; + return data; +} + +/** @DeclareState: IntList *q; */ + +/** @Transition: STATE(q)->push_back(data); */ +void enqueue(spsc_queue *q, int data) { + q->enqueue(data); +} + +/** @PreCondition: return STATE(q)->empty() ? !C_RET : STATE(q)->front() == C_RET; + @Transition: if (!C_RET) STATE(q)->pop_front(); */ +int dequeue(spsc_queue *q) { + return q->dequeue(); +} diff --git a/spsc-bugfix/queue.h b/spsc-bugfix/queue.h index 2e2f494..38be1dc 100644 --- a/spsc-bugfix/queue.h +++ b/spsc-bugfix/queue.h @@ -1,3 +1,6 @@ +#ifndef _SPSC_QUEUE_H +#define _SPSC_QUEUE_H + #include #include @@ -17,39 +20,20 @@ public: ~spsc_queue() { RL_ASSERT(head == tail); - delete ((node*)head($)); + //delete ((node*)head($)); + delete ((node*)head); } - void enqueue(T data) - { - node* n = new node (data); - head($)->next.store(n, std::memory_order_release); - head = n; - ec.signal(); - } + void enqueue(T data); - T dequeue() - { - T data = try_dequeue(); - while (0 == data) - { - int cmp = ec.get(); - data = try_dequeue(); - if (data) - break; - ec.wait(cmp); - data = try_dequeue(); - if (data) - break; - } - return data; - } + T dequeue(); private: struct node { std::atomic next; - rl::var data; + //rl::var data; + T data; node(T data = T()) : data(data) @@ -58,20 +42,20 @@ private: } }; + /* Use normal memory access rl::var head; rl::var tail; + */ + node *head; + node *tail; eventcount ec; - T try_dequeue() - { - node* t = tail($); - node* n = t->next.load(std::memory_order_acquire); - if (0 == n) - return 0; - T data = n->data($); - delete (t); - tail = n; - return data; - } + T try_dequeue(); }; + +// C Interface +void enqueue(spsc_queue *q, int data); +int dequeue(spsc_queue *q); + +#endif diff --git a/spsc-bugfix/eventcount-relacy.h b/spsc-bugfix/relacy/eventcount-relacy.h similarity index 100% rename from spsc-bugfix/eventcount-relacy.h rename to spsc-bugfix/relacy/eventcount-relacy.h diff --git a/spsc-bugfix/queue-relacy.h b/spsc-bugfix/relacy/queue-relacy.h similarity index 100% rename from spsc-bugfix/queue-relacy.h rename to spsc-bugfix/relacy/queue-relacy.h diff --git a/spsc-bugfix/spsc-relacy.cc b/spsc-bugfix/relacy/spsc-relacy.cc similarity index 100% rename from spsc-bugfix/spsc-relacy.cc rename to spsc-bugfix/relacy/spsc-relacy.cc diff --git a/spsc-bugfix/spsc-queue.cc b/spsc-bugfix/testcase1.cc similarity index 66% rename from spsc-bugfix/spsc-queue.cc rename to spsc-bugfix/testcase1.cc index f8528a8..5dcb4ea 100644 --- a/spsc-bugfix/spsc-queue.cc +++ b/spsc-bugfix/testcase1.cc @@ -4,23 +4,23 @@ spsc_queue *q; - void thread(unsigned thread_index) +void thread(unsigned thread_index) +{ + if (0 == thread_index) + { + enqueue(q, 11); + } + else { - if (0 == thread_index) - { - q->enqueue(11); - } - else - { - int d = q->dequeue(); - RL_ASSERT(11 == d); - } + int d = dequeue(q); + //RL_ASSERT(11 == d); } +} int user_main(int argc, char **argv) { thrd_t A, B; - + /** @Entry */ q = new spsc_queue(); thrd_create(&A, (thrd_start_t)&thread, (void *)0); diff --git a/spsc-queue/.gitignore b/spsc-queue/.gitignore deleted file mode 100644 index 2485456..0000000 --- a/spsc-queue/.gitignore +++ /dev/null @@ -1,2 +0,0 @@ -/spsc-queue -/spsc-relacy diff --git a/spsc-queue/Makefile b/spsc-queue/Makefile deleted file mode 100644 index 33b9d01..0000000 --- a/spsc-queue/Makefile +++ /dev/null @@ -1,23 +0,0 @@ -include ../benchmarks.mk - -TESTNAME = spsc-queue -RELACYNAME = spsc-relacy - -all: $(TESTNAME) - -$(TESTNAME): $(TESTNAME).cc queue.h eventcount.h - $(CXX) -o $@ $< $(CXXFLAGS) $(LDFLAGS) - -relacy: $(RELACYNAME) - -$(RELACYNAME): spsc-relacy.cc queue-relacy.h eventcount-relacy.h -ifdef RELACYPATH - $(CXX) -o $(RELACYNAME) spsc-relacy.cc -I$(RELACYPATH) -Wno-deprecated -else - @echo "Please define RELACYPATH" - @echo " e.g., make RELACYPATH=/path-to-relacy" - @exit 1 -endif - -clean: - rm -f $(TESTNAME) $(RELACYNAME) *.o diff --git a/spsc-queue/eventcount-relacy.h b/spsc-queue/eventcount-relacy.h deleted file mode 100644 index 9eadcf3..0000000 --- a/spsc-queue/eventcount-relacy.h +++ /dev/null @@ -1,64 +0,0 @@ -class eventcount -{ -public: - eventcount() : waiters(0) - { - count($) = 0; - } - - void signal_relaxed() - { - unsigned cmp = count.load(std::memory_order_relaxed); - signal_impl(cmp); - } - - void signal() - { - unsigned cmp = count.fetch_add(0, std::memory_order_seq_cst); - signal_impl(cmp); - } - - unsigned get() - { - unsigned cmp = count.fetch_or(0x80000000, -std::memory_order_seq_cst); - return cmp & 0x7FFFFFFF; - } - - void wait(unsigned cmp) - { - unsigned ec = count.load(std::memory_order_seq_cst); - if (cmp == (ec & 0x7FFFFFFF)) - { - guard.lock($); - ec = count.load(std::memory_order_seq_cst); - if (cmp == (ec & 0x7FFFFFFF)) - { - waiters($) += 1; - cv.wait(guard, $); - } - guard.unlock($); - } - } - -private: - std::atomic count; - rl::var waiters; - std::mutex guard; - std::condition_variable cv; - - void signal_impl(unsigned cmp) - { - if (cmp & 0x80000000) - { - guard.lock($); - while (false == count.compare_exchange_weak(cmp, - (cmp + 1) & 0x7FFFFFFF, std::memory_order_relaxed)); - unsigned w = waiters($); - waiters($) = 0; - guard.unlock($); - if (w) - cv.notify_all($); - } - } -}; diff --git a/spsc-queue/eventcount.h b/spsc-queue/eventcount.h deleted file mode 100644 index aec3e8c..0000000 --- a/spsc-queue/eventcount.h +++ /dev/null @@ -1,69 +0,0 @@ -#include -#include -#include -#include - -class eventcount -{ -public: - eventcount() : waiters(0) - { - count = 0; - } - - void signal_relaxed() - { - unsigned cmp = count.load(std::memory_order_relaxed); - signal_impl(cmp); - } - - void signal() - { - unsigned cmp = count.fetch_add(0, std::memory_order_seq_cst); - signal_impl(cmp); - } - - unsigned get() - { - unsigned cmp = count.fetch_or(0x80000000, -std::memory_order_seq_cst); - return cmp & 0x7FFFFFFF; - } - - void wait(unsigned cmp) - { - unsigned ec = count.load(std::memory_order_seq_cst); - if (cmp == (ec & 0x7FFFFFFF)) - { - guard.lock($); - ec = count.load(std::memory_order_seq_cst); - if (cmp == (ec & 0x7FFFFFFF)) - { - waiters += 1; - cv.wait(guard); - } - guard.unlock($); - } - } - -private: - std::atomic count; - rl::var waiters; - std::mutex guard; - std::condition_variable cv; - - void signal_impl(unsigned cmp) - { - if (cmp & 0x80000000) - { - guard.lock($); - while (false == count.compare_exchange_weak(cmp, - (cmp + 1) & 0x7FFFFFFF, std::memory_order_relaxed)); - unsigned w = waiters($); - waiters = 0; - guard.unlock($); - if (w) - cv.notify_all($); - } - } -}; diff --git a/spsc-queue/queue-relacy.h b/spsc-queue/queue-relacy.h deleted file mode 100644 index 71aac2a..0000000 --- a/spsc-queue/queue-relacy.h +++ /dev/null @@ -1,74 +0,0 @@ -#include "eventcount-relacy.h" - -template -class spsc_queue -{ -public: - spsc_queue() - { - node* n = new node (); - head($) = n; - tail($) = n; - } - - ~spsc_queue() - { - RL_ASSERT(head($) == tail($)); - delete ((node*)head($)); - } - - void enqueue(T data) - { - node* n = new node (data); - head($)->next.store(n, std::memory_order_release); - head($) = n; - ec.signal_relaxed(); - } - - T dequeue() - { - T data = try_dequeue(); - while (0 == data) - { - int cmp = ec.get(); - data = try_dequeue(); - if (data) - break; - ec.wait(cmp); - data = try_dequeue(); - if (data) - break; - } - return data; - } - -private: - struct node - { - std::atomic next; - rl::var data; - - node(T data = T()) - : data(data) - { - next($) = 0; - } - }; - - rl::var head; - rl::var tail; - - eventcount ec; - - T try_dequeue() - { - node* t = tail($); - node* n = t->next.load(std::memory_order_acquire); - if (0 == n) - return 0; - T data = n->data($); - delete (t); - tail($) = n; - return data; - } -}; diff --git a/spsc-queue/queue.h b/spsc-queue/queue.h deleted file mode 100644 index c77425f..0000000 --- a/spsc-queue/queue.h +++ /dev/null @@ -1,77 +0,0 @@ -#include -#include - -#include "eventcount.h" - -template -class spsc_queue -{ -public: - spsc_queue() - { - node* n = new node (); - head = n; - tail = n; - } - - ~spsc_queue() - { - RL_ASSERT(head == tail); - delete ((node*)head($)); - } - - void enqueue(T data) - { - node* n = new node (data); - head($)->next.store(n, std::memory_order_release); - head = n; - ec.signal_relaxed(); - } - - T dequeue() - { - T data = try_dequeue(); - while (0 == data) - { - int cmp = ec.get(); - data = try_dequeue(); - if (data) - break; - ec.wait(cmp); - data = try_dequeue(); - if (data) - break; - } - return data; - } - -private: - struct node - { - std::atomic next; - rl::var data; - - node(T data = T()) - : data(data) - { - next = 0; - } - }; - - rl::var head; - rl::var tail; - - eventcount ec; - - T try_dequeue() - { - node* t = tail($); - node* n = t->next.load(std::memory_order_acquire); - if (0 == n) - return 0; - T data = n->data($); - delete (t); - tail = n; - return data; - } -}; diff --git a/spsc-queue/spsc-relacy.cc b/spsc-queue/spsc-relacy.cc deleted file mode 100644 index 37ed989..0000000 --- a/spsc-queue/spsc-relacy.cc +++ /dev/null @@ -1,27 +0,0 @@ -#include - -#include "queue-relacy.h" - -struct spsc_queue_test : rl::test_suite -{ - spsc_queue q; - - void thread(unsigned thread_index) - { - if (0 == thread_index) - { - q.enqueue(11); - } - else - { - int d = q.dequeue(); - RL_ASSERT(11 == d); - } - } -}; - - -int main() -{ - rl::simulate(); -} diff --git a/ticket-lock/Makefile b/ticket-lock/Makefile new file mode 100644 index 0000000..e222765 --- /dev/null +++ b/ticket-lock/Makefile @@ -0,0 +1,23 @@ +include ../benchmarks.mk + +BENCH := lock + +BENCH_BINARY := $(BENCH).o + +TESTS := main testcase1 + +all: $(TESTS) + ../generate.sh $(notdir $(shell pwd)) + +%.o : %.c + $(CC) -c -fPIC -MMD -MF .$@.d -o $@ $< $(CFLAGS) $(LDFLAGS) + +$(TESTS): % : %.o $(BENCH_BINARY) + $(CC) -o $@ $^ $(CFLAGS) $(LDFLAGS) + +-include .*.d + +clean: + rm -rf $(TESTS) *.o .*.d *.dSYM + +.PHONY: clean all diff --git a/ticket-lock/lock.c b/ticket-lock/lock.c new file mode 100644 index 0000000..b572950 --- /dev/null +++ b/ticket-lock/lock.c @@ -0,0 +1,48 @@ +#include + +#include "librace.h" +#include "lock.h" + +/** + This ticket lock implementation is derived from the original Mellor-Crummey + & Scott paper in 1991. + It assumes that the ticket and turn counter are large enough to accommodate + the maximum number of simultaneous requests for the lock. +*/ + +/** @DeclareState: bool lock; */ + + +void initTicketLock(TicketLock *l) { + atomic_init(&l->ticket, 0); + atomic_init(&l->turn, 0); +} + +/** @PreCondition: return STATE(lock) == false; +@Transition: STATE(lock) = true; */ +void lock(struct TicketLock *l) { + // First grab a ticket + unsigned ticket = atomic_fetch_add_explicit(&l->ticket, 1, + memory_order_relaxed); + // Spinning for my turn + while (true) { + /********** Detected Correctness (testcase1 with -Y) **********/ + unsigned turn = atomic_load_explicit(&l->turn, memory_order_acquire); + /** @OPDefine: turn == ticket */ + if (turn == ticket) { // Now it's my turn + return; + } else { + thrd_yield(); // Added for CDSChecker + } + } +} + +/** @PreCondition: return STATE(lock) == true; +@Transition: STATE(lock) = false; */ +void unlock(struct TicketLock *l) { + unsigned turn = atomic_load_explicit(&l->turn, memory_order_relaxed); + /********** Detected Correctness (testcase1 with -Y) **********/ + atomic_store_explicit(&l->turn, turn + 1, memory_order_release); + /** @OPDefine: true */ +} diff --git a/ticket-lock/lock.h b/ticket-lock/lock.h new file mode 100644 index 0000000..2e5d5a9 --- /dev/null +++ b/ticket-lock/lock.h @@ -0,0 +1,19 @@ +#ifndef _LOCK_H +#define _LOCK_H + +#include +#include +#include + +typedef struct TicketLock { + atomic_uint ticket; + atomic_uint turn; +} TicketLock; + +void initTicketLock(TicketLock* l); + +void lock(TicketLock *l); + +void unlock(TicketLock *l); + +#endif diff --git a/ticket-lock/main.c b/ticket-lock/main.c new file mode 100644 index 0000000..1b4ff83 --- /dev/null +++ b/ticket-lock/main.c @@ -0,0 +1,39 @@ +#include +#include + +#include "librace.h" +#include "lock.h" + +TicketLock mylock; +int shareddata; + +static void a(void *obj) +{ + int i; + for(i = 0; i < 2; i++) { + if ((i % 2) == 0) { + lock(&mylock); + //load_32(&shareddata); + unlock(&mylock); + } else { + lock(&mylock); + //store_32(&shareddata,(unsigned int)i); + unlock(&mylock); + } + } +} + +int user_main(int argc, char **argv) +{ + thrd_t t1, t2; + /** @Entry */ + initTicketLock(&mylock); + + thrd_create(&t1, (thrd_start_t)&a, NULL); + thrd_create(&t2, (thrd_start_t)&a, NULL); + + thrd_join(t1); + thrd_join(t2); + + return 0; +} diff --git a/ticket-lock/testcase1.c b/ticket-lock/testcase1.c new file mode 100644 index 0000000..1b4ff83 --- /dev/null +++ b/ticket-lock/testcase1.c @@ -0,0 +1,39 @@ +#include +#include + +#include "librace.h" +#include "lock.h" + +TicketLock mylock; +int shareddata; + +static void a(void *obj) +{ + int i; + for(i = 0; i < 2; i++) { + if ((i % 2) == 0) { + lock(&mylock); + //load_32(&shareddata); + unlock(&mylock); + } else { + lock(&mylock); + //store_32(&shareddata,(unsigned int)i); + unlock(&mylock); + } + } +} + +int user_main(int argc, char **argv) +{ + thrd_t t1, t2; + /** @Entry */ + initTicketLock(&mylock); + + thrd_create(&t1, (thrd_start_t)&a, NULL); + thrd_create(&t2, (thrd_start_t)&a, NULL); + + thrd_join(t1); + thrd_join(t2); + + return 0; +} diff --git a/treiber-stack/Makefile b/treiber-stack/Makefile deleted file mode 100644 index 99cac3f..0000000 --- a/treiber-stack/Makefile +++ /dev/null @@ -1,10 +0,0 @@ -include ../benchmarks.mk - -main: my_stack.o main.c - $(CC) -o $@ $^ $(CFLAGS) $(LDFLAGS) - -%.o: %.c - $(CC) -c -o $@ $^ $(CFLAGS) - -clean: - rm -f *.o diff --git a/treiber-stack/main.c b/treiber-stack/main.c deleted file mode 100644 index 6342d84..0000000 --- a/treiber-stack/main.c +++ /dev/null @@ -1,89 +0,0 @@ -#include -#include -#include - -#include "my_stack.h" -#include "model-assert.h" - -static int procs = 4; -static mystack_t *stack; -static thrd_t *threads; -static int num_threads; - -unsigned int idx1, idx2; -unsigned int a, b; - - -atomic_int x[3]; - -int get_thread_num() -{ - thrd_t curr = thrd_current(); - int i; - for (i = 0; i < num_threads; i++) - if (curr.priv == threads[i].priv) - return i; - MODEL_ASSERT(0); - return -1; -} - -static void main_task(void *param) -{ - unsigned int val; - int pid = *((int *)param); - - if (pid % 4 == 0) { - atomic_store_explicit(&x[1], 17, relaxed); - push(stack, 1); - } else if (pid % 4 == 1) { - atomic_store_explicit(&x[2], 37, relaxed); - push(stack, 2); - } else if (pid % 4 == 2) {/* - idx1 = pop(stack); - if (idx1 != 0) { - a = atomic_load_explicit(&x[idx1], relaxed); - printf("a: %d\n", a); - }*/ - } else { - idx2 = pop(stack); - if (idx2 != 0) { - b = atomic_load_explicit(&x[idx2], relaxed); - printf("b: %d\n", b); - } - } -} - -int user_main(int argc, char **argv) -{ - int i; - int *param; - unsigned int in_sum = 0, out_sum = 0; - - atomic_init(&x[1], 0); - atomic_init(&x[2], 0); - - stack = calloc(1, sizeof(*stack)); - - num_threads = procs; - threads = malloc(num_threads * sizeof(thrd_t)); - param = malloc(num_threads * sizeof(*param)); - - init_stack(stack, num_threads); - - for (i = 0; i < num_threads; i++) { - param[i] = i; - thrd_create(&threads[i], main_task, ¶m[i]); - } - for (i = 0; i < num_threads; i++) - thrd_join(threads[i]); - - bool correct = false; - //correct |= (a == 17 || a == 37 || a == 0); - //MODEL_ASSERT(correct); - - free(param); - free(threads); - free(stack); - - return 0; -} diff --git a/treiber-stack/my_stack.c b/treiber-stack/my_stack.c deleted file mode 100644 index f65417d..0000000 --- a/treiber-stack/my_stack.c +++ /dev/null @@ -1,123 +0,0 @@ -#include -#include -#include "librace.h" -#include "model-assert.h" - -#include "my_stack.h" - -#define MAX_FREELIST 4 /* Each thread can own up to MAX_FREELIST free nodes */ -#define INITIAL_FREE 2 /* Each thread starts with INITIAL_FREE free nodes */ - -#define POISON_IDX 0x666 - -static unsigned int (*free_lists)[MAX_FREELIST]; - -/* Search this thread's free list for a "new" node */ -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 = free_lists[t][i]; - if (node) { - //store_32(&free_lists[t][i], 0); - free_lists[t][i] = 0; - return node; - } - } - /* free_list is empty? */ - MODEL_ASSERT(0); - return 0; -} - -/* Place this node index back on this thread's free list */ -static void reclaim(unsigned int node) -{ - int i; - int t = get_thread_num(); - - /* Don't reclaim NULL 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 = free_lists[t][i]; - - /* Found empty spot in free list */ - if (idx == 0) { - //store_32(&free_lists[t][i], node); - free_lists[t][i] = node; - return; - } - } - /* free list is full? */ - MODEL_ASSERT(0); -} - -void init_stack(mystack_t *s, int num_threads) -{ - int i, j; - - /* Initialize each thread's free list with INITIAL_FREE pointers */ - /* The actual nodes are initialized with poison indexes */ - free_lists = malloc(num_threads * sizeof(*free_lists)); - for (i = 0; i < num_threads; i++) { - for (j = 0; j < INITIAL_FREE; j++) { - free_lists[i][j] = 1 + i * MAX_FREELIST + j; - atomic_init(&s->nodes[free_lists[i][j]].next, MAKE_POINTER(POISON_IDX, 0)); - } - } - - /* initialize stack */ - atomic_init(&s->top, MAKE_POINTER(0, 0)); -} - -void push(mystack_t *s, unsigned int val) { - unsigned int nodeIdx = new_node(); - node_t *node = &s->nodes[nodeIdx]; - node->value = val; - pointer oldTop, newTop; - bool success; - while (true) { - // acquire - oldTop = atomic_load_explicit(&s->top, acquire); - newTop = MAKE_POINTER(nodeIdx, get_count(oldTop) + 1); - // relaxed - atomic_store_explicit(&node->next, oldTop, relaxed); - - // release & relaxed - success = atomic_compare_exchange_strong_explicit(&s->top, &oldTop, - newTop, release, relaxed); - if (success) - break; - } -} - -unsigned int pop(mystack_t *s) -{ - pointer oldTop, newTop, next; - node_t *node; - bool success; - int val; - while (true) { - // acquire - oldTop = atomic_load_explicit(&s->top, acquire); - if (get_ptr(oldTop) == 0) - return 0; - node = &s->nodes[get_ptr(oldTop)]; - // relaxed - next = atomic_load_explicit(&node->next, relaxed); - newTop = MAKE_POINTER(get_ptr(next), get_count(oldTop) + 1); - // release & relaxed - success = atomic_compare_exchange_strong_explicit(&s->top, &oldTop, - newTop, release, relaxed); - if (success) - break; - } - val = node->value; - /* Reclaim the used slot */ - reclaim(get_ptr(oldTop)); - return val; -} -- 2.34.1