--- /dev/null
+/* spec-compiler.jj Grammer definition for the specification */
+
+
+/*
+ SPEC constructs:
+ Each construct should be embraced by /DOUBLE_STAR ... STAR/ annotation.
+ Within there, any line beginning with a "#" is a comment of the annotation.
+ Each constrcut should begin with @Begin and end with @End. Otherwise, the
+ annotation would be considered as normal comments of the source.
+
+ a) Global construct
+ @Begin
+ @Options:
+ # If LANG is not define, it's C++ by default. C does not support class
+ # and template, so if it's defined as C, we should also have a explicit
+ # entry point.
+ LANG = C;
+ @Global_define:
+ @DeclareVar:
+ @InitVar:
+ @DefineFunc:
+ ...
+ @Interface_cluster:
+ ...
+ @Happens-before:
+ ...
+ @End
+
+ b) Interface construct
+ @Begin
+ @Interface: ...
+ @Commit_point_set:
+ IDENTIFIER | IDENTIFIER ...
+ @Condition: ... (Optional)
+ @HB_Condition:
+ IDENTIFIER :: <C_CPP_Condition>
+ @HB_Condition: ...
+ @ID: ... (Optional, use default ID)
+ @Check: (Optional)
+ ...
+ @Action: (Optional)
+ # Type here must be a pointer
+ @DefineVar: Type var1 = SomeExpression (Optional)
+ @Code (Optional)
+ ...
+ @Post_action: (Optional)
+ @Post_check: (Optional)
+ @End
+
+ c) Potential commit construct
+ @Begin
+ @Potential_commit_point_define: ...
+ @Label: ...
+ @End
+
+ d) Commit point define construct
+ @Begin
+ @Commit_point_define_check: ...
+ @Label: ...
+ @End
+
+ OR
+
+ @Begin
+ @Commit_point_define: ...
+ @Potential_commit_point_label: ...
+ @Label: ...
+ @End
+
+ e) Entry point construct
+ @Begin
+ @Entry_point
+ @End
+
+ f) Interface define construct
+ @Begin
+ @Interface_define: <Interface_Name>
+ @End
+*/
+
+
+
+options {
+ STATIC = false;
+ JAVA_UNICODE_ESCAPE = true;
+}
+
+PARSER_BEGIN(SpecParser)
+package edu.uci.eecs.specCompiler.grammerParser;
+
+import java.io.FileInputStream;
+import java.io.FileNotFoundException;
+import java.io.InputStream;
+import java.io.ByteArrayInputStream;
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.HashSet;
+
+import edu.uci.eecs.specCompiler.specExtraction.Construct;
+import edu.uci.eecs.specCompiler.specExtraction.GlobalConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.InterfaceConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.PotentialCPDefineConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.CPDefineConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface;
+import edu.uci.eecs.specCompiler.specExtraction.ActionSubConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.ActionSubConstruct.DefineVar;
+import edu.uci.eecs.specCompiler.specExtraction.SequentialDefineSubConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.InterfaceDefineConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.EntryPointConstruct;
+
+ public class SpecParser {
+ public static void main(String[] argvs)
+ throws ParseException, TokenMgrError {
+ try {
+ FileInputStream fis = new FileInputStream("./grammer/spec.txt");
+ SpecParser parser = new SpecParser(fis);
+ //parser.Parse();
+ System.out.println("Parsing finished!");
+ ArrayList<String> typeParams = parser.FormalParamList();
+ } catch (FileNotFoundException e) {
+ e.printStackTrace();
+ }
+ }
+
+ public static Construct parseSpec(String text)
+ throws ParseException, TokenMgrError {
+ InputStream input = new ByteArrayInputStream(text.getBytes());
+ SpecParser parser = new SpecParser(input);
+ return parser.Parse();
+ }
+
+
+ }
+PARSER_END(SpecParser)
+
+ "/*"}
+
+< IN_COMMENT > SKIP : { < ~[] > }
+
+< IN_COMMENT > SKIP : {
+ "*/": DEFAULT
+}
+
+<IN_COMMENT> TOKEN : {
+ <A: "@A"> |
+ <B: "@B">
+}
+
+SKIP :
+{
+ " "
+|
+ "\n"
+|
+ "\r"
+|
+ "\r\n"
+|
+ "\t"
+|
+ // "#" comment for the specification
+ <"#" (~["\n", "\r"])* (["\n", "\r"])>
+|
+ // "//" comment for the specification
+ <"//" (~["\n", "\r"])* (["\n", "\r"])>
+}
+
+<IN_COMMENT, DEFAULT> TOKEN :
+{
+/* Above are specification-only tokens */
+ <HEAD: "/**" : IN_COMMENT>
+|
+ <TAIL: "*/" : DEFAULT>
+|
+ <BEGIN: "@Begin">
+|
+ <END: "@End">
+|
+ <OPTIONS: "@Options:">
+|
+ <GLOBAL_DEFINE: "@Global_define:">
+|
+ <DECLARE_VAR: "@DeclareVar:">
+|
+ <INIT_VAR: "@InitVar:">
+|
+ <DEFINE_FUNC: "@DefineFunc:">
+|
+ <INTERFACE_CLUSTER: "@Interface_cluster:">
+|
+ <HAPPENS_BEFORE: "@Happens_before:">
+|
+ <INTERFACE: "@Interface:">
+|
+ <COMMIT_POINT_SET: "@Commit_point_set:">
+|
+ <ENTRY_POINT: "@Entry_point">
+|
+ <INTERFACE_DEFINE: "@Interface_define:">
+|
+ <CONDITION: "@Condition:">
+|
+ <HB_CONDITION: "@HB_condition:">
+|
+ <ID: "@ID:">
+|
+ <CHECK: "@Check:">
+|
+ <ACTION: "@Action:">
+|
+ <DEFINEVAR: "@DefineVar:">
+|
+ <CODE: "@Code:">
+|
+ <POST_ACTION: "@Post_action:">
+|
+ <POST_CHECK: "@Post_check:">
+|
+ <POTENTIAL_COMMIT_POINT_DEFINE: "@Potential_commit_point_define:">
+|
+ <LABEL: "@Label:">
+|
+ <COMMIT_POINT_DEFINE_CHECK: "@Commit_point_define_check:">
+|
+ <COMMIT_POINT_DEFINE: "@Commit_point_define:">
+|
+ <POTENTIAL_COMMIT_POINT_LABEL: "@Potential_commit_point_label:">
+
+
+/* Specification & C/C++ shared tokens */
+
+// Reserved keywords
+|
+ <CONST: "const">
+|
+ <STRUCT: "struct">
+|
+ <TYPENAME: "typename">
+
+
+|
+ <#DIGIT: ["0"-"9"]>
+|
+ <#LETTER: ["a"-"z", "A"-"Z"]>
+|
+ <IDENTIFIER: (<LETTER> | "_") (<LETTER> | <DIGIT> | "_")*>
+|
+ <EQUALS: "=">
+|
+ <OPEN_PAREN: "{">
+|
+ <CLOSE_PAREN: "}">
+|
+ <OPEN_BRACKET: "(">
+|
+ <CLOSE_BRACKET: ")">
+|
+ <HB_SYMBOL: "->">
+|
+ <COMMA: ",">
+
+|
+/* C/C++ only token*/
+ <DOT: ".">
+|
+ <STAR: "*">
+|
+ <NEGATE: "~">
+|
+ <EXCLAMATION: "!">
+|
+ <AND: "&">
+|
+ <OR: "|">
+|
+ <MOD: "%">
+|
+ <PLUS: "+">
+|
+ <PLUSPLUS: "++">
+|
+ <MINUS: "-">
+|
+ <MINUSMINUS: "--">
+|
+ <DIVIDE: "/">
+|
+ <BACKSLASH: "\\">
+|
+ <LESS_THAN: "<">
+|
+ <GREATER_THAN: ">">
+|
+ <GREATER_EQUALS: ">=">
+|
+ <LESS_EQUALS: "<=">
+|
+ <LOGICAL_EQUALS: "==">
+|
+ <NOT_EQUALS: "!=">
+|
+ <LOGICAL_AND: "&&">
+|
+ <LOGICAL_OR: "||">
+|
+ <XOR: "^">
+|
+ <QUESTION_MARK: "?">
+|
+ <COLON: ":">
+|
+ <DOUBLECOLON: "::">
+|
+ <SEMI_COLON: ";">
+|
+ <STRING_LITERAL:
+ "\""
+ ((~["\"","\\","\n","\r"])
+ | ("\\"
+ ( ["n","t","b","r","f","\\","'","\""]
+ | ["0"-"7"] ( ["0"-"7"] )?
+ | ["0"-"3"] ["0"-"7"]
+ ["0"-"7"]
+ )
+ )
+ )*
+ "\"">
+|
+ <CHARACTER_LITERAL:
+ "'"
+ ((~["'","\\","\n","\r"])
+ | ("\\"
+ (["n","t","b","r","f","\\","'","\""]
+ | ["0"-"7"] ( ["0"-"7"] )?
+ | ["0"-"3"] ["0"-"7"]
+ ["0"-"7"]
+ )
+ )
+ )
+ "'">
+|
+ < INTEGER_LITERAL:
+ <DECIMAL_LITERAL> (["l","L"])?
+ | <HEX_LITERAL> (["l","L"])?
+ | <OCTAL_LITERAL> (["l","L"])?>
+|
+ < #DECIMAL_LITERAL: ["1"-"9"] (["0"-"9"])* >
+|
+ < #HEX_LITERAL: "0" ["x","X"] (["0"-"9","a"-"f","A"-"F"])+ >
+|
+ < #OCTAL_LITERAL: "0" (["0"-"7"])* >
+|
+ < FLOATING_POINT_LITERAL:
+ <DECIMAL_FLOATING_POINT_LITERAL>
+ | <HEXADECIMAL_FLOATING_POINT_LITERAL> >
+|
+ < #DECIMAL_FLOATING_POINT_LITERAL:
+ (["0"-"9"])+ "." (["0"-"9"])* (<DECIMAL_EXPONENT>)? (["f","F","d","D"])?
+ | "." (["0"-"9"])+ (<DECIMAL_EXPONENT>)? (["f","F","d","D"])?
+ | (["0"-"9"])+ <DECIMAL_EXPONENT> (["f","F","d","D"])?
+ | (["0"-"9"])+ (<DECIMAL_EXPONENT>)? ["f","F","d","D"]>
+|
+ < #DECIMAL_EXPONENT: ["e","E"] (["+","-"])? (["0"-"9"])+ >
+|
+ < #HEXADECIMAL_FLOATING_POINT_LITERAL:
+ "0" ["x", "X"] (["0"-"9","a"-"f","A"-"F"])+ (".")? <HEXADECIMAL_EXPONENT> (["f","F","d","D"])?
+ | "0" ["x", "X"] (["0"-"9","a"-"f","A"-"F"])* "." (["0"-"9","a"-"f","A"-"F"])+ <HEXADECIMAL_EXPONENT> (["f","F","d","D"])?>
+|
+ < #HEXADECIMAL_EXPONENT: ["p","P"] (["+","-"])? (["0"-"9"])+ >
+}
+
+String Type() :
+{
+ String type;
+ String str;
+}
+{
+ { type = ""; }
+ ("const"
+ { type = "const"; }
+ )?
+ (("struct" { type = type + " struct"; })?
+ (str = <IDENTIFIER>.image {
+ if (!type.equals(""))
+ type = type + " " + str;
+ else
+ type = str;
+ }))
+ ((str = "const".image {
+ if (!type.equals(""))
+ type = type + " " + str;
+ else
+ type = str;
+ }) |
+ (str = <STAR>.image {
+ if (!type.equals(""))
+ type = type + " " + str;
+ else
+ type = str;
+ }) |
+ (str = <AND>.image {
+ if (!type.equals(""))
+ type = type + " " + str;
+ else
+ type = str;
+ })
+ )*
+ {
+ return type;
+ }
+}
+
+ArrayList<String> FormalParamList() :
+{
+ ArrayList<String> typeParams;
+}
+{
+ {
+ typeParams = new ArrayList<String>();
+ }
+ (TypeParam(typeParams) (<COMMA> TypeParam(typeParams))*)?
+ {
+ System.out.println(typeParams);
+ return typeParams;
+ }
+}
+
+void TypeParam(ArrayList<String> typeParams) :
+{
+ String type, param;
+}
+{
+ (type = Type()) (param = <IDENTIFIER>.image)
+ {
+ typeParams.add(type);
+ typeParams.add(param);
+ }
+}
+
+Construct Parse() :
+{
+ Construct res;
+}
+{
+ (
+ LOOKAHEAD(3) res = Global_construct() |
+ LOOKAHEAD(3) res = Interface() |
+ LOOKAHEAD(3) res = Potential_commit_point_define() |
+ LOOKAHEAD(3) res = Commit_point_define() |
+ LOOKAHEAD(3) res = Commit_point_define_check() |
+ LOOKAHEAD(3) res = Entry_point() |
+ LOOKAHEAD(3) res = Interface_define()
+ )
+ <EOF>
+ {
+ //System.out.println(res);
+ return res;
+ }
+}
+
+GlobalConstruct Global_construct() :
+{
+ GlobalConstruct res;
+ SequentialDefineSubConstruct code;
+ HashMap<String, String> options;
+ String key, value;
+}
+{
+ {
+ res = null;
+ options = new HashMap<String, String>();
+ }
+ <HEAD>
+ <BEGIN>
+ (<OPTIONS>
+ ((key = <IDENTIFIER>.image)
+ <EQUALS>
+ (value = <IDENTIFIER>.image)
+ {
+ if (options.containsKey(key)) {
+ throw new ParseException("Duplicate options!");
+ }
+ options.put(key, value);
+ }
+ <SEMI_COLON>
+ )*
+ )?
+ (code = Global_define())
+ { res = new GlobalConstruct(code, options); }
+ (Interface_clusters(res))?
+ (Happens_before(res))?
+ <END>
+ <TAIL>
+ {
+ res.unfoldInterfaceCluster();
+ return res;
+ }
+}
+
+String C_CPP_CODE() :
+{
+ StringBuilder text;
+ Token t;
+}
+{
+ {
+ text = new StringBuilder();
+ t = new Token();
+ }
+ (
+ //LOOKAHEAD(2)
+ (
+ t = <CONST> | t = <STRUCT> |
+ t = <IDENTIFIER> | t = <EQUALS> | t = <OPEN_PAREN> | t = <CLOSE_PAREN> |
+ t = <OPEN_BRACKET> | t = <CLOSE_BRACKET> | t = <HB_SYMBOL> | t = <COMMA> |
+ t = <DOT> | t = <STAR> | t = <NEGATE> | t = <EXCLAMATION> | t = <AND> | t = <OR> | t = <MOD> | t = <PLUS> |
+ t = <PLUSPLUS> | t = <MINUS> | t = <MINUSMINUS> | t = <DIVIDE> | t = <BACKSLASH> |
+ t = <LESS_THAN> | t = <GREATER_THAN> | t = <GREATER_EQUALS> | t = <LESS_EQUALS> |
+ t = <LOGICAL_EQUALS> | t = <NOT_EQUALS> | t = <LOGICAL_AND> | t = <LOGICAL_OR> | t = <XOR> |
+ t = <QUESTION_MARK> | t = <COLON> | t = <DOUBLECOLON> |
+ t = <SEMI_COLON> | t = <STRING_LITERAL> | t = <CHARACTER_LITERAL> |
+ t = <INTEGER_LITERAL> | t = <FLOATING_POINT_LITERAL>
+ )
+ {
+ text.append(t.image);
+ if (t.image.equals(";") || t.image.equals("\\")
+ || t.image.equals("{") || t.image.equals("}"))
+ text.append("\n");
+ else
+ text.append(" ");
+ }
+ )+
+ {
+ //System.out.println(text);
+ return text.toString();
+ }
+}
+
+SequentialDefineSubConstruct Global_define() :
+{
+ String declareVar, initVar, defineFunc;
+}
+{
+ {
+ declareVar = "";
+ initVar = "";
+ defineFunc = "";
+ }
+ <GLOBAL_DEFINE>
+ (<DECLARE_VAR> (declareVar = C_CPP_CODE()))?
+ (<INIT_VAR> (initVar = C_CPP_CODE()))?
+ (<DEFINE_FUNC> (defineFunc = C_CPP_CODE()))?
+ {
+ SequentialDefineSubConstruct res = new SequentialDefineSubConstruct(declareVar, initVar, defineFunc);
+ //System.out.println(res);
+ return res;
+ }
+}
+
+ConditionalInterface Conditional_interface() :
+{
+ String interfaceName, hbConditionLabel;
+}
+{
+ {
+ hbConditionLabel = "";
+ }
+ interfaceName = <IDENTIFIER>.image (<OPEN_BRACKET> hbConditionLabel =
+ <IDENTIFIER>.image <CLOSE_BRACKET>)?
+ {
+ return new ConditionalInterface(interfaceName, hbConditionLabel);
+ }
+}
+
+void Interface_cluster(GlobalConstruct inst) :
+{
+ String clusterName;
+ ConditionalInterface condInterface;
+}
+{
+ (clusterName= <IDENTIFIER>.image)
+ <EQUALS> <OPEN_PAREN>
+ (condInterface = Conditional_interface()
+ { inst.addInterface2Cluster(clusterName, condInterface); }
+ )
+ (<COMMA> condInterface = Conditional_interface()
+ { inst.addInterface2Cluster(clusterName, condInterface); }
+ )*
+ <CLOSE_PAREN>
+}
+
+void Interface_clusters(GlobalConstruct inst) :
+{}
+{
+ <INTERFACE_CLUSTER> (Interface_cluster(inst))+
+}
+
+void Happens_before(GlobalConstruct inst) :
+{
+ ConditionalInterface left, right;
+}
+{
+ <HAPPENS_BEFORE>
+ (
+ left = Conditional_interface() <HB_SYMBOL> right = Conditional_interface()
+ { inst.addHBCondition(left, right); }
+ )+
+}
+
+InterfaceConstruct Interface() :
+{
+ InterfaceConstruct res;
+ String interfaceName, condition, idCode, check, postAction,
+ postCheck, commitPoint, hbLabel, hbCondition;
+ ActionSubConstruct action;
+ ArrayList<String> commitPointSet;
+ HashMap<String, String> hbConditions;
+}
+{
+ {
+ res = null;
+ action = null;
+ condition = "";
+ idCode = "";
+ check = "";
+ postAction = "";
+ postCheck = "";
+ commitPointSet = new ArrayList<String>();
+ hbConditions = new HashMap<String, String>();
+ }
+ <HEAD>
+ <BEGIN>
+ <INTERFACE> (interfaceName = <IDENTIFIER>.image)
+ <COMMIT_POINT_SET>
+ (commitPoint = <IDENTIFIER>.image
+ { commitPointSet.add(commitPoint); }
+ )
+ (<OR>
+ (commitPoint = <IDENTIFIER>.image)
+ {
+ if (commitPointSet.contains(commitPoint)) {
+ throw new ParseException(interfaceName + " has" +
+ "duplicate commit point labels");
+ }
+ commitPointSet.add(commitPoint);
+ }
+ )*
+
+ (<CONDITION> (condition = C_CPP_CODE()))?
+ (
+ <HB_CONDITION>
+ (hbLabel = <IDENTIFIER>.image)
+ (hbCondition = C_CPP_CODE())
+ {
+ if (hbConditions.containsKey(hbLabel)) {
+ throw new ParseException(interfaceName + " has" +
+ "duplicate happens-before condtion labels");
+ }
+ hbConditions.put(hbLabel, hbCondition);
+ }
+ )*
+ (<ID> (idCode = C_CPP_CODE()))?
+ (<CHECK> (check = C_CPP_CODE()))?
+ (action = Action())?
+ (<POST_ACTION> (postAction = C_CPP_CODE()))?
+ (<POST_CHECK> (postCheck = C_CPP_CODE()))?
+ <END>
+ <TAIL>
+ {
+ res = new InterfaceConstruct(interfaceName, commitPointSet, condition,
+ hbConditions, idCode, check, action, postAction, postCheck);
+ return res;
+ }
+}
+
+ActionSubConstruct Action() :
+{
+ String type, name, expr, defineVarStr, code;
+ ArrayList<DefineVar> defineVars;
+}
+{
+ {
+ defineVars = new ArrayList<DefineVar>();
+ code = "";
+ }
+ <ACTION>
+ (
+ (
+ (<DEFINEVAR> (defineVarStr = C_CPP_CODE())
+ {
+ int eqIdx = defineVarStr.indexOf('=');
+ int typeEnd = defineVarStr.lastIndexOf(' ', eqIdx - 2);
+ type = defineVarStr.substring(0, typeEnd);
+ name = defineVarStr.substring(typeEnd + 1, eqIdx - 1);
+ expr = defineVarStr.substring(eqIdx + 2);
+ DefineVar defineVar = new DefineVar(type, name, expr);
+ defineVars.add(defineVar);
+ })* (<CODE> (code = C_CPP_CODE()))? )
+ )
+
+ {
+ ActionSubConstruct res = new ActionSubConstruct(defineVars, code);
+ return res;
+ }
+}
+
+PotentialCPDefineConstruct Potential_commit_point_define() :
+{
+ PotentialCPDefineConstruct res;
+ String label, condition;
+}
+{
+
+ { res = null; }
+ <HEAD>
+ <BEGIN>
+ <POTENTIAL_COMMIT_POINT_DEFINE> (condition = C_CPP_CODE())
+ <LABEL> (label = <IDENTIFIER>.image)
+ <END>
+ <TAIL>
+ {
+ res = new PotentialCPDefineConstruct(label, condition);
+ return res;
+ }
+}
+
+
+CPDefineConstruct Commit_point_define() :
+{
+ CPDefineConstruct res;
+ String label, potentialCPLabel, condition;
+}
+{
+
+ { res = null; }
+ <HEAD>
+ <BEGIN>
+ <COMMIT_POINT_DEFINE> (condition = C_CPP_CODE())
+ <POTENTIAL_COMMIT_POINT_LABEL> (potentialCPLabel = <IDENTIFIER>.image)
+ <LABEL> (label = <IDENTIFIER>.image)
+ <END>
+ <TAIL>
+ {
+ res = new CPDefineConstruct(label, potentialCPLabel, condition);
+ return res;
+ }
+}
+
+
+CPDefineCheckConstruct Commit_point_define_check() :
+{
+ CPDefineCheckConstruct res;
+ String label, condition;
+}
+{
+
+ { res = null; }
+ <HEAD>
+ <BEGIN>
+ <COMMIT_POINT_DEFINE_CHECK> (condition = C_CPP_CODE())
+ <LABEL> (label = <IDENTIFIER>.image)
+ <END>
+ <TAIL>
+ {
+ res = new CPDefineCheckConstruct(label, condition);
+ return res;
+ }
+}
+
+EntryPointConstruct Entry_point() :
+{}
+{
+
+ <HEAD>
+ <BEGIN>
+ <ENTRY_POINT>
+ <END>
+ <TAIL>
+ {
+ return new EntryPointConstruct();
+ }
+}
+
+InterfaceDefineConstruct Interface_define() :
+{
+ String name;
+}
+{
+ <HEAD>
+ <BEGIN>
+ <INTERFACE_DEFINE> (name = <IDENTIFIER>.image)
+ <END>
+ <TAIL>
+ {
+ return new InterfaceDefineConstruct(name);
+ }
+}
+
+
try {
FileInputStream fis = new FileInputStream("./grammer/spec.txt");
SpecParser parser = new SpecParser(fis);
- parser.Parse();
+ parser.ParseSpec();
System.out.println("Parsing finished!");
} catch (FileNotFoundException e) {
e.printStackTrace();
}
PARSER_END(SpecParser)
-SKIP :
-{
- " "
-|
- "\n"
-|
- "\r"
-|
- "\r\n"
-|
- "\t"
-|
- // "#" comment for the specification
- <"#" (~["\n", "\r"])* (["\n", "\r"])>
-|
- // "//" comment for the specification
- <"//" (~["\n", "\r"])* (["\n", "\r"])>
+< IN_COMMENT > SKIP : { < ~[] > }
+
+< IN_COMMENT, IN_SPEC > SKIP : {
+ "*/": DEFAULT
}
-TOKEN :
-{
-/* Above are specification-only tokens */
- <HEAD: "/**">
-|
- <TAIL: "*/">
-|
+SKIP : {
+ "/*": IN_COMMENT
+}
+
+SKIP : {
+ "/**": IN_SPEC
+}
+
+<IN_SPEC> TOKEN : {
<BEGIN: "@Begin">
|
<END: "@End">
<COMMIT_POINT_DEFINE: "@Commit_point_define:">
|
<POTENTIAL_COMMIT_POINT_LABEL: "@Potential_commit_point_label:">
+}
+SKIP :
+{
+ " "
+|
+ "\n"
+|
+ "\r"
+|
+ "\r\n"
+|
+ "\t"
+|
+ // "#" comment for the specification
+ <"#" (~["\n", "\r"])* (["\n", "\r"])>
+|
+ // "//" comment for the specification
+ <"//" (~["\n", "\r"])* (["\n", "\r"])>
+}
+<IN_SPEC, DEFAULT> TOKEN :
+{
/* Specification & C/C++ shared tokens */
+// Reserved keywords
+ <CONST: "const">
+|
+ <STRUCT: "struct">
+|
+ <TYPENAME: "typename">
|
<#DIGIT: ["0"-"9"]>
|
< #HEXADECIMAL_EXPONENT: ["p","P"] (["+","-"])? (["0"-"9"])+ >
}
-Construct Parse() :
+String Type() :
{
- Construct res;
+ String type;
+ String str;
}
{
- (
- LOOKAHEAD(3) res = Global_construct() |
- LOOKAHEAD(3) res = Interface() |
- LOOKAHEAD(3) res = Potential_commit_point_define() |
- LOOKAHEAD(3) res = Commit_point_define() |
- LOOKAHEAD(3) res = Commit_point_define_check() |
- LOOKAHEAD(3) res = Entry_point() |
- LOOKAHEAD(3) res = Interface_define()
- )
- <EOF>
+ { type = ""; }
+ ("const"
+ { type = "const"; }
+ )?
+ (("struct" { type = type + " struct"; })?
+ (str = <IDENTIFIER>.image {
+ if (!type.equals(""))
+ type = type + " " + str;
+ else
+ type = str;
+ }))
+ ((str = "const".image {
+ if (!type.equals(""))
+ type = type + " " + str;
+ else
+ type = str;
+ }) |
+ (str = <STAR>.image {
+ if (!type.equals(""))
+ type = type + " " + str;
+ else
+ type = str;
+ }) |
+ (str = <AND>.image {
+ if (!type.equals(""))
+ type = type + " " + str;
+ else
+ type = str;
+ })
+ )*
{
- //System.out.println(res);
- return res;
+ return type;
}
}
-GlobalConstruct Global_construct() :
+ArrayList<String> FormalParamList() :
{
- GlobalConstruct res;
- SequentialDefineSubConstruct code;
- HashMap<String, String> options;
- String key, value;
+ ArrayList<String> typeParams;
}
{
{
- res = null;
- options = new HashMap<String, String>();
+ typeParams = new ArrayList<String>();
}
- <HEAD>
- <BEGIN>
- (<OPTIONS>
- ((key = <IDENTIFIER>.image)
- <EQUALS>
- (value = <IDENTIFIER>.image)
- {
- if (options.containsKey(key)) {
- throw new ParseException("Duplicate options!");
- }
- options.put(key, value);
- }
- <SEMI_COLON>
- )*
- )?
- (code = Global_define())
- { res = new GlobalConstruct(code, options); }
- (Interface_clusters(res))?
- (Happens_before(res))?
- <END>
- <TAIL>
+ (TypeParam(typeParams) (<COMMA> TypeParam(typeParams))*)?
{
- res.unfoldInterfaceCluster();
- return res;
+ System.out.println(typeParams);
+ return typeParams;
}
}
+void TypeParam(ArrayList<String> typeParams) :
+{
+ String type, param;
+}
+{
+ (type = Type()) (param = <IDENTIFIER>.image)
+ {
+ typeParams.add(type);
+ typeParams.add(param);
+ }
+}
+
+void ParseSpec() :
+{}
+{
+ <BEGIN> <POTENTIAL_COMMIT_POINT_DEFINE> C_CPP_CODE() <LABEL> <END>
+}
+
String C_CPP_CODE() :
{
StringBuilder text;
(
//LOOKAHEAD(2)
(
+ t = <CONST> | t = <STRUCT> |
t = <IDENTIFIER> | t = <EQUALS> | t = <OPEN_PAREN> | t = <CLOSE_PAREN> |
t = <OPEN_BRACKET> | t = <CLOSE_BRACKET> | t = <HB_SYMBOL> | t = <COMMA> |
t = <DOT> | t = <STAR> | t = <NEGATE> | t = <EXCLAMATION> | t = <AND> | t = <OR> | t = <MOD> | t = <PLUS> |
}
}
-SequentialDefineSubConstruct Global_define() :
-{
- String declareVar, initVar, defineFunc;
-}
-{
- {
- declareVar = "";
- initVar = "";
- defineFunc = "";
- }
- <GLOBAL_DEFINE>
- (<DECLARE_VAR> (declareVar = C_CPP_CODE()))?
- (<INIT_VAR> (initVar = C_CPP_CODE()))?
- (<DEFINE_FUNC> (defineFunc = C_CPP_CODE()))?
- {
- SequentialDefineSubConstruct res = new SequentialDefineSubConstruct(declareVar, initVar, defineFunc);
- //System.out.println(res);
- return res;
- }
-}
-
-ConditionalInterface Conditional_interface() :
-{
- String interfaceName, hbConditionLabel;
-}
-{
- {
- hbConditionLabel = "";
- }
- interfaceName = <IDENTIFIER>.image (<OPEN_BRACKET> hbConditionLabel =
- <IDENTIFIER>.image <CLOSE_BRACKET>)?
- {
- return new ConditionalInterface(interfaceName, hbConditionLabel);
- }
-}
-
-void Interface_cluster(GlobalConstruct inst) :
-{
- String clusterName;
- ConditionalInterface condInterface;
-}
-{
- (clusterName= <IDENTIFIER>.image)
- <EQUALS> <OPEN_PAREN>
- (condInterface = Conditional_interface()
- { inst.addInterface2Cluster(clusterName, condInterface); }
- )
- (<COMMA> condInterface = Conditional_interface()
- { inst.addInterface2Cluster(clusterName, condInterface); }
- )*
- <CLOSE_PAREN>
-}
-void Interface_clusters(GlobalConstruct inst) :
+void Comment() :
{}
{
- <INTERFACE_CLUSTER> (Interface_cluster(inst))+
-}
-
-void Happens_before(GlobalConstruct inst) :
-{
- ConditionalInterface left, right;
-}
-{
- <HAPPENS_BEFORE>
- (
- left = Conditional_interface() <HB_SYMBOL> right = Conditional_interface()
- { inst.addHBCondition(left, right); }
- )+
-}
-
-InterfaceConstruct Interface() :
-{
- InterfaceConstruct res;
- String interfaceName, condition, idCode, check, postAction,
- postCheck, commitPoint, hbLabel, hbCondition;
- ActionSubConstruct action;
- ArrayList<String> commitPointSet;
- HashMap<String, String> hbConditions;
-}
-{
- {
- res = null;
- action = null;
- condition = "";
- idCode = "";
- check = "";
- postAction = "";
- postCheck = "";
- commitPointSet = new ArrayList<String>();
- hbConditions = new HashMap<String, String>();
- }
- <HEAD>
- <BEGIN>
- <INTERFACE> (interfaceName = <IDENTIFIER>.image)
- <COMMIT_POINT_SET>
- (commitPoint = <IDENTIFIER>.image
- { commitPointSet.add(commitPoint); }
- )
- (<OR>
- (commitPoint = <IDENTIFIER>.image)
- {
- if (commitPointSet.contains(commitPoint)) {
- throw new ParseException(interfaceName + " has" +
- "duplicate commit point labels");
- }
- commitPointSet.add(commitPoint);
- }
- )*
-
- (<CONDITION> (condition = C_CPP_CODE()))?
- (
- <HB_CONDITION>
- (hbLabel = <IDENTIFIER>.image)
- (hbCondition = C_CPP_CODE())
- {
- if (hbConditions.containsKey(hbLabel)) {
- throw new ParseException(interfaceName + " has" +
- "duplicate happens-before condtion labels");
- }
- hbConditions.put(hbLabel, hbCondition);
- }
- )*
- (<ID> (idCode = C_CPP_CODE()))?
- (<CHECK> (check = C_CPP_CODE()))?
- (action = Action())?
- (<POST_ACTION> (postAction = C_CPP_CODE()))?
- (<POST_CHECK> (postCheck = C_CPP_CODE()))?
- <END>
- <TAIL>
- {
- res = new InterfaceConstruct(interfaceName, commitPointSet, condition,
- hbConditions, idCode, check, action, postAction, postCheck);
- return res;
- }
-}
-
-ActionSubConstruct Action() :
-{
- String type, name, expr, defineVarStr, code;
- ArrayList<DefineVar> defineVars;
-}
-{
- {
- defineVars = new ArrayList<DefineVar>();
- code = "";
- }
- <ACTION>
- (
- (
- (<DEFINEVAR> (defineVarStr = C_CPP_CODE())
- {
- int eqIdx = defineVarStr.indexOf('=');
- int typeEnd = defineVarStr.lastIndexOf(' ', eqIdx - 2);
- type = defineVarStr.substring(0, typeEnd);
- name = defineVarStr.substring(typeEnd + 1, eqIdx - 1);
- expr = defineVarStr.substring(eqIdx + 2);
- DefineVar defineVar = new DefineVar(type, name, expr);
- defineVars.add(defineVar);
- })* (<CODE> (code = C_CPP_CODE()))? )
- )
-
- {
- ActionSubConstruct res = new ActionSubConstruct(defineVars, code);
- return res;
- }
-}
-
-PotentialCPDefineConstruct Potential_commit_point_define() :
-{
- PotentialCPDefineConstruct res;
- String label, condition;
-}
-{
-
- { res = null; }
- <HEAD>
- <BEGIN>
- <POTENTIAL_COMMIT_POINT_DEFINE> (condition = C_CPP_CODE())
- <LABEL> (label = <IDENTIFIER>.image)
- <END>
- <TAIL>
- {
- res = new PotentialCPDefineConstruct(label, condition);
- return res;
- }
-}
-
-
-CPDefineConstruct Commit_point_define() :
-{
- CPDefineConstruct res;
- String label, potentialCPLabel, condition;
-}
-{
-
- { res = null; }
- <HEAD>
- <BEGIN>
- <COMMIT_POINT_DEFINE> (condition = C_CPP_CODE())
- <POTENTIAL_COMMIT_POINT_LABEL> (potentialCPLabel = <IDENTIFIER>.image)
- <LABEL> (label = <IDENTIFIER>.image)
- <END>
- <TAIL>
- {
- res = new CPDefineConstruct(label, potentialCPLabel, condition);
- return res;
- }
+ C_CPP_CODE()
}
-
-CPDefineCheckConstruct Commit_point_define_check() :
-{
- CPDefineCheckConstruct res;
- String label, condition;
-}
-{
-
- { res = null; }
- <HEAD>
- <BEGIN>
- <COMMIT_POINT_DEFINE_CHECK> (condition = C_CPP_CODE())
- <LABEL> (label = <IDENTIFIER>.image)
- <END>
- <TAIL>
- {
- res = new CPDefineCheckConstruct(label, condition);
- return res;
- }
-}
-
-EntryPointConstruct Entry_point() :
+void Parse() :
{}
{
-
- <HEAD>
- <BEGIN>
- <ENTRY_POINT>
- <END>
- <TAIL>
- {
- return new EntryPointConstruct();
- }
-}
-
-InterfaceDefineConstruct Interface_define() :
-{
- String name;
-}
-{
- <HEAD>
- <BEGIN>
- <INTERFACE_DEFINE> (name = <IDENTIFIER>.image)
- <END>
- <TAIL>
- {
- return new InterfaceDefineConstruct(name);
- }
+ C_CPP_CODE() |
+ <EOF>
}
-
-
--- /dev/null
+#include <threads.h>
+#include <stdlib.h>
+#include "librace.h"
+#include "model-assert.h"
+
+#include "my_queue.h"
+
+#define relaxed memory_order_relaxed
+#define release memory_order_release
+#define acquire memory_order_acquire
+
+#define MAX_FREELIST 4 /* Each thread can own up to MAX_FREELIST free nodes */
+#define INITIAL_FREE 2 /* Each thread starts with INITIAL_FREE free nodes */
+
+#define POISON_IDX 0x666
+
+static unsigned int (*free_lists)[MAX_FREELIST];
+
+/* Search this thread's free list for a "new" node */
+static unsigned int new_node()
+{
+ int i;
+ int t = get_thread_num();
+ for (i = 0; i < MAX_FREELIST; i++) {
+ unsigned int node = load_32(&free_lists[t][i]);
+ if (node) {
+ store_32(&free_lists[t][i], 0);
+ return node;
+ }
+ }
+ /* free_list is empty? */
+ MODEL_ASSERT(0);
+ return 0;
+}
+
+/* Place this node index back on this thread's free list */
+static void reclaim(unsigned int node)
+{
+ int i;
+ int t = get_thread_num();
+
+ /* Don't reclaim NULL node */
+ MODEL_ASSERT(node);
+
+ for (i = 0; i < MAX_FREELIST; i++) {
+ /* Should never race with our own thread here */
+ unsigned int idx = load_32(&free_lists[t][i]);
+
+ /* Found empty spot in free list */
+ if (idx == 0) {
+ store_32(&free_lists[t][i], node);
+ return;
+ }
+ }
+ /* free list is full? */
+ MODEL_ASSERT(0);
+}
+
+void init_queue(queue_t *q, int num_threads)
+{
+ /*
+ @Begin
+ @Entry_point
+ @End
+ */
+
+ int i, j;
+
+ /* Initialize each thread's free list with INITIAL_FREE pointers */
+ /* The actual nodes are initialized with poison indexes */
+ free_lists = malloc(num_threads * sizeof(*free_lists));
+ for (i = 0; i < num_threads; i++) {
+ for (j = 0; j < INITIAL_FREE; j++) {
+ free_lists[i][j] = 2 + i * MAX_FREELIST + j;
+ atomic_init(&q->nodes[free_lists[i][j]].next, MAKE_POINTER(POISON_IDX, 0));
+ }
+ }
+
+ /* initialize queue */
+ atomic_init(&q->head, MAKE_POINTER(1, 0));
+ atomic_init(&q->tail, MAKE_POINTER(1, 0));
+ atomic_init(&q->nodes[1].next, MAKE_POINTER(0, 0));
+}
+
+/*
+ @Begin
+ @Interface_define: Enqueue
+ @End
+*/
+void enqueue(queue_t *q, unsigned int val)
+{
+ int success = 0;
+ unsigned int node;
+ pointer tail;
+ pointer next;
+ pointer tmp;
+
+ node = new_node();
+ store_32(&q->nodes[node].value, val);
+ tmp = atomic_load_explicit(&q->nodes[node].next, relaxed);
+ set_ptr(&tmp, 0); // NULL
+ atomic_store_explicit(&q->nodes[node].next, tmp, relaxed);
+
+ while (!success) {
+ tail = atomic_load_explicit(&q->tail, acquire);
+ next = atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire);
+ if (tail == atomic_load_explicit(&q->tail, relaxed)) {
+
+ /* Check for uninitialized 'next' */
+ MODEL_ASSERT(get_ptr(next) != POISON_IDX);
+
+ if (get_ptr(next) == 0) { // == NULL
+ pointer value = MAKE_POINTER(node, get_count(next) + 1);
+ success = atomic_compare_exchange_strong_explicit(&q->nodes[get_ptr(tail)].next,
+ &next, value, release, release);
+ }
+ if (!success) {
+ unsigned int ptr = get_ptr(atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire));
+ pointer value = MAKE_POINTER(ptr,
+ get_count(tail) + 1);
+ int commit_success = 0;
+ commit_success = atomic_compare_exchange_strong_explicit(&q->tail,
+ &tail, value, release, release);
+ /**
+ @Begin
+ @Potential_commit_point_check: __ATOMIC_RET__ == true
+ @Label: Enqueue_Success_Point
+ @End
+ */
+ thrd_yield();
+ }
+ }
+ }
+ atomic_compare_exchange_strong_explicit(&q->tail,
+ &tail,
+ MAKE_POINTER(node, get_count(tail) + 1),
+ release, release);
+}
+
+
+/*
+ @Begin
+ @Interface_define: Dequeue
+ @End
+*/
+unsigned int dequeue(queue_t *q)
+{
+ unsigned int value;
+ int success = 0;
+ pointer head;
+ pointer tail;
+ pointer next;
+
+ while (!success) {
+ head = atomic_load_explicit(&q->head, acquire);
+ tail = atomic_load_explicit(&q->tail, relaxed);
+ next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, acquire);
+ if (atomic_load_explicit(&q->head, relaxed) == head) {
+ if (get_ptr(head) == get_ptr(tail)) {
+
+ /* Check for uninitialized 'next' */
+ MODEL_ASSERT(get_ptr(next) != POISON_IDX);
+
+ if (get_ptr(next) == 0) { // NULL
+ return 0; // NULL
+ }
+ atomic_compare_exchange_strong_explicit(&q->tail,
+ &tail,
+ MAKE_POINTER(get_ptr(next), get_count(tail) + 1),
+ release, release);
+ thrd_yield();
+ } else {
+ value = load_32(&q->nodes[get_ptr(next)].value);
+ success = atomic_compare_exchange_strong_explicit(&q->head,
+ &head,
+ MAKE_POINTER(get_ptr(next), get_count(head) + 1),
+ release, release);
+ /*
+ @Begin
+ @Commit_point_define_check: __ATOMIC_RET__ == true
+ @Label: Dequeue_Success_Point
+ @End
+ */
+ if (!success)
+ thrd_yield();
+ }
+ }
+ }
+ reclaim(get_ptr(head));
+ return value;
+}
projects / cdsspec-compiler.git / commitdiff