X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker-benchmarks.git;a=blobdiff_plain;f=ms-queue%2Fmain.c;h=e46413840bf7e46cba895693392a1153853ddfe5;hp=51e0e79c478e64c0267ba794b074115b7f69d822;hb=HEAD;hpb=4f919e0a75b2bbc708bee3d109349fe24e4b264c

diff --git a/ms-queue/main.c b/ms-queue/main.c
index 51e0e79..e464138 100644
--- a/ms-queue/main.c
+++ b/ms-queue/main.c
@@ -1,14 +1,15 @@
 #include <stdlib.h>
-#include <assert.h>
 #include <stdio.h>
 #include <threads.h>
 
 #include "my_queue.h"
+#include "model-assert.h"
 
 static int procs = 2;
-static int iterations = 1;
 static queue_t *queue;
 static thrd_t *threads;
+static unsigned int *input;
+static unsigned int *output;
 static int num_threads;
 
 int get_thread_num()
@@ -18,42 +19,25 @@ int get_thread_num()
 	for (i = 0; i < num_threads; i++)
 		if (curr.priv == threads[i].priv)
 			return i;
-	assert(0);
+	MODEL_ASSERT(0);
 	return -1;
 }
 
-static void parse_args(int argc, char **argv)
-{
-	extern char *optarg;
-	int c;
-
-	while ((c = getopt(argc, argv, "i:p:")) != EOF) {
-		switch (c) {
-		case 'i':
-			iterations = atoi(optarg);
-			break;
-		case 'p':
-			procs = atoi(optarg);
-			break;
-		default:
-			assert(0);
-		}
-	}
-}
+bool succ1, succ2;
 
 static void main_task(void *param)
 {
-	unsigned int i, j;
 	unsigned int val;
 	int pid = *((int *)param);
-
-	for (i = 0; i < iterations; i++) {
-		val = 1 + pid * iterations + i;
-		printf("worker %d, enqueueing: %u\n", pid, val);
-		enqueue(queue, val);
-
-		val = dequeue(queue);
-		printf("worker %d, dequeued: %u\n", pid, val);
+	if (!pid) {
+		input[0] = 17;
+		enqueue(queue, input[0]);
+		succ1 = dequeue(queue, &output[0]);
+		//printf("Dequeue: %d\n", output[0]);
+	} else {
+		input[1] = 37;
+		enqueue(queue, input[1]);
+		succ2 = dequeue(queue, &output[1]);
 	}
 }
 
@@ -61,16 +45,16 @@ int user_main(int argc, char **argv)
 {
 	int i;
 	int *param;
-
-	parse_args(argc, argv);
-	iterations = (iterations + (procs >> 1)) / procs;
+	unsigned int in_sum = 0, out_sum = 0;
 
 	queue = calloc(1, sizeof(*queue));
-	assert(queue);
+	MODEL_ASSERT(queue);
 
 	num_threads = procs;
 	threads = malloc(num_threads * sizeof(thrd_t));
 	param = malloc(num_threads * sizeof(*param));
+	input = calloc(num_threads, sizeof(*input));
+	output = calloc(num_threads, sizeof(*output));
 
 	init_queue(queue, num_threads);
 	for (i = 0; i < num_threads; i++) {
@@ -80,6 +64,19 @@ int user_main(int argc, char **argv)
 	for (i = 0; i < num_threads; i++)
 		thrd_join(threads[i]);
 
+	for (i = 0; i < num_threads; i++) {
+		in_sum += input[i];
+		out_sum += output[i];
+	}
+	for (i = 0; i < num_threads; i++)
+		printf("input[%d] = %u\n", i, input[i]);
+	for (i = 0; i < num_threads; i++)
+		printf("output[%d] = %u\n", i, output[i]);
+	if (succ1 && succ2)
+		MODEL_ASSERT(in_sum == out_sum);
+	else
+		MODEL_ASSERT (false);
+
 	free(param);
 	free(threads);
 	free(queue);