From: Peizhao Ou <peizhaoo@uci.edu>
Date: Thu, 15 Jan 2015 21:29:39 +0000 (-0800)
Subject: additional_ordering_point for ms-queue
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=a0721aba5feb313cce48120d4e98e0165bb476bc

additional_ordering_point for ms-queue
---

diff --git a/benchmark/ms-queue/my_queue.c b/benchmark/ms-queue/my_queue.c
index f59d777..6d86c4a 100644
--- 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 0768428..6618a52 100644
--- 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 43faebf..575dcf3 100644
--- 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 0ee2ee0..cdc8771 100644
--- 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 680e48c..a9ccb75 100644
--- 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 8c31a9b..b92bd06 100644
--- 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 f0eb403..f8499cd 100644
--- 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;
 	}