edits: add comments to demonstrate the found bugs and bug injections

diff --git a/Makefile b/Makefile
index 74716564c9699f272cfd2f085ac85994b1f8f0b3..194e1ffce7c48be2806ca63f406ca5810ece4f37 100644 (file)
--- 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)
 
 
 .PHONY: $(DIRS)
 

diff --git a/bench.sh b/bench.sh
deleted file mode 100755 (executable)
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 (file)
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 (file)
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<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;
-  }
-}
-};

diff --git a/blocking-mpmc-example/main.cc b/blocking-mpmc-example/main.cc
deleted file mode 100644 (file)
index 9b3a6af..0000000
--- a/blocking-mpmc-example/main.cc
+++ /dev/null
@@ -1,56 +0,0 @@
-#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, &param[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 (file)
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 (file)
index e7d1515..0000000
--- a/blocking-mpmc-example/queue.h
+++ /dev/null
@@ -1,36 +0,0 @@
-#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

diff --git a/blocking-mpmc-example/testcase1.cc b/blocking-mpmc-example/testcase1.cc
deleted file mode 100644 (file)
index 3851988..0000000
--- a/blocking-mpmc-example/testcase1.cc
+++ /dev/null
@@ -1,86 +0,0 @@
-#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, &param[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 (file)
index 1e66c2e..0000000
--- a/blocking-mpmc-example/testcase2.cc
+++ /dev/null
@@ -1,88 +0,0 @@
-#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, &param[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 (file)
index 5a2bbbe..0000000
--- a/blocking-mpmc-example/testcase3.cc
+++ /dev/null
@@ -1,88 +0,0 @@
-#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, &param[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 (file)
index fbb0cea..0000000
--- a/blocking-mpmc-example/testcase4.cc
+++ /dev/null
@@ -1,89 +0,0 @@
-#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, &param[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 dca2e818edf9f319860b204d2ddf0c7bd2547f43..2389f070120d25468c11a2bd4446bf5529e79fdf 100644 (file)
--- a/chase-lev-deque-bugfix/Makefile
+++ b/chase-lev-deque-bugfix/Makefile
@@ -4,7 +4,7 @@ BENCH := deque
 
 BENCH_BINARY := $(BENCH).o
 
 
 BENCH_BINARY := $(BENCH).o
 

-TESTS := main testcase1 testcase2 testcase3 testcase4 testcase5 testcase6
+TESTS := main testcase1 testcase2 testcase3

 
 all: $(TESTS)
        ../generate.sh $(notdir $(shell pwd))
 
 all: $(TESTS)
        ../generate.sh $(notdir $(shell pwd))

diff --git a/chase-lev-deque-bugfix/deque.c b/chase-lev-deque-bugfix/deque.c
index b851e5163f906ec7d2cb0371c9ff8b856fd0554b..71aeff7457758b2b8752e7382cae3f08caf260bf 100644 (file)
--- 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));
 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);
        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.
        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
        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);
        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);
        /**********    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. */
                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. */
                        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 *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;
        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);
        }
        
        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");
        /**********    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);
 /** @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);
        /**********    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 */
        // 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);
        /**********    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) {
            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);
        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);
        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)    **********/
        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);
                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 */
                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 b61f8c739ed4bea6ea1e1a08189d879a1d57c838..9927f9df5a5a9075bc7fc232ade5f51a8a400176 100644 (file)
--- 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 *) */
 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);
 } Deque;
 
 Deque * create_size(int size);

diff --git a/chase-lev-deque-bugfix/testcase3.c b/chase-lev-deque-bugfix/testcase3.c
index 15cbd4e3f084b517a0fe64b0679f8e90f1cb315d..c2f8e78527a9096163682b82a240424e268a65fc 100644 (file)
--- 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 ;
 
        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)
 /*
        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 (file)
index 060c5f8..0000000
--- a/chase-lev-deque-bugfix/testcase4.c
+++ /dev/null
@@ -1,54 +0,0 @@
-#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;
-}

diff --git a/chase-lev-deque-bugfix/testcase5.c b/chase-lev-deque-bugfix/testcase5.c
deleted file mode 100644 (file)
index f9552a7..0000000
--- a/chase-lev-deque-bugfix/testcase5.c
+++ /dev/null
@@ -1,55 +0,0 @@
-#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;
-}

diff --git a/chase-lev-deque-bugfix/testcase6.c b/chase-lev-deque-bugfix/testcase6.c
deleted file mode 100644 (file)
index e2b3451..0000000
--- a/chase-lev-deque-bugfix/testcase6.c
+++ /dev/null
@@ -1,55 +0,0 @@
-#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;
-}

diff --git a/chase-lev-deque/.gitignore b/chase-lev-deque/.gitignore
deleted file mode 100644 (file)
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 (file)
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 (file)
index 0ad7830..0000000
--- a/chase-lev-deque/deque.c
+++ /dev/null
@@ -1,85 +0,0 @@
-#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;
-}

diff --git a/chase-lev-deque/deque.h b/chase-lev-deque/deque.h
deleted file mode 100644 (file)
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 (file)
index f2e8dca..0000000
--- a/chase-lev-deque/main.c
+++ /dev/null
@@ -1,46 +0,0 @@
-#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;
-}

diff --git a/concurrent-hashmap/hashmap.cc b/concurrent-hashmap/hashmap.cc
index 9b0ede6caa40af24b2c563d0847b4070d33d646f..65aa1693d7d954fefb977071aa281a92901e0471 100644 (file)
--- 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
        
        // 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)) {
        /**********    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 */
                        /**********    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);
                        // 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 */
                        /**********    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);
        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);
        /**********    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 (executable)
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 (file)
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 (file)
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 408f35b6af1ecb3787f131a0da37f3d13812f34a..4fa29a1aecf12c46b41c1032bffcbbcaca4d190d 100644 (file)
--- 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)
 {
        
 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 */
        /**********  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();
                }
                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 */
            /**********  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)
 {
 @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 */
        /**********  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();
                }
                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 */
            /**********  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)
 {
 @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 */
        /**********  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)
 {
 @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 */
        /**********  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)
 {
 @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 */
        /**********  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)
 {
 @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 */
        /**********  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 a6e87250e4b5c53c0b6fd468b20d52c684286a7b..525ef9b07a947c9fe7ccf39b4586576bff204cd9 100644 (file)
--- 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 );
 
        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 **********/
        /**********  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);
        /** 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
 
                // (*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 :
                // 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       
                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;
                // 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 *********/
                /**********  Detected Correctness *********/

-           /** Run this in the -Y mode to expose the HB bug */

                while ( me->gate.load(std::mo_acquire) ) {
                        thrd_yield();
                }
                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);
 
 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;
        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(
                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;
                        // 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(;;) {
                // (*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;
                        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        
 
        // (*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 */
        // 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 0b6999ee0b95a1dd38ecde9be72f7d5d036241f4..7e6d60d5d1de56cc47104a0abaec48e1fbe007cd 100644 (file)
--- a/mpmc-queue/mpmc-queue.cc
+++ b/mpmc-queue/mpmc-queue.cc
@@ -3,7 +3,7 @@
 
 template <typename t_element>
 t_element * mpmc_boundq_1_alt<t_element>::read_fetch() {
 
 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;
        // 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<t_element>::read_fetch() {
 
                if ( wr == rd ) // empty
                        return NULL;
 
                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
                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<t_element>::read_fetch() {
 
        // (*1)
        rl::backoff bo;
 
        // (*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();
        /**********    Detected Admissibility (testcase1)    **********/
        while ( (m_written.load(mo_acquire) & 0xFFFF) != wr ) {
                thrd_yield();


@@ -36,8 +53,10 @@ t_element * mpmc_boundq_1_alt<t_element>::read_fetch() {
 
 template <typename t_element>
 void mpmc_boundq_1_alt<t_element>::read_consume(t_element *bin) {
 
 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)    **********/
        /**********    Detected Admissibility (testcase2)    **********/

-    // run with -Y

        m_read.fetch_add(1,mo_release);
        /** @OPDefine: true */
 }
        m_read.fetch_add(1,mo_release);
        /** @OPDefine: true */
 }


@@ -45,7 +64,7 @@ void mpmc_boundq_1_alt<t_element>::read_consume(t_element *bin) {
 
 template <typename t_element>
 t_element * mpmc_boundq_1_alt<t_element>::write_prepare() {
 
 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;
        // 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<t_element>::write_prepare() {
                if ( wr == ((rd + t_size)&0xFFFF) ) // full
                        return NULL;
 
                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
                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<t_element>::write_prepare() {
 
        // (*1)
        rl::backoff bo;
 
        // (*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 ) {
        /**********    Detected Admissibility (testcase2)    **********/
     // run with -Y
        while ( (m_read.load(mo_acquire) & 0xFFFF) != rd ) {


@@ -79,6 +115,9 @@ t_element * mpmc_boundq_1_alt<t_element>::write_prepare() {
 template <typename t_element>
 void mpmc_boundq_1_alt<t_element>::write_publish(t_element *bin)
 {
 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 */
        /**********    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 (file)
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 (file)
index a148ad4..0000000
--- a/ms-queue-loose/main.c
+++ /dev/null
@@ -1,86 +0,0 @@
-#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, &param[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 (file)
index 4ac901e..0000000
--- a/ms-queue-loose/queue.c
+++ /dev/null
@@ -1,199 +0,0 @@
-#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;
-}

diff --git a/ms-queue-loose/queue.h b/ms-queue-loose/queue.h
deleted file mode 100644 (file)
index c15838a..0000000
--- a/ms-queue-loose/queue.h
+++ /dev/null
@@ -1,37 +0,0 @@
-#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

diff --git a/ms-queue-loose/testcase1.c b/ms-queue-loose/testcase1.c
deleted file mode 100644 (file)
index 9edf77a..0000000
--- a/ms-queue-loose/testcase1.c
+++ /dev/null
@@ -1,92 +0,0 @@
-#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, &param[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 (file)
index 20e79c4..0000000
--- a/ms-queue-loose/testcase2.c
+++ /dev/null
@@ -1,101 +0,0 @@
-#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, &param[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 (file)
index 80e0f0d..0000000
--- a/ms-queue-loose/testcase3.c
+++ /dev/null
@@ -1,100 +0,0 @@
-#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, &param[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 (file)
index 1e1d151..0000000
--- a/ms-queue-loose/testcase4.c
+++ /dev/null
@@ -1,90 +0,0 @@
-#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, &param[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 a148ad47b81626ae0e539b97961ca002b19f7644..7fb6701eaa32c46cad1896e3d6bda620fdcec8d1 100644 (file)
--- 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) {
        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 {
                succ1 = dequeue(queue, &idx1, &reclaimNode);
        } else {

-               enqueue(queue, 1, 0);
+               enqueue(queue, 2, 0);

                succ2 = dequeue(queue, &idx2, &reclaimNode);
        }
 }
                succ2 = dequeue(queue, &idx2, &reclaimNode);
        }
 }

diff --git a/ms-queue/queue.c b/ms-queue/queue.c
index 8a0f4eb97b08a504779072613b9cbd111ddc7eb9..20de1289db00f019efc9eb9f6e8ce6ab535f3506 100644 (file)
--- 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
        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 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);
                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)) {
                /**********    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);
 
                        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 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);
                                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,
                                /**********    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,
        /**********    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();
 }
 
 /** @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;
 @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) {
        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);
                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);
                /**********    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 */
                /**********    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
                                }
                                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),
                                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;
                        } 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,
                                /**********    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 9edf77aa39b6011f3bfb73d06ac5d1d9ecc841d7..46ba6adfdc500d71b8ec68159b56c27aab333933 100644 (file)
--- 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);
        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);
        } 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 20e79c47dc8d4c8580a915ba0ce5f6ec16adf384..f84554432022826bde367c18566a17b84b881a41 100644 (file)
--- 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);
        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);
        } 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) {
        } 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 52a82db028651ace056766b5aa4205564e6f3774..8c6a956dd18f5d6e4e90ba8c96edce9b0ce600ca 100644 (file)
--- a/read-copy-update/rcu.cc
+++ b/read-copy-update/rcu.cc
@@ -12,6 +12,9 @@ atomic<Data*> dataPtr;
 
 /** @JustifyingPrecondition: return STATE(data1) == *data1 && STATE(data2) == *data2; */
 void read(int *data1, int *data2) {
 
 /** @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 */
        /**********    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 {
        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);
                /**********    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);
                /**********    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 16298bd04baa8010463ce8047a258b93c1c53754..ca4a55c0823e676dab31fab07f9d75d137894252 100644 (file)
--- a/seqlock/seqlock.cc
+++ b/seqlock/seqlock.cc
@@ -13,9 +13,10 @@ seqlock::seqlock() {
 
 void seqlock::read(int *data1, int *data2) {
        while (true) {
 
 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) {
                /**********    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
         }
        
                // 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 */
                *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
                /**********    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
 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) {
                /**********    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.
        // 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 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
 }
 
        _seq.fetch_add(1, memory_order_release); // release
 }
 

diff --git a/spsc-bugfix/queue.cc b/spsc-bugfix/queue.cc
index 85903d08907a9fe213111b1827c81f7c50899c90..505fc4b6e6e93b5a138af95806754006b8af3571 100644 (file)
--- a/spsc-bugfix/queue.cc
+++ b/spsc-bugfix/queue.cc
@@ -4,6 +4,9 @@ template<typename T>
 void spsc_queue<T>::enqueue(T data)
 {
        node* n = new node (data);
 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);
        /**********    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<T>::try_dequeue()
 {
        //node* t = tail($);
        node* t = tail;
 {
        //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 */
        /**********    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 b57295024189fce9b4e12069ec6a2c43a36b8e07..752e371b4844fa1bdd1169d612fd1158103c0df8 100644 (file)
--- 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) {
                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 */
                /**********    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);
 @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 */
        /**********    Detected Correctness (testcase1 with -Y)    **********/
        atomic_store_explicit(&l->turn, turn + 1, memory_order_release);
        /** @OPDefine: true */