changes to ms-queue spec

diff --git a/benchmark/ms-queue/main.c b/benchmark/ms-queue/main.c
index d3bc9c238b1d7734281bfa1b641e16bf6cd662e1..4a9f689d7e766daaa81c5b1416a52b59b836e528 100644 (file)
--- 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 c70adacaf33a7e4deb7d6dfab728edd90708d886..1d9e924538d16bd9dc192846b1785b38d7811907 100644 (file)
--- 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 d6b2a695d6789a9b732bfd75eac564842bf3ecd6..714be4f83d71daeb98b68a9f1681fd3076d5a39d 100644 (file)
--- 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 43e4e76dcd0307f01e91c7768b6015c9007be405..0ee2ee0c9e7c13eee1261db84ae7f1ca92108658 100644 (file)
--- 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"