edits

diff --git a/benchmark/ms-queue/Makefile b/benchmark/ms-queue/Makefile
index da3a0e46b3ee7f4c5d5a9e4f8165db58d00c1774..ac8427698f44318631cd1c3bebcc32b74ad0fc03 100644 (file)
--- a/benchmark/ms-queue/Makefile
+++ b/benchmark/ms-queue/Makefile
@@ -1,15 +1,18 @@
 include ../benchmarks.mk
 
-TESTNAME = main
+TESTNAME = main testcase1
 
 HEADERS = my_queue.h
 OBJECTS = main.o my_queue.o
 
 all: $(TESTNAME)
 
-$(TESTNAME): $(HEADERS) $(OBJECTS)
+main: $(HEADERS) $(OBJECTS)
        $(CC) -o $@ $(OBJECTS) $(CFLAGS) $(LDFLAGS)
 
+testcase1: $(HEADERS) my_queue.o testcase1.o 
+       $(CC) -o $@ my_queue.o testcase1.o $(CFLAGS) $(LDFLAGS)
+
 %.o: %.c
        $(CC) -c -o $@ $< $(CFLAGS)
 

diff --git a/benchmark/ms-queue/my_queue.c b/benchmark/ms-queue/my_queue.c
index 145c91d30dcd8723ceb5da0c57918ee3a711d097..e30535cabbcfb93e8f1cf873a1516d9860349105 100644 (file)
--- a/benchmark/ms-queue/my_queue.c
+++ b/benchmark/ms-queue/my_queue.c
@@ -183,6 +183,13 @@ bool dequeue(queue_t *q, int *retVal)
                */
                /**** detected correctness error ****/
                head = atomic_load_explicit(&q->head, acquire);
+               /**
+                       @Begin
+                       @Commit_point_define_check: true
+                       @Label: DequeueReadHead
+                       @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) correctness bug!!

diff --git a/benchmark/ms-queue/my_queue.h b/benchmark/ms-queue/my_queue.h
index a09fb10454292ee217a7f8e6cd6329bf87474642..2da355a94c29bf05e2da8c3e3e06c1a3685fc2de 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);
 /**
        @Begin
        @Interface: Dequeue
-       @Commit_point_set: DequeueUpdateHead | DequeueReadNextVerify
+       @Commit_point_set: DequeueReadHead | DequeueUpdateHead | DequeueReadNextVerify
        @ID: get_id(front(__queue))
        @Action:
                unsigned int _Old_Val = 0;

diff --git a/benchmark/ms-queue/testcase1.c b/benchmark/ms-queue/testcase1.c
index c7c7b9c8badf936d2ff153f0d903d7c1b067741c..0e5b20dbb00514b55263b5babbca761bbef9ff2a 100644 (file)
--- a/benchmark/ms-queue/testcase1.c
+++ b/benchmark/ms-queue/testcase1.c
@@ -5,7 +5,7 @@
 #include "my_queue.h"
 #include "model-assert.h"
 
-static int procs = 4;
+static int procs = 2;
 static queue_t *queue;
 static thrd_t *threads;
 static unsigned int *input;
@@ -39,20 +39,7 @@ static void main_task(void *param)
                else
                        printf("Thrd 2: Dequeue NULL.\n");
        } else if (pid % 4 == 1) {
-               output2 = 2;
-               succ2 = dequeue(queue, &output2);
-               if (succ2)
-                       printf("Thrd 3: Dequeue %d.\n", output2);
-               else
-                       printf("Thrd 3: Dequeue NULL.\n");
-       } else if (pid % 4 == 2) {
-               int input = 47;
-               enqueue(queue, input);
-               printf("Thrd 4 Enqueue %d.\n", input);
-       } else {
-               int input = 27;
-               enqueue(queue, input);
-               printf("Thrd 5 Enqueue %d.\n", input);
+               enqueue(queue, 2);
        }
 }
 

diff --git a/output/ms-queue/Makefile b/output/ms-queue/Makefile
index da3a0e46b3ee7f4c5d5a9e4f8165db58d00c1774..ac8427698f44318631cd1c3bebcc32b74ad0fc03 100644 (file)
--- a/output/ms-queue/Makefile
+++ b/output/ms-queue/Makefile
@@ -1,15 +1,18 @@
 include ../benchmarks.mk
 
-TESTNAME = main
+TESTNAME = main testcase1
 
 HEADERS = my_queue.h
 OBJECTS = main.o my_queue.o
 
 all: $(TESTNAME)
 
-$(TESTNAME): $(HEADERS) $(OBJECTS)
+main: $(HEADERS) $(OBJECTS)
        $(CC) -o $@ $(OBJECTS) $(CFLAGS) $(LDFLAGS)
 
+testcase1: $(HEADERS) my_queue.o testcase1.o 
+       $(CC) -o $@ my_queue.o testcase1.o $(CFLAGS) $(LDFLAGS)
+
 %.o: %.c
        $(CC) -c -o $@ $< $(CFLAGS)