-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)
+++ /dev/null
-#!/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
+++ /dev/null
-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
+++ /dev/null
-class Queue {
-/** @DeclareState: IntList *q;
-@Commutativity:enq<->deq(true)
-@Commutativity:deq<->deq(!M1->RET||!M2->RET) */
-public: atomic<Node*> 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;
- }
-}
-};
+++ /dev/null
-#include <stdlib.h>
-#include <stdio.h>
-#include <threads.h>
-#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;
-}
+++ /dev/null
-#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();
-}
+++ /dev/null
-#ifndef _QUEUE_H
-#define _QUEUE_H
-#include <atomic>
-#include "unrelacy.h"
-
-#define CAS compare_exchange_strong
-using namespace std;
-
-typedef struct Node {
- int data;
- atomic<Node*> next;
-
- Node() {
- data = 0;
- next.store(NULL, relaxed);
- }
-
- Node(int d) {
- data = d;
- next.store(NULL, relaxed);
- }
-} Node;
-
-class Queue {
-public: atomic<Node*> 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
+++ /dev/null
-#include <stdlib.h>
-#include <stdio.h>
-#include <threads.h>
-
-#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;
-}
+++ /dev/null
-#include <stdlib.h>
-#include <stdio.h>
-#include <threads.h>
-
-#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;
-}
+++ /dev/null
-#include <stdlib.h>
-#include <stdio.h>
-#include <threads.h>
-
-#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;
-}
+++ /dev/null
-#include <stdlib.h>
-#include <stdio.h>
-#include <threads.h>
-
-#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;
-}
BENCH_BINARY := $(BENCH).o
-TESTS := main testcase1 testcase2 testcase3 testcase4 testcase5 testcase6
+TESTS := main testcase1 testcase2 testcase3
all: $(TESTS)
../generate.sh $(notdir $(shell pwd))
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);
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
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);
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. */
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");
/** @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);
// 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);
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 */
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);
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)
+++ /dev/null
-#include <stdlib.h>
-#include <assert.h>
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#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;
-}
+++ /dev/null
-#include <stdlib.h>
-#include <assert.h>
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#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;
-}
+++ /dev/null
-#include <stdlib.h>
-#include <assert.h>
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#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;
-}
+++ /dev/null
-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
+++ /dev/null
-#include <stdatomic.h>
-#include <inttypes.h>
-#include "deque.h"
-#include <stdlib.h>
-#include <stdio.h>
-
-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;
-}
+++ /dev/null
-#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
+++ /dev/null
-#include <stdlib.h>
-#include <assert.h>
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#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;
-}
// 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 */
// 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 */
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);
+++ /dev/null
-#!/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[*]}
+++ /dev/null
-*** 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
-
+++ /dev/null
-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)
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 */
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 */
@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 */
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 */
@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 */
@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 */
@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 */
@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 */
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);
// (*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
// 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();
}
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;
// (*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;
// (*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 */
template <typename t_element>
t_element * mpmc_boundq_1_alt<t_element>::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;
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
// (*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();
template <typename t_element>
void mpmc_boundq_1_alt<t_element>::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 */
}
template <typename t_element>
t_element * mpmc_boundq_1_alt<t_element>::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;
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
// (*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 ) {
template <typename t_element>
void mpmc_boundq_1_alt<t_element>::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 */
+++ /dev/null
-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
+++ /dev/null
-#include <stdlib.h>
-#include <stdio.h>
-#include <threads.h>
-
-#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;
-}
+++ /dev/null
-#include <threads.h>
-#include <stdlib.h>
-#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;
-}
+++ /dev/null
-#ifndef _QUEUE_H
-#define _QUEUE_H
-
-#include <stdatomic.h>
-
-#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
+++ /dev/null
-#include <stdlib.h>
-#include <stdio.h>
-#include <threads.h>
-
-#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;
-}
+++ /dev/null
-#include <stdlib.h>
-#include <stdio.h>
-#include <threads.h>
-
-#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;
-}
+++ /dev/null
-#include <stdlib.h>
-#include <stdio.h>
-#include <threads.h>
-
-#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;
-}
+++ /dev/null
-#include <stdlib.h>
-#include <stdio.h>
-#include <threads.h>
-
-#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;
-}
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);
}
}
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)) {
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,
}
}
}
+
+ // 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,
}
/** @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;
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 */
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),
} 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,
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);
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) {
/** @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 */
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);
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) {
}
// 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
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) {
}
}
- // 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
}
void spsc_queue<T>::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);
{
//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 */
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 */
@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 */
projects / model-checker-benchmarks.git / commitdiff