From: Peizhao Ou Date: Tue, 17 Nov 2015 06:46:29 +0000 (-0800) Subject: edits X-Git-Url: http://demsky.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=b568a7063faeb671240c8b3a169ea60cee01858e edits --- 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 +#include +#include + +#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") };