fixing
authorPeizhao Ou <peizhaoo@uci.edu>
Fri, 13 Dec 2013 23:38:29 +0000 (15:38 -0800)
committerPeizhao Ou <peizhaoo@uci.edu>
Fri, 13 Dec 2013 23:38:29 +0000 (15:38 -0800)
benchmark/ms-queue/main.c
benchmark/ms-queue/my_queue.c
benchmark/ms-queue/my_queue.h
src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java

index b541b01..8fc3136 100644 (file)
@@ -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;
index 7d19e02..11cd258 100644 (file)
@@ -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,
index 6f4685d..d499929 100644 (file)
@@ -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));
index b23ec8c..74fd32c 100644 (file)
@@ -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();
index c87e688..b79d38b 100644 (file)
@@ -26,6 +26,7 @@ public class CodeVariables {
        public static final String HEADER_STDLIB = "<stdlib.h>";
        public static final String HEADER_THREADS = "<threads.h>";
        public static final String HEADER_STDINT = "<stdint.h>";
+       public static final String HEADER_MODELMEMORY = "<model_memory.h>";
        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<String> code = new ArrayList<String>();
-               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<String> generateHBInitAnnotation(
                        SemanticsChecker semantics) {
                ArrayList<String> newCode = new ArrayList<String>();
+
                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<String> generateEntryPointInitCall() {
-               ArrayList<String> newCode = new ArrayList<String>(1);
+               ArrayList<String> newCode = new ArrayList<String>();
                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