From 8ac7b8682c102a5c2661e7798c9a0f11cfcec4e3 Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Sun, 15 Nov 2015 21:26:28 -0800 Subject: [PATCH] edits --- benchmark/ms-queue/my_queue.c | 35 +++++++------------ benchmark/ms-queue/my_queue.h | 9 ++--- .../codeGenerator/CodeVariables.java | 20 +++++++---- 3 files changed, 30 insertions(+), 34 deletions(-) diff --git a/benchmark/ms-queue/my_queue.c b/benchmark/ms-queue/my_queue.c index 9cd2f8e..145c91d 100644 --- 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 2f18fbc..a09fb10 100644 --- 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 bcc6e41..7e4ab29 100644 --- 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)); -- 2.34.1