From: Peizhao Ou Date: Wed, 7 Dec 2016 21:24:43 +0000 (-0800) Subject: edits: add comments to demonstrate the found bugs and bug injections X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=fd62fd9d7f0bb39d19155db6af758c44e3dbb43b;p=model-checker-benchmarks.git edits: add comments to demonstrate the found bugs and bug injections --- diff --git a/Makefile b/Makefile index 7471656..194e1ff 100644 --- a/Makefile +++ b/Makefile @@ -1,7 +1,6 @@ -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 +DIRS := ms-queue linuxrwlocks mcs-lock \ + chase-lev-deque-bugfix ticket-lock seqlock read-copy-update \ + concurrent-hashmap spsc-bugfix mpmc-queue .PHONY: $(DIRS) diff --git a/bench.sh b/bench.sh deleted file mode 100755 index 7c9eec8..0000000 --- a/bench.sh +++ /dev/null @@ -1,71 +0,0 @@ -#!/bin/bash - -# A (work-in-progress) test script for running our benchmarks -# Runs all tests, with timing information - -DATECMD="date +%Y-%m-%d-%R" -DATE="`${DATECMD}`" - -TESTS="chase-lev-deque/main" -TESTS+=" spsc-queue/spsc-queue" -TESTS+=" spsc-bugfix/spsc-queue" -TESTS+=" barrier/barrier" -TESTS+=" dekker-fences/dekker-fences" -TESTS+=" mcs-lock/mcs-lock" -TESTS+=" mpmc-queue/mpmc-queue-rdwr" -TESTS+=" ms-queue/main" -TESTS+=" linuxrwlocks/linuxrwlocks" - -MODEL_ARGS="-y -m 2 -u 3" - -#TESTS+=" mpmc-queue/mpmc-2r1w" -#TESTS+=" mpmc-queue/mpmc-1r2w-noinit" -#TESTS+=" mpmc-queue/mpmc-queue-rdwr" -#TESTS+=" mpmc-queue/mpmc-queue-noinit" - -COUNT=0 - -function run_test { - t=$1 - shift - ARGS="$@" - RUN="./run.sh" - - echo "-----------------------------------------------" - echo "*******************************" - echo "Running test ${COUNT} (${t})" - echo "ARGS=${ARGS}" - echo "*******************************" - (time ${RUN} ${t} ${ARGS} 2>&1) 2>&1 - echo - echo "Test done; sleeping for a few seconds" - echo - - let COUNT++ -} - -function run_all_tests { - echo ${DATE} - - for t in ${TESTS} - do - run_test ${t} ${MODEL_ARGS} - done - #run_test mpmc-queue/mpmc-queue ${MODEL_ARGS} -- -r 2 -w 1 - #run_test mpmc-queue/mpmc-queue ${MODEL_ARGS} -- -r 1 -w 2 - #run_test mpmc-queue/mpmc-queue ${MODEL_ARGS} -- -r 2 -w 2 -} - -# Check if git is available, and this is a git repository -GIT=0 -which git &> /dev/null && git rev-parse &> /dev/null && GIT=1 - -# Print out some git information, if available -if [ ${GIT} -ne 0 ]; then - cd .. - git log --oneline -1 - cd - > /dev/null - git log --oneline -1 - echo -fi -run_all_tests diff --git a/blocking-mpmc-example/Makefile b/blocking-mpmc-example/Makefile deleted file mode 100644 index 8dd491a..0000000 --- a/blocking-mpmc-example/Makefile +++ /dev/null @@ -1,23 +0,0 @@ -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 deleted file mode 100644 index dd9a83c..0000000 --- a/blocking-mpmc-example/example.txt +++ /dev/null @@ -1,39 +0,0 @@ -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 deleted file mode 100644 index 9b3a6af..0000000 --- a/blocking-mpmc-example/main.cc +++ /dev/null @@ -1,56 +0,0 @@ -#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 deleted file mode 100644 index f86547b..0000000 --- a/blocking-mpmc-example/queue.cc +++ /dev/null @@ -1,49 +0,0 @@ -#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 deleted file mode 100644 index e7d1515..0000000 --- a/blocking-mpmc-example/queue.h +++ /dev/null @@ -1,36 +0,0 @@ -#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 deleted file mode 100644 index 3851988..0000000 --- a/blocking-mpmc-example/testcase1.cc +++ /dev/null @@ -1,86 +0,0 @@ -#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 deleted file mode 100644 index 1e66c2e..0000000 --- a/blocking-mpmc-example/testcase2.cc +++ /dev/null @@ -1,88 +0,0 @@ -#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 deleted file mode 100644 index 5a2bbbe..0000000 --- a/blocking-mpmc-example/testcase3.cc +++ /dev/null @@ -1,88 +0,0 @@ -#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 deleted file mode 100644 index fbb0cea..0000000 --- a/blocking-mpmc-example/testcase4.cc +++ /dev/null @@ -1,89 +0,0 @@ -#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 dca2e81..2389f07 100644 --- a/chase-lev-deque-bugfix/Makefile +++ b/chase-lev-deque-bugfix/Makefile @@ -4,7 +4,7 @@ BENCH := deque BENCH_BINARY := $(BENCH).o -TESTS := main testcase1 testcase2 testcase3 testcase4 testcase5 testcase6 +TESTS := main testcase1 testcase2 testcase3 all: $(TESTS) ../generate.sh $(notdir $(shell pwd)) diff --git a/chase-lev-deque-bugfix/deque.c b/chase-lev-deque-bugfix/deque.c index b851e51..71aeff7 100644 --- a/chase-lev-deque-bugfix/deque.c +++ b/chase-lev-deque-bugfix/deque.c @@ -25,6 +25,24 @@ Deque * create_size(int size) { Deque * create() { Deque * q = (Deque *) calloc(1, sizeof(Deque)); Array * a = (Array *) calloc(1, sizeof(Array)+2*sizeof(atomic_int)); + + /** + * We specifically create the space of the new array in this initialization + * method just to make up the fact that the new array can potentially be + * used by other things or contains just junk data. Please see Section 6.4.1 + * for more detail. + */ + /********** BEGIN **********/ + int new_size = 8; + Array *new_a = (Array *) calloc(1, new_size * sizeof(atomic_int) + sizeof(Array)); + atomic_store_explicit(&new_a->size, new_size, memory_order_relaxed); + int i; + for(i=0; i < new_size; i++) { + atomic_store_explicit(&new_a->buffer[i % new_size], 0, memory_order_relaxed); + } + q->newArray = new_a; + /********** END **********/ + 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); @@ -42,7 +60,6 @@ Deque * create() { 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 @@ -71,6 +88,10 @@ int take(Deque *q) { 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); + + // XXX-injection-#1: Weaken the parameter "memory_order_seq_cst" to + // "memory_order_acq_rel", run "make" to recompile, and then run: + // "./run.sh ./chase-lev-deque-bugfix/testcase2 -m2 -y -u3 -tSPEC" /********** Detected Correctness (testcase2) **********/ atomic_thread_fence(memory_order_seq_cst); size_t t = atomic_load_explicit(&q->top, memory_order_relaxed); @@ -82,7 +103,9 @@ int take(Deque *q) { x = atomic_load_explicit(&a->buffer[b % sz], memory_order_relaxed); if (t == b) { /* Single last element in queue. */ - // FIXME: This might not be necessary!!! We don't know yet + // XXX-overly-strong-#1: This was confirmed by the original authors + // that the first parameter doesn't have to be memory_order_seq_cst + // (which was the original one in the PPoPP'13 paper). if (!atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1, memory_order_relaxed, memory_order_relaxed)) { /* Failed race. */ @@ -105,24 +128,23 @@ void resize(Deque *q) { Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed); size_t size=atomic_load_explicit(&a->size, memory_order_relaxed); size_t new_size=size << 1; - Array *new_a = (Array *) calloc(1, new_size * sizeof(atomic_int) + sizeof(Array)); + + // Suppose the allocation returns a pack of memroy that was used by + // something else before. + // Array *new_a = (Array *) calloc(1, new_size * sizeof(atomic_int) + sizeof(Array)); // This is the original line + Array *new_a = (Array *) q->newArray; + size_t top=atomic_load_explicit(&q->top, memory_order_relaxed); size_t bottom=atomic_load_explicit(&q->bottom, memory_order_relaxed); atomic_store_explicit(&new_a->size, new_size, memory_order_relaxed); size_t i; - - // 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); } + // XXX-injection-#2: Weaken the parameter "memory_order_release" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./chase-lev-deque-bugfix/testcase1 -m2 -y -u3 -tSPEC" /********** Detected UL **********/ atomic_store_explicit(&q->array, new_a, memory_order_release); printf("resize\n"); @@ -131,6 +153,9 @@ void resize(Deque *q) { /** @Transition: STATE(deque)->push_back(x); */ void push(Deque *q, int x) { size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed); + // XXX-injection-#3: Weaken the parameter "memory_order_acquire" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./chase-lev-deque-bugfix/testcase1 -x1000 -m2 -y -u3 -tSPEC" /********** 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); @@ -143,6 +168,10 @@ void push(Deque *q, int x) { // 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 */ + + // XXX-injection-#4: Weaken the parameter "memory_order_release" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./chase-lev-deque-bugfix/testcase1 -m2 -y -u3 -tSPEC" /********** Detected UL (testcase1) **********/ atomic_thread_fence(memory_order_release); atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed); @@ -155,21 +184,39 @@ void push(Deque *q, int x) { STATE(deque)->pop_front(); } */ int steal(Deque *q) { - // XXX: The following load should be just relaxed (cause it's followed by an - // SC fence (discussed in AutoMO) + // XXX-overly-strong-#2: This was found by AutoMO and was confirmed by the + // original authors that the parameter doesn't have to be + // memory_order_acquire (which was the original one in the PPoPP'13 paper). + // The reason is that this load is followed by an SC fence (discussed in + // AutoMO). size_t t = atomic_load_explicit(&q->top, memory_order_relaxed); - /********** Detected Correctness (testcase2) **********/ + + // XXX-injection-#5: Weaken the parameter "memory_order_seq_cst" to + // "memory_order_acq_rel", run "make" to recompile, and then run: + // "./run.sh ./chase-lev-deque-bugfix/testcase3 -m2 -y -u3 -x200 -tSPEC" + /********** Detected Correctness (testcase3) **********/ atomic_thread_fence(memory_order_seq_cst); + + // XXX-injection-#6: Weaken the parameter "memory_order_acquire" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./chase-lev-deque-bugfix/testcase1 -x100 -m2 -y -u3 -tSPEC" /********** 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) **********/ + // XXX-known-bug-#1: To reproduce the bug, weaken the parameter + // "memory_order_acquire" to "memory_order_relaxed", run "make" to + // recompile, and then run: + // "./run.sh ./chase-lev-deque-bugfix/testcase1 -x100 -m2 -y -u3 -tSPEC" + /********** Detected Correctness after initializing the array (testcase1 -x100) **********/ Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_acquire); 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) **********/ + // XXX-injection-#7: Weaken the parameter "memory_order_seq_cst" to + // "memory_order_acq_rel", run "make" to recompile, and then run: + // "./run.sh ./chase-lev-deque-bugfix/testcase3 -x500 -m2 -y -u3 -tSPEC" + /********** Detected Correctness (testcase3 -x500) **********/ bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1, memory_order_seq_cst, memory_order_relaxed); /** @OPDefine: true */ diff --git a/chase-lev-deque-bugfix/deque.h b/chase-lev-deque-bugfix/deque.h index b61f8c7..9927f9d 100644 --- a/chase-lev-deque-bugfix/deque.h +++ b/chase-lev-deque-bugfix/deque.h @@ -12,6 +12,12 @@ typedef struct { typedef struct { atomic_size_t top, bottom; atomic_uintptr_t array; /* Atomic(Array *) */ + + // This is just used to mask the uninitialized loads in the known bugs to + // show that even without the CDSChecker's internal check, CDSSpec can + // also + // detects the known bug. + void *newArray; } Deque; Deque * create_size(int size); diff --git a/chase-lev-deque-bugfix/testcase3.c b/chase-lev-deque-bugfix/testcase3.c index 15cbd4e..c2f8e78 100644 --- a/chase-lev-deque-bugfix/testcase3.c +++ b/chase-lev-deque-bugfix/testcase3.c @@ -42,7 +42,7 @@ int user_main(int argc, char **argv) int d =take(q); bool correct= b == 1 && c == 2 && a == 2 ; - MODEL_ASSERT(!correct); + //MODEL_ASSERT(!correct); /* bool correct=true; if (a!=1 && a!=2 && a!=4 && a!= EMPTY) diff --git a/chase-lev-deque-bugfix/testcase4.c b/chase-lev-deque-bugfix/testcase4.c deleted file mode 100644 index 060c5f8..0000000 --- a/chase-lev-deque-bugfix/testcase4.c +++ /dev/null @@ -1,54 +0,0 @@ -#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 deleted file mode 100644 index f9552a7..0000000 --- a/chase-lev-deque-bugfix/testcase5.c +++ /dev/null @@ -1,55 +0,0 @@ -#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 deleted file mode 100644 index e2b3451..0000000 --- a/chase-lev-deque-bugfix/testcase6.c +++ /dev/null @@ -1,55 +0,0 @@ -#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/chase-lev-deque/.gitignore b/chase-lev-deque/.gitignore deleted file mode 100644 index 95811e0..0000000 --- a/chase-lev-deque/.gitignore +++ /dev/null @@ -1 +0,0 @@ -/main diff --git a/chase-lev-deque/Makefile b/chase-lev-deque/Makefile deleted file mode 100644 index 0e20427..0000000 --- a/chase-lev-deque/Makefile +++ /dev/null @@ -1,17 +0,0 @@ -include ../benchmarks.mk - -TESTNAME = main - -HEADERS = deque.h -OBJECTS = main.o deque.o - -all: $(TESTNAME) - -$(TESTNAME): $(HEADERS) $(OBJECTS) - $(CC) -o $@ $(OBJECTS) $(CFLAGS) $(LDFLAGS) - -%.o: %.c - $(CC) -c -o $@ $< $(CFLAGS) - -clean: - rm -f $(TESTNAME) *.o diff --git a/chase-lev-deque/deque.c b/chase-lev-deque/deque.c deleted file mode 100644 index 0ad7830..0000000 --- a/chase-lev-deque/deque.c +++ /dev/null @@ -1,85 +0,0 @@ -#include -#include -#include "deque.h" -#include -#include - -Deque * create() { - Deque * q = (Deque *) calloc(1, sizeof(Deque)); - Array * a = (Array *) calloc(1, sizeof(Array)+2*sizeof(atomic_int)); - atomic_store_explicit(&q->array, a, memory_order_relaxed); - atomic_store_explicit(&q->top, 0, memory_order_relaxed); - atomic_store_explicit(&q->bottom, 0, memory_order_relaxed); - atomic_store_explicit(&a->size, 2, memory_order_relaxed); - return q; -} - -int take(Deque *q) { - size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed) - 1; - Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed); - atomic_store_explicit(&q->bottom, b, memory_order_relaxed); - atomic_thread_fence(memory_order_seq_cst); - size_t t = atomic_load_explicit(&q->top, memory_order_relaxed); - int x; - if (t <= b) { - /* Non-empty queue. */ - x = atomic_load_explicit(&a->buffer[b % atomic_load_explicit(&a->size,memory_order_relaxed)], memory_order_relaxed); - if (t == b) { - /* Single last element in queue. */ - if (!atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1, memory_order_seq_cst, memory_order_relaxed)) - /* Failed race. */ - x = EMPTY; - atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed); - } - } else { /* Empty queue. */ - x = EMPTY; - atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed); - } - return x; -} - -void resize(Deque *q) { - Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed); - size_t size=atomic_load_explicit(&a->size, memory_order_relaxed); - size_t new_size=size << 1; - Array *new_a = (Array *) calloc(1, new_size * sizeof(atomic_int) + sizeof(Array)); - size_t top=atomic_load_explicit(&q->top, memory_order_relaxed); - size_t bottom=atomic_load_explicit(&q->bottom, memory_order_relaxed); - atomic_store_explicit(&new_a->size, new_size, memory_order_relaxed); - size_t i; - for(i=top; i < bottom; i++) { - atomic_store_explicit(&new_a->buffer[i % new_size], atomic_load_explicit(&a->buffer[i % size], memory_order_relaxed), memory_order_relaxed); - } - atomic_store_explicit(&q->array, new_a, memory_order_relaxed); - printf("resize\n"); -} - -void push(Deque *q, int x) { - size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed); - size_t t = atomic_load_explicit(&q->top, memory_order_acquire); - Array *a = (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); - //Bug in paper...should have next line... - a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed); - } - atomic_store_explicit(&a->buffer[b % atomic_load_explicit(&a->size, memory_order_relaxed)], x, memory_order_relaxed); - atomic_thread_fence(memory_order_release); - atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed); -} - -int steal(Deque *q) { - size_t t = atomic_load_explicit(&q->top, memory_order_acquire); - atomic_thread_fence(memory_order_seq_cst); - size_t b = atomic_load_explicit(&q->bottom, memory_order_acquire); - int x = EMPTY; - if (t < b) { - /* Non-empty queue. */ - Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed); - x = atomic_load_explicit(&a->buffer[t % atomic_load_explicit(&a->size, memory_order_relaxed)], memory_order_relaxed); - if (!atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1, memory_order_seq_cst, memory_order_relaxed)) - /* Failed race. */ - return ABORT; - } - return x; -} diff --git a/chase-lev-deque/deque.h b/chase-lev-deque/deque.h deleted file mode 100644 index 91f4ab0..0000000 --- a/chase-lev-deque/deque.h +++ /dev/null @@ -1,23 +0,0 @@ -#ifndef DEQUE_H -#define DEQUE_H - -typedef struct { - atomic_size_t size; - atomic_int buffer[]; -} Array; - -typedef struct { - atomic_size_t top, bottom; - atomic_uintptr_t array; /* Atomic(Array *) */ -} Deque; - -Deque * create(); -int take(Deque *q); -int steal(Deque *q); -void resize(Deque *q); -void push(Deque *q, int x); - -#define EMPTY 0xffffffff -#define ABORT 0xfffffffe - -#endif diff --git a/chase-lev-deque/main.c b/chase-lev-deque/main.c deleted file mode 100644 index f2e8dca..0000000 --- a/chase-lev-deque/main.c +++ /dev/null @@ -1,46 +0,0 @@ -#include -#include -#include -#include -#include - -#include "model-assert.h" - -#include "deque.h" - -Deque *q; -int a; -int b; -int c; - -static void task(void * param) { - a=steal(q); -} - -int user_main(int argc, char **argv) -{ - thrd_t t; - q=create(); - thrd_create(&t, task, 0); - push(q, 1); - push(q, 2); - push(q, 4); - b=take(q); - c=take(q); - thrd_join(t); - - bool correct=true; - if (a!=1 && a!=2 && a!=4 && a!= EMPTY) - correct=false; - if (b!=1 && b!=2 && b!=4 && b!= EMPTY) - correct=false; - if (c!=1 && c!=2 && c!=4 && a!= EMPTY) - correct=false; - if (a!=EMPTY && b!=EMPTY && c!=EMPTY && (a+b+c)!=7) - correct=false; - if (!correct) - printf("a=%d b=%d c=%d\n",a,b,c); - MODEL_ASSERT(correct); - - return 0; -} diff --git a/concurrent-hashmap/hashmap.cc b/concurrent-hashmap/hashmap.cc index 9b0ede6..65aa169 100644 --- a/concurrent-hashmap/hashmap.cc +++ b/concurrent-hashmap/hashmap.cc @@ -20,12 +20,18 @@ int HashMap::get(int key) { // lock, we ignore this operation for the SC analysis, and otherwise we // take it into consideration + // XXX-injection-#1: Weaken the parameter "mo_acquire" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./concurrent-hashmap/testcase2 -m2 -y -u3 -tSPEC" /********** Detected UL (testcase2) **********/ Entry *firstPtr = first->load(mo_acquire); e = firstPtr; while (e != NULL) { if (e->hash == hash && eq(key, e->key)) { + // XXX-injection-#2: Weaken the parameter "mo_seqcst" to + // "memory_order_acq_rel", run "make" to recompile, and then run: + // "./run.sh ./concurrent-hashmap/testcase1 -m2 -y -u3 -tSPEC" /********** Detected Correctness (testcase1) **********/ res = e->value.load(mo_seqcst); /** @OPClearDefine: res != 0 */ @@ -88,6 +94,9 @@ int HashMap::put(int key, int value) { // FIXME: This could be a relaxed (because locking synchronize // with the previous put())?? no need to be acquire oldValue = e->value.load(relaxed); + // XXX-injection-#3: Weaken the parameter "mo_seqcst" to + // "memory_order_acq_rel", run "make" to recompile, and then run: + // "./run.sh ./concurrent-hashmap/testcase1 -m2 -y -u3 -tSPEC" /********** Detected Correctness (testcase1) **********/ e->value.store(value, mo_seqcst); /** @OPClearDefine: true */ @@ -105,6 +114,9 @@ int HashMap::put(int key, int value) { newEntry->value.store(value, relaxed); /** @OPClearDefine: true */ newEntry->next.store(firstPtr, relaxed); + // XXX-injection-#4: Weaken the parameter "mo_release" to + // "memory_order_acquire", run "make" to recompile, and then run: + // "./run.sh ./concurrent-hashmap/testcase2 -m2 -y -u3 -tSPEC" /********** Detected UL (testcase2) **********/ // Publish the newEntry to others first->store(newEntry, mo_release); diff --git a/count-lines.sh b/count-lines.sh deleted file mode 100755 index 8e4081a..0000000 --- a/count-lines.sh +++ /dev/null @@ -1,32 +0,0 @@ -#!/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/doc/benchmark-list.txt b/doc/benchmark-list.txt deleted file mode 100644 index 9b64195..0000000 --- a/doc/benchmark-list.txt +++ /dev/null @@ -1,38 +0,0 @@ -*** LOCK LIKE THINGS *** - -barrier [36 LOC in .h] - C++ implementation of a spinlock barrier with a wait() call - -seqlock [50 LOC] - C implementation of a lock; two atomic_ints of state - -dekker-fences [75 LOC] - C++ implementation of Dekker's critical seciton algorithm, implemented with fences - -linuxrwlocks [80 LOC] - C implementation of linux-like RW lock - -*** ARRAY-BASED DATA STRUCTURES *** - -mpmc-queue [97 LOC] - C++ implementation of bounded queue - uses 3 atomic ints as state, plus the queue itself---an array of fixed size - -chase-lev-deque-bugfix [23 LOC in .h, 85 LOC in .c] - C implementation of a deque ADT, uses atomic_store_explicit, and an array - -*** LINKED DATA STRUCTURES **** - -mcs-lock [93 LOC] - C++ implementation of mcs mutex, implements a linked list - -treiber-stack [158 LOC] -ms-queue [192 LOC] - C implementation of a stack and queue, respectively. Uses -> next, indexes an array. - -spsc-queue [77 LOC in queue.h] - C++ implementation of a queue via linked list - -cliffc-hashtable [971 LOC in .h file] - C++ implementation of a simplified Java NonblockingHashMap - diff --git a/doc/scanalysis_result.txt b/doc/scanalysis_result.txt deleted file mode 100644 index 981329b..0000000 --- a/doc/scanalysis_result.txt +++ /dev/null @@ -1,15 +0,0 @@ -Chase-Lev (buggy) 65 24 0.0020 0.10 68 3.0*10^-5 | 0.099 1953 -Chase-Lev (correct) 49 1 0.0016 0.05 75 3.2*10^-5 | 0.050 1561 -SPSC (buggy) 10 2 0.0003 0.01 26 2.5*10^-5 | 0.009 254 -SPSC (correct) 15 0 0.0005 0.01 29 3.4*10^-5 | 0.013 509 -Barrier 7 0 0.0002 0.01 23 3.5*10^-5 | 0.007 245 -Dekker 2313 0 0.0793 9.51 52 3.4*10^-5 | 9.511 79343 -MCS lock 12609 0 0.3417 4.43 65 2.7*10^-5 | 4.432 341693 -MPMC queue 11306 6282 0.3593 9.90 49 3.2*10^-5 | 9.904 359345 -M&S queue 114 0 0.0029 0.06 55 2.5*10^-5 | 0.060 2854 -Linux RW lock 1348 0 0.0272 13.06 30 2.0*10^-5 | 13.064 27211 -Seqlock 9124 0 0.4902 3.84 38 5.4*10^-5 | 3.838 490303 - -# All run with -m -y2 (also -u10 for chase-lev deque) -# We ran mpmc-queue-rdwr for mpmc queue -# Date: 08/07/2014 10:49am (PST) diff --git a/linuxrwlocks/linuxrwlocks.c b/linuxrwlocks/linuxrwlocks.c index 408f35b..4fa29a1 100644 --- a/linuxrwlocks/linuxrwlocks.c +++ b/linuxrwlocks/linuxrwlocks.c @@ -53,6 +53,9 @@ int write_can_lock(rwlock_t *lock) void read_lock(rwlock_t *rw) { + // XXX-injection-#1: Weaken the parameter "memory_order_acquire" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./linuxrwlocks/testcase1 -m2 -y -u3 -tSPEC" /********** Detected Correctness (testcase1) **********/ int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire); /** @OPDefine: priorvalue > 0 */ @@ -61,6 +64,9 @@ void read_lock(rwlock_t *rw) while (atomic_load_explicit(&rw->lock, memory_order_relaxed) <= 0) { thrd_yield(); } + // XXX-injection-#2: Weaken the parameter "memory_order_acquire" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./linuxrwlocks/testcase1 -m2 -y -u3 -tSPEC" /********** Detected Correctness (testcase1) **********/ priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire); /** @OPDefine: priorvalue > 0 */ @@ -72,6 +78,9 @@ void read_lock(rwlock_t *rw) @Transition: STATE(writerLockAcquired) = true; */ void write_lock(rwlock_t *rw) { + // XXX-injection-#3: Weaken the parameter "memory_order_acquire" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./linuxrwlocks/testcase1 -m2 -y -u3 -tSPEC" /********** Detected Correctness (testcase1) **********/ int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire); /** @OPDefine: priorvalue == RW_LOCK_BIAS */ @@ -80,6 +89,9 @@ void write_lock(rwlock_t *rw) while (atomic_load_explicit(&rw->lock, memory_order_relaxed) != RW_LOCK_BIAS) { thrd_yield(); } + // XXX-injection-#4: Weaken the parameter "memory_order_acquire" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./linuxrwlocks/testcase1 -m2 -y -u3 -tSPEC" /********** Detected Correctness (testcase1) **********/ priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire); /** @OPDefine: priorvalue == RW_LOCK_BIAS */ @@ -90,6 +102,9 @@ void write_lock(rwlock_t *rw) @Transition: if (C_RET) STATE(readerLockCnt)++; */ int read_trylock(rwlock_t *rw) { + // XXX-injection-#5: Weaken the parameter "memory_order_acquire" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./linuxrwlocks/testcase2 -m2 -y -u3 -tSPEC" /********** Detected Correctness (testcase2) **********/ int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire); /** @OPDefine: true */ @@ -104,6 +119,9 @@ int read_trylock(rwlock_t *rw) @Transition: if (C_RET) STATE(writerLockAcquired) = true; */ int write_trylock(rwlock_t *rw) { + // XXX-injection-#6: Weaken the parameter "memory_order_acquire" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./linuxrwlocks/testcase2 -m2 -y -u3 -tSPEC" /********** Detected Correctness (testcase2) **********/ int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire); /** @OPDefine: true */ @@ -118,6 +136,9 @@ int write_trylock(rwlock_t *rw) @Transition: STATE(readerLockCnt)--; */ void read_unlock(rwlock_t *rw) { + // XXX-injection-#7: Weaken the parameter "memory_order_release" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./linuxrwlocks/testcase1 -m2 -y -u3 -tSPEC" /********** Detected Correctness (testcase1) **********/ atomic_fetch_add_explicit(&rw->lock, 1, memory_order_release); /** @OPDefine: true */ @@ -127,6 +148,9 @@ void read_unlock(rwlock_t *rw) @Transition: STATE(writerLockAcquired) = false; */ void write_unlock(rwlock_t *rw) { + // XXX-injection-#8: Weaken the parameter "memory_order_release" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./linuxrwlocks/testcase1 -m2 -y -u3 -tSPEC" /********** Detected Correctness (testcase1) **********/ atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_release); /** @OPDefine: true */ diff --git a/mcs-lock/mcs-lock.cc b/mcs-lock/mcs-lock.cc index a6e8725..525ef9b 100644 --- a/mcs-lock/mcs-lock.cc +++ b/mcs-lock/mcs-lock.cc @@ -8,7 +8,18 @@ void mcs_mutex::lock(guard * I) { me->next.store(NULL, std::mo_relaxed ); me->gate.store(1, std::mo_relaxed ); + // XXX-injection-#1: Weaken the parameter "memory_order_acq_rel" to + // "memory_order_acquire", run "make" to recompile, and then run: + // "./run.sh ./mcs-lock/testcase -m2 -y -u3 -tSPEC" + // You can see that the model checker runs out of memory (in fact it + // encounters an infinite loop). + /********** Detected Infinite Loop (model checker out of memroy) **********/ + + // XXX-injection-#2: Weaken the parameter "memory_order_acq_rel" to + // "memory_order_release", run "make" to recompile, and then run: + // "./run.sh ./mcs-lock/testcase -m2 -Y -u3 -tSPEC" /********** 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); @@ -17,10 +28,18 @@ void mcs_mutex::lock(guard * I) { // (*1) race here // unlock of pred can see me in the tail before I fill next - // 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 : + + // XXX-injection-#3: Weaken the parameter "memory_order_release" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./mcs-lock/testcase -m2 -y -u3 -tSPEC -v" + // You can see that the model checker never ends, and that those printed + // executions have a very long repeated pattern of read and thrd_yield + // operations (and its length just keeps increasing) which means + // infinite loops. + /********** Detected Infinite Loop **********/ pred->next.store(me, std::mo_release ); // (*2) pred not touched any more @@ -28,8 +47,10 @@ void mcs_mutex::lock(guard * I) { // now this is the spin - // wait on predecessor setting my flag - rl::linear_backoff bo; + // XXX-injection-#4: Weaken the parameter "memory_order_acquire" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./mcs-lock/testcase -m2 -Y -u3 -tSPEC" /********** Detected Correctness *********/ - /** Run this in the -Y mode to expose the HB bug */ while ( me->gate.load(std::mo_acquire) ) { thrd_yield(); } @@ -39,16 +60,25 @@ void mcs_mutex::lock(guard * I) { void mcs_mutex::unlock(guard * I) { mcs_node * me = &(I->m_node); - - // FIXME: detection miss, execution never ends + // XXX-injection-#5: Weaken the parameter "memory_order_acquire" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./mcs-lock/testcase -m2 -y -u3 -tSPEC -v" + // You can see that the model checker never ends, and that those printed + // executions have a very long repeated pattern of read and thrd_yield + // operations (and its length just keeps increasing) which means + // infinite loops. + /********** Detected Infinite Loop **********/ 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 */ + + // XXX-injection-#6: Weaken the parameter "memory_order_release" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./mcs-lock/testcase -m2 -Y -u3 -tSPEC" + /********** Detected Correctness **********/ if ( m_tail.compare_exchange_strong( - tail_was_me,NULL,std::mo_acq_rel) ) { + tail_was_me,NULL,std::mo_release) ) { // got null in tail, mutex is unlocked /** @OPDefine: true */ return; @@ -57,7 +87,14 @@ void mcs_mutex::unlock(guard * I) { // (*1) catch the race : rl::linear_backoff bo; for(;;) { - // FIXME: detection miss, execution never ends + // XXX-injection-#7: Weaken the parameter "memory_order_acquire" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./mcs-lock/testcase -m2 -y -u3 -tSPEC -v" + // You can see that the model checker never ends, and that those printed + // executions have a very long repeated pattern of read and thrd_yield + // operations (and its length just keeps increasing) which means + // infinite loops. + /********** Detected Infinite Loop **********/ next = me->next.load(std::mo_acquire); if ( next != NULL ) break; @@ -68,8 +105,11 @@ void mcs_mutex::unlock(guard * I) { // (*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 */ + // XXX-injection-#8: Weaken the parameter "memory_order_release" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./mcs-lock/testcase -m2 -Y -u3 -tSPEC" + /********** 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 */ diff --git a/mpmc-queue/mpmc-queue.cc b/mpmc-queue/mpmc-queue.cc index 0b6999e..7e6d60d 100644 --- a/mpmc-queue/mpmc-queue.cc +++ b/mpmc-queue/mpmc-queue.cc @@ -3,7 +3,7 @@ template t_element * mpmc_boundq_1_alt::read_fetch() { - // FIXME: We can have a relaxed for sure here since the next CAS + // 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; @@ -13,7 +13,21 @@ t_element * mpmc_boundq_1_alt::read_fetch() { if ( wr == rd ) // empty return NULL; - + + // XXX-injection-#1: Weaken the parameter "mo_acq_rel" to + // "memory_order_release", run "make" to recompile, and then run: + // "./run.sh ./mpmc-queue/testcase2 -m2 -Y -u3 -tSPEC" + + // XXX-injection-#2: Weaken the parameter "mo_acq_rel" to + // "memory_order_acquire", run "make" to recompile, and then run: + // "./run.sh ./mpmc-queue/testcase2 -m2 -Y -u3 -tSPEC" + + // We missed both injections (#1 & #2). For the reason, you can see the + // discussion on MPMC queue in the last paragraph in Section 6.4.2 of + // our paper. Note that we have more injections than the original + // submission since we directly weakened mo_acq_rel to mo_relaxed. + // Reviews suggest us to do a partial relaxations, i.e., mo_acq_rel -> + // mo_acquire and mo_acq_rel -> mo_release. if ( m_rdwr.compare_exchange_weak(rdwr,rdwr+(1<<16),mo_acq_rel) ) break; else @@ -22,6 +36,9 @@ t_element * mpmc_boundq_1_alt::read_fetch() { // (*1) rl::backoff bo; + // XXX-injection-#3: Weaken the parameter "mo_acquire" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./mpmc-queue/testcase1 -m2 -y -u3 -tSPEC" /********** Detected Admissibility (testcase1) **********/ while ( (m_written.load(mo_acquire) & 0xFFFF) != wr ) { thrd_yield(); @@ -36,8 +53,10 @@ t_element * mpmc_boundq_1_alt::read_fetch() { template void mpmc_boundq_1_alt::read_consume(t_element *bin) { + // XXX-injection-#4: Weaken the parameter "mo_release" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./mpmc-queue/testcase2 -m2 -Y -u3 -tSPEC" /********** Detected Admissibility (testcase2) **********/ - // run with -Y m_read.fetch_add(1,mo_release); /** @OPDefine: true */ } @@ -45,7 +64,7 @@ void mpmc_boundq_1_alt::read_consume(t_element *bin) { template t_element * mpmc_boundq_1_alt::write_prepare() { - // FIXME: We can have a relaxed for sure here since the next CAS + // 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; @@ -56,6 +75,20 @@ t_element * mpmc_boundq_1_alt::write_prepare() { if ( wr == ((rd + t_size)&0xFFFF) ) // full return NULL; + // XXX-injection-#5: Weaken the parameter "mo_acq_rel" to + // "memory_order_release", run "make" to recompile, and then run: + // "./run.sh ./mpmc-queue/testcase2 -m2 -Y -u3 -tSPEC" + + // XXX-injection-#6: Weaken the parameter "mo_acq_rel" to + // "memory_order_acquire", run "make" to recompile, and then run: + // "./run.sh ./mpmc-queue/testcase2 -m2 -Y -u3 -tSPEC" + + // We missed both injections (#5 & #6). For the reason, you can see the + // discussion on MPMC queue in the last paragraph in Section 6.4.2 of + // our paper. Note that we have more injections than the original + // submission since we directly weakened mo_acq_rel to mo_relaxed. + // Reviews suggest us to do a partial relaxations, i.e., mo_acq_rel -> + // mo_acquire and mo_acq_rel -> mo_release. if ( m_rdwr.compare_exchange_weak(rdwr,(rd<<16) | ((wr+1)&0xFFFF),mo_acq_rel) ) break; else @@ -64,6 +97,9 @@ t_element * mpmc_boundq_1_alt::write_prepare() { // (*1) rl::backoff bo; + // XXX-injection-#7: Weaken the parameter "mo_acquire" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./mpmc-queue/testcase2 -m2 -Y -u3 -tSPEC" /********** Detected Admissibility (testcase2) **********/ // run with -Y while ( (m_read.load(mo_acquire) & 0xFFFF) != rd ) { @@ -79,6 +115,9 @@ t_element * mpmc_boundq_1_alt::write_prepare() { template void mpmc_boundq_1_alt::write_publish(t_element *bin) { + // XXX-injection-#8: Weaken the parameter "mo_release" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./mpmc-queue/testcase1 -m2 -y -u3 -tSPEC" /********** Detected Admissibility (testcase1) **********/ m_written.fetch_add(1,mo_release); /** @OPDefine: true */ diff --git a/ms-queue-loose/Makefile b/ms-queue-loose/Makefile deleted file mode 100644 index a50ca70..0000000 --- a/ms-queue-loose/Makefile +++ /dev/null @@ -1,23 +0,0 @@ -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 deleted file mode 100644 index a148ad4..0000000 --- a/ms-queue-loose/main.c +++ /dev/null @@ -1,86 +0,0 @@ -#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-loose/queue.c b/ms-queue-loose/queue.c deleted file mode 100644 index 4ac901e..0000000 --- a/ms-queue-loose/queue.c +++ /dev/null @@ -1,199 +0,0 @@ -#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; -@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; - 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 - 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); - - 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: 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; - pointer tail; - pointer next; - - while (!success) { - /********** Dectected Admissibility (testcase3) **********/ - head = atomic_load_explicit(&q->head, acquire); - /********** 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)) { - - /* 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 Admissibility (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-loose/queue.h b/ms-queue-loose/queue.h deleted file mode 100644 index c15838a..0000000 --- a/ms-queue-loose/queue.h +++ /dev/null @@ -1,37 +0,0 @@ -#ifndef _QUEUE_H -#define _QUEUE_H - -#include - -#define MAX_NODES 0xf - -typedef unsigned long long pointer; -typedef atomic_ullong pointer_t; - -#define MAKE_POINTER(ptr, count) ((((pointer)count) << 32) | ptr) -#define PTR_MASK 0xffffffffLL -#define COUNT_MASK (0xffffffffLL << 32) - -static inline void set_count(pointer *p, unsigned int val) { *p = (*p & ~COUNT_MASK) | ((pointer)val << 32); } -static inline void set_ptr(pointer *p, unsigned int val) { *p = (*p & ~PTR_MASK) | val; } -static inline unsigned int get_count(pointer p) { return (p & COUNT_MASK) >> 32; } -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 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); - -int get_thread_num(); - -#endif diff --git a/ms-queue-loose/testcase1.c b/ms-queue-loose/testcase1.c deleted file mode 100644 index 9edf77a..0000000 --- a/ms-queue-loose/testcase1.c +++ /dev/null @@ -1,92 +0,0 @@ -#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 deleted file mode 100644 index 20e79c4..0000000 --- a/ms-queue-loose/testcase2.c +++ /dev/null @@ -1,101 +0,0 @@ -#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 deleted file mode 100644 index 80e0f0d..0000000 --- a/ms-queue-loose/testcase3.c +++ /dev/null @@ -1,100 +0,0 @@ -#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 deleted file mode 100644 index 1e1d151..0000000 --- a/ms-queue-loose/testcase4.c +++ /dev/null @@ -1,90 +0,0 @@ -#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/main.c b/ms-queue/main.c index a148ad4..7fb6701 100644 --- a/ms-queue/main.c +++ b/ms-queue/main.c @@ -33,10 +33,10 @@ static void main_task(void *param) unsigned int val; int pid = *((int *)param); if (pid % 2 == 0) { - enqueue(queue, 0, 0); + enqueue(queue, 1, 0); succ1 = dequeue(queue, &idx1, &reclaimNode); } else { - enqueue(queue, 1, 0); + enqueue(queue, 2, 0); succ2 = dequeue(queue, &idx2, &reclaimNode); } } diff --git a/ms-queue/queue.c b/ms-queue/queue.c index 8a0f4eb..20de128 100644 --- a/ms-queue/queue.c +++ b/ms-queue/queue.c @@ -109,13 +109,25 @@ void enqueue(queue_t *q, unsigned int val, int n) 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 + // XXX-known-bug-#1: This is a found bug in AutoMO, and testcase4 can reveal + // this known bug. + // To reproduce, weaken the parameter "memory_order_release" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./ms-queue/testcase4 -m2 -y -u3 -tSPEC" /********** Detected KNOWN BUG (testcase4) **********/ atomic_store_explicit(&q->nodes[node].next, tmp, release); while (!success) { - /********** Detected UL **********/ + // XXX-injection-#1: To reproduce, weaken the parameter + // "memory_order_acquire" to "memory_order_relaxed", run "make" to + // recompile, and then run: + // "./run.sh ./ms-queue/testcase2 -m2 -y -u3 -tSPEC" + /********** Detected UL (testcase2) **********/ tail = atomic_load_explicit(&q->tail, acquire); + // XXX-injection-#2: To reproduce, weaken the parameter + // "memory_order_acquire" to "memory_order_relaxed", run "make" to + // recompile, and then run: + // "./run.sh ./ms-queue/testcase4 -m2 -y -u3 -tSPEC" /********** Detected Correctness (testcase4) **********/ next = atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire); if (tail == atomic_load_explicit(&q->tail, relaxed)) { @@ -125,16 +137,28 @@ void enqueue(queue_t *q, unsigned int val, int n) if (get_ptr(next) == 0) { // == NULL pointer value = MAKE_POINTER(node, get_count(next) + 1); + // XXX-injection-#3: To reproduce, weaken the parameter + // "memory_order_release" to "memory_order_relaxed", run "make" to + // recompile, and then run: + // "./run.sh ./ms-queue/testcase1 -m2 -y -u3 -tSPEC" /********** 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 **********/ + // XXX-injection-#4: To reproduce, weaken the parameter + // "memory_order_acquire" to "memory_order_relaxed", run "make" to + // recompile, and then run: + // "./run.sh ./ms-queue/testcase2 -m2 -y -u3 -tSPEC" + /********** Detected UL (testcase2) **********/ unsigned int ptr = get_ptr(atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire)); pointer value = MAKE_POINTER(ptr, get_count(tail) + 1); + // XXX-injection-#5: To reproduce, weaken the parameter + // "memory_order_release" to "memory_order_relaxed", run "make" to + // recompile, and then run: + // "./run.sh ./ms-queue/testcase2 -m2 -y -u3 -tSPEC" /********** Detected Correctness (testcase2) **********/ atomic_compare_exchange_strong_explicit(&q->tail, &tail, value, @@ -143,6 +167,11 @@ void enqueue(queue_t *q, unsigned int val, int n) } } } + + // XXX-injection-#6: To reproduce, weaken the parameter + // "memory_order_release" to "memory_order_relaxed", run "make" to + // recompile, and then run: + // "./run.sh ./ms-queue/testcase1 -m2 -y -u3 -tSPEC" /********** Detected Corrctness (testcase1) **********/ atomic_compare_exchange_strong_explicit(&q->tail, &tail, @@ -151,7 +180,7 @@ void enqueue(queue_t *q, unsigned int val, int n) } /** @Transition: S_RET = STATE(q)->empty() ? 0 : STATE(q)->front(); -if (S_RET) STATE(q)->pop_front(); +if (S_RET && C_RET) STATE(q)->pop_front(); @JustifyingPostcondition: if (!C_RET) return S_RET == C_RET; @PostCondition: return C_RET ? *retVal == S_RET : true; @@ -166,10 +195,24 @@ int dequeue(queue_t *q, unsigned int *retVal, unsigned int *reclaimNode) pointer next; while (!success) { - /********** Dectected Correctness (testcase3) **********/ + // XXX-injection-#7: To reproduce, weaken the parameter + // "memory_order_acquire" to "memory_order_relaxed", run "make" to + // recompile, and then run: + // "./run.sh ./ms-queue/testcase3 -m2 -y -u3 -tSPEC" + /********** Detected Correctness (testcase3) **********/ head = atomic_load_explicit(&q->head, acquire); + // To reproduce, weaken the parameter "memory_order_acquire" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./ms-queue/testcase4 -m2 -y -u3 -tSPEC" + // XXX-known-bug-#2: This is another known bug, and testcase2 can reveal + // this known bug /********** Detected KNOWN BUG (testcase2) **********/ tail = atomic_load_explicit(&q->tail, acquire); + + // XXX-injection-#8: To reproduce, weaken the parameter + // "memory_order_acquire" to "memory_order_relaxed", run "make" to + // recompile, and then run: + // "./run.sh ./ms-queue/testcase1 -m2 -y -u3 -tSPEC" /********** Detected Correctness (testcase1) **********/ next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, acquire); /** @OPClearDefine: true */ @@ -182,7 +225,12 @@ int dequeue(queue_t *q, unsigned int *retVal, unsigned int *reclaimNode) if (get_ptr(next) == 0) { // NULL return false; // NULL } - /********** Detected UL **********/ + + // XXX-injection-#9: To reproduce, weaken the parameter + // "memory_order_release" to "memory_order_relaxed", run "make" to + // recompile, and then run: + // "./run.sh ./ms-queue/testcase2 -m2 -y -u3 -tSPEC" + /********** Detected UL (testcase2) **********/ atomic_compare_exchange_strong_explicit(&q->tail, &tail, MAKE_POINTER(get_ptr(next), get_count(tail) + 1), @@ -191,6 +239,11 @@ int dequeue(queue_t *q, unsigned int *retVal, unsigned int *reclaimNode) } else { //*retVal = load_32(&q->nodes[get_ptr(next)].value); *retVal = q->nodes[get_ptr(next)].value; + + // XXX-injection-#10: To reproduce, weaken the parameter + // "memory_order_release" to "memory_order_relaxed", run "make" to + // recompile, and then run: + // "./run.sh ./ms-queue/testcase3 -m2 -y -u3 -tSPEC" /********** Detected Correctness (testcase3) **********/ success = atomic_compare_exchange_strong_explicit(&q->head, &head, diff --git a/ms-queue/testcase1.c b/ms-queue/testcase1.c index 9edf77a..46ba6ad 100644 --- a/ms-queue/testcase1.c +++ b/ms-queue/testcase1.c @@ -34,7 +34,7 @@ static void main_task(void *param) int pid = *((int *)param); if (pid % procs == 0) { //atomic_store_explicit(&x[0], 1, memory_order_relaxed); - enqueue(queue, 0, 0); + enqueue(queue, 1, 0); } else if (pid % procs == 1) { //atomic_store_explicit(&x[1], 1, memory_order_relaxed); succ1 = dequeue(queue, &idx1, &reclaimNode); diff --git a/ms-queue/testcase2.c b/ms-queue/testcase2.c index 20e79c4..f845544 100644 --- a/ms-queue/testcase2.c +++ b/ms-queue/testcase2.c @@ -34,10 +34,10 @@ static void main_task(void *param) int pid = *((int *)param); if (pid % 4 == 0) { //atomic_store_explicit(&x[0], 1, memory_order_relaxed); - enqueue(queue, 0, 0); + enqueue(queue, 1, 0); } else if (pid % 4 == 1) { //atomic_store_explicit(&x[1], 1, memory_order_relaxed); - enqueue(queue, 1, 0); + enqueue(queue, 2, 0); } else if (pid % 4 == 2) { succ1 = dequeue(queue, &idx1, &reclaimNode); if (succ1) { diff --git a/read-copy-update/rcu.cc b/read-copy-update/rcu.cc index 52a82db..8c6a956 100644 --- a/read-copy-update/rcu.cc +++ b/read-copy-update/rcu.cc @@ -12,6 +12,9 @@ atomic dataPtr; /** @JustifyingPrecondition: return STATE(data1) == *data1 && STATE(data2) == *data2; */ void read(int *data1, int *data2) { + // XXX-injection-#1: Weaken the parameter "memory_order_acquire" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./read-copy-update/testcase -m2 -y -u3 -tSPEC" /********** Detected Correctness **********/ Data *res = dataPtr.load(memory_order_acquire); /** @OPDefine: true */ @@ -31,9 +34,16 @@ void write(int data1, int data2) { bool succ = false; Data *tmp = new Data; do { + // XXX-injection-#2: Weaken the parameter "memory_order_acquire" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./read-copy-update/testcase -m2 -y -u3 -tSPEC" /********** Detected Correctness **********/ Data *prev = dataPtr.load(memory_order_acquire); inc(tmp, prev, data1, data2); + + // XXX-injection-#3: Weaken the parameter "memory_order_release" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./read-copy-update/testcase -m2 -y -u3 -tSPEC" /********** Detected Correctness **********/ succ = dataPtr.compare_exchange_strong(prev, tmp, memory_order_release, memory_order_relaxed); diff --git a/seqlock/seqlock.cc b/seqlock/seqlock.cc index 16298bd..ca4a55c 100644 --- a/seqlock/seqlock.cc +++ b/seqlock/seqlock.cc @@ -13,9 +13,10 @@ seqlock::seqlock() { 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. + // XXX-injection-#1: Weaken the parameter "memory_order_acquire" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./seqlock/testcase1 -m2 -y -u3 -tSPEC" + /********** Detected Correctness (testcase1) **********/ int old_seq = _seq.load(memory_order_acquire); // acquire if (old_seq % 2 == 1) { @@ -24,10 +25,13 @@ void seqlock::read(int *data1, int *data2) { } // 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 */ + + // XXX-injection-#2: Weaken the parameter "memory_order_acquire" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./seqlock/testcase1 -m2 -y -u3 -tSPEC" /********** Detected Correctness (testcase1) **********/ atomic_thread_fence(memory_order_acquire); if (_seq.load(memory_order_relaxed) == old_seq) { // relaxed @@ -41,6 +45,9 @@ void seqlock::read(int *data1, int *data2) { void seqlock::write(int data1, int data2) { while (true) { // #1: either here or #2 must be acquire + // XXX-injection-#3: Weaken the parameter "memory_order_acquire" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./seqlock/testcase2 -m2 -y -u3 -x1000 -tSPEC" /********** Detected Correctness (testcase2 with -y -x1000) **********/ int old_seq = _seq.load(memory_order_acquire); // acquire if (old_seq % 2 == 1) { @@ -56,17 +63,24 @@ void seqlock::write(int data1, int data2) { } } - // XXX: Update the data. It needs to be release since this version use + // 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. + + // XXX-injection-#4: Weaken the parameter "memory_order_release" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./seqlock/testcase1 -m2 -y -u3 -tSPEC" /********** 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) **********/ + // XXX-injection-#5: Weaken the parameter "memory_order_release" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./seqlock/testcase1 -m2 -y -u3 -tSPEC" + /********** Detected Correctness (testcase1) **********/ _seq.fetch_add(1, memory_order_release); // release } diff --git a/spsc-bugfix/queue.cc b/spsc-bugfix/queue.cc index 85903d0..505fc4b 100644 --- a/spsc-bugfix/queue.cc +++ b/spsc-bugfix/queue.cc @@ -4,6 +4,9 @@ template void spsc_queue::enqueue(T data) { node* n = new node (data); + // XXX-injection-#1: Weaken the parameter "memory_order_release" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./spsc-bugfix/testcase1 -m2 -y -u3 -tSPEC" /********** Detected Correctness **********/ //head($)->next.store(n, std::memory_order_release); head->next.store(n, std::memory_order_release); @@ -36,6 +39,9 @@ T spsc_queue::try_dequeue() { //node* t = tail($); node* t = tail; + // XXX-injection-#2: Weaken the parameter "memory_order_acquire" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./spsc-bugfix/testcase1 -m2 -y -u3 -tSPEC" /********** Detected Correctness **********/ node* n = t->next.load(std::memory_order_acquire); /** @OPClearDefine: true */ diff --git a/ticket-lock/lock.c b/ticket-lock/lock.c index b572950..752e371 100644 --- a/ticket-lock/lock.c +++ b/ticket-lock/lock.c @@ -27,6 +27,9 @@ void lock(struct TicketLock *l) { memory_order_relaxed); // Spinning for my turn while (true) { + // XXX-injection-#1: Weaken the parameter "memory_order_acquire" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./ticket-lock/testcase1 -m2 -Y -u3 -tSPEC" /********** Detected Correctness (testcase1 with -Y) **********/ unsigned turn = atomic_load_explicit(&l->turn, memory_order_acquire); /** @OPDefine: turn == ticket */ @@ -42,6 +45,9 @@ void lock(struct TicketLock *l) { @Transition: STATE(lock) = false; */ void unlock(struct TicketLock *l) { unsigned turn = atomic_load_explicit(&l->turn, memory_order_relaxed); + // XXX-injection-#2: Weaken the parameter "memory_order_release" to + // "memory_order_relaxed", run "make" to recompile, and then run: + // "./run.sh ./ticket-lock/testcase1 -m2 -Y -u3 -tSPEC" /********** Detected Correctness (testcase1 with -Y) **********/ atomic_store_explicit(&l->turn, turn + 1, memory_order_release); /** @OPDefine: true */