From: Peizhao Ou Date: Wed, 15 Jan 2014 19:18:38 +0000 (-0800) Subject: fixed rcu X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=c9d0845c129ac0c7d8ced2e04677006c333b2c73;hp=2aaf563ff863189d7774f01dc86c19d69c12c930;p=cdsspec-compiler.git fixed rcu --- diff --git a/benchmark/linuxrwlocks/linuxrwlocks.c b/benchmark/linuxrwlocks/linuxrwlocks.c index 142e376..c96eb95 100644 --- a/benchmark/linuxrwlocks/linuxrwlocks.c +++ b/benchmark/linuxrwlocks/linuxrwlocks.c @@ -42,6 +42,8 @@ typedef union { /** @Begin + @Options: + LANG = C; @Global_define: @DeclareVar: bool writer_lock_acquired; diff --git a/benchmark/ms-queue/my_queue.h b/benchmark/ms-queue/my_queue.h index d499929..ff3d42d 100644 --- 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 + @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; diff --git a/benchmark/read-copy-update/rcu.cc b/benchmark/read-copy-update/rcu.cc index 75f470b..8aad9d1 100644 --- a/benchmark/read-copy-update/rcu.cc +++ b/benchmark/read-copy-update/rcu.cc @@ -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; @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; diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java index e68c27d..84ba735 100644 --- 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.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()); } 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(); + 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 additions = codeAdditions.get(file); - + if (additions.size() == 0) // Simply do nothing continue; ArrayList content = _semantics.srcFilesInfo.get(file).content; @@ -242,7 +245,8 @@ public class CodeGenerator { // Insert generated annotation to the source files ArrayList newContent = insertAnnotation2Src(additions, content); - ArrayList finalContent = new ArrayList(headerCode.size() + newContent.size()); + ArrayList finalContent = new ArrayList( + 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(); diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java index a97edc3..aeace48 100644 --- 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 = ""; public static final String HEADER_SPECANNOTATION = ""; public static final String HEADER_CDSTRACE = ""; - // 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 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 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 generateInterfaceWrapperDeclaration( - SemanticsChecker semantics, InterfaceConstruct construct) { - ArrayList newCode = new ArrayList(); +// public static ArrayList generateInterfaceWrapperDeclaration( +// SemanticsChecker semantics, InterfaceConstruct construct) { +// ArrayList newCode = new ArrayList(); +// 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 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 declaration = new ArrayList(); + 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; } diff --git a/src/edu/uci/eecs/specCompiler/specExtraction/FunctionHeader.java b/src/edu/uci/eecs/specCompiler/specExtraction/FunctionHeader.java index cb6da9d..0df12ac 100644 --- 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; } + + // 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 + "(";