fixed minor bugs
authorPeizhao Ou <peizhaoo@uci.edu>
Thu, 21 Nov 2013 02:25:42 +0000 (18:25 -0800)
committerPeizhao Ou <peizhaoo@uci.edu>
Thu, 21 Nov 2013 02:25:42 +0000 (18:25 -0800)
benchmark/ms-queue/my_queue.c
benchmark/ms-queue/my_queue.h
grammer/spec_compiler.jj
src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java
src/edu/uci/eecs/specCompiler/specExtraction/ConditionalInterface.java

index 634a051..3b1784b 100644 (file)
@@ -1,9 +1,63 @@
 #include <threads.h>
 #include <stdlib.h>
 #include <threads.h>
 #include <stdlib.h>
+#include <stdatomic.h>
 #include "librace.h"
 #include "model-assert.h"
 
 #include "librace.h"
 #include "model-assert.h"
 
-#include "my_queue.h"
+
+typedef unsigned long long pointer;
+typedef atomic_ullong pointer_t;
+
+#define MAKE_POINTER(ptr, count)       ((((pointer)count) << 32) | ptr)
+#define PTR_MASK 0xffffffffLL
+#define COUNT_MASK (0xffffffffLL << 32)
+
+static inline void set_count(pointer *p, unsigned int val) { *p = (*p & ~COUNT_MASK) | ((pointer)val << 32); }
+static inline void set_ptr(pointer *p, unsigned int val) { *p = (*p & ~PTR_MASK) | val; }
+static inline unsigned int get_count(pointer p) { return (p & COUNT_MASK) >> 32; }
+static inline unsigned int get_ptr(pointer p) { return p & PTR_MASK; }
+
+typedef struct node {
+       unsigned int value;
+       pointer_t next;
+} node_t;
+
+typedef struct {
+       pointer_t head;
+       pointer_t tail;
+       node_t nodes[MAX_NODES + 1];
+} queue_t;
+
+void init_queue(queue_t *q, int num_threads);
+
+#include <list>
+using namespace std;
+/**
+       @Begin
+       @Global_define:
+               @DeclareStruct:
+               typedef struct tag_elem {
+                       Tag id;
+                       unsigned int data;
+               } tag_elem_t;
+               
+               @DeclareVar:
+               list<tag_elem_t> __queue;
+               Tag tag;
+               @InitVar:
+                       __queue = list<tag_elem_t>();
+                       tag = 1; // Beginning of available id
+       @Happens_before:
+               # Only check the happens-before relationship according to the id of the
+               # commit_point_set. For commit_point_set that has same ID, A -> B means
+               # B happens after the previous A.
+               Enqueue -> Dequeue
+       @End
+*/
+
+
+int get_thread_num();
+
 
 #define relaxed memory_order_relaxed
 #define release memory_order_release
 
 #define relaxed memory_order_relaxed
 #define release memory_order_release
@@ -68,7 +122,7 @@ void init_queue(queue_t *q, int num_threads)
 
        /* Initialize each thread's free list with INITIAL_FREE pointers */
        /* The actual nodes are initialized with poison indexes */
 
        /* Initialize each thread's free list with INITIAL_FREE pointers */
        /* The actual nodes are initialized with poison indexes */
-       free_lists = malloc(num_threads * sizeof(*free_lists));
+       free_lists = (unsigned int**) malloc(num_threads * sizeof(*free_lists));
        for (i = 0; i < num_threads; i++) {
                for (j = 0; j < INITIAL_FREE; j++) {
                        free_lists[i][j] = 2 + i * MAX_FREELIST + j;
        for (i = 0; i < num_threads; i++) {
                for (j = 0; j < INITIAL_FREE; j++) {
                        free_lists[i][j] = 2 + i * MAX_FREELIST + j;
@@ -84,7 +138,16 @@ void init_queue(queue_t *q, int num_threads)
 
 /**
        @Begin
 
 /**
        @Begin
-       @Interface_define: Enqueue
+       @Interface: Enqueue
+       @Commit_point_set: Enqueue_Success_Point
+       @ID: tag++
+       @Action:
+               # __ID__ is an internal macro that refers to the id of the current
+               # interface call
+               tag_elem_t elem;
+               elem.id = __ID__;
+               elem.data = val;
+               __queue.push_back(elem);
        @End
 */
 void enqueue(queue_t *q, unsigned int val)
        @End
 */
 void enqueue(queue_t *q, unsigned int val)
@@ -123,7 +186,7 @@ void enqueue(queue_t *q, unsigned int val)
                                                &tail, value, release, release);
                                /**
                                        @Begin
                                                &tail, value, release, release);
                                /**
                                        @Begin
-                                       @Commit_point_define_check: __ATOMIC_RET__ == true
+                                       @Commit_point_define_check: commit_success == true
                                        @Label: Enqueue_Success_Point
                                        @End
                                */
                                        @Label: Enqueue_Success_Point
                                        @End
                                */
@@ -137,10 +200,16 @@ void enqueue(queue_t *q, unsigned int val)
                        release, release);
 }
 
                        release, release);
 }
 
-
 /**
        @Begin
 /**
        @Begin
-       @Interface_define: Dequeue
+       @Interface: Dequeue
+       @Commit_point_set: Dequeue_Success_Point
+       @ID: __queue.back().id
+       @Action:
+               unsigned int _Old_Val = __queue.front().data;
+               __queue.pop_front();
+       @Post_check:
+               _Old_Val == __RET__
        @End
 */
 unsigned int dequeue(queue_t *q)
        @End
 */
 unsigned int dequeue(queue_t *q)
@@ -177,7 +246,7 @@ unsigned int dequeue(queue_t *q)
                                                release, release);
                                /**
                                        @Begin
                                                release, release);
                                /**
                                        @Begin
-                                       @Commit_point_define_check: __ATOMIC_RET__ == true
+                                       @Commit_point_define_check: success == true
                                        @Label: Dequeue_Success_Point
                                        @End
                                */
                                        @Label: Dequeue_Success_Point
                                        @End
                                */
@@ -189,3 +258,86 @@ unsigned int dequeue(queue_t *q)
        reclaim(get_ptr(head));
        return value;
 }
        reclaim(get_ptr(head));
        return value;
 }
+
+
+
+#include <stdlib.h>
+#include <stdio.h>
+#include <threads.h>
+
+#include "my_queue.h"
+#include "model-assert.h"
+
+static int procs = 2;
+static queue_t *queue;
+static thrd_t *threads;
+static unsigned int *input;
+static unsigned int *output;
+static int num_threads;
+
+int get_thread_num()
+{
+       thrd_t curr = thrd_current();
+       int i;
+       for (i = 0; i < num_threads; i++)
+               if (curr.priv == threads[i].priv)
+                       return i;
+       MODEL_ASSERT(0);
+       return -1;
+}
+
+static void main_task(void *param)
+{
+       unsigned int val;
+       int pid = *((int *)param);
+
+       if (!pid) {
+               input[0] = 17;
+               enqueue(queue, input[0]);
+               output[0] = dequeue(queue);
+       } else {
+               input[1] = 37;
+               enqueue(queue, input[1]);
+               output[1] = dequeue(queue);
+       }
+}
+
+int user_main(int argc, char **argv)
+{
+       int i;
+       int *param;
+       unsigned int in_sum = 0, out_sum = 0;
+
+       queue = (queue_t*) calloc(1, sizeof(*queue));
+       MODEL_ASSERT(queue);
+
+       num_threads = procs;
+       threads = (thrd_t*) malloc(num_threads * sizeof(thrd_t));
+       param = (int*) malloc(num_threads * sizeof(*param));
+       input = (unsigned int*) calloc(num_threads, sizeof(*input));
+       output = (unsigned int*) calloc(num_threads, sizeof(*output));
+
+       init_queue(queue, num_threads);
+       for (i = 0; i < num_threads; i++) {
+               param[i] = i;
+               thrd_create(&threads[i], main_task, &param[i]);
+       }
+       for (i = 0; i < num_threads; i++)
+               thrd_join(threads[i]);
+
+       for (i = 0; i < num_threads; i++) {
+               in_sum += input[i];
+               out_sum += output[i];
+       }
+       for (i = 0; i < num_threads; i++)
+               printf("input[%d] = %u\n", i, input[i]);
+       for (i = 0; i < num_threads; i++)
+               printf("output[%d] = %u\n", i, output[i]);
+       MODEL_ASSERT(in_sum == out_sum);
+
+       free(param);
+       free(threads);
+       free(queue);
+
+       return 0;
+}
index 4161b33..cc10de4 100644 (file)
@@ -1,3 +1,6 @@
+#ifndef _MY_QUEUE_H
+#define _MY_QUEUE_H
+
 #include <stdatomic.h>
 
 #define MAX_NODES                      0xf
 #include <stdatomic.h>
 
 #define MAX_NODES                      0xf
@@ -27,6 +30,8 @@ typedef struct {
 
 void init_queue(queue_t *q, int num_threads);
 
 
 void init_queue(queue_t *q, int num_threads);
 
+#include <list>
+using namespace std;
 /**
        @Begin
        @Global_define:
 /**
        @Begin
        @Global_define:
@@ -34,18 +39,14 @@ void init_queue(queue_t *q, int num_threads);
                typedef struct tag_elem {
                        Tag id;
                        unsigned int data;
                typedef struct tag_elem {
                        Tag id;
                        unsigned int data;
-                       
-                       tag_elem(Tag _id, unsigned int _data) {
-                               id = _id;
-                               data = _data;
-                       }
                } tag_elem_t;
                } tag_elem_t;
+               
                @DeclareVar:
                @DeclareVar:
-               spec_queue<tag_elem_t> queue;
+               list<tag_elem_t> __queue;
                Tag tag;
                @InitVar:
                Tag tag;
                @InitVar:
-                       queue = spec_queue<tag_elem_t>();
-                       tag = Tag();
+                       __queue = list<tag_elem_t>();
+                       tag = 1; // Beginning of available id
        @Happens_before:
                # Only check the happens-before relationship according to the id of the
                # commit_point_set. For commit_point_set that has same ID, A -> B means
        @Happens_before:
                # Only check the happens-before relationship according to the id of the
                # commit_point_set. For commit_point_set that has same ID, A -> B means
@@ -60,11 +61,14 @@ void init_queue(queue_t *q, int num_threads);
        @Begin
        @Interface: Enqueue
        @Commit_point_set: Enqueue_Success_Point
        @Begin
        @Interface: Enqueue
        @Commit_point_set: Enqueue_Success_Point
-       @ID: __sequential.tag.getCurAndInc()
+       @ID: tag++
        @Action:
                # __ID__ is an internal macro that refers to the id of the current
                # interface call
        @Action:
                # __ID__ is an internal macro that refers to the id of the current
                # interface call
-               __sequential.queue.enqueue(tag_elem_t(__ID__, val));
+               tag_elem_t elem;
+               elem.id = __ID__;
+               elem.data = val;
+               __queue.push_back(elem);
        @End
 */
 void enqueue(queue_t *q, unsigned int val);
        @End
 */
 void enqueue(queue_t *q, unsigned int val);
@@ -73,12 +77,15 @@ void enqueue(queue_t *q, unsigned int val);
        @Begin
        @Interface: Dequeue
        @Commit_point_set: Dequeue_Success_Point
        @Begin
        @Interface: Dequeue
        @Commit_point_set: Dequeue_Success_Point
-       @ID: __sequential.queue.peak().tag
+       @ID: __queue.back().id
        @Action:
        @Action:
-               unsigned int _Old_Val = __sequential.queue.dequeue().data;
+               unsigned int _Old_Val = __queue.front().data;
+               __queue.pop_front();
        @Post_check:
                _Old_Val == __RET__
        @End
 */
 unsigned int dequeue(queue_t *q);
 int get_thread_num();
        @Post_check:
                _Old_Val == __RET__
        @End
 */
 unsigned int dequeue(queue_t *q);
 int get_thread_num();
+
+#endif
index 6a4f61b..24accc9 100644 (file)
@@ -392,6 +392,29 @@ SKIP : {
        <COLON: ":">
 |
        <DOUBLECOLON: "::">
        <COLON: ":">
 |
        <DOUBLECOLON: "::">
+|
+       <DOUBLELESSTHAN: "<<">
+|
+       <DOUBLEGREATERTHAN: ">>">
+|
+       <TRIPLEGREATERTHAN: ">>>">
+|
+       <PLUS_EQUALS: "+=">
+|
+       <MINUS_EQUALS: "-=">
+|
+       <TIMES_EQUALS: "*=">
+|
+       <DIVIDE_EQUALS: "/=">
+|
+       <MOD_EQUALS: "%=">
+|
+       <XOR_EQUALS: "^=">
+|
+       <OR_EQUALS: "|=">
+|
+       <AND_EQUALS: "&=">
+
 |
        <SEMI_COLON: ";">
 |
 |
        <SEMI_COLON: ";">
 |
@@ -667,6 +690,19 @@ ArrayList<String> C_CPP_CODE(ArrayList<String> headers) :
        t = <GREATER_EQUALS>    | t = <LESS_EQUALS> |
        t = <LOGICAL_EQUALS> | t = <NOT_EQUALS> | t = <LOGICAL_AND> | t = <LOGICAL_OR> | t = <XOR> |
        t = <QUESTION_MARK> | t = <COLON> | t = <DOUBLECOLON> |
        t = <GREATER_EQUALS>    | t = <LESS_EQUALS> |
        t = <LOGICAL_EQUALS> | t = <NOT_EQUALS> | t = <LOGICAL_AND> | t = <LOGICAL_OR> | t = <XOR> |
        t = <QUESTION_MARK> | t = <COLON> | t = <DOUBLECOLON> |
+       t = <DOUBLELESSTHAN> | 
+       t = <DOUBLEGREATERTHAN> |
+       t = <TRIPLEGREATERTHAN> | 
+
+       t = <PLUS_EQUALS> |
+       t = <MINUS_EQUALS> |
+       t = <TIMES_EQUALS> |
+       t = <DIVIDE_EQUALS> |
+       t = <MOD_EQUALS> |
+       t = <XOR_EQUALS> |
+       t = <OR_EQUALS> |
+       t = <AND_EQUALS> |
+
        (t = <SEMI_COLON> { newLine = true; } )
        | t = <STRING_LITERAL> | t = <CHARACTER_LITERAL> |
        t = <INTEGER_LITERAL> | t = <FLOATING_POINT_LITERAL> |
        (t = <SEMI_COLON> { newLine = true; } )
        | t = <STRING_LITERAL> | t = <CHARACTER_LITERAL> |
        t = <INTEGER_LITERAL> | t = <FLOATING_POINT_LITERAL> |
index 008ef66..39e3f3b 100644 (file)
@@ -206,12 +206,12 @@ 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(Environment.MODEL_CHECKER_TEST_DIR + "/backup_linuxrwlocks.c") };
-//              new File(homeDir + "/benchmark/linuxrwlocks/linuxrwlocks.c") };
+//                             new File(Environment.MODEL_CHECKER_TEST_DIR + "/backup_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/my_queue.c") };
 //             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();
index 4abd569..f98250d 100644 (file)
@@ -545,6 +545,19 @@ public class CodeVariables {
                        newCode.add("}");
                        newCode.add("");
                }
                        newCode.add("}");
                        newCode.add("");
                }
+               // Also add the true condition if any
+               if (semantics.containsConditionalInterface(new ConditionalInterface(interfaceName, ""))) {
+                       structName = "hb_condition";
+                       newCode.add(STRUCT_NEW_DECLARE_DEFINE(ANNO_HB_CONDITION, structName));
+                       newCode.add(ASSIGN_TO_PTR(structName, "interface_num", interfaceNum));
+                       newCode.add(ASSIGN_TO_PTR(structName, "hb_condition_num", "0"));
+                       anno = "annotation_hb_condition";
+                       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("");
+               }
                // Interface end
                String infoStructType = null, infoName = null;
                if (!header.returnType.equals("void") || header.args.size() > 0) {
                // Interface end
                String infoStructType = null, infoName = null;
                if (!header.returnType.equals("void") || header.args.size() > 0) {
@@ -620,6 +633,7 @@ public class CodeVariables {
                newCode.add(COMMENT("Include redundant headers"));
                newCode.add(INCLUDE(HEADER_STDINT));
                newCode.add(INCLUDE(HEADER_CDSANNOTATE));
                newCode.add(COMMENT("Include redundant headers"));
                newCode.add(INCLUDE(HEADER_STDINT));
                newCode.add(INCLUDE(HEADER_CDSANNOTATE));
+               newCode.add(INCLUDE(HEADER_SPECANNOTATION));
                newCode.add("");
                // Add annotation
                newCode.add("if (" + construct.condition + ") {");
                newCode.add("");
                // Add annotation
                newCode.add("if (" + construct.condition + ") {");
index ae53d3b..6073230 100644 (file)
@@ -100,6 +100,21 @@ public class SemanticsChecker {
        public HashMap<ConditionalInterface, HashSet<ConditionalInterface>> getHBConditions() {
                return this.hbConditions;
        }
        public HashMap<ConditionalInterface, HashSet<ConditionalInterface>> getHBConditions() {
                return this.hbConditions;
        }
+       
+       /**
+        * Check if the conditional interface is in the HB checking list
+        * @param condInterface
+        * @return
+        */
+       public boolean containsConditionalInterface(ConditionalInterface condInterface) {
+               if (hbConditions.containsKey(condInterface))
+                       return true;
+               for (ConditionalInterface key : hbConditions.keySet()) {
+                       if (hbConditions.get(key).contains(condInterface))
+                               return true;
+               }
+               return false;
+       }
 
        public String getOption(String key) {
                return options.get(key);
 
        public String getOption(String key) {
                return options.get(key);
index 791a205..2ef95a6 100644 (file)
@@ -3,24 +3,25 @@ package edu.uci.eecs.specCompiler.specExtraction;
 public class ConditionalInterface {
        public final String interfaceName;
        public final String hbConditionLabel;
 public class ConditionalInterface {
        public final String interfaceName;
        public final String hbConditionLabel;
-       
+
        public ConditionalInterface(String interfaceName, String hbConditionLabel) {
                this.interfaceName = interfaceName;
                this.hbConditionLabel = hbConditionLabel;
        }
        public ConditionalInterface(String interfaceName, String hbConditionLabel) {
                this.interfaceName = interfaceName;
                this.hbConditionLabel = hbConditionLabel;
        }
-       
-       public boolean equals(ConditionalInterface other) {
+
+       public boolean equals(Object other) {
                if (!(other instanceof ConditionalInterface))
                        return false;
                ConditionalInterface another = (ConditionalInterface) other;
                if (!(other instanceof ConditionalInterface))
                        return false;
                ConditionalInterface another = (ConditionalInterface) other;
-               return another.interfaceName.equals(interfaceName) && 
-                               another.hbConditionLabel.equals(hbConditionLabel);
+               return another.interfaceName.equals(interfaceName)
+                               && (another.hbConditionLabel.equals(hbConditionLabel) || another.hbConditionLabel
+                                               .equals(""));
        }
        }
-       
+
        public int hashCode() {
                return interfaceName.hashCode() << 5 ^ hbConditionLabel.hashCode();
        }
        public int hashCode() {
                return interfaceName.hashCode() << 5 ^ hbConditionLabel.hashCode();
        }
-       
+
        public String toString() {
                if (hbConditionLabel.equals(""))
                        return interfaceName + "(true)";
        public String toString() {
                if (hbConditionLabel.equals(""))
                        return interfaceName + "(true)";