changes

diff --git a/benchmark/chase-lev-deque-bugfix/deque.c b/benchmark/chase-lev-deque-bugfix/deque.c
index c9fc8a9327f5d2a20fe623ba796527fe6cd52f81..4dcb9bbd156fe3581452fbec1dd6ff3291ef8463 100644 (file)
--- a/benchmark/chase-lev-deque-bugfix/deque.c
+++ b/benchmark/chase-lev-deque-bugfix/deque.c
@@ -99,20 +99,32 @@ void push(Deque *q, int x) {
                resize(q);
                //Bug in paper...should have next line...
                a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
+               /**
+                       @Begin
+                       @Commit_point_define_check: true
+                       @Label: Push_Read_Array
+                       @End
+               */
        }
        int size = atomic_load_explicit(&a->size, memory_order_relaxed);
+
        atomic_store_explicit(&a->buffer[b % size], x, memory_order_relaxed);
        /**
                @Begin
                @Commit_point_define_check: true
-               @Label: Push_Point
+               @Label: Push_Update_Buffer
                @End
        */
        /**** correctness error ****/
        atomic_thread_fence(memory_order_release);
        
        atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
-       
+       /**
+               @Begin
+               @Commit_point_define_check: true
+               @Label: Push_Update_Bottom
+               @End
+       */
 }
 
 /**

diff --git a/benchmark/chase-lev-deque-bugfix/deque.h b/benchmark/chase-lev-deque-bugfix/deque.h
index 8a3e857a4de8b47c4133884625921c0658859f04..da81cfa13cf76d998a508b3e7bbc01b0b3dff899 100644 (file)
--- a/benchmark/chase-lev-deque-bugfix/deque.h
+++ b/benchmark/chase-lev-deque-bugfix/deque.h
@@ -91,7 +91,7 @@ int take(Deque *q);
 /**
     @Begin
     @Interface: Push 
-    @Commit_point_set: Push_Point
+    @Commit_point_set: Push_Read_Array | Push_Update_Buffer | Push_Update_Bottom
     @ID: get_and_inc(tag);
     @Action:
         tag_elem_t *elem = new_tag_elem(__ID__, x);

diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
index dfa597610122cfcb12ac08de69c8d39873a7ed10..7386052cdd3f44c293b140df41852cf2eb45cb2c 100644 (file)
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
@@ -321,11 +321,11 @@ public class CodeGenerator {
                File[] srcMPMCQueue = {
                                new File(homeDir + "/benchmark/mpmc-queue/mpmc-queue.h"),
                                new File(homeDir + "/benchmark/mpmc-queue/mpmc-queue.cc") };
+//
+//             File[][] sources = { srcLinuxRWLocks,  srcMSQueue, srcRCU,
+//                             srcDeque, srcMCSLock, srcSPSCQueue, srcMPMCQueue, srcHashtable };
 
-               File[][] sources = { srcLinuxRWLocks,  srcMSQueue, srcRCU,
-                               srcDeque, srcMCSLock, srcSPSCQueue, srcMPMCQueue, srcHashtable };
-
-//              File[][] sources = { srcHashtable, srcMPMCQueue };
+                File[][] sources = {srcMSQueue };
                // Compile all the benchmarks
                for (int i = 0; i < sources.length; i++) {
                        CodeGenerator gen = new CodeGenerator(sources[i]);

diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
index 12d0383e7965ce81e88038ad7dd9cffae5c13c09..43e4e76dcd0307f01e91c7768b6015c9007be405 100644 (file)
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
@@ -854,11 +854,11 @@ 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 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));
                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));