fixing

diff --git a/benchmark/ms-queue/main.c b/benchmark/ms-queue/main.c
index b541b010c2837d04e798b6db73a2eb4d3dbc4f31..8fc31361cbe47eb29ee72a52bedd9ab6f2d11f7f 100644 (file)
--- 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)
 {
 
 int user_main(int argc, char **argv)
 {

+       /**
+               @Begin
+               @Entry_point
+               @End
+       */

        int i;
        int *param;
        unsigned int in_sum = 0, out_sum = 0;
        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 7d19e02f678ec2c53e828a606f26b0d954630037..11cd25845ed20574d8877274a0b9034404cd8b7a 100644 (file)
--- 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);
                                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);
                        }
                        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);
                                                &tail, value, release, release);

-                               /**
-                                       @Begin
-                                       @Commit_point_define_check: commit_success == true
-                                       @Label: Enqueue_Success_Point
-                                       @End
-                               */

                                thrd_yield();
                        }
                }
                                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
                                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,
                                        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 6f4685de6295b3deb90690f9714f755b3e2e2f30..d4999299351daa98109cf96b938cce0cdfeb1fd7 100644 (file)
--- 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 = 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;
                                e->id = id;
                                e->data = data;
                                return e;


@@ -91,7 +91,7 @@ void enqueue(queue_t *q, unsigned int val);
 /**
        @Begin
        @Interface: Dequeue
 /**
        @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));
        @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 b23ec8c2818585a01c3b35b9bcab0f45aa5d042e..74fd32c9d09876e4593c8070e7f3b01f629fe592 100644 (file)
--- 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") };
                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/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();
                // 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 c87e6883681c5196185fc1962a006bdc555cb514..b79d38b962202a170664a65a696e99bd579325b9 100644 (file)
--- 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 = "<stdlib.h>";
        public static final String HEADER_THREADS = "<threads.h>";
        public static final String HEADER_STDINT = "<stdint.h>";
        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";
        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 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";
        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 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";
        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 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__";
 
        // 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>();
                        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) {
                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("");
                // 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));
                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"));
                                .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"));
 
                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(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(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));
 
                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"));
 
                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"));
                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));
                        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"));
                } 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);
                        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>();
        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;
                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
                                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(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() {
                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;
        }
                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));
                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));
                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));
                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
                newCode.add(header.getTemplateFullStr());
                newCode.add(header.getFuncStr() + " {");
                // Wrapper function body