From f7d72aaac976fe732a65c775855ee2e588ba847f Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Fri, 13 Dec 2013 15:38:29 -0800 Subject: [PATCH] fixing --- benchmark/ms-queue/main.c | 5 ++ benchmark/ms-queue/my_queue.c | 21 +++-- benchmark/ms-queue/my_queue.h | 4 +- .../codeGenerator/CodeGenerator.java | 9 +- .../codeGenerator/CodeVariables.java | 82 +++++++++++++------ 5 files changed, 81 insertions(+), 40 deletions(-) diff --git a/benchmark/ms-queue/main.c b/benchmark/ms-queue/main.c index b541b01..8fc3136 100644 --- a/benchmark/ms-queue/main.c +++ b/benchmark/ms-queue/main.c @@ -41,6 +41,11 @@ static void main_task(void *param) int user_main(int argc, char **argv) { + /** + @Begin + @Entry_point + @End + */ int i; int *param; unsigned int in_sum = 0, out_sum = 0; diff --git a/benchmark/ms-queue/my_queue.c b/benchmark/ms-queue/my_queue.c index 7d19e02..11cd258 100644 --- a/benchmark/ms-queue/my_queue.c +++ b/benchmark/ms-queue/my_queue.c @@ -107,20 +107,19 @@ void enqueue(queue_t *q, unsigned int val) 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); + /** + @Begin + @Commit_point_define_check: success = true + @Label: Enqueue_Success_Point + @End + */ } 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, + atomic_compare_exchange_strong_explicit(&q->tail, &tail, value, release, release); - /** - @Begin - @Commit_point_define_check: commit_success == true - @Label: Enqueue_Success_Point - @End - */ thrd_yield(); } } @@ -155,6 +154,12 @@ unsigned int dequeue(queue_t *q) MODEL_ASSERT(get_ptr(next) != POISON_IDX); if (get_ptr(next) == 0) { // NULL + /** + @Begin + @Commit_point_define_check: true + @Label: Dequeue_Empty_Point + @End + */ return 0; // NULL } atomic_compare_exchange_strong_explicit(&q->tail, diff --git a/benchmark/ms-queue/my_queue.h b/benchmark/ms-queue/my_queue.h index 6f4685d..d499929 100644 --- a/benchmark/ms-queue/my_queue.h +++ b/benchmark/ms-queue/my_queue.h @@ -47,7 +47,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*) malloc(sizeof(tag_elem_t)); + tag_elem_t *e = (tag_elem_t*) MODEL_MALLOC(sizeof(tag_elem_t)); e->id = id; e->data = data; return e; @@ -91,7 +91,7 @@ void enqueue(queue_t *q, unsigned int val); /** @Begin @Interface: Dequeue - @Commit_point_set: Dequeue_Success_Point + @Commit_point_set: Dequeue_Success_Point | Dequeue_Empty_Point @ID: get_id(back(__queue)) @Action: unsigned int _Old_Val = get_data(front(__queue)); diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java index b23ec8c..74fd32c 100644 --- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java @@ -246,14 +246,15 @@ public class CodeGenerator { File[] srcFiles = { // new File(Environment.MODEL_CHECKER_TEST_DIR + // "/backup_linuxrwlocks.c") }; - new File(homeDir + "/benchmark/linuxrwlocks/linuxrwlocks.c") - }; +// 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/my_queue.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/test/test.c") }; 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 c87e688..b79d38b 100644 --- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java @@ -26,6 +26,7 @@ public class CodeVariables { public static final String HEADER_STDLIB = ""; public static final String HEADER_THREADS = ""; public static final String HEADER_STDINT = ""; + public static final String HEADER_MODELMEMORY = ""; public static final String ThreadIDType = "thrd_t"; public static final String GET_THREAD_ID = "thrd_current"; public static final String BOOLEAN = "bool"; @@ -42,7 +43,7 @@ public class CodeVariables { public static final String IDType = "call_id_t"; public static final String SPEC_ANNO_TYPE = "spec_anno_type"; - public static final String SPEC_ANNO_TYPE_FUNC_TABLE_INIT = "FUNC_TABLE_INIT"; + public static final String SPEC_ANNO_TYPE_INIT = "INIT"; public static final String SPEC_ANNO_TYPE_HB_INIT = "HB_INIT"; public static final String SPEC_ANNO_TYPE_INTERFACE_BEGIN = "INTERFACE_BEGIN"; public static final String SPEC_ANNO_TYPE_HB_CONDITION = "HB_CONDITION"; @@ -54,7 +55,7 @@ public class CodeVariables { public static final String SPEC_ANNOTATION_FIELD_TYPE = "type"; public static final String SPEC_ANNOTATION_FIELD_ANNO = "annotation"; - public static final String ANNO_FUNC_TABLE_INIT = "anno_func_table_init"; + public static final String ANNO_INIT = "anno_init"; public static final String ANNO_HB_INIT = "anno_hb_init"; public static final String ANNO_INTERFACE_BEGIN = "anno_interface_begin"; public static final String ANNO_INTERFACE_END = "anno_interface_end"; @@ -77,6 +78,8 @@ public class CodeVariables { public static final String SPEC_TAG = "spec_tag"; 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__"; @@ -194,8 +197,9 @@ public class CodeVariables { InterfaceConstruct construct, FunctionHeader header) { String interfaceName = construct.name; ArrayList code = new ArrayList(); - code.add("inline static bool " + interfaceName + "_check_action(void *info, " - + IDType + " " + MACRO_ID + ") {"); + code.add("inline static bool " + interfaceName + + "_check_action(void *info, " + IDType + " " + MACRO_ID + + ") {"); code.add(DECLARE("bool", "check_passed")); // Read info struct if (!header.returnType.equals("void") || header.args.size() != 0) { @@ -299,6 +303,7 @@ public class CodeVariables { newCode.add(""); // Other necessary headers newCode.add(INCLUDE(HEADER_STDLIB)); + newCode.add(INCLUDE(HEADER_MODELMEMORY)); newCode.add(INCLUDE(HEADER_STDINT)); newCode.add(INCLUDE(HEADER_CDSANNOTATE)); newCode.add(INCLUDE(HEADER_COMMON)); @@ -366,6 +371,8 @@ public class CodeVariables { .toString(semantics.interfaceName2Construct.size()); newCode.add(DEFINE("INTERFACE_SIZE", interfaceSize)); newCode.add(DECLARE("void**", "func_ptr_table")); + // Happens-before initialization rules + newCode.add(DECLARE(ANNO_HB_INIT + "**", "hb_init_table")); newCode.add(""); newCode.add(COMMENT("Define function for sequential code initialization")); @@ -382,22 +389,28 @@ public class CodeVariables { newCode.add(ASSIGN("func_ptr_table[2 * " + interfaceNum + " + 1]", "(void*) &" + interfaceName + "_check_action")); } - newCode.add(""); - // Init user-defined variables - newCode.addAll(construct.code.initVar); - // Pass function table info - newCode.add(COMMENT("Pass function table info")); - String structName = "anno_func_table_init", anno = "func_init"; - newCode.add(STRUCT_NEW_DECLARE_DEFINE(ANNO_FUNC_TABLE_INIT, structName)); - newCode.add(ASSIGN_TO_PTR(structName, "size", "INTERFACE_SIZE")); - newCode.add(ASSIGN_TO_PTR(structName, "table", "func_ptr_table")); + // Init Happens-before rules table + newCode.addAll(generateHBInitAnnotation(semantics)); + + // Pass init info, including function table info & HB rules + newCode.add(COMMENT("Pass init info, including function table info & HB rules")); + String structName = "anno_init", anno = "init"; + newCode.add(STRUCT_NEW_DECLARE_DEFINE(ANNO_INIT, structName)); + newCode.add(ASSIGN_TO_PTR(structName, "func_table", "func_ptr_table")); + newCode.add(ASSIGN_TO_PTR(structName, "func_table_size", + "INTERFACE_SIZE")); + newCode.add(ASSIGN_TO_PTR(structName, "hb_init_table", "hb_init_table")); + newCode.add(ASSIGN_TO_PTR(structName, "hb_init_table_size", + "HB_INIT_TABLE_SIZE")); newCode.add(STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno)); - newCode.add(ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_FUNC_TABLE_INIT)); + newCode.add(ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_INIT)); newCode.add(ASSIGN_TO_PTR(anno, "annotation", structName)); newCode.add(ANNOTATE(anno)); - // Pass Happens-before relationship - newCode.addAll(generateHBInitAnnotation(semantics)); + newCode.add(""); + // Init user-defined variables + newCode.addAll(construct.code.initVar); + newCode.add("}"); newCode.add(COMMENT("End of Global construct generation in class")); @@ -421,6 +434,7 @@ public class CodeVariables { String templateDecl = semantics.getTemplateFullStr(); if (templateList == null) { newCode.add(DECLARE("void**", varPrefix + "func_ptr_table")); + newCode.add(DECLARE("void**", varPrefix + "hb_init_table")); for (int i = 0; i < construct.code.declareVar.size(); i++) { VariableDeclaration varDecl = construct.code.declareVar.get(i); newCode.add(DECLARE(varDecl.type, varPrefix + varDecl.name)); @@ -428,6 +442,8 @@ public class CodeVariables { } else { newCode.add(templateDecl); newCode.add(DECLARE("void**", varPrefix + "func_ptr_table")); + newCode.add(templateDecl); + newCode.add(DECLARE("void**", varPrefix + "hb_init_table")); for (int i = 0; i < construct.code.declareVar.size(); i++) { VariableDeclaration varDecl = construct.code.declareVar.get(i); newCode.add(templateDecl); @@ -440,12 +456,13 @@ public class CodeVariables { private static ArrayList generateHBInitAnnotation( SemanticsChecker semantics) { ArrayList newCode = new ArrayList(); + int hbConditionInitIdx = 0; for (ConditionalInterface left : semantics.getHBConditions().keySet()) { for (ConditionalInterface right : semantics.getHBConditions().get( left)) { String structVarName = "hbConditionInit" + hbConditionInitIdx; - String annotationVarName = "hb_init" + hbConditionInitIdx; + // String annotationVarName = "hb_init" + hbConditionInitIdx; hbConditionInitIdx++; String interfaceNumBefore = Integer .toString(semantics.interface2Num @@ -469,20 +486,32 @@ public class CodeVariables { newCode.add(ASSIGN_TO_PTR(structVarName, "hb_condition_num_after", hbLabelNumAfter)); - newCode.add(STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, - annotationVarName)); - newCode.add(ASSIGN_TO_PTR(annotationVarName, - SPEC_ANNOTATION_FIELD_TYPE, SPEC_ANNO_TYPE_HB_INIT)); - newCode.add(ASSIGN_TO_PTR(annotationVarName, - SPEC_ANNOTATION_FIELD_ANNO, structVarName)); - newCode.add(ANNOTATE(annotationVarName)); + // newCode.add(STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, + // annotationVarName)); + // newCode.add(ASSIGN_TO_PTR(annotationVarName, + // SPEC_ANNOTATION_FIELD_TYPE, SPEC_ANNO_TYPE_HB_INIT)); + // newCode.add(ASSIGN_TO_PTR(annotationVarName, + // SPEC_ANNOTATION_FIELD_ANNO, structVarName)); + // newCode.add(ANNOTATE(annotationVarName)); } } + // Init hb_init_table + newCode.add(COMMENT("Init hb_init_table")); + newCode.add(ASSIGN("hb_init_table", "(" + ANNO_HB_INIT + + "**) malloc(sizeof(" + ANNO_HB_INIT + "*) * " + + hbConditionInitIdx + ")")); + // Define HB_INIT_TABLE_SIZE + newCode.add(DEFINE("HB_INIT_TABLE_SIZE", + Integer.toString(hbConditionInitIdx))); + for (int i = 0; i < hbConditionInitIdx; i++) { + newCode.add(ASSIGN("hb_init_table[" + i + "]", "hbConditionInit" + + i)); + } return newCode; } public static ArrayList generateEntryPointInitCall() { - ArrayList newCode = new ArrayList(1); + ArrayList newCode = new ArrayList(); newCode.add("__sequential_init();"); return newCode; } @@ -508,6 +537,7 @@ public class CodeVariables { String interfaceName = construct.name; // Generate necessary header file (might be redundant but never mind) newCode.add(INCLUDE(HEADER_STDLIB)); + newCode.add(INCLUDE(HEADER_MODELMEMORY)); newCode.add(INCLUDE(HEADER_CDSANNOTATE)); newCode.add(INCLUDE(HEADER_SPECANNOTATION)); newCode.add(INCLUDE(HEADER_SPEC_LIB)); @@ -515,7 +545,7 @@ public class CodeVariables { FunctionHeader header = getFunctionHeader(semantics, construct); String interfaceNum = Integer.toString(semantics.interface2Num .get(construct.name)); - + newCode.add(header.getTemplateFullStr()); newCode.add(header.getFuncStr() + " {"); // Wrapper function body -- 2.34.1