fixed rcu

diff --git a/benchmark/linuxrwlocks/linuxrwlocks.c b/benchmark/linuxrwlocks/linuxrwlocks.c
index 142e3766cf350e504a79079b3d80b8d14a9c8faf..c96eb956e9728b73bb443c55530508ae62e5a869 100644 (file)
--- a/benchmark/linuxrwlocks/linuxrwlocks.c
+++ b/benchmark/linuxrwlocks/linuxrwlocks.c
@@ -42,6 +42,8 @@ typedef union {
 
 /**
        @Begin
 
 /**
        @Begin

+       @Options:
+               LANG = C;

        @Global_define:
                @DeclareVar:
                        bool writer_lock_acquired;
        @Global_define:
                @DeclareVar:
                        bool writer_lock_acquired;

diff --git a/benchmark/ms-queue/my_queue.h b/benchmark/ms-queue/my_queue.h
index d4999299351daa98109cf96b938cce0cdfeb1fd7..ff3d42d4697354fa96985e9f457425a1957d3fdc 100644 (file)
--- a/benchmark/ms-queue/my_queue.h
+++ b/benchmark/ms-queue/my_queue.h
@@ -32,6 +32,8 @@ void init_queue(queue_t *q, int num_threads);
 
 /**
        @Begin
 
 /**
        @Begin

+       @Options:
+               LANG = C;

        @Global_define:
                @DeclareStruct:
                typedef struct tag_elem {
        @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 = 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;
                                e->id = id;
                                e->data = data;
                                return e;

diff --git a/benchmark/read-copy-update/rcu.cc b/benchmark/read-copy-update/rcu.cc
index 75f470b2ee53b5c764d06cb3bb7c887b649957f0..8aad9d19b56be3bfb439156f84e15ff08ec10690 100644 (file)
--- a/benchmark/read-copy-update/rcu.cc
+++ b/benchmark/read-copy-update/rcu.cc
@@ -6,8 +6,6 @@
 
 #include "librace.h"
 
 
 #include "librace.h"
 

-using namespace std;
-

 /**
        This is an example about how to specify the correctness of the
        read-copy-update synchronization mechanism.
 /**
        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) {
                
                @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;
                                && 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;
        */
        
        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;
        Data *data_init = (Data*) malloc(sizeof(Data));
        data_init->data1 = 1;
        data_init->data2 = 2;

diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
index e68c27d666f4fd29d3c4ebdf90e0ebd71df254c4..84ba735ada5970d527349bbaa3fb703a3ecc4af4 100644 (file)
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
@@ -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.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;
 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);
                                                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
                        // 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);
                        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);
                }
                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;
                        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);
                        // 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
                        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 = {
        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();
                 new File(homeDir + "/benchmark/read-copy-update/rcu.cc") };
                CodeGenerator gen = new CodeGenerator(srcFiles);
                gen.generateCode();

diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
index a97edc34e2aa968452e886ed83a0411b924721dd..aeace485b78e6c8453c9a7bfee3d1d9d3f07010f 100644 (file)
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
@@ -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 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";
        // 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 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__";
 
        // 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++) {
 
        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 + ";";
        }
 
                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,
        }
 
        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(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
 
                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
        }
 
        // 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);
                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
        }
 
        // 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(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) + ";");
                // 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(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("");
                }
                        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(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
                        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(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 + ";");
                // 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(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;
        }
                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(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;
        }
                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(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;
        }
                newCode.add("}");
                return newCode;
        }

diff --git a/src/edu/uci/eecs/specCompiler/specExtraction/FunctionHeader.java b/src/edu/uci/eecs/specCompiler/specExtraction/FunctionHeader.java
index cb6da9dbae743a229bbebc8fe2ffc0dd34be5be6..0df12ace576c87ef70a5d8eec43fe733f2e85656 100644 (file)
--- a/src/edu/uci/eecs/specCompiler/specExtraction/FunctionHeader.java
+++ b/src/edu/uci/eecs/specCompiler/specExtraction/FunctionHeader.java
@@ -85,6 +85,19 @@ public class FunctionHeader {
                                new QualifiedName(newFullName), args);
                return newHeader;
        }
                                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 + "(";
 
        public String getRenamedCall(String prefix) {
                String res = prefix + "_" + qualifiedName.fullName + "(";