changes

diff --git a/benchmark/ms-queue/main.c b/benchmark/ms-queue/main.c
index 4a9f689d7e766daaa81c5b1416a52b59b836e528..f6973a706ced450952d2e7180579ddb0d9c4acc9 100644 (file)
--- a/benchmark/ms-queue/main.c
+++ b/benchmark/ms-queue/main.c
@@ -5,7 +5,7 @@
 #include "my_queue.h"
 #include "model-assert.h"
 
-static int procs = 2;
+static int procs = 3;
 static queue_t *queue;
 static thrd_t *threads;
 static unsigned int *input;
@@ -40,24 +40,36 @@ static void main_task(void *param)
        }
 */
 
-       if (!pid) {
+       if (pid % 3 == 0) {
                input[0] = 17;
                enqueue(queue, input[0]);
                printf("Enqueue %d.\n", 17);
+               
                succ1 = dequeue(queue, &input[0]);
                if (succ1)
-                       printf("Dequeue %d.\n", input[0]);
+                       printf("Thrd 2: Dequeue %d.\n", input[0]);
                else
-                       printf("Dequeue NULL.\n");
-       } else {
+                       printf("Thrd 2: Dequeue NULL.\n");
+               
+       } else if (pid % 3 == 1) {
+               
                input[1] = 37;
                enqueue(queue, input[1]);
                printf("Enqueue %d.\n", 37);
+               
+               succ1 = dequeue(queue, &input[0]);
+               if (succ1)
+                       printf("Thrd 3: Dequeue %d.\n", input[0]);
+               else
+                       printf("Thrd 3: Dequeue NULL.\n");
+       } else if (pid %3 == 2) {
+               /*
                succ2 = dequeue(queue, &output[1]);
                if (succ2)
                        printf("Dequeue %d.\n", input[1]);
                else
                        printf("Dequeue NULL.\n");
+                       */
        }
 
 }

diff --git a/benchmark/ms-queue/my_queue.c b/benchmark/ms-queue/my_queue.c
index 1d9e924538d16bd9dc192846b1785b38d7811907..bb237bf6c0df386167749820c007ad7fe7e9908c 100644 (file)
--- a/benchmark/ms-queue/my_queue.c
+++ b/benchmark/ms-queue/my_queue.c
@@ -162,8 +162,8 @@ void enqueue(queue_t *q, unsigned int val)
                        MAKE_POINTER(node, get_count(tail) + 1),
                        release, relaxed);
        /**
-               @Begin
-               @Commit_point_define_check: succ 
+               //@Begin
+               @Commit_point_define_check: succ
                @Label: Enqueue_UpdateOrLoad_Tail
                @End
        */
@@ -174,7 +174,7 @@ void enqueue(queue_t *q, unsigned int val)
        @Interface_define: Dequeue
        @End
 */
-bool dequeue(queue_t *q, int *output)
+bool dequeue(queue_t *q, int *retVal)
 {
        unsigned int value;
        int success = 0;
@@ -197,7 +197,7 @@ bool dequeue(queue_t *q, int *output)
                        @Label: Dequeue_Read_Head
                        @End
                */
-               tail = atomic_load_explicit(&q->tail, relaxed);
+               tail = atomic_load_explicit(&q->tail, acquire);
                /**
                        @Begin
                        @Potential_commit_point_define: true
@@ -251,6 +251,7 @@ bool dequeue(queue_t *q, int *output)
                                        @End
                                */
                                value = load_32(&q->nodes[get_ptr(next)].value);
+                               *retVal = value;
                                //value = q->nodes[get_ptr(next)].value;
                                /****FIXME: correctness error ****/
                                success = atomic_compare_exchange_strong_explicit(&q->head,
@@ -263,6 +264,5 @@ bool dequeue(queue_t *q, int *output)
                }
        }
        reclaim(get_ptr(head));
-       *output = value;
        return true;
 }

diff --git a/benchmark/ms-queue/my_queue.h b/benchmark/ms-queue/my_queue.h
index 714be4f83d71daeb98b68a9f1681fd3076d5a39d..576ce9eab8788465d6d5652ec21f43366c2d29c1 100644 (file)
--- a/benchmark/ms-queue/my_queue.h
+++ b/benchmark/ms-queue/my_queue.h
@@ -88,13 +88,14 @@ void init_queue(queue_t *q, int num_threads);
 /**
        @Begin
        @Interface: Enqueue
-       @Commit_point_set: Enqueue_Read_Tail | Enqueue_UpdateNext | Enqueue_UpdateOrLoad_Tail
+       @Commit_point_set: Enqueue_Read_Tail | Enqueue_UpdateNext
        @ID: get_and_inc(tag)
        @Action:
                # __ID__ is an internal macro that refers to the id of the current
                # interface call
                tag_elem_t *elem = new_tag_elem(__ID__, val);
                push_back(__queue, elem);
+               model_print("Enqueue: input=%d\n", val);
        @End
 */
 void enqueue(queue_t *q, unsigned int val);
@@ -109,14 +110,13 @@ void enqueue(queue_t *q, unsigned int val);
                if (size(__queue) > 0) {
                        _Old_Val = get_data(front(__queue));
                        pop_front(__queue);
-               } else {
-                       _Old_Val = 0;
                }
+               model_print("Dequeue: __RET=%d, retVal=%d\n", __RET__, *retVal);
        @Post_check:
-               __RET__ ? *output == _Old_Val : _Old_Val == 0
+               _Old_Val == 0 ? !__RET__ : _Old_Val == *retVal
        @End
 */
-bool dequeue(queue_t *q, int *output);
+bool dequeue(queue_t *q, int *retVal);
 int get_thread_num();
 
 #endif