From: Peizhao Ou <peizhaoo@uci.edu>
Date: Mon, 16 Nov 2015 11:04:09 +0000 (-0800)
Subject: edits
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=d81ef0a8f5a876f83b327107451bff887c2cb305

edits
---

diff --git a/benchmark/ms-queue/Makefile b/benchmark/ms-queue/Makefile
index da3a0e4..ac84276 100644
--- 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 145c91d..e30535c 100644
--- 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 a09fb10..2da355a 100644
--- 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 c7c7b9c..0e5b20d 100644
--- 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 da3a0e4..ac84276 100644
--- 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)