fixed rcu
authorPeizhao Ou <peizhaoo@uci.edu>
Wed, 15 Jan 2014 19:18:38 +0000 (11:18 -0800)
committerPeizhao Ou <peizhaoo@uci.edu>
Wed, 15 Jan 2014 19:18:38 +0000 (11:18 -0800)
benchmark/linuxrwlocks/linuxrwlocks.c
benchmark/ms-queue/my_queue.h
benchmark/read-copy-update/rcu.cc
src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
src/edu/uci/eecs/specCompiler/specExtraction/FunctionHeader.java

index 142e376..c96eb95 100644 (file)
@@ -42,6 +42,8 @@ typedef union {
 
 /**
        @Begin
+       @Options:
+               LANG = C;
        @Global_define:
                @DeclareVar:
                        bool writer_lock_acquired;
index d499929..ff3d42d 100644 (file)
@@ -32,6 +32,8 @@ void init_queue(queue_t *q, int num_threads);
 
 /**
        @Begin
+       @Options:
+               LANG = C;
        @Global_define:
                @DeclareStruct:
                typedef struct tag_elem {
@@ -47,7 +49,7 @@ void init_queue(queue_t *q, int num_threads);
                        tag = new_id_tag(); // Beginning of available id
                @DefineFunc:
                        tag_elem_t* new_tag_elem(call_id_t id, unsigned int data) {
-                               tag_elem_t *e = (tag_elem_t*) MODEL_MALLOC(sizeof(tag_elem_t));
+                               tag_elem_t *e = (tag_elem_t*) CMODEL_MALLOC(sizeof(tag_elem_t));
                                e->id = id;
                                e->data = data;
                                return e;
index 75f470b..8aad9d1 100644 (file)
@@ -6,8 +6,6 @@
 
 #include "librace.h"
 
-using namespace std;
-
 /**
        This is an example about how to specify the correctness of the
        read-copy-update synchronization mechanism.
@@ -31,7 +29,7 @@ atomic<Data*> data;
                
                @DefineFunc:
                bool equals(Data *ptr1, Data *ptr2) {
-                       if (ptr1->data1 == ptr2->data2
+                       if (ptr1->data1 == ptr2->data1
                                && ptr1->data2 == ptr2->data2
                                && ptr1->data3 == ptr2->data3) {
                                return true;
@@ -115,6 +113,7 @@ int user_main(int argc, char **argv) {
        */
        
        thrd_t t1, t2;
+       data.store(NULL, memory_order_relaxed);
        Data *data_init = (Data*) malloc(sizeof(Data));
        data_init->data1 = 1;
        data_init->data2 = 2;
index e68c27d..84ba735 100644 (file)
@@ -17,6 +17,7 @@ import edu.uci.eecs.specCompiler.specExtraction.ClassEndConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface;
 import edu.uci.eecs.specCompiler.specExtraction.Construct;
 import edu.uci.eecs.specCompiler.specExtraction.EntryPointConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.FunctionHeader;
 import edu.uci.eecs.specCompiler.specExtraction.GlobalConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.IDExtractor;
 import edu.uci.eecs.specCompiler.specExtraction.InterfaceConstruct;
@@ -121,10 +122,12 @@ public class CodeGenerator {
                                                new ArrayList<CodeAddition>());
                        }
                        codeAdditions.get(defineConstruct.file).add(addition);
-               } else { // No declaration needed
+               } else { // No declaration needed but should add forward declaration
                        // Last generate the definition
-                       newCode = CodeVariables.generateInterfaceWrapperDefinition(
-                                       _semantics, construct);
+                       newCode = new ArrayList<String>();
+                       newCode.addAll(CodeVariables.generateInterfaceWrapperDeclaration(_semantics, construct));
+                       newCode.addAll(CodeVariables.generateInterfaceWrapperDefinition(
+                                       _semantics, construct));
                        lineNum = construct.beginLineNum;
                        // Add the wrapper declaration
                        addition = new CodeAddition(lineNum, newCode);
@@ -234,7 +237,7 @@ public class CodeGenerator {
                }
                for (File file : codeAdditions.keySet()) {
                        ArrayList<CodeAddition> additions = codeAdditions.get(file);
-                       
+
                        if (additions.size() == 0) // Simply do nothing
                                continue;
                        ArrayList<String> content = _semantics.srcFilesInfo.get(file).content;
@@ -242,7 +245,8 @@ public class CodeGenerator {
                        // Insert generated annotation to the source files
                        ArrayList<String> newContent = insertAnnotation2Src(additions,
                                        content);
-                       ArrayList<String> finalContent = new ArrayList<String>(headerCode.size() + newContent.size());
+                       ArrayList<String> finalContent = new ArrayList<String>(
+                                       headerCode.size() + newContent.size());
                        finalContent.addAll(headerCode);
                        finalContent.addAll(newContent);
                        // Write it back to file
@@ -254,16 +258,16 @@ public class CodeGenerator {
        public static void main(String[] argvs) {
                String homeDir = Environment.HOME_DIRECTORY;
                File[] srcFiles = {
-//                              new File(homeDir + "/benchmark/linuxrwlocks/linuxrwlocks.c")
-//                              };
-                               // new File(homeDir
-                               // +
-                               // "/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h"),
-                               // };
-//                             new File(homeDir + "/benchmark/ms-queue/my_queue.c"),
-//                             new File(homeDir + "/benchmark/ms-queue/main.c"),
-//                             new File(homeDir + "/benchmark/ms-queue/my_queue.h") };
-               
+//                             new File(homeDir
+//                             + "/benchmark/linuxrwlocks/linuxrwlocks.c") };
+               // new File(homeDir
+               // +
+               // "/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h"),
+               // };
+//              new File(homeDir + "/benchmark/ms-queue/my_queue.c"),
+//              new File(homeDir + "/benchmark/ms-queue/main.c"),
+//              new File(homeDir + "/benchmark/ms-queue/my_queue.h") };
+
                 new File(homeDir + "/benchmark/read-copy-update/rcu.cc") };
                CodeGenerator gen = new CodeGenerator(srcFiles);
                gen.generateCode();
index a97edc3..aeace48 100644 (file)
@@ -38,8 +38,8 @@ public class CodeVariables {
        public static final String HEADER_COMMON = "<common.h>";
        public static final String HEADER_SPECANNOTATION = "<specannotation.h>";
        public static final String HEADER_CDSTRACE = "<cdstrace.h>";
-       // public static final String CDSAnnotate = "cdsannotate";
-       public static final String CDSAnnotate = "_Z11cdsannotatemPv";
+       public static final String CDSAnnotate = "cdsannotate";
+       public static final String C_CDSAnnotate = "_Z11cdsannotatemPv";
        // public static final String CDSAnnotate = "cdsannotate";
        public static final String CDSAnnotateType = "SPEC_ANALYSIS";
        public static final String IDType = "call_id_t";
@@ -81,13 +81,22 @@ public class CodeVariables {
        public static final String SPEC_TAG_CURRENT = "current";
        public static final String SPEC_TAG_NEXT = "next";
 
-       public static final String MODEL_MALLOC = "model_malloc";
 
        // Macro
        public static final String MACRO_ID = "__ID__";
        public static final String MACRO_COND = "__COND_SAT__";
        public static final String MACRO_RETURN = "__RET__";
        public static final String MACRO_ATOMIC_RETURN = "__ATOMIC_RET__";
+       
+       public static String CDSAnnotate(SemanticsChecker semantics) {
+               String LANG = semantics.getOption("LANG");
+               boolean isCPP = LANG == null || !LANG.equals("C");
+               if (isCPP) {
+                       return CDSAnnotate;
+               } else {
+                       return C_CDSAnnotate;
+               }
+       }
 
        public static void printCode(ArrayList<String> code) {
                for (int i = 0; i < code.size(); i++) {
@@ -163,8 +172,8 @@ public class CodeVariables {
                return type + " " + var + " = " + val + ";";
        }
 
-       private static String ANNOTATE(String structName) {
-               return CDSAnnotate + "(" + CDSAnnotateType + ", " + structName + ");";
+       private static String ANNOTATE(SemanticsChecker semantics, String structName) {
+               return CDSAnnotate(semantics) + "(" + CDSAnnotateType + ", " + structName + ");";
        }
 
        private static ArrayList<String> DEFINE_INFO_STRUCT(String interfaceName,
@@ -400,7 +409,7 @@ public class CodeVariables {
                newCode.add(STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno));
                newCode.add(ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_INIT));
                newCode.add(ASSIGN_TO_PTR(anno, "annotation", structName));
-               newCode.add(ANNOTATE(anno));
+               newCode.add(ANNOTATE(semantics, anno));
 
                newCode.add("");
                // Init user-defined variables
@@ -512,17 +521,24 @@ public class CodeVariables {
        }
 
        // Only generate the declaration of the wrapper, don't do any renaming
-       public static ArrayList<String> generateInterfaceWrapperDeclaration(
-                       SemanticsChecker semantics, InterfaceConstruct construct) {
-               ArrayList<String> newCode = new ArrayList<String>();
+//     public static ArrayList<String> generateInterfaceWrapperDeclaration(
+//                     SemanticsChecker semantics, InterfaceConstruct construct) {
+//             ArrayList<String> newCode = new ArrayList<String>();
+//             FunctionHeader header = getFunctionHeader(semantics, construct);
+//             newCode.add(COMMENT("Declaration of the wrapper"));
+//             String templateStr = header.getTemplateFullStr();
+//             newCode.add(templateStr);
+//             newCode.add(header.getFuncStr() + ";");
+//             newCode.add("");
+//
+//             return newCode;
+//     }
+       
+       public static ArrayList<String> generateInterfaceWrapperDeclaration(SemanticsChecker semantics, InterfaceConstruct construct) {
                FunctionHeader header = getFunctionHeader(semantics, construct);
-               newCode.add(COMMENT("Declaration of the wrapper"));
-               String templateStr = header.getTemplateFullStr();
-               newCode.add(templateStr);
-               newCode.add(header.getFuncStr() + ";");
-               newCode.add("");
-
-               return newCode;
+               ArrayList<String> declaration = new ArrayList<String>();
+               declaration.add(header.getRenamedHeader(SPEC_INTERFACE_WRAPPER).getDeclaration() + ";");
+               return declaration;
        }
 
        // Only generate the definition of the wrapper, don't do any renaming
@@ -548,7 +564,7 @@ public class CodeVariables {
                newCode.add(STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno));
                newCode.add(ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_INTERFACE_BEGIN));
                newCode.add(ASSIGN_TO_PTR(anno, "annotation", structName));
-               newCode.add(ANNOTATE(anno));
+               newCode.add(ANNOTATE(semantics, anno));
                // Call original renamed function
                if (header.returnType.equals("void")) {
                        newCode.add(header.getRenamedCall(SPEC_INTERFACE_WRAPPER) + ";");
@@ -571,7 +587,7 @@ public class CodeVariables {
                        newCode.add(STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno));
                        newCode.add(ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_HB_CONDITION));
                        newCode.add(ASSIGN_TO_PTR(anno, "annotation", structName));
-                       newCode.add(ANNOTATE(anno));
+                       newCode.add(ANNOTATE(semantics, anno));
                        newCode.add("}");
                        newCode.add("");
                }
@@ -586,7 +602,7 @@ public class CodeVariables {
                        newCode.add(STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno));
                        newCode.add(ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_HB_CONDITION));
                        newCode.add(ASSIGN_TO_PTR(anno, "annotation", structName));
-                       newCode.add(ANNOTATE(anno));
+                       newCode.add(ANNOTATE(semantics, anno));
                        newCode.add("");
                }
                // Interface end
@@ -615,7 +631,7 @@ public class CodeVariables {
                newCode.add(STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno));
                newCode.add(ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_INTERFACE_END));
                newCode.add(ASSIGN_TO_PTR(anno, "annotation", structName));
-               newCode.add(ANNOTATE(anno));
+               newCode.add(ANNOTATE(semantics, anno));
                // Return __RET__ if it's not void
                if (!header.returnType.equals("void")) {
                        newCode.add("return " + MACRO_RETURN + ";");
@@ -689,7 +705,7 @@ public class CodeVariables {
                newCode.add(ASSIGN_TO_PTR(anno, "type",
                                SPEC_ANNO_TYPE_POTENTIAL_CP_DEFINE));
                newCode.add(ASSIGN_TO_PTR(anno, "annotation", structName));
-               newCode.add(ANNOTATE(anno));
+               newCode.add(ANNOTATE(semantics, anno));
                newCode.add("}");
                return newCode;
        }
@@ -715,7 +731,7 @@ public class CodeVariables {
                newCode.add(STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno));
                newCode.add(ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_CP_DEFINE_CHECK));
                newCode.add(ASSIGN_TO_PTR(anno, "annotation", structName));
-               newCode.add(ANNOTATE(anno));
+               newCode.add(ANNOTATE(semantics, anno));
                newCode.add("}");
                return newCode;
        }
@@ -737,7 +753,7 @@ public class CodeVariables {
                newCode.add(STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno));
                newCode.add(ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_CP_DEFINE));
                newCode.add(ASSIGN_TO_PTR(anno, "annotation", structName));
-               newCode.add(ANNOTATE(anno));
+               newCode.add(ANNOTATE(semantics, anno));
                newCode.add("}");
                return newCode;
        }
index cb6da9d..0df12ac 100644 (file)
@@ -85,6 +85,19 @@ public class FunctionHeader {
                                new QualifiedName(newFullName), args);
                return newHeader;
        }
+       
+       // No support for template right now
+       public String getDeclaration() {
+               String res = returnType + " " + qualifiedName.fullName + "(";
+               if (args.size() >= 1) {
+                       res = res + args.get(0).type + " " + args.get(0).name;
+               }
+               for (int i = 1; i < args.size(); i++) {
+                       res = res + ", " + args.get(i).type + " " + args.get(i).name;
+               }
+               res = res + ")";
+               return res;
+       }
 
        public String getRenamedCall(String prefix) {
                String res = prefix + "_" + qualifiedName.fullName + "(";