additional_ordering_point for ms-queue

diff --git a/benchmark/ms-queue/my_queue.c b/benchmark/ms-queue/my_queue.c
index f59d77736a13ec6b4d343772a6a0117c921123bf..6d86c4acc21076ad3e78fbfd67a6d18288552647 100644 (file)
--- a/benchmark/ms-queue/my_queue.c
+++ b/benchmark/ms-queue/my_queue.c
@@ -164,6 +164,13 @@ void enqueue(queue_t *q, unsigned int val)
                        &tail,
                        MAKE_POINTER(node, get_count(tail) + 1),
                        release, relaxed);
+       /**
+               @Begin
+               @Additional_ordering_point_define_check: true
+               @Label: Enqueue_Additional_Tail_LoadOrCAS
+               @End
+       */
+
 }
 
 /**
@@ -198,7 +205,7 @@ bool dequeue(queue_t *q, int *retVal)
                 * relaxed (it introduces a bug when there's two dequeuers and one
                 * enqueuer)
                 */
-               tail = atomic_load_explicit(&q->tail, relaxed);
+               tail = atomic_load_explicit(&q->tail, acquire);
                /**
                        @Begin
                        @Potential_commit_point_define: true

diff --git a/benchmark/ms-queue/my_queue.h b/benchmark/ms-queue/my_queue.h
index 0768428df5d9fadc1a1b29195b3de2c94068e87b..6618a52c4d9651b85e14274f5ba450849eb02fd6 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_Read_Tail | Enqueue_UpdateNext
+       @Commit_point_set: Enqueue_Read_Tail | Enqueue_UpdateNext | Enqueue_Additional_Tail_LoadOrCAS
        @ID: get_and_inc(tag)
        @Action:
                # __ID__ is an internal macro that refers to the id of the current

diff --git a/grammer/spec_compiler.jj b/grammer/spec_compiler.jj
index 43faebf46a2222051b09295db1b19fbc44f3baed..575dcf32b569fcf2aec4b24a1ebea85031760497 100644 (file)
--- a/grammer/spec_compiler.jj
+++ b/grammer/spec_compiler.jj
@@ -50,19 +50,46 @@
        @Begin
        @Potential_commit_point_define: ...
        @Label: ...
+       @End
+
+               OR
+
+       @Begin
+       @Potential_additional_ordering_point_define: ...
+       @Label: ...
        @End
 
        d) Commit point define construct
        @Begin
        @Commit_point_define_check: ...
        @Label: ...
+       @End
+
+               OR
+       
+       # Addition ordering point is used to order operations when there are "equal"
+       # commit point operations on the same location and that we cannot decide
+       # which operation goes first, we will use additional ordering point to order
+       # them (it's just similar to commit points). In implementation, we can just
+       # treat them as commit points with a special flag.
+
+       @Begin
+       @Additional_ordering_point_define: ...
+       @Potential_additional_ordering_point_label: ...
+       @Label: ...
        @End
        
                OR
+       
+       @Begin
+       @Additional_ordering_point_define: ...
+       @Label: ...
+       @End
+
+               OR
 
        @Begin
-       @Commit_point_define: ...
-       @Potential_commit_point_label: ...
+       @Additional_ordering_point_define_check: ...
        @Label: ...
        @End
 
@@ -375,16 +402,24 @@ SKIP : {
        <POST_CHECK: "@Post_check:">
 |
        <POTENTIAL_COMMIT_POINT_DEFINE: "@Potential_commit_point_define:">
+|
+       <POTENTIAL_ADDITIONAL_ORDERING_POINT_DEFINE: "@Potential_additional_ordering_point_define:">
 |
        <LABEL: "@Label:">
 |
        <COMMIT_POINT_DEFINE_CHECK: "@Commit_point_define_check:">
+|
+       <ADDITIONAL_ORDERING_POINT_DEFINE_CHECK: "@Additional_ordering_point_define_check:">
 |
        <COMMIT_POINT_DEFINE: "@Commit_point_define:">
+|
+       <ADDITIONAL_ORDERING_POINT_DEFINE: "@Additional_ordering_point_define:">
 |
        <COMMIT_POINT_CLEAR: "@Commit_point_clear:">
 |
        <POTENTIAL_COMMIT_POINT_LABEL: "@Potential_commit_point_label:">
+|
+       <POTENTIAL_ADDITIONAL_ORDERING_POINT_LABEL: "@Potential_additional_ordering_point_label:">
 }
 
 
@@ -895,6 +930,9 @@ Construct ParseSpec() :
        LOOKAHEAD(2) res = Potential_commit_point_define() |
        LOOKAHEAD(2) res = Commit_point_define() |
        LOOKAHEAD(2) res = Commit_point_define_check() |
+       LOOKAHEAD(2) res = Potential_additional_ordering_point_define() |
+       LOOKAHEAD(2) res = Additional_ordering_point_define() |
+       LOOKAHEAD(2) res = Additional_ordering_point_define_check() |
        LOOKAHEAD(2) res = Commit_point_clear() |
        LOOKAHEAD(2) res = Entry_point() |
        LOOKAHEAD(2) res = Class_begin() |
@@ -1110,6 +1148,26 @@ PotentialCPDefineConstruct Potential_commit_point_define() :
        }
 }
 
+PotentialCPDefineConstruct Potential_additional_ordering_point_define() :
+{
+       PotentialCPDefineConstruct res;
+       String label, condition;
+       ArrayList<String> content;
+}
+{
+
+       { res = null; }
+               <BEGIN>
+                       <POTENTIAL_ADDITIONAL_ORDERING_POINT_DEFINE> (content = C_CPP_CODE(null) { condition = stringArray2String(content); })
+                       <LABEL> (label = <IDENTIFIER>.image)
+               <END>
+       {
+               // Set the boolean flag isAdditionalOrderingPoint to be true
+               res = new PotentialCPDefineConstruct(_file, _content.size(), true, label, condition); 
+               return res;
+       }
+}
+
 
 CPDefineConstruct Commit_point_define() :
 {
@@ -1126,7 +1184,28 @@ CPDefineConstruct Commit_point_define() :
                        <LABEL> (label = <IDENTIFIER>.image)
                <END>
        {
-               res = new CPDefineConstruct(_file, _content.size(), label, potentialCPLabel, condition);
+               res = new CPDefineConstruct(_file, _content.size(), false, label, potentialCPLabel, condition);
+               return res;
+       }
+}
+
+CPDefineConstruct Additional_ordering_point_define() :
+{
+       CPDefineConstruct res;
+       String label, potentialCPLabel, condition;
+       ArrayList<String> content;
+}
+{
+
+       { res = null; }
+               <BEGIN>
+                       <ADDITIONAL_ORDERING_POINT_DEFINE> (content = C_CPP_CODE(null) { condition = stringArray2String(content); })
+                       <POTENTIAL_ADDITIONAL_ORDERING_POINT_LABEL> (potentialCPLabel = <IDENTIFIER>.image)
+                       <LABEL> (label = <IDENTIFIER>.image)
+               <END>
+       {
+               // Set the boolean flag isAdditionalOrderingPoint to be true
+               res = new CPDefineConstruct(_file, _content.size(), true, label, potentialCPLabel, condition);
                return res;
        }
 }
@@ -1165,7 +1244,27 @@ CPDefineCheckConstruct Commit_point_define_check() :
                        <LABEL> (label = <IDENTIFIER>.image)
                <END>
        {
-               res = new CPDefineCheckConstruct(_file, _content.size(), label, condition);
+               res = new CPDefineCheckConstruct(_file, _content.size(), false, label, condition);
+               return res;
+       }
+}
+
+CPDefineCheckConstruct Additional_ordering_point_define_check() :
+{
+       CPDefineCheckConstruct res;     
+       String label, condition;
+       ArrayList<String> content;
+}
+{
+
+       { res = null; }
+               <BEGIN> 
+                       <ADDITIONAL_ORDERING_POINT_DEFINE_CHECK> (content = C_CPP_CODE(null) { condition = stringArray2String(content); })
+                       <LABEL> (label = <IDENTIFIER>.image)
+               <END>
+       {
+               // Set the boolean flag isAdditionalOrderingPoint to be true
+               res = new CPDefineCheckConstruct(_file, _content.size(), true, label, condition);
                return res;
        }
 }

diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
index 0ee2ee0c9e7c13eee1261db84ae7f1ca92108658..cdc8771fdf5ed5cdbb15663e28d54025353d3dba 100644 (file)
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
@@ -767,6 +767,11 @@ public class CodeVariables {
                                .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 + "\""));
+               if (construct.isAdditionalOrderingPoint) {
+                       newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "is_additional_point", "true"));
+               } else {
+                       newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "is_additional_point", "false"));
+               }
                newCode.add("\t\t" + STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno));
                newCode.add("\t\t"
                                + ASSIGN_TO_PTR(anno, "type",
@@ -820,6 +825,11 @@ public class CodeVariables {
                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));
+               if (construct.isAdditionalOrderingPoint) {
+                       newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "is_additional_point", "true"));
+               } else {
+                       newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "is_additional_point", "false"));
+               }
                newCode.add("\t\t" + STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno));
                newCode.add("\t\t"
                                + ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_CP_DEFINE_CHECK));
@@ -907,6 +917,11 @@ public class CodeVariables {
                                                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));
+               if (construct.isAdditionalOrderingPoint) {
+                       newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "is_additional_point", "true"));
+               } else {
+                       newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "is_additional_point", "false"));
+               }
                newCode.add("\t\t" + STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno));
                newCode.add("\t\t"
                                + ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_CP_DEFINE));

diff --git a/src/edu/uci/eecs/specCompiler/specExtraction/CPDefineCheckConstruct.java b/src/edu/uci/eecs/specCompiler/specExtraction/CPDefineCheckConstruct.java
index 680e48caf4b589a5c38bb590ebf29f7fcaa46fdd..a9ccb75f16e6b8ab6f114c167c52964036e2027f 100644 (file)
--- a/src/edu/uci/eecs/specCompiler/specExtraction/CPDefineCheckConstruct.java
+++ b/src/edu/uci/eecs/specCompiler/specExtraction/CPDefineCheckConstruct.java
@@ -3,19 +3,30 @@ package edu.uci.eecs.specCompiler.specExtraction;
 import java.io.File;
 
 public class CPDefineCheckConstruct extends Construct {
+       public final boolean isAdditionalOrderingPoint;
+
        public final String label;
        public final String condition;
 
        public CPDefineCheckConstruct(File file, int beginLineNum, String label,
                        String condition) {
                super(file, beginLineNum);
+               this.isAdditionalOrderingPoint = false;
+               this.label = label;
+               this.condition = condition;
+       }
+
+       public CPDefineCheckConstruct(File file, int beginLineNum,
+                       boolean isAdditionalOrderingPoint, String label, String condition) {
+               super(file, beginLineNum);
+               this.isAdditionalOrderingPoint = isAdditionalOrderingPoint;
                this.label = label;
                this.condition = condition;
        }
 
        public String toString() {
                StringBuffer res = new StringBuffer();
-               res.append("@Commit_point_clear:\n");
+               res.append("@Commit_point_define_check:\n");
                res.append("Label: " + label + "\n");
                res.append("Condition: " + condition + "\n");
                return res.toString();

diff --git a/src/edu/uci/eecs/specCompiler/specExtraction/CPDefineConstruct.java b/src/edu/uci/eecs/specCompiler/specExtraction/CPDefineConstruct.java
index 8c31a9b7a691ecf9c649d12724adf056d97b92b6..b92bd065002eb4ced18a3b3443364d47ecc86f78 100644 (file)
--- a/src/edu/uci/eecs/specCompiler/specExtraction/CPDefineConstruct.java
+++ b/src/edu/uci/eecs/specCompiler/specExtraction/CPDefineConstruct.java
@@ -3,6 +3,7 @@ package edu.uci.eecs.specCompiler.specExtraction;
 import java.io.File;
 
 public class CPDefineConstruct extends Construct {
+       public final boolean isAdditionalOrderingPoint;
        public final String label;
        public final String potentialCPLabel;
        public final String condition;
@@ -10,6 +11,17 @@ public class CPDefineConstruct extends Construct {
        public CPDefineConstruct(File file, int beginLineNum, String label,
                        String potentialCPLabel, String condition) {
                super(file, beginLineNum);
+               this.isAdditionalOrderingPoint = false;
+               this.label = label;
+               this.potentialCPLabel = potentialCPLabel;
+               this.condition = condition;
+       }
+
+       public CPDefineConstruct(File file, int beginLineNum,
+                       boolean isAdditionalOrderingPoint, String label,
+                       String potentialCPLabel, String condition) {
+               super(file, beginLineNum);
+               this.isAdditionalOrderingPoint = isAdditionalOrderingPoint;
                this.label = label;
                this.potentialCPLabel = potentialCPLabel;
                this.condition = condition;

diff --git a/src/edu/uci/eecs/specCompiler/specExtraction/PotentialCPDefineConstruct.java b/src/edu/uci/eecs/specCompiler/specExtraction/PotentialCPDefineConstruct.java
index f0eb403c863ea7843d99e76e8871b9bd8d343935..f8499cdae00e5ced1c01f02d1d89b577db35c852 100644 (file)
--- a/src/edu/uci/eecs/specCompiler/specExtraction/PotentialCPDefineConstruct.java
+++ b/src/edu/uci/eecs/specCompiler/specExtraction/PotentialCPDefineConstruct.java
@@ -3,12 +3,23 @@ package edu.uci.eecs.specCompiler.specExtraction;
 import java.io.File;
 
 public class PotentialCPDefineConstruct extends Construct {
+       public final boolean isAdditionalOrderingPoint;
+
        public final String label;
        public final String condition;
 
        public PotentialCPDefineConstruct(File file, int beginLineNum,
                        String label, String condition) {
                super(file, beginLineNum);
+               this.isAdditionalOrderingPoint = false;
+               this.label = label;
+               this.condition = condition;
+       }
+
+       public PotentialCPDefineConstruct(File file, int beginLineNum,
+                       boolean isAdditionalOrderingPoint, String label, String condition) {
+               super(file, beginLineNum);
+               this.isAdditionalOrderingPoint = isAdditionalOrderingPoint;
                this.label = label;
                this.condition = condition;
        }