X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=benchmark%2Fms-queue%2Fmy_queue.c;h=b942be572b09d83aca4892ac11f2ba1588ee0342;hb=dddb190f43cd31d29dd0ce06739fc9cd22f25f73;hp=232e5d839347794a2056a5c0de5c7e17c6d50811;hpb=e551d9733ed4e29fe2928713c34ad3e58e424e95;p=cdsspec-compiler.git diff --git a/benchmark/ms-queue/my_queue.c b/benchmark/ms-queue/my_queue.c index 232e5d8..b942be5 100644 --- a/benchmark/ms-queue/my_queue.c +++ b/benchmark/ms-queue/my_queue.c @@ -10,7 +10,7 @@ #define acquire memory_order_acquire #define MAX_FREELIST 4 /* Each thread can own up to MAX_FREELIST free nodes */ -#define INITIAL_FREE 2 /* Each thread starts with INITIAL_FREE free nodes */ +#define INITIAL_FREE 3 /* Each thread starts with INITIAL_FREE free nodes */ #define POISON_IDX 0x666 @@ -22,14 +22,16 @@ static unsigned int new_node() int i; int t = get_thread_num(); for (i = 0; i < MAX_FREELIST; i++) { - unsigned int node = load_32(&free_lists[t][i]); + //unsigned int node = load_32(&free_lists[t][i]); + unsigned int node = free_lists[t][i]; if (node) { - store_32(&free_lists[t][i], 0); + //store_32(&free_lists[t][i], 0); + free_lists[t][i] = 0; return node; } } /* free_list is empty? */ - MODEL_ASSERT(0); + //MODEL_ASSERT(0); return 0; } @@ -40,25 +42,30 @@ static void reclaim(unsigned int node) int t = get_thread_num(); /* Don't reclaim NULL node */ - MODEL_ASSERT(node); + //MODEL_ASSERT(node); for (i = 0; i < MAX_FREELIST; i++) { /* Should never race with our own thread here */ - unsigned int idx = load_32(&free_lists[t][i]); + //unsigned int idx = load_32(&free_lists[t][i]); + unsigned int idx = free_lists[t][i]; /* Found empty spot in free list */ if (idx == 0) { store_32(&free_lists[t][i], node); + //free_lists[t][i] = node; return; } } /* free list is full? */ - MODEL_ASSERT(0); + //MODEL_ASSERT(0); } void init_queue(queue_t *q, int num_threads) { int i, j; + for (i = 0; i < MAX_NODES; i++) { + atomic_init(&q->nodes[i].next, MAKE_POINTER(POISON_IDX, 0)); + } /* Initialize each thread's free list with INITIAL_FREE pointers */ /* The actual nodes are initialized with poison indexes */ @@ -90,44 +97,68 @@ void enqueue(queue_t *q, unsigned int val) pointer tmp; node = new_node(); - store_32(&q->nodes[node].value, val); + //store_32(&q->nodes[node].value, val); + q->nodes[node].value = val; tmp = atomic_load_explicit(&q->nodes[node].next, relaxed); set_ptr(&tmp, 0); // NULL atomic_store_explicit(&q->nodes[node].next, tmp, relaxed); while (!success) { + + /** + @Begin + @Commit_point_clear: true + @Label: Enqueue_Clear + @End + */ + /**** UL & inadmissible ****/ tail = atomic_load_explicit(&q->tail, acquire); + /****FIXME: miss ****/ next = atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire); + //printf("miss1_enqueue\n"); if (tail == atomic_load_explicit(&q->tail, relaxed)) { /* Check for uninitialized 'next' */ - MODEL_ASSERT(get_ptr(next) != POISON_IDX); + //MODEL_ASSERT(get_ptr(next) != POISON_IDX); if (get_ptr(next) == 0) { // == NULL pointer value = MAKE_POINTER(node, get_count(next) + 1); + /**** 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, release); + &next, value, release, relaxed); /** @Begin - @Commit_point_define_check: success == true - @Label: Enqueue_Success_Point + @Commit_point_define_check: success + @Label: EnqueueUpdateNext @End */ } if (!success) { + // This routine helps the other enqueue to update the tail + /**** 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); - atomic_compare_exchange_strong_explicit(&q->tail, - &tail, value, release, release); + /**** SPEC (sequential, testcase2.c) ****/ + // Second release can be just relaxed + bool succ = false; + succ = atomic_compare_exchange_strong_explicit(&q->tail, + &tail, value, relaxed, relaxed); + if (succ) { + //printf("miss2_enqueue CAS succ\n"); + } + //printf("miss2_enqueue\n"); thrd_yield(); } } } - atomic_compare_exchange_strong_explicit(&q->tail, + /**** UL & Inadmissible ****/ + // Second release can be just relaxed + bool succ = atomic_compare_exchange_strong_explicit(&q->tail, &tail, MAKE_POINTER(node, get_count(tail) + 1), - release, release); + release, relaxed); } /** @@ -135,48 +166,86 @@ void enqueue(queue_t *q, unsigned int val) @Interface_define: Dequeue @End */ -unsigned int dequeue(queue_t *q) +bool dequeue(queue_t *q, int *retVal) { - unsigned int value; + unsigned int value = 0; int success = 0; pointer head; pointer tail; pointer next; while (!success) { + /** + @Begin + @Commit_point_clear: true + @Label: Dequeue_Clear + @End + */ + /**** Inadmissible ****/ head = atomic_load_explicit(&q->head, acquire); - tail = atomic_load_explicit(&q->tail, relaxed); + /** + @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!! + */ + /**** New bug ****/ + tail = atomic_load_explicit(&q->tail, acquire); + + /**** SPEC Error (testcase1.c) ****/ next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, acquire); + /** + @Begin + @Potential_commit_point_define: true + @Label: DequeueReadNext + @End + */ if (atomic_load_explicit(&q->head, relaxed) == head) { if (get_ptr(head) == get_ptr(tail)) { /* Check for uninitialized 'next' */ - MODEL_ASSERT(get_ptr(next) != POISON_IDX); - - if (get_ptr(next) == 0) { // NULL - /** - @Begin - @Commit_point_define_check: true - @Label: Dequeue_Empty_Point - @End - */ - return 0; // NULL + //MODEL_ASSERT(get_ptr(next) != POISON_IDX); + + if (get_ptr(next) == 0) { // NULL + return false; // NULL } - atomic_compare_exchange_strong_explicit(&q->tail, + /**** SPEC (sequential testcase3.c) ****/ + // Second release can be just relaxed + bool succ = false; + succ = atomic_compare_exchange_strong_explicit(&q->tail, &tail, MAKE_POINTER(get_ptr(next), get_count(tail) + 1), - release, release); + release, relaxed); + if (succ) { + //printf("miss4_dequeue CAS succ\n"); + } + //printf("miss4_dequeue\n"); thrd_yield(); } else { - value = load_32(&q->nodes[get_ptr(next)].value); + //value = load_32(&q->nodes[get_ptr(next)].value); + value = q->nodes[get_ptr(next)].value; + /**** inadmissibility ****/ success = atomic_compare_exchange_strong_explicit(&q->head, &head, MAKE_POINTER(get_ptr(next), get_count(head) + 1), - release, release); + release, relaxed); + /** + @Begin + @Commit_point_define_check: success + @Label: DequeueUpdateHead + @End + */ + /** @Begin - @Commit_point_define_check: success == true - @Label: Dequeue_Success_Point + @Commit_point_define: success + @Potential_commit_point_label: DequeueReadNext + @Label: DequeueReadNextVerify @End */ if (!success) @@ -185,5 +254,6 @@ unsigned int dequeue(queue_t *q) } } reclaim(get_ptr(head)); - return value; + *retVal = value; + return true; }