From b568a7063faeb671240c8b3a169ea60cee01858e Mon Sep 17 00:00:00 2001
From: Peizhao Ou <peizhaoo@uci.edu>
Date: Mon, 16 Nov 2015 22:46:29 -0800
Subject: [PATCH] edits
---
benchmark/ms-queue/my_queue.c | 19 ++--
benchmark/ms-queue/testcase.c | 19 ++--
benchmark/ms-queue/testcase3.c | 96 +++++++++++++++++++
.../codeGenerator/CodeGenerator.java | 1 +
4 files changed, 117 insertions(+), 18 deletions(-)
create mode 100644 benchmark/ms-queue/testcase3.c
diff --git a/benchmark/ms-queue/my_queue.c b/benchmark/ms-queue/my_queue.c
index b8189c9..ae33b7d 100644
--- a/benchmark/ms-queue/my_queue.c
+++ b/benchmark/ms-queue/my_queue.c
@@ -111,7 +111,7 @@ void enqueue(queue_t *q, unsigned int val)
@Label: Enqueue_Clear
@End
*/
- /**** detected UL ****/
+ /**** UL & inadmissible ****/
tail = atomic_load_explicit(&q->tail, acquire);
/****FIXME: miss ****/
next = atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire);
@@ -123,7 +123,7 @@ void enqueue(queue_t *q, unsigned int val)
if (get_ptr(next) == 0) { // == NULL
pointer value = MAKE_POINTER(node, get_count(next) + 1);
- /**** detected UL ****/
+ /**** SPEC Error (testcase1.c) ****/
// Second release can be just relaxed
success = atomic_compare_exchange_strong_explicit(&q->nodes[get_ptr(tail)].next,
&next, value, release, relaxed);
@@ -136,7 +136,7 @@ void enqueue(queue_t *q, unsigned int val)
}
if (!success) {
// This routine helps the other enqueue to update the tail
- /**** detected UL ****/
+ /**** UL & Inadmissible ****/
unsigned int ptr = get_ptr(atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire));
pointer value = MAKE_POINTER(ptr,
get_count(tail) + 1);
@@ -153,7 +153,7 @@ void enqueue(queue_t *q, unsigned int val)
}
}
}
- /**** dectected UL ****/
+ /**** UL & Inadmissible ****/
// Second release can be just relaxed
bool succ = atomic_compare_exchange_strong_explicit(&q->tail,
&tail,
@@ -181,7 +181,7 @@ bool dequeue(queue_t *q, int *retVal)
@Label: Dequeue_Clear
@End
*/
- /**** detected correctness error ****/
+ /**** Inadmissible ****/
head = atomic_load_explicit(&q->head, acquire);
/**
@Begin
@@ -194,10 +194,11 @@ bool dequeue(queue_t *q, int *retVal)
* relaxed (it introduces a bug when there's two dequeuers and one
* enqueuer) correctness bug!!
*/
+ /**** New bug ****/
tail = atomic_load_explicit(&q->tail, acquire);
- /**** Detected UL/DR (testcase1.c) ****/
- next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, acquire);
+ /**** SPEC Error (testcase1.c) ****/
+ next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, relaxed);
/**
@Begin
@Potential_commit_point_define: true
@@ -213,7 +214,7 @@ bool dequeue(queue_t *q, int *retVal)
if (get_ptr(next) == 0) { // NULL
return false; // NULL
}
- /**** Detected UL (testcase1.c) ****/
+ /**** FIXME: miss ****/
// Second release can be just relaxed
bool succ = false;
succ = atomic_compare_exchange_strong_explicit(&q->tail,
@@ -228,7 +229,7 @@ bool dequeue(queue_t *q, int *retVal)
} else {
//value = load_32(&q->nodes[get_ptr(next)].value);
value = q->nodes[get_ptr(next)].value;
- /**** correctness error ****/
+ /**** inadmissibility ****/
success = atomic_compare_exchange_strong_explicit(&q->head,
&head,
MAKE_POINTER(get_ptr(next), get_count(head) + 1),
diff --git a/benchmark/ms-queue/testcase.c b/benchmark/ms-queue/testcase.c
index 9deb686..5271a54 100644
--- a/benchmark/ms-queue/testcase.c
+++ b/benchmark/ms-queue/testcase.c
@@ -33,22 +33,23 @@ static void main_task(void *param)
int pid = *((int *)param);
if (pid % 3 == 0) {
output1 = 1;
- succ1 = dequeue(queue, &output1);
- if (succ1)
- printf("Thrd 2: Dequeue %d.\n", output1);
- else
- printf("Thrd 2: Dequeue NULL.\n");
+
+ enqueue(queue, 1);
+ printf("Thrd 1 Enqueue %d.\n", 1);
+ }
} else if (pid % 3 == 1) {
output2 = 2;
+ enqueue(queue, 2);
+ printf("Thrd 2 Enqueue %d.\n", 2);
+ } else if (pid %3 == 2) {
+ int input = 47;
+ enqueue(queue, 3);
+ printf("Thrd 3 Enqueue %d.\n", 3);
succ2 = dequeue(queue, &output2);
if (succ2)
printf("Thrd 3: Dequeue %d.\n", output2);
else
printf("Thrd 3: Dequeue NULL.\n");
- } else if (pid %3 == 2) {
- int input = 47;
- enqueue(queue, input);
- printf("Thrd 4 Enqueue %d.\n", input);
}
}
diff --git a/benchmark/ms-queue/testcase3.c b/benchmark/ms-queue/testcase3.c
new file mode 100644
index 0000000..8ab6dbf
--- /dev/null
+++ b/benchmark/ms-queue/testcase3.c
@@ -0,0 +1,96 @@
+#include <stdlib.h>
+#include <stdio.h>
+#include <threads.h>
+
+#include "my_queue.h"
+#include "model-assert.h"
+
+static int procs = 2;
+static queue_t *queue;
+static thrd_t *threads;
+static unsigned int *input;
+static unsigned int *output;
+static int num_threads;
+
+int get_thread_num()
+{
+ thrd_t curr = thrd_current();
+ int i;
+ for (i = 0; i < num_threads; i++)
+ if (curr.priv == threads[i].priv)
+ return i;
+ //MODEL_ASSERT(0);
+ return -1;
+}
+
+/** Be careful, we must make these variables to be global so that they will be
+ * 'available' when the execution is generated */
+bool succ1, succ2;
+unsigned int output1, output2;
+
+static void main_task(void *param)
+{
+ int pid = *((int *)param);
+ if (pid % 4 == 0) {
+ output1 = 1;
+ succ1 = dequeue(queue, &output1);
+ if (succ1)
+ printf("Thrd 1: Dequeue %d.\n", output1);
+ else
+ printf("Thrd 1: Dequeue NULL.\n");
+ } else if (pid % 4 == 1) {
+ enqueue(queue, 2);
+ output2 = 1;
+ succ2 = dequeue(queue, &output2);
+ if (succ2)
+ printf("Thrd 2: Dequeue %d.\n", output2);
+ else
+ printf("Thrd 2: Dequeue NULL.\n");
+ }
+}
+
+int user_main(int argc, char **argv)
+{
+ /**
+ @Begin
+ @Entry_point
+ @End
+ */
+ int i;
+ int *param;
+ unsigned int in_sum = 0, out_sum = 0;
+
+ queue = calloc(1, sizeof(*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++) {
+ param[i] = i;
+ thrd_create(&threads[i], main_task, ¶m[i]);
+ }
+ 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]);
+ //MODEL_ASSERT(in_sum == out_sum);
+ */
+
+ free(param);
+ free(threads);
+ free(queue);
+
+ return 0;
+}
diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
index 6df7c76..377d70a 100644
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
@@ -300,6 +300,7 @@ public class CodeGenerator {
new File(homeDir + "/benchmark/ms-queue/my_queue.c"),
new File(homeDir + "/benchmark/ms-queue/testcase1.c"),
new File(homeDir + "/benchmark/ms-queue/testcase2.c"),
+ new File(homeDir + "/benchmark/ms-queue/testcase3.c"),
new File(homeDir + "/benchmark/ms-queue/main.c"),
new File(homeDir + "/benchmark/ms-queue/my_queue.h") };
--
2.34.1