edits
authorPeizhao Ou <peizhaoo@uci.edu>
Mon, 16 Nov 2015 11:04:09 +0000 (03:04 -0800)
committerPeizhao Ou <peizhaoo@uci.edu>
Mon, 16 Nov 2015 11:04:09 +0000 (03:04 -0800)
benchmark/ms-queue/Makefile
benchmark/ms-queue/my_queue.c
benchmark/ms-queue/my_queue.h
benchmark/ms-queue/testcase1.c
output/ms-queue/Makefile

index da3a0e4..ac84276 100644 (file)
@@ -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)
 
index 145c91d..e30535c 100644 (file)
@@ -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!!
index a09fb10..2da355a 100644 (file)
@@ -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;
index c7c7b9c..0e5b20d 100644 (file)
@@ -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);
        }
 }
 
index da3a0e4..ac84276 100644 (file)
@@ -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)