changes

diff --git a/benchmark/ms-queue/main.c b/benchmark/ms-queue/main.c
index f6973a706ced450952d2e7180579ddb0d9c4acc9..63846670512c3f5e9ff64b36a4ca54d00a712011 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 = 3;
+static int procs = 2;
 static queue_t *queue;
 static thrd_t *threads;
 static unsigned int *input;
@@ -39,39 +39,28 @@ static void main_task(void *param)
                enqueue(queue, input[1]);
        }
 */
-
-       if (pid % 3 == 0) {
+       if (pid % 2 == 0) {
                input[0] = 17;
                enqueue(queue, input[0]);
-               printf("Enqueue %d.\n", 17);
+               printf("Thrd %d Enqueue %d.\n", get_thread_num(), input[0]);
                
-               succ1 = dequeue(queue, &input[0]);
+               succ1 = dequeue(queue, &output[0]);
                if (succ1)
-                       printf("Thrd 2: Dequeue %d.\n", input[0]);
+                       printf("Thrd %d: Dequeue %d.\n", get_thread_num(), output[0]);
                else
-                       printf("Thrd 2: Dequeue NULL.\n");
-               
-       } else if (pid % 3 == 1) {
+                       printf("Thrd %d: Dequeue NULL.\n", get_thread_num());
                
+       } else if (pid % 2 == 1) {
                input[1] = 37;
                enqueue(queue, input[1]);
-               printf("Enqueue %d.\n", 37);
+               printf("Thrd %d Enqueue %d.\n", get_thread_num(), input[1]);
                
-               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]);
+                       printf("Thrd %d: Dequeue %d.\n", get_thread_num(), output[1]);
                else
-                       printf("Dequeue NULL.\n");
-                       */
+                       printf("Thrd %d: Dequeue NULL.\n", get_thread_num());
        }
-
 }
 
 int user_main(int argc, char **argv)

diff --git a/benchmark/ms-queue/my_queue.c b/benchmark/ms-queue/my_queue.c
index bb237bf6c0df386167749820c007ad7fe7e9908c..fe4da51fe7275a87dd062a6fef9af7152c46855f 100644 (file)
--- a/benchmark/ms-queue/my_queue.c
+++ b/benchmark/ms-queue/my_queue.c
@@ -161,12 +161,6 @@ void enqueue(queue_t *q, unsigned int val)
                        &tail,
                        MAKE_POINTER(node, get_count(tail) + 1),
                        release, relaxed);
-       /**
-               //@Begin
-               @Commit_point_define_check: succ
-               @Label: Enqueue_UpdateOrLoad_Tail
-               @End
-       */
 }
 
 /**
@@ -176,7 +170,7 @@ void enqueue(queue_t *q, unsigned int val)
 */
 bool dequeue(queue_t *q, int *retVal)
 {
-       unsigned int value;
+       unsigned int value = 0;
        int success = 0;
        pointer head;
        pointer tail;
@@ -197,6 +191,10 @@ bool dequeue(queue_t *q, int *retVal)
                        @Label: Dequeue_Read_Head
                        @End
                */
+               /** A new bug has been found here!!! It should be acquire instead of
+                * relaxed (it introduces a bug when there's two dequeuers and one
+                * enqueuer)
+                */
                tail = atomic_load_explicit(&q->tail, acquire);
                /**
                        @Begin
@@ -243,26 +241,26 @@ bool dequeue(queue_t *q, int *retVal)
                                //printf("miss4_dequeue\n");
                                thrd_yield();
                        } else {
-                               /**
-                                       @Begin
-                                       @Commit_point_define: true
-                                       @Potential_commit_point_label: Dequeue_Potential_LoadNext
-                                       @Label: Dequeue_LoadNext
-                                       @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,
                                                &head,
                                                MAKE_POINTER(get_ptr(next), get_count(head) + 1),
                                                release, relaxed);
+                               /**
+                                       @Begin
+                                       @Commit_point_define: success
+                                       @Potential_commit_point_label: Dequeue_Potential_LoadNext
+                                       @Label: Dequeue_LoadNext
+                                       @End
+                               */
                                if (!success)
                                        thrd_yield();
                        }
                }
        }
        reclaim(get_ptr(head));
+       *retVal = value;
        return true;
 }

diff --git a/benchmark/ms-queue/my_queue.h b/benchmark/ms-queue/my_queue.h
index 576ce9eab8788465d6d5652ec21f43366c2d29c1..90f57755d74dfe261330c73ef77139a10533ced6 100644 (file)
--- a/benchmark/ms-queue/my_queue.h
+++ b/benchmark/ms-queue/my_queue.h
@@ -111,7 +111,7 @@ void enqueue(queue_t *q, unsigned int val);
                        _Old_Val = get_data(front(__queue));
                        pop_front(__queue);
                }
-               model_print("Dequeue: __RET=%d, retVal=%d\n", __RET__, *retVal);
+               model_print("Dequeue: __RET__=%d, retVal=%d, Old_Val=%d\n", __RET__, *retVal, _Old_Val);
        @Post_check:
                _Old_Val == 0 ? !__RET__ : _Old_Val == *retVal
        @End

diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
index 7386052cdd3f44c293b140df41852cf2eb45cb2c..e95ff5fb2ef5439bfd1f7c1833eae1cd388d42fc 100644 (file)
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
@@ -298,6 +298,7 @@ public class CodeGenerator {
 
                File[] srcMSQueue = {
                                new File(homeDir + "/benchmark/ms-queue/my_queue.c"),
+                               new File(homeDir + "/benchmark/ms-queue/testcase.c"),
                                new File(homeDir + "/benchmark/ms-queue/main.c"),
                                new File(homeDir + "/benchmark/ms-queue/my_queue.h") };
 
@@ -325,7 +326,7 @@ public class CodeGenerator {
 //             File[][] sources = { srcLinuxRWLocks,  srcMSQueue, srcRCU,
 //                             srcDeque, srcMCSLock, srcSPSCQueue, srcMPMCQueue, srcHashtable };
 
-                File[][] sources = {srcMSQueue };
+                File[][] sources = {srcMSQueue, srcHashtable };
                // Compile all the benchmarks
                for (int i = 0; i < sources.length; i++) {
                        CodeGenerator gen = new CodeGenerator(sources[i]);