From: Peizhao Ou Date: Tue, 13 Jan 2015 21:06:33 +0000 (-0800) Subject: changes to ms-queue spec X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=d37341bf7e15cffc4367435b89dc94736dbe72d1 changes to ms-queue spec --- diff --git a/benchmark/ms-queue/main.c b/benchmark/ms-queue/main.c index d3bc9c2..4a9f689 100644 --- a/benchmark/ms-queue/main.c +++ b/benchmark/ms-queue/main.c @@ -43,11 +43,21 @@ static void main_task(void *param) if (!pid) { input[0] = 17; enqueue(queue, input[0]); + printf("Enqueue %d.\n", 17); succ1 = dequeue(queue, &input[0]); + if (succ1) + printf("Dequeue %d.\n", input[0]); + else + printf("Dequeue NULL.\n"); } else { input[1] = 37; enqueue(queue, input[1]); + printf("Enqueue %d.\n", 37); succ2 = dequeue(queue, &output[1]); + if (succ2) + printf("Dequeue %d.\n", input[1]); + else + printf("Dequeue NULL.\n"); } } diff --git a/benchmark/ms-queue/my_queue.c b/benchmark/ms-queue/my_queue.c index c70adac..1d9e924 100644 --- a/benchmark/ms-queue/my_queue.c +++ b/benchmark/ms-queue/my_queue.c @@ -22,12 +22,10 @@ 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 = 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); - free_lists[t][i] = 0; + store_32(&free_lists[t][i], 0); //free_lists[t][i] = 0; return node; } @@ -48,14 +46,12 @@ static void reclaim(unsigned int 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 = 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; + store_32(&free_lists[t][i], node); //free_lists[t][i] = node; return; } @@ -98,18 +94,30 @@ void enqueue(queue_t *q, unsigned int val) pointer tmp; node = new_node(); - //store_32(&q->nodes[node].value, val); - 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) { - /**** detected UL (2 threads, 1 enqueue & 1 dequeue) ****/ + /** + @Begin + @Commit_point_clear: true + @Label: Enqueue_Clear + @End + */ + /**** detected UL ****/ tail = atomic_load_explicit(&q->tail, acquire); + /** + @Begin + @Commit_point_define_check: true + @Label: Enqueue_Read_Tail + @End + */ /****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' */ @@ -117,23 +125,25 @@ void enqueue(queue_t *q, unsigned int val) if (get_ptr(next) == 0) { // == NULL pointer value = MAKE_POINTER(node, get_count(next) + 1); - /**** correctness error (1 dequeue & 1 enqueue) ****/ + /**** detected UL ****/ + // Second release can be just relaxed success = atomic_compare_exchange_strong_explicit(&q->nodes[get_ptr(tail)].next, &next, value, release, relaxed); /** @Begin - @Commit_point_define_check: success == true - @Label: Enqueue_Success_Point + @Commit_point_define_check: success + @Label: Enqueue_UpdateNext @End */ } if (!success) { // This routine helps the other enqueue to update the tail - /**** detected UL (2 threads, 1 enqueue & 1 dequeue) ****/ + /**** detected UL ****/ unsigned int ptr = get_ptr(atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire)); pointer value = MAKE_POINTER(ptr, get_count(tail) + 1); /****FIXME: miss ****/ + // Second release can be just relaxed bool succ = false; succ = atomic_compare_exchange_strong_explicit(&q->tail, &tail, value, release, relaxed); @@ -145,11 +155,18 @@ void enqueue(queue_t *q, unsigned int val) } } } - /**** correctness error (1 dequeue & 1 enqueue) ****/ - atomic_compare_exchange_strong_explicit(&q->tail, + /**** dectected UL ****/ + // Second release can be just relaxed + bool succ = atomic_compare_exchange_strong_explicit(&q->tail, &tail, MAKE_POINTER(node, get_count(tail) + 1), release, relaxed); + /** + @Begin + @Commit_point_define_check: succ + @Label: Enqueue_UpdateOrLoad_Tail + @End + */ } /** @@ -157,7 +174,7 @@ void enqueue(queue_t *q, unsigned int val) @Interface_define: Dequeue @End */ -bool dequeue(queue_t *q, unsigned int *retVal) +bool dequeue(queue_t *q, int *output) { unsigned int value; int success = 0; @@ -166,15 +183,37 @@ bool dequeue(queue_t *q, unsigned int *retVal) pointer next; while (!success) { - /**** FIXME: miss ****/ + /** + @Begin + @Commit_point_clear: true + @Label: Dequeue_Clear + @End + */ + /**** detected correctness error ****/ head = atomic_load_explicit(&q->head, acquire); - // This must be acquire otherwise we have a bug with 1 enqueue & - // 1 dequeue - /**** correctness error (1 dequeue & 1 enqueue) ****/ - tail = atomic_load_explicit(&q->tail, acquire); - /**** correctness error (1 dequeue & 1 enqueue) ****/ + /** + @Begin + @Commit_point_define_check: true + @Label: Dequeue_Read_Head + @End + */ + tail = atomic_load_explicit(&q->tail, relaxed); + /** + @Begin + @Potential_commit_point_define: true + @Label: Dequeue_Potential_Read_Tail + @End + */ + + /****FIXME: miss ****/ next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, acquire); - //printf("miss3_dequeue\n"); + /** + @Begin + @Potential_commit_point_define: true + @Label: Dequeue_Potential_LoadNext + @End + */ + if (atomic_load_explicit(&q->head, relaxed) == head) { if (get_ptr(head) == get_ptr(tail)) { @@ -184,13 +223,15 @@ bool dequeue(queue_t *q, unsigned int *retVal) if (get_ptr(next) == 0) { // NULL /** @Begin - @Commit_point_define_check: true - @Label: Dequeue_Empty_Point + @Commit_point_define: true + @Potential_commit_point_label: Dequeue_Potential_Read_Tail + @Label: Dequeue_Read_Tail @End */ return false; // NULL } /****FIXME: miss (not reached) ****/ + // Second release can be just relaxed bool succ = false; succ = atomic_compare_exchange_strong_explicit(&q->tail, &tail, @@ -202,25 +243,26 @@ bool dequeue(queue_t *q, unsigned int *retVal) //printf("miss4_dequeue\n"); thrd_yield(); } else { - //*retVal = load_32(&q->nodes[get_ptr(next)].value); - *retVal = q->nodes[get_ptr(next)].value; + /** + @Begin + @Commit_point_define: true + @Potential_commit_point_label: Dequeue_Potential_LoadNext + @Label: Dequeue_LoadNext + @End + */ + value = load_32(&q->nodes[get_ptr(next)].value); //value = q->nodes[get_ptr(next)].value; - /**** FIXME: miss (not reached) ****/ + /****FIXME: correctness error ****/ success = atomic_compare_exchange_strong_explicit(&q->head, &head, MAKE_POINTER(get_ptr(next), get_count(head) + 1), release, relaxed); - /** - @Begin - @Commit_point_define_check: success == true - @Label: Dequeue_Success_Point - @End - */ if (!success) thrd_yield(); } } } reclaim(get_ptr(head)); + *output = value; return true; } diff --git a/benchmark/ms-queue/my_queue.h b/benchmark/ms-queue/my_queue.h index d6b2a69..714be4f 100644 --- a/benchmark/ms-queue/my_queue.h +++ b/benchmark/ms-queue/my_queue.h @@ -88,7 +88,7 @@ void init_queue(queue_t *q, int num_threads); /** @Begin @Interface: Enqueue - @Commit_point_set: Enqueue_Success_Point + @Commit_point_set: Enqueue_Read_Tail | Enqueue_UpdateNext | Enqueue_UpdateOrLoad_Tail @ID: get_and_inc(tag) @Action: # __ID__ is an internal macro that refers to the id of the current @@ -102,7 +102,7 @@ void enqueue(queue_t *q, unsigned int val); /** @Begin @Interface: Dequeue - @Commit_point_set: Dequeue_Success_Point | Dequeue_Empty_Point + @Commit_point_set: Dequeue_Read_Head | Dequeue_Read_Tail | Dequeue_LoadNext @ID: get_id(front(__queue)) @Action: unsigned int _Old_Val = 0; @@ -113,10 +113,10 @@ void enqueue(queue_t *q, unsigned int val); _Old_Val = 0; } @Post_check: - _Old_Val == 0 ? !__RET__ : _Old_Val == *retVal + __RET__ ? *output == _Old_Val : _Old_Val == 0 @End */ -bool dequeue(queue_t *q, unsigned int *retVal); +bool dequeue(queue_t *q, int *output); int get_thread_num(); #endif diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java index 43e4e76..0ee2ee0 100644 --- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java @@ -597,6 +597,7 @@ public class CodeVariables { newCode.add("\t" + ASSIGN_TO_PTR(structName, "interface_num", interfaceNum) + SHORT_COMMENT(construct.name)); + newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "interface_name", "\"" + construct.name + "\"")); String anno = "annotation_interface_begin"; newCode.add("\t" + STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno)); @@ -765,6 +766,7 @@ public class CodeVariables { String labelNum = Integer.toString(semantics.commitPointLabel2Num .get(construct.label)); newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "label_num", labelNum)); + newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "label_name", "\"" + construct.label + "\"")); newCode.add("\t\t" + STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno)); newCode.add("\t\t" + ASSIGN_TO_PTR(anno, "type", @@ -816,6 +818,7 @@ public class CodeVariables { .get(construct.label)); String interfaceNum = getCPInterfaceNum(semantics, construct.label); newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "label_num", labelNum)); + newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "label_name", "\"" + construct.label + "\"")); newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "interface_num", interfaceNum)); newCode.add("\t\t" + STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno)); newCode.add("\t\t" @@ -898,9 +901,11 @@ public class CodeVariables { .toString(semantics.commitPointLabel2Num .get(construct.potentialCPLabel)); newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "label_num", labelNum)); + newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "label_name", "\"" + construct.label + "\"")); newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "potential_cp_label_num", potentialLabelNum)); + newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "potential_label_name", "\"" + construct.potentialCPLabel + "\"")); newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "interface_num", interfaceNum)); newCode.add("\t\t" + STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno)); newCode.add("\t\t"