ms-queue note

diff --git a/ms-queue/Makefile b/ms-queue/Makefile
index 34881f49ac5d2cab966b392d81fa5b3713423e12..46554a1509f0669859e08cd6c24e67ed9549a709 100644 (file)
--- a/ms-queue/Makefile
+++ b/ms-queue/Makefile
@@ -2,7 +2,7 @@ include ../benchmarks.mk
 
 BENCH := queue
 
-NORMAL_TESTS := testcase1
+NORMAL_TESTS := testcase1 testcase2
 
 WILDCARD_TESTS := $(patsubst %, %_wildcard, $(NORMAL_TESTS))
 

diff --git a/ms-queue/note.txt b/ms-queue/note.txt
new file mode 100644 (file)
index 0000000..eb2b995
--- /dev/null
+++ b/ms-queue/note.txt
@@ -0,0 +1,6 @@
+We ran testcase1 (two enqueuers and 1 dequeuer) and get result1.txt, then we ran
+testcase2 (1 enqueuers and 2 dequeuers) based on result1.txt and got
+result2.txt. We can't infer the wildcard(4) to be acquire because we can't reach
+"that case"!!! 
+See
+http://stackoverflow.com/questions/3873689/lock-free-queue-algorithm-repeated-reads-for-consistency

diff --git a/ms-queue/queue_wildcard.c b/ms-queue/queue_wildcard.c
index 43a2de2cf743fbe0d6b85530ae648866b3e3548f..73289a7af9f044581841c0b671fc05db005b1d62 100644 (file)
--- a/ms-queue/queue_wildcard.c
+++ b/ms-queue/queue_wildcard.c
@@ -103,12 +103,19 @@ void enqueue(queue_t *q, unsigned int val)
 
                        if (get_ptr(next) == 0) { // == NULL
                                pointer value = MAKE_POINTER(node, get_count(next) + 1);
+                               
+                               // ***********************************
+                               // Inference analysis results have two choices here, it either
+                               // makes wildcard(6) acq_rel and wildcard(8) relaxed or
+                               // wildcard(6) release and wildcard(8) acquire. The
+                               // synchronization here is for enqueue() to dequeue(), and
+                               // actually either synchronization options will work!!!
                                success = atomic_compare_exchange_strong_explicit(&q->nodes[get_ptr(tail)].next,
                                                &next, value, wildcard(6), wildcard(7)); // release & relaxed
                        }
                        if (!success) {
                                unsigned int ptr =
-                               get_ptr(atomic_load_explicit(&q->nodes[get_ptr(tail)].next, wildcard(8))); // acquire
+                                       get_ptr(atomic_load_explicit(&q->nodes[get_ptr(tail)].next, wildcard(8))); // acquire
                                pointer value = MAKE_POINTER(ptr,
                                                get_count(tail) + 1);
                                atomic_compare_exchange_strong_explicit(&q->tail,
@@ -154,7 +161,6 @@ bool dequeue(queue_t *q, unsigned int *retVal)
                        } else {
                                //value = load_32(&q->nodes[get_ptr(next)].value);
                                value = q->nodes[get_ptr(next)].value;
-                               // FIXME: SCFence makes this relaxed 
                                success = atomic_compare_exchange_strong_explicit(&q->head,
                                                &head, MAKE_POINTER(get_ptr(next), get_count(head) + 1),
                                                wildcard(19), wildcard(20)); // release & relaxed

diff --git a/ms-queue/result1.txt b/ms-queue/result1.txt
new file mode 100644 (file)
index 0000000..f1c01e6
--- /dev/null
+++ b/ms-queue/result1.txt
@@ -0,0 +1,64 @@
+Result 0:
+wildcard 1 -> memory_order_relaxed
+wildcard 2 -> memory_order_relaxed
+wildcard 3 -> memory_order_acquire
+wildcard 4 -> memory_order_relaxed
+wildcard 5 -> memory_order_relaxed
+wildcard 6 -> memory_order_acq_rel
+wildcard 8 -> memory_order_relaxed
+wildcard 9 -> memory_order_release
+wildcard 11 -> memory_order_release
+wildcard 13 -> memory_order_relaxed
+wildcard 14 -> memory_order_acquire
+wildcard 15 -> memory_order_acquire
+wildcard 16 -> memory_order_relaxed
+wildcard 17 -> memory_order_release
+wildcard 19 -> memory_order_relaxed
+Result 1:
+wildcard 1 -> memory_order_relaxed
+wildcard 2 -> memory_order_relaxed
+wildcard 3 -> memory_order_acquire
+wildcard 4 -> memory_order_relaxed
+wildcard 5 -> memory_order_relaxed
+wildcard 6 -> memory_order_release
+wildcard 8 -> memory_order_acquire
+wildcard 9 -> memory_order_release
+wildcard 11 -> memory_order_release
+wildcard 13 -> memory_order_relaxed
+wildcard 14 -> memory_order_acquire
+wildcard 15 -> memory_order_acquire
+wildcard 16 -> memory_order_relaxed
+wildcard 17 -> memory_order_release
+wildcard 19 -> memory_order_relaxed
+Result 2:
+wildcard 1 -> memory_order_relaxed
+wildcard 2 -> memory_order_relaxed
+wildcard 3 -> memory_order_acquire
+wildcard 4 -> memory_order_relaxed
+wildcard 5 -> memory_order_relaxed
+wildcard 6 -> memory_order_acq_rel
+wildcard 8 -> memory_order_relaxed
+wildcard 9 -> memory_order_acq_rel
+wildcard 11 -> memory_order_release
+wildcard 13 -> memory_order_relaxed
+wildcard 14 -> memory_order_acquire
+wildcard 15 -> memory_order_acquire
+wildcard 16 -> memory_order_relaxed
+wildcard 17 -> memory_order_release
+wildcard 19 -> memory_order_relaxed
+Result 3:
+wildcard 1 -> memory_order_relaxed
+wildcard 2 -> memory_order_relaxed
+wildcard 3 -> memory_order_acquire
+wildcard 4 -> memory_order_relaxed
+wildcard 5 -> memory_order_relaxed
+wildcard 6 -> memory_order_release
+wildcard 8 -> memory_order_acquire
+wildcard 9 -> memory_order_acq_rel
+wildcard 11 -> memory_order_release
+wildcard 13 -> memory_order_relaxed
+wildcard 14 -> memory_order_acquire
+wildcard 15 -> memory_order_acquire
+wildcard 16 -> memory_order_relaxed
+wildcard 17 -> memory_order_release
+wildcard 19 -> memory_order_relaxed

diff --git a/ms-queue/testcase1.c b/ms-queue/testcase1.c
index 6548366cab6a0458e9d36a75b01827826d45f75b..78feaa441f41f087a7b79bd823d69375e2ad45db 100644 (file)
--- a/ms-queue/testcase1.c
+++ b/ms-queue/testcase1.c
@@ -5,7 +5,6 @@
 #include "queue.h"
 #include "model-assert.h"
 
-static int procs = 4;
 static queue_t *queue;
 static thrd_t *threads;
 static unsigned int *input;
@@ -24,24 +23,32 @@ int get_thread_num()
 }
 
 bool succ1, succ2;
+atomic_int x[3];
+int idx1, idx2;
 
+static int procs = 4;
 static void main_task(void *param)
 {
        unsigned int val;
        int pid = *((int *)param);
        if (pid % 4 == 0) {
-               input[0] = 17;
-               enqueue(queue, input[0]);
-               succ1 = dequeue(queue, &output[0]);
-               //printf("Dequeue: %d\n", output[0]);
+               atomic_store_explicit(&x[0], 1, memory_order_relaxed);
+               enqueue(queue, 0);
        } else if (pid % 4 == 1) {
-               input[1] = 37;
-               enqueue(queue, input[1]);
-               succ2 = dequeue(queue, &output[1]);
+               atomic_store_explicit(&x[1], 1, memory_order_relaxed);
+               enqueue(queue, 1);
        } else if (pid % 4 == 2) {
-       
+               succ1 = dequeue(queue, &idx1);
+               if (succ1) {
+                       atomic_load_explicit(&x[idx1], memory_order_relaxed);
+               }
        } else if (pid % 4 == 3) {
-
+               /*
+               succ2 = dequeue(queue, &idx2);
+               if (succ2) {
+                       atomic_load_explicit(&x[idx2], memory_order_relaxed);
+               }
+               */
        }
 }
 
@@ -60,6 +67,9 @@ int user_main(int argc, char **argv)
        input = calloc(num_threads, sizeof(*input));
        output = 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;

diff --git a/ms-queue/testcase2.c b/ms-queue/testcase2.c
new file mode 100644 (file)
index 0000000..3431b26
--- /dev/null
+++ b/ms-queue/testcase2.c
@@ -0,0 +1,99 @@
+#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];
+int idx1, idx2;
+
+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);
+               */
+       } else if (pid % 4 == 1) {
+               atomic_store_explicit(&x[1], 1, memory_order_relaxed);
+               enqueue(queue, 1);
+       } else if (pid % 4 == 2) {
+               succ1 = dequeue(queue, &idx1);
+               if (succ1) {
+                       atomic_load_explicit(&x[idx1], memory_order_relaxed);
+               }
+       } else if (pid % 4 == 3) {
+               succ2 = dequeue(queue, &idx2);
+               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;
+
+       queue = calloc(1, sizeof(*queue));
+       MODEL_ASSERT(queue);
+
+       num_threads = procs;
+       threads = malloc(num_threads * sizeof(thrd_t));
+       param = malloc(num_threads * sizeof(*param));
+       input = calloc(num_threads, sizeof(*input));
+       output = calloc(num_threads, sizeof(*output));
+
+       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/testcase3.c b/ms-queue/testcase3.c
new file mode 100644 (file)
index 0000000..f6243f9
--- /dev/null
+++ b/ms-queue/testcase3.c
@@ -0,0 +1,101 @@
+#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];
+int idx1, idx2;
+
+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);
+       
+               succ1 = dequeue(queue, &idx1);
+               if (succ1) {
+                       atomic_load_explicit(&x[idx1], memory_order_relaxed);
+               }
+       } else if (pid % 4 == 1) {
+               atomic_store_explicit(&x[1], 1, memory_order_relaxed);
+               enqueue(queue, 1);
+
+               succ2 = dequeue(queue, &idx2);
+               if (succ2) {
+                       atomic_load_explicit(&x[idx2], memory_order_relaxed);
+               }
+       } else if (pid % 4 == 2) {
+
+       } else if (pid % 4 == 3) {
+       
+       }
+}
+
+int user_main(int argc, char **argv)
+{
+       int i;
+       int *param;
+       unsigned int in_sum = 0, out_sum = 0;
+
+       queue = calloc(1, sizeof(*queue));
+       MODEL_ASSERT(queue);
+
+       num_threads = procs;
+       threads = malloc(num_threads * sizeof(thrd_t));
+       param = malloc(num_threads * sizeof(*param));
+       input = calloc(num_threads, sizeof(*input));
+       output = calloc(num_threads, sizeof(*output));
+
+       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;
+}