add support for unattached ordering points

diff --git a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
index fffeae5971928535b3ea3ab4de76cfb48c6adca4..272f4aae6c68ad08ddda366f473ea0909620f14b 100644 (file)
--- a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
+++ b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
@@ -169,6 +169,18 @@ public class CodeGeneratorUtils {
                code.addLine("#endif");
                code.addLine("");
 
                code.addLine("#endif");
                code.addLine("");
 

+               // Declare _createOPDefineUnattached
+               code.addLine(ShortComment("Declare _createOPDefineUnattached"));
+               // void _createOPDefineUnattached();
+               code.addLine("void _createOPDefineUnattached();");
+               code.addLine("");
+
+               // Declare _createOPClearDefineUnattached
+               code.addLine(ShortComment("Declare _createOPClearDefineUnattached"));
+               // void _createOPClearDefineUnattached();
+               code.addLine("void _createOPClearDefineUnattached();");
+               code.addLine("");
+

                code.addLine(ShortComment("Declaration of some c-strings (CSTR)"));
 
                // Interface name strings
                code.addLine(ShortComment("Declaration of some c-strings (CSTR)"));
 
                // Interface name strings


@@ -296,6 +308,31 @@ public class CodeGeneratorUtils {
                code.addLine("");
                code.addLine("");
 
                code.addLine("");
                code.addLine("");
 

+               // Define the fake ordering point operation
+               code.addLine(ShortComment("Define the fake ordering point operation"));
+               // atomic_int _FAKE_OP_;
+               code.addLine("atomic_int " + SpecNaming.FakeOP + ";");
+               code.addLine("");
+
+               // Define _createOPDefineUnattached
+               code.addLine(ShortComment("Define _createOPDefineUnattached"));
+               code.addLine("void " + SpecNaming.CreateOPDefineUnattachedFunc + "() {");
+               code.addLine(TabbedLine(ShortComment("A load acting as the fake OP")));
+               code.addLine(TabbedLine(SpecNaming.FakeOP
+                               + ".load(memory_order_relaxed);"));
+               code.addLine(TabbedLine(SpecNaming.CreateOPDefineAnnoFunc + "();"));
+               code.addLine("}");
+
+               // Define _createOPClearDefineUnattached
+               code.addLine(ShortComment("Define _createOPClearDefineUnattached"));
+               code.addLine("void " + SpecNaming.CreateOPClearDefineUnattachedFunc
+                               + "() {");
+               code.addLine(TabbedLine(ShortComment("A load acting as the fake OP")));
+               code.addLine(TabbedLine(SpecNaming.FakeOP
+                               + ".load(memory_order_relaxed);"));
+               code.addLine(TabbedLine(SpecNaming.CreateOPClearDefineAnnoFunc + "();"));
+               code.addLine("}");
+

                code.addLine(ShortComment("Definition of some c-strings (CSTR)"));
                code.addLine(ShortComment("A special empty string"));
                code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.EmptyCString,
                code.addLine(ShortComment("Definition of some c-strings (CSTR)"));
                code.addLine(ShortComment("A special empty string"));
                code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.EmptyCString,


@@ -571,11 +608,11 @@ public class CodeGeneratorUtils {
                                        construct.preCondition.align(1);
                                        code.addLine(TabbedLine(ShortComment("Execute PreCondition")));
                                        code.addLines(construct.preCondition);
                                        construct.preCondition.align(1);
                                        code.addLine(TabbedLine(ShortComment("Execute PreCondition")));
                                        code.addLines(construct.preCondition);

-                                       
+

                                        // By default, we will return true for @PreCondition
                                        code.addLine(TabbedLine(ShortComment("By default @PreCondition returns true")));
                                        code.addLine(TabbedLine("return true;"));
                                        // By default, we will return true for @PreCondition
                                        code.addLine(TabbedLine(ShortComment("By default @PreCondition returns true")));
                                        code.addLine(TabbedLine("return true;"));

-                                       
+

                                        code.addLine("}");
                                        code.addLine("");
 
                                        code.addLine("}");
                                        code.addLine("");
 


@@ -603,7 +640,7 @@ public class CodeGeneratorUtils {
                                        // By default, we will return true for @PostCondition
                                        code.addLine(TabbedLine(ShortComment("By default @PostCondition returns true")));
                                        code.addLine(TabbedLine("return true;"));
                                        // By default, we will return true for @PostCondition
                                        code.addLine(TabbedLine(ShortComment("By default @PostCondition returns true")));
                                        code.addLine(TabbedLine("return true;"));

-                                       
+

                                        code.addLine("}");
                                        code.addLine("");
                                }
                                        code.addLine("}");
                                        code.addLine("");
                                }


@@ -639,6 +676,11 @@ public class CodeGeneratorUtils {
                code.addLine(ShortComment("Define INIT annotation instrumentation function"));
                code.addLine("void _createInitAnnotation() {");
 
                code.addLine(ShortComment("Define INIT annotation instrumentation function"));
                code.addLine("void _createInitAnnotation() {");
 

+               // Init the fake ordering point place holder
+               code.addLine(TabbedLine(ShortComment("Init the fake ordering point place holder")));
+               code.addLine(TabbedLine(SpecNaming.FakeOP
+                               + ".store(1, memory_order_relaxed);"));
+

                // Init commutativity rules
                code.addLine(TabbedLine(ShortComment("Init commutativity rules")));
                code.addLine(TabbedLine(DeclareDefine("int",
                // Init commutativity rules
                code.addLine(TabbedLine(ShortComment("Init commutativity rules")));
                code.addLine(TabbedLine(DeclareDefine("int",


@@ -917,6 +959,10 @@ public class CodeGeneratorUtils {
                case OPDefine:
                        code.addLine(prefixTabs + SpecNaming.CreateOPDefineAnnoFunc + "();");
                        break;
                case OPDefine:
                        code.addLine(prefixTabs + SpecNaming.CreateOPDefineAnnoFunc + "();");
                        break;

+               case OPDefineUnattached:
+                       code.addLine(prefixTabs + SpecNaming.CreateOPDefineUnattachedFunc
+                                       + "();");
+                       break;

                case PotentialOP:
                        code.addLine(prefixTabs + SpecNaming.CreatePotentialOPAnnoFunc
                                        + "(" + SpecNaming.AppendStr(label) + ");");
                case PotentialOP:
                        code.addLine(prefixTabs + SpecNaming.CreatePotentialOPAnnoFunc
                                        + "(" + SpecNaming.AppendStr(label) + ");");


@@ -932,6 +978,10 @@ public class CodeGeneratorUtils {
                        code.addLine(prefixTabs + SpecNaming.CreateOPClearDefineAnnoFunc
                                        + "();");
                        break;
                        code.addLine(prefixTabs + SpecNaming.CreateOPClearDefineAnnoFunc
                                        + "();");
                        break;

+               case OPClearDefineUnattached:
+                       code.addLine(prefixTabs
+                                       + SpecNaming.CreateOPClearDefineUnattachedFunc + "();");
+                       break;

                default:
                        break;
                }
                default:
                        break;
                }

diff --git a/src/edu/uci/eecs/specExtraction/OPType.java b/src/edu/uci/eecs/specExtraction/OPType.java
index 11c26b79684166edacef264dcd7943108d563b02..4be12691bf97280a905bb289fe30472e45467907 100644 (file)
--- a/src/edu/uci/eecs/specExtraction/OPType.java
+++ b/src/edu/uci/eecs/specExtraction/OPType.java
@@ -9,5 +9,5 @@ package edu.uci.eecs.specExtraction;
  * 
  */
 public enum OPType {
  * 
  */
 public enum OPType {

-       OPDefine, PotentialOP, OPCheck, OPClear, OPClearDefine
+       OPDefine, PotentialOP, OPCheck, OPClear, OPClearDefine, OPDefineUnattached, OPClearDefineUnattached

 }
 }

diff --git a/src/edu/uci/eecs/specExtraction/SpecExtractor.java b/src/edu/uci/eecs/specExtraction/SpecExtractor.java
index afa42f78033b5d34475c38c5601fa251950563fc..df0b5f1cb78d5c1928d6d49796e01274a604bf9a 100644 (file)
--- a/src/edu/uci/eecs/specExtraction/SpecExtractor.java
+++ b/src/edu/uci/eecs/specExtraction/SpecExtractor.java
@@ -38,8 +38,8 @@ public class SpecExtractor {
        public final HashMap<File, EntryConstruct> entryMap;
 
        public final HashSet<String> headerFiles;
        public final HashMap<File, EntryConstruct> entryMap;
 
        public final HashSet<String> headerFiles;

-       
-       // In the generated header file, we need to forward the user-defined 
+
+       // In the generated header file, we need to forward the user-defined

        public final HashSet<String> forwardClass;
 
        private GlobalConstruct globalConstruct;
        public final HashSet<String> forwardClass;
 
        private GlobalConstruct globalConstruct;


@@ -54,10 +54,9 @@ public class SpecExtractor {
                forwardClass = new HashSet<String>();
                globalConstruct = null;
        }
                forwardClass = new HashSet<String>();
                globalConstruct = null;
        }

-       
+

        private void addDefineConstruct(DefineConstruct construct) {
        private void addDefineConstruct(DefineConstruct construct) {

-               ArrayList<DefineConstruct> list = defineListMap
-                               .get(construct.file);
+               ArrayList<DefineConstruct> list = defineListMap.get(construct.file);

                if (list == null) {
                        list = new ArrayList<DefineConstruct>();
                        defineListMap.put(construct.file, list);
                if (list == null) {
                        list = new ArrayList<DefineConstruct>();
                        defineListMap.put(construct.file, list);


@@ -385,7 +384,7 @@ public class SpecExtractor {
                // -1 means the curl symbols in the interface do not match
                return -1;
        }
                // -1 means the curl symbols in the interface do not match
                return -1;
        }

-       
+

        /**
         * <p>
         * A sub-routine to extract the define construct. When called, we have
        /**
         * <p>
         * A sub-routine to extract the define construct. When called, we have


@@ -408,17 +407,16 @@ public class SpecExtractor {
         * @throws IOException
         * @throws ParseException
         */
         * @throws IOException
         * @throws ParseException
         */

-       private void extractDefineConstruct(File file,
-                       LineNumberReader lineReader, String curLine, int beginLineNum)
-                       throws WrongAnnotationException, IOException, ParseException {
+       private void extractDefineConstruct(File file, LineNumberReader lineReader,
+                       String curLine, int beginLineNum) throws WrongAnnotationException,
+                       IOException, ParseException {

                ArrayList<String> annotations = extractTillConstructEnd(file,
                                lineReader, curLine, beginLineNum);
                int endLineNum = lineReader.getLineNumber();
                ArrayList<String> annotations = extractTillConstructEnd(file,
                                lineReader, curLine, beginLineNum);
                int endLineNum = lineReader.getLineNumber();

-               DefineConstruct construct = new DefineConstruct(file,
-                               beginLineNum, endLineNum, annotations);
+               DefineConstruct construct = new DefineConstruct(file, beginLineNum,
+                               endLineNum, annotations);

                addDefineConstruct(construct);
        }
                addDefineConstruct(construct);
        }

-       

 
        /**
         * <p>
 
        /**
         * <p>


@@ -461,7 +459,7 @@ public class SpecExtractor {
                        line = lineReader.readLine();
                        lineNum = lineReader.getLineNumber();
                        construct.processFunctionDeclaration(line);
                        line = lineReader.readLine();
                        lineNum = lineReader.getLineNumber();
                        construct.processFunctionDeclaration(line);

-                       
+

                        // Record those user-defined struct
                        // RET
                        String returnType = construct.getFunctionHeader().returnType;
                        // Record those user-defined struct
                        // RET
                        String returnType = construct.getFunctionHeader().returnType;


@@ -472,7 +470,7 @@ public class SpecExtractor {
                                if (SpecUtils.isUserDefinedStruct(decl.type))
                                        forwardClass.add(SpecUtils.getPlainType(decl.type));
                        }
                                if (SpecUtils.isUserDefinedStruct(decl.type))
                                        forwardClass.add(SpecUtils.getPlainType(decl.type));
                        }

-                       
+

                } catch (IOException e) {
                        errMsg = "Spec error in file \""
                                        + file.getName()
                } catch (IOException e) {
                        errMsg = "Spec error in file \""
                                        + file.getName()


@@ -590,7 +588,9 @@ public class SpecExtractor {
                                extractEntryConstruct(file, beginLineNum, curLine);
                        else if (name.equals("OPDefine") || name.equals("PotentialOP")
                                        || name.equals("OPCheck") || name.equals("OPClear")
                                extractEntryConstruct(file, beginLineNum, curLine);
                        else if (name.equals("OPDefine") || name.equals("PotentialOP")
                                        || name.equals("OPCheck") || name.equals("OPClear")

-                                       || name.equals("OPClearDefine"))
+                                       || name.equals("OPClearDefine")
+                                       || name.equals("OPDefineUnattached")
+                                       || name.equals("OPClearDefineUnattached"))

                                extractOPConstruct(file, beginLineNum, curLine,
                                                OPType.valueOf(name));
                }
                                extractOPConstruct(file, beginLineNum, curLine,
                                                OPType.valueOf(name));
                }

diff --git a/src/edu/uci/eecs/specExtraction/SpecNaming.java b/src/edu/uci/eecs/specExtraction/SpecNaming.java
index f1f97ffd11f7011f0602501e1e683f6b3dc20116..78ea9039c9d970f4ef1a09f5e7e7c14ffc24970c 100644 (file)
--- a/src/edu/uci/eecs/specExtraction/SpecNaming.java
+++ b/src/edu/uci/eecs/specExtraction/SpecNaming.java
@@ -170,6 +170,8 @@ public class SpecNaming {
        public static final String CreateInterfaceBeginAnnoFunc = "_createInterfaceBeginAnnotation";
        public static final String SetInterfaceBeginAnnoValueFunc = "_setInterfaceBeginAnnotationValue";
        public static final String CreateOPDefineAnnoFunc = "_createOPDefineAnnotation";
        public static final String CreateInterfaceBeginAnnoFunc = "_createInterfaceBeginAnnotation";
        public static final String SetInterfaceBeginAnnoValueFunc = "_setInterfaceBeginAnnotationValue";
        public static final String CreateOPDefineAnnoFunc = "_createOPDefineAnnotation";

+       public static final String CreateOPDefineUnattachedFunc = "_createOPDefineUnattached";
+       public static final String CreateOPClearDefineUnattachedFunc = "_createOPClearDefineUnattached";

        public static final String CreatePotentialOPAnnoFunc = "_createPotentialOPAnnotation";
        public static final String CreateOPCheckAnnoFunc = "_createOPCheckAnnotation";
        public static final String CreateOPClearAnnoFunc = "_createOPClearAnnotation";
        public static final String CreatePotentialOPAnnoFunc = "_createPotentialOPAnnotation";
        public static final String CreateOPCheckAnnoFunc = "_createOPCheckAnnotation";
        public static final String CreateOPClearAnnoFunc = "_createOPClearAnnotation";


@@ -192,6 +194,9 @@ public class SpecNaming {
        public static final String RET = "RET";
        public static final String InterfaceValueInst = "__value";
        
        public static final String RET = "RET";
        public static final String InterfaceValueInst = "__value";
        

+       // The fake ordering point operation
+       public static final String FakeOP = "_FAKE_OP_";
+       

        // The wrapper prefix that we want to attach to the function name
        public static final String WrapperPrefix = "Wrapper";
 
        // The wrapper prefix that we want to attach to the function name
        public static final String WrapperPrefix = "Wrapper";