save

diff --git a/benchmark/mpmc-queue/mpmc-queue.cc b/benchmark/mpmc-queue/mpmc-queue.cc
index bf172ea1ef4f4900361d27f72274cd791891335c..ca063e9891aa0657e85a6501fa2a5ecaccdc3586 100644 (file)
--- a/benchmark/mpmc-queue/mpmc-queue.cc
+++ b/benchmark/mpmc-queue/mpmc-queue.cc
@@ -11,7 +11,7 @@
 void threadA(struct mpmc_boundq_1_alt<int32_t, sizeof(int32_t)> *queue)
 {
        int32_t *bin = queue->write_prepare();
-       //store_32(bin, 1);
+       store_32(bin, 1);
        *bin = 1;
        printf("write_bin %d, val %d\n", bin, 1);
        queue->write_publish(bin);
@@ -21,8 +21,8 @@ void threadB(struct mpmc_boundq_1_alt<int32_t, sizeof(int32_t)> *queue)
 {
        int32_t *bin;
        while (bin = queue->read_fetch()) {
-               //printf("Read: %d\n", load_32(bin));
-               //printf("read_bin %d, val %d\n", bin, load_32(bin));
+               printf("Read: %d\n", load_32(bin));
+               printf("read_bin %d, val %d\n", bin, load_32(bin));
                printf("Read: %d\n", *bin);
                queue->read_consume(bin);
        }
@@ -31,12 +31,12 @@ void threadB(struct mpmc_boundq_1_alt<int32_t, sizeof(int32_t)> *queue)
 void threadC(struct mpmc_boundq_1_alt<int32_t, sizeof(int32_t)> *queue)
 {
        int32_t *bin = queue->write_prepare();
-       //store_32(bin, 1);
+       store_32(bin, 1);
        *bin = 1;
        queue->write_publish(bin);
 
        while (bin = queue->read_fetch()) {
-               //printf("Read: %d\n", load_32(bin));
+               printf("Read: %d\n", load_32(bin));
                printf("Read: %d\n", *bin);
                queue->read_consume(bin);
        }
@@ -119,7 +119,7 @@ int user_main(int argc, char **argv)
 #ifndef CONFIG_MPMC_NO_INITIAL_ELEMENT
        printf("Adding initial element\n");
        int32_t *bin = queue.write_prepare();
-       //store_32(bin, 17);
+       store_32(bin, 17);
        *bin, 17;
        printf("init_write_bin %d, val %d\n", bin, 17);
        queue.write_publish(bin);

diff --git a/benchmark/ms-queue/my_queue.c b/benchmark/ms-queue/my_queue.c
index 017670b5703a7c678fea23c9a7b0fb69867f8b71..186745eaec079251e7e49ce57b9cfe68def3db1a 100644 (file)
--- a/benchmark/ms-queue/my_queue.c
+++ b/benchmark/ms-queue/my_queue.c
@@ -22,16 +22,16 @@ 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];
+               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;
+                       store_32(&free_lists[t][i], 0);
+                       //free_lists[t][i] = 0;
                        return node;
                }
        }
        /* free_list is empty? */
-       //MODEL_ASSERT(0);
+       MODEL_ASSERT(0);
        return 0;
 }
 
@@ -42,22 +42,22 @@ static void reclaim(unsigned int node)
        int t = get_thread_num();
 
        /* Don't reclaim NULL node */
-       //MODEL_ASSERT(node);
+       MODEL_ASSERT(node);
 
        for (i = 0; i < MAX_FREELIST; i++) {
                /* Should never race with our own thread here */
-               //unsigned int idx = load_32(&free_lists[t][i]);
-               unsigned int idx = free_lists[t][i];
+               unsigned int idx = load_32(&free_lists[t][i]);
+               //unsigned int idx = free_lists[t][i];
 
                /* Found empty spot in free list */
                if (idx == 0) {
-                       //store_32(&free_lists[t][i], node);
-                       free_lists[t][i] = node;
+                       store_32(&free_lists[t][i], node);
+                       //free_lists[t][i] = node;
                        return;
                }
        }
        /* free list is full? */
-       //MODEL_ASSERT(0);
+       MODEL_ASSERT(0);
 }
 
 void init_queue(queue_t *q, int num_threads)
@@ -94,8 +94,8 @@ void enqueue(queue_t *q, unsigned int val)
        pointer tmp;
 
        node = new_node();
-       //store_32(&q->nodes[node].value, val);
-       q->nodes[node].value = val;
+       store_32(&q->nodes[node].value, val);
+       //q->nodes[node].value = val;
        tmp = atomic_load_explicit(&q->nodes[node].next, relaxed);
        set_ptr(&tmp, 0); // NULL
        atomic_store_explicit(&q->nodes[node].next, tmp, relaxed);
@@ -105,6 +105,7 @@ void enqueue(queue_t *q, unsigned int val)
                tail = atomic_load_explicit(&q->tail, acquire);
                /****FIXME: miss ****/
                next = atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire);
+               printf("miss1_enqueue\n");
                if (tail == atomic_load_explicit(&q->tail, relaxed)) {
 
                        /* Check for uninitialized 'next' */
@@ -112,9 +113,10 @@ void enqueue(queue_t *q, unsigned int val)
 
                        if (get_ptr(next) == 0) { // == NULL
                                pointer value = MAKE_POINTER(node, get_count(next) + 1);
-                               /****FIXME: first release UL, second release miss ****/
+                               /****FIXME: first release UL ****/
+                               // Second release can be just relaxed
                                success = atomic_compare_exchange_strong_explicit(&q->nodes[get_ptr(tail)].next,
-                                               &next, value, release, release);
+                                               &next, value, release, relaxed);
                                /**
                                        @Begin
                                        @Commit_point_define_check: success == true
@@ -127,18 +129,21 @@ void enqueue(queue_t *q, unsigned int val)
                                unsigned int ptr = get_ptr(atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire));
                                pointer value = MAKE_POINTER(ptr,
                                                get_count(tail) + 1);
-                               /****FIXME: both miss ****/
+                               /****FIXME: miss ****/
+                               // Seconde release can be just relaxed
                                atomic_compare_exchange_strong_explicit(&q->tail,
-                                               &tail, value, release, release);
+                                               &tail, value, release, relaxed);
+                               printf("miss2_enqueue\n");
                                thrd_yield();
                        }
                }
        }
-       /****FIXME: first UL, second miss ****/
+       /****FIXME: first UL ****/
+       // Seconde release can be just relaxed
        atomic_compare_exchange_strong_explicit(&q->tail,
                        &tail,
                        MAKE_POINTER(node, get_count(tail) + 1),
-                       release, release);
+                       release, relaxed);
 }
 
 /**
@@ -160,11 +165,12 @@ unsigned int dequeue(queue_t *q)
                tail = atomic_load_explicit(&q->tail, relaxed);
                /****FIXME: miss ****/
                next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, acquire);
+               printf("miss3_dequeue\n");
                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);
+                               MODEL_ASSERT(get_ptr(next) != POISON_IDX);
 
                                if (get_ptr(next) == 0) { // NULL
                                        /**
@@ -175,20 +181,23 @@ unsigned int dequeue(queue_t *q)
                                        */
                                        return 0; // NULL
                                }
-                               /****FIXME: both miss ****/
+                               /****FIXME: miss (not reached) ****/
+                               // Seconde release can be just relaxed
                                atomic_compare_exchange_strong_explicit(&q->tail,
                                                &tail,
                                                MAKE_POINTER(get_ptr(next), get_count(tail) + 1),
-                                               release, release);
+                                               release, relaxed);
+                               printf("miss4_dequeue\n");
                                thrd_yield();
                        } else {
-                               //value = load_32(&q->nodes[get_ptr(next)].value);
-                               value = q->nodes[get_ptr(next)].value;
-                               /****FIXME: first correctness error, second miss ****/
+                               value = load_32(&q->nodes[get_ptr(next)].value);
+                               //value = q->nodes[get_ptr(next)].value;
+                               /****FIXME: correctness error ****/
+                               // Seconde release can be just relaxed
                                success = atomic_compare_exchange_strong_explicit(&q->head,
                                                &head,
                                                MAKE_POINTER(get_ptr(next), get_count(head) + 1),
-                                               release, release);
+                                               release, relaxed);
                                /**
                                        @Begin
                                        @Commit_point_define_check: success == true