edits

diff --git a/benchmark/ms-queue/my_queue.c b/benchmark/ms-queue/my_queue.c
index 9cd2f8e9fea9bd87117cc6d9c00e4691caa662a8..145c91d30dcd8723ceb5da0c57918ee3a711d097 100644 (file)
--- a/benchmark/ms-queue/my_queue.c
+++ b/benchmark/ms-queue/my_queue.c
@@ -104,6 +104,7 @@ void enqueue(queue_t *q, unsigned int val)
        atomic_store_explicit(&q->nodes[node].next, tmp, relaxed);
 
        while (!success) {
+               
                /**
                        @Begin
                        @Commit_point_clear: true
@@ -129,7 +130,7 @@ void enqueue(queue_t *q, unsigned int val)
                                /**
                                        @Begin
                                        @Commit_point_define_check: success
-                                       @Label: Enqueue_Update_Next
+                                       @Label: EnqueueUpdateNext
                                        @End
                                */
                        }
@@ -158,13 +159,6 @@ void enqueue(queue_t *q, unsigned int val)
                        &tail,
                        MAKE_POINTER(node, get_count(tail) + 1),
                        release, relaxed);
-       /**
-               @Begin
-               @Commit_point_define_check: true
-               @Label: Enqueue_Update_Tail
-               @End
-       */
-
 }
 
 /**
@@ -189,30 +183,18 @@ bool dequeue(queue_t *q, int *retVal)
                */
                /**** detected correctness error ****/
                head = atomic_load_explicit(&q->head, acquire);
-               /**
-                       @Begin
-                       @Commit_point_define_check: true
-                       @Label: Dequeue_Read_Head
-                       @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!!
                 */
                tail = atomic_load_explicit(&q->tail, acquire);
-               /**
-                       @Begin
-                       @Potential_commit_point_define: true
-                       @Label: Dequeue_Potential_Read_Tail
-                       @End
-               */
 
                /**** Detected UL/DR (testcase1.c) ****/
                next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, acquire);
                /**
                        @Begin
                        @Potential_commit_point_define: true
-                       @Label: Dequeue_Potential_Read_Next
+                       @Label: DequeueReadNext
                        @End
                */
                if (atomic_load_explicit(&q->head, relaxed) == head) {
@@ -244,11 +226,18 @@ bool dequeue(queue_t *q, int *retVal)
                                                &head,
                                                MAKE_POINTER(get_ptr(next), get_count(head) + 1),
                                                release, relaxed);
+                               /**
+                                       @Begin
+                                       @Commit_point_define_check: success
+                                       @Label: DequeueUpdateHead
+                                       @End
+                               */
+
                                /**
                                        @Begin
                                        @Commit_point_define: success
-                                       @Potential_commit_point_label: Dequeue_Potential_Read_Next
-                                       @Label: Dequeue_Read_Next
+                                       @Potential_commit_point_label: DequeueReadNext
+                                       @Label: DequeueReadNextVerify
                                        @End
                                */
                                if (!success)

diff --git a/benchmark/ms-queue/my_queue.h b/benchmark/ms-queue/my_queue.h
index 2f18fbc09ff8e3ad971f7bc4d83027f03e88c493..a09fb10454292ee217a7f8e6cd6329bf87474642 100644 (file)
--- a/benchmark/ms-queue/my_queue.h
+++ b/benchmark/ms-queue/my_queue.h
@@ -85,8 +85,9 @@ void init_queue(queue_t *q, int num_threads);
                # Only check the happens-before relationship according to the id of the
                # commit_point_set. For commit_point_set that has same ID, A -> B means
                # B happens after the previous A.
-       @Commutativity: Enqueue <-> Dequeue: _Method2.__RET__ == NULL 
-       @Commutativity: Enqueue <-> Dequeue: _Method1.q != _Method2.q 
+       @Commutativity: Enqueue <-> Dequeue: true
+       @Commutativity: Enqueue <-> Enqueue: _Method1.q != _Method2.q
+       @Commutativity: Dequeue <-> Dequeue: _Method1.q != _Method2.q
        @End
 */
 
@@ -95,7 +96,7 @@ void init_queue(queue_t *q, int num_threads);
 /**
        @Begin
        @Interface: Enqueue
-       @Commit_point_set: Enqueue_Update_Next | Enqueue_Update_Tail
+       @Commit_point_set: EnqueueUpdateNext
        @ID: get_and_inc(tag)
        @Action:
                # __ID__ is an internal macro that refers to the id of the current
@@ -110,7 +111,7 @@ void enqueue(queue_t *q, unsigned int val);
 /**
        @Begin
        @Interface: Dequeue
-       @Commit_point_set: Dequeue_Read_Head | Dequeue_Read_Tail | Dequeue_Read_Next
+       @Commit_point_set: DequeueUpdateHead | DequeueReadNextVerify
        @ID: get_id(front(__queue))
        @Action:
                unsigned int _Old_Val = 0;

diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
index bcc6e418ca80a8eab903606a567160306d0b3ab5..7e4ab29c446c74db5683957664c197fe86600aa7 100644 (file)
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
@@ -671,6 +671,10 @@ public class CodeVariables {
                        newCode.add("\t"
                                        + ASSIGN_TO_PTR("rule", "interface_num_after",
                                                        interfaceNumAfter));
+                       newCode.add("\t"
+                                       + ASSIGN_TO_PTR("rule", "rule",
+                                                       "\"" + rule.condition + "\""));
+                       
                        newCode.add("\t"
                                        + ASSIGN_TO_PTR("rule", "condition", conditionFuncName));
 
@@ -989,13 +993,15 @@ public class CodeVariables {
                String structName = "cp_clear", anno = "annotation_cp_clear";
                newCode.add("\t\t"
                                + STRUCT_NEW_DECLARE_DEFINE(ANNO_CP_CLEAR, structName));
-               // String labelNum = Integer.toString(semantics.commitPointLabel2Num
-               // .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, "interface_num",
-               // interfaceNum));
+                
+               String labelNum = Integer.toString(semantics.commitPointLabel2Num
+                               .get(construct.label));
+               String labelName = construct.label;
+               newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "label_name",
+                               "\"" + labelName + "\""));
+               newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "label_num",
+                               labelNum));
+               
                newCode.add("\t\t" + STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno));
                newCode.add("\t\t"
                                + ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_CP_CLEAR));