try to generate in-place code
authorPeizhao Ou <peizhaoo@uci.edu>
Wed, 16 Oct 2013 19:47:41 +0000 (12:47 -0700)
committerPeizhao Ou <peizhaoo@uci.edu>
Wed, 16 Oct 2013 19:47:41 +0000 (12:47 -0700)
benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h
benchmark/linuxrwlocks/linuxrwlocks.c
benchmark/ms-queue/my_queue.c
grammer/spec-compiler.jj
src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
src/edu/uci/eecs/specCompiler/specExtraction/GlobalConstruct.java
src/edu/uci/eecs/specCompiler/specExtraction/SequentialDefineSubConstruct.java [new file with mode: 0644]

index 0e7031e..89efb8f 100644 (file)
@@ -84,26 +84,30 @@ class cliffc_hashtable {
        
                @Begin
                @Global_define:
-
-                       spec_hashtable<TypeK, TypeV*> __map;
-                       spec_hashtable<TypeK, Tag> __id_map;
-                       Tag __tag;
-
-                       static bool _val_equals(TypeV *ptr1, TypeV *ptr2) {
+                       @DeclareVar:
+                       spec_hashtable<TypeK, TypeV*> map;
+                       spec_hashtable<TypeK, Tag> id_map;
+                       Tag tag;
+                       @InitVar:
+                               map = spec_hashtable<TypeK, TypeV*>();
+                               id_map = spec_hashtable<TypeK, TypeV*>();
+                               tag = Tag();
+                       @DefineFunc:
+                       static bool equals_val(TypeV *ptr1, TypeV *ptr2) {
                                // ...
                        }
                        
                        # Update the tag for the current key slot if the corresponding tag
                        # is NULL, otherwise just return that tag. It will update the next
                        # available tag too if it requires a new tag for that key slot.
-                       static Tag _getKeyTag(TypeK &key) {
-                               if (__id_map.get(key) == NULL) {
+                       static Tag getKeyTag(TypeK &key) {
+                               if (id_map.get(key) == NULL) {
                                        Tag cur_tag = tag.current();
-                                       __id_map.put(key, cur_tag);
-                                       __tag.next();
+                                       id_map.put(key, cur_tag);
+                                       tag.next();
                                        return cur_tag;
                                } else {
-                                       return __id_map.get(key);
+                                       return id_map.get(key);
                                }
                        }
                
@@ -360,11 +364,11 @@ friend class CHM;
                @Begin
                @Interface: Get
                @Commit_point_set: Read_Val_Point1 | Read_Val_Point2 | Read_Val_Point3
-               @ID: _getKeyTag(key)
+               @ID: __sequential.getKeyTag(key)
                @Action:
-                       @DefineVar: TypeV *_Old_Val = __map.get(key)
+                       @DefineVar: TypeV *_Old_Val = __sequential.map.get(key)
                @Post_check:
-                       _equals_val(_Old_Val, __RET__)
+                       __sequential.equals_val(_Old_Val, __RET__)
                @End
        */
        shared_ptr<TypeV> get(TypeK& key) {
@@ -381,13 +385,13 @@ friend class CHM;
                @Begin
                @Interface: Put
                @Commit_point_set: Write_Val_Point
-               @ID: _getKeyTag(key)
+               @ID: __sequential.getKeyTag(key)
                @Action:
                        # Remember this old value at checking point
-                       @DefineVar: TypeV *_Old_Val = __map.get(key)
-                       @Code: __map.put(key, &val);
+                       @DefineVar: TypeV *_Old_Val = __sequential.map.get(key)
+                       @Code: __sequential.map.put(key, &val);
                @Post_check:
-                       _equals_val(__RET__, _Old_Val)
+                       __sequential.equals_val(__RET__, _Old_Val)
                @End
        */
        shared_ptr<TypeV> put(TypeK& key, TypeV& val) {
@@ -399,17 +403,17 @@ friend class CHM;
                @Interface: PutIfAbsent
                @Commit_point_set:
                        Write_Val_Point | PutIfAbsent_Fail_Point
-               @Condition: __map.get(key) == NULL
+               @Condition: __sequential.map.get(key) == NULL
                @HB_condition:
                        COND_PutIfAbsentSucc :: __RET__ == NULL
-               @ID: _getKeyTag(key)
+               @ID: __sequential.getKeyTag(key)
                @Action:
-                       @DefineVar: TypeV *_Old_Val = __map.get(key)
+                       @DefineVar: TypeV *_Old_Val = __sequential.map.get(key)
                        @Code:
-                       if (COND_SAT)
-                               __map.put(key, &value);
+                       if (__COND_SAY__)
+                               __sequential.map.put(key, &value);
                @Post_check:
-                       COND_SAT ? __RET__ == NULL : _equals_val(_Old_Val, __RET__) 
+                       __COND_SAY__ ? __RET__ == NULL : __sequential.equals_val(_Old_Val, __RET__) 
                @End
        */
        shared_ptr<TypeV> putIfAbsent(TypeK& key, TypeV& value) {
@@ -420,12 +424,12 @@ friend class CHM;
                @Begin
                @Interface: RemoveAny
                @Commit_point_set: Write_Val_Point
-               @ID: _getKeyTag(key)
+               @ID: __sequential.getKeyTag(key)
                @Action:
-                       @DefineVar: TypeV *_Old_Val = __map.get(key)
-                       @Code: __map.put(key, NULL);
+                       @DefineVar: TypeV *_Old_Val = __sequential.map.get(key)
+                       @Code: __sequential.map.put(key, NULL);
                @Post_check:
-                       _equals_val(__RET__, _Old_Val)
+                       __sequential.equals_val(__RET__, _Old_Val)
                @End
        */
        shared_ptr<TypeV> remove(TypeK& key) {
@@ -438,16 +442,16 @@ friend class CHM;
                @Commit_point_set:
                        Write_Val_Point | RemoveIfMatch_Fail_Point
                @Condition:
-                       _equals_val(__map.get(key), &val)
+                       __sequential.equals_val(__sequential.map.get(key), &val)
                @HB_condition:
                        COND_RemoveIfMatchSucc :: __RET__ == true
-               @ID: _getKeyTag(key)
+               @ID: __sequential.getKeyTag(key)
                @Action:
                        @Code:
-                       if (COND_SAT)
-                               __map.put(key, NULL);
+                       if (__COND_SAY__)
+                               __sequential.map.put(key, NULL);
                @Post_check:
-                       COND_SAT ? __RET__ : !__RET__
+                       __COND_SAY__ ? __RET__ : !__RET__
                @End
        */
        bool remove(TypeK& key, TypeV& val) {
@@ -461,11 +465,11 @@ friend class CHM;
                @Interface: ReplaceAny
                @Commit_point_set:
                        Write_Val_Point
-               @ID: _getKeyTag(key)
+               @ID: __sequential.getKeyTag(key)
                @Action:
-                       @DefineVar: TypeV *_Old_Val = __map.get(key)
+                       @DefineVar: TypeV *_Old_Val = __sequential.map.get(key)
                @Post_check:
-                       _equals_val(__RET__, _Old_Val)
+                       __sequential.equals_val(__RET__, _Old_Val)
                @End
        */
        shared_ptr<TypeV> replace(TypeK& key, TypeV& val) {
@@ -478,16 +482,16 @@ friend class CHM;
                @Commit_point_set:
                        Write_Val_Point | ReplaceIfMatch_Fail_Point
                @Condition:
-                       _equals_val(__map.get(key), &oldval)
+                       __sequential.equals_val(__sequential.map.get(key), &oldval)
                @HB_condition:
                        COND_ReplaceIfMatchSucc :: __RET__ == true
-               @ID: _getKeyTag(key)
+               @ID: __sequential.getKeyTag(key)
                @Action:
                        @Code:
-                       if (COND_SAT)
-                               __map.put(key, &newval);
+                       if (__COND_SAY__)
+                               __sequential.map.put(key, &newval);
                @Post_check:
-                       COND_SAT ? __RET__ : !__RET__
+                       __COND_SAY__ ? __RET__ : !__RET__
                @End
        */
        bool replace(TypeK& key, TypeV& oldval, TypeV& newval) {
index 7fb604c..9dd2bf8 100644 (file)
 /**
        @Begin
        @Global_define:
-               bool __writer_lock_acquired = false;
-               int __reader_lock_cnt = 0;
-       
+               @DeclareVar:
+                       bool writer_lock_acquired;
+                       int reader_lock_cnt;
+               @InitVar:
+                       writer_lock_acquired = false;
+                       reader_lock_cnt = 0;
+               @DefineFunc:
        @Happens_before:
                # Since commit_point_set has no ID attached, A -> B means that for any B,
                # the previous A happens before B.
@@ -80,10 +84,10 @@ static inline int write_can_lock(rwlock_t *lock)
        @Commit_point_set:
                Read_Lock_Success_1 | Read_Lock_Success_2
        @Check:
-               !__writer_lock_acquired
+               !__sequential.writer_lock_acquired
        @Action:
                @Code:
-               __reader_lock_cnt++;
+               __sequential.reader_lock_cnt++;
        @End
 */
 static inline void read_lock(rwlock_t *rw)
@@ -117,10 +121,10 @@ static inline void read_lock(rwlock_t *rw)
        @Commit_point_set:
                Write_Lock_Success_1 | Write_Lock_Success_2
        @Check:
-               !__writer_lock_acquired && __reader_lock_cnt == 0
+               !__sequential.writer_lock_acquired && __sequential.reader_lock_cnt == 0
        @Action:
                @Code:
-               __writer_lock_acquired = true;
+               __sequential.writer_lock_acquired = true;
        @End
 */
 static inline void write_lock(rwlock_t *rw)
@@ -153,15 +157,15 @@ static inline void write_lock(rwlock_t *rw)
        @Commit_point_set:
                Read_Trylock_Point
        @Condition:
-               __writer_lock_acquired == false
+               __sequential.writer_lock_acquired == false
        @HB_condition:
                HB_Read_Trylock_Succ :: __RET__ == 1
        @Action:
                @Code:
-               if (COND_SAT)
-                       __reader_lock_cnt++;
+               if (__COND_SAY__)
+                       __sequential.reader_lock_cnt++;
        @Post_check:
-               COND_SAT ? __RET__ == 1 : __RET__ == 0
+               __COND_SAY__ ? __RET__ == 1 : __RET__ == 0
        @End
 */
 static inline int read_trylock(rwlock_t *rw)
@@ -186,15 +190,15 @@ static inline int read_trylock(rwlock_t *rw)
        @Commit_point_set:
                Write_Trylock_Point
        @Condition:
-               !__writer_lock_acquired && __reader_lock_cnt == 0
+               !__sequential.writer_lock_acquired && __sequential.reader_lock_cnt == 0
        @HB_condition:
                HB_Write_Trylock_Succ :: __RET__ == 1
        @Action:
                @Code:
-               if (COND_SAT)
-                       __writer_lock_acquired = true;
+               if (__COND_SAY__)
+                       __sequential.writer_lock_acquired = true;
        @Post_check:
-               COND_SAT ? __RET__ == 1 : __RET__ == 0
+               __COND_SAY__ ? __RET__ == 1 : __RET__ == 0
        @End
 */
 static inline int write_trylock(rwlock_t *rw)
@@ -218,7 +222,7 @@ static inline int write_trylock(rwlock_t *rw)
        @Interface: Read_Unlock
        @Commit_point_set: Read_Unlock_Point
        @Check:
-               __reader_lock_cnt > 0 && !__writer_lock_acquired
+               __sequential.reader_lock_cnt > 0 && !__sequential.writer_lock_acquired
        @Action: 
                @Code:
                reader_lock_cnt--;
@@ -243,7 +247,7 @@ static inline void read_unlock(rwlock_t *rw)
                reader_lock_cnt == 0 && writer_lock_acquired
        @Action: 
                @Code:
-               __writer_lock_acquired = false;
+               __sequential.writer_lock_acquired = false;
        @End
 */
 
index fc8e02a..6a2737f 100644 (file)
@@ -79,6 +79,7 @@ void init_queue(queue_t *q, int num_threads)
 /**
        @Begin
        @Global_define:
+               @DeclareVar:
                typedef struct tag_elem {
                        Tag id;
                        unsigned int data;
@@ -89,8 +90,11 @@ void init_queue(queue_t *q, int num_threads)
                        }
                } tag_elem_t;
 
-               spec_queue<tag_elem_t> __queue;
-               Tag __tag;
+               spec_queue<tag_elem_t> queue;
+               Tag tag;
+               @InitVar:
+                       queue = spec_queue<tag_elem_t>();
+                       tag = Tag();
        @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
@@ -103,12 +107,12 @@ void init_queue(queue_t *q, int num_threads)
        @Begin
        @Interface: Enqueue
        @Commit_point_set: Enqueue_Success_Point
-       @ID: __tag.getCurAndInc()
+       @ID: __sequential.tag.getCurAndInc()
        @Action:
                # __ID__ is an internal macro that refers to the id of the current
                # interface call
                @Code:
-               __queue.enqueue(tag_elem_t(__ID__, val));
+               __sequential.queue.enqueue(tag_elem_t(__ID__, val));
        @End
 */
 void enqueue(queue_t *q, unsigned int val)
@@ -165,10 +169,10 @@ void enqueue(queue_t *q, unsigned int val)
        @Begin
        @Interface: Dequeue
        @Commit_point_set: Dequeue_Success_Point
-       @ID: __queue.peak().tag
+       @ID: __sequential.queue.peak().tag
        @Action:
                @Code:
-               unsigned int _Old_Val = __queue.dequeue().data;
+               unsigned int _Old_Val = __sequential.queue.dequeue().data;
        @Post_check:
                _Old_Val == __RET__
        @End
index 2238268..6776986 100644 (file)
@@ -11,6 +11,9 @@
        a) Global construct
        @Begin
        @Global_define:
+               @DeclareVar:
+               @InitVar:
+               @DefineFunc:
                ...
        @Interface_cluster:
                ...
@@ -86,6 +89,7 @@ import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface;
 import edu.uci.eecs.specCompiler.specExtraction.ActionSubConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.ActionSubConstruct.DefineVar;
+import edu.uci.eecs.specCompiler.specExtraction.SequentialDefineSubConstruct;
 
        public class SpecParser {
                public static void main(String[] argvs)
@@ -142,6 +146,12 @@ TOKEN :
        <END: "@End">
 |
        <GLOBAL_DEFINE: "@Global_define:">
+|
+       <DECLARE_VAR: "@DeclareVar:">
+|
+       <INIT_VAR: "@InitVar:">
+|
+       <DEFINE_FUNC: "@DefineFunc:">
 |
        <INTERFACE_CLUSTER: "@Interface_cluster:">
 |
@@ -334,7 +344,7 @@ Construct Parse() :
 GlobalConstruct Global_construct() :
 {
        GlobalConstruct res;
-       String code;
+       SequentialDefineSubConstruct code;
 }
 {
        { res = null; }
@@ -390,14 +400,24 @@ String C_CPP_CODE() :
        }
 }
 
-String Global_define() :
+SequentialDefineSubConstruct Global_define() :
 {
-       String code;    
+       String declareVar, initVar, defineFunc;
 }
 {
-       <GLOBAL_DEFINE> (code = C_CPP_CODE())
        {
-               return code;
+               declareVar = "";
+               initVar = "";
+               defineFunc = "";
+       }
+       <GLOBAL_DEFINE> 
+       (<DECLARE_VAR> (declareVar = C_CPP_CODE()))?
+       (<INIT_VAR> (initVar = C_CPP_CODE()))?
+       (<DEFINE_FUNC> (defineFunc = C_CPP_CODE()))?
+       {
+               SequentialDefineSubConstruct res = new SequentialDefineSubConstruct(declareVar, initVar, defineFunc);
+               //System.out.println(res);
+               return res;
        }
 }
 
index b53b482..ab3e7ec 100644 (file)
@@ -14,6 +14,7 @@ import edu.uci.eecs.specCompiler.specExtraction.Construct;
 import edu.uci.eecs.specCompiler.specExtraction.GlobalConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.InterfaceConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.PotentialCPDefineConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.SequentialDefineSubConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.SpecConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.SpecExtractor;
 import edu.uci.eecs.specCompiler.specExtraction.SpecNotMatchException;
@@ -94,27 +95,46 @@ public class CodeGenerator {
                GlobalConstruct construct = (GlobalConstruct) inst.construct; 
                ArrayList<String> newCode = new ArrayList<String>();
                
+               // Generate the inner class definition
+               newCode.add("class Sequential {\n");
+               newCode.add("public:\n");
+               
                // Generate the code in global construct first
-               String globalCode = construct.code;
-               int begin = 0, end = 0;
-               while (end < globalCode.length()) {
-                       if (globalCode.charAt(end) == '\n') {
-                               String line = globalCode.substring(begin, end);
-                               newCode.add(line);
-                               begin = end + 1;
-                       }
-                       end++;
-               }
+               SequentialDefineSubConstruct globalCode = construct.code;
+               breakCodeLines(newCode, globalCode.declareVar);
+               breakCodeLines(newCode, globalCode.defineFunc);
                
-               // Generate code from the DefineVar and __COND_SAT__
+               // Generate code from the DefineVar, __COND_SAT__ and __ID__
                
                
+               // Generate the end of the inner class definition
+               newCode.add("};\n");
+//             printCode(newCode);
+               
                CodeAddition addition = new CodeAddition(lineNum, newCode);
                if (!codeAdditions.containsKey(inst.file)) {
                        codeAdditions.put(inst.file, new ArrayList<CodeAddition>());
                }
                codeAdditions.get(inst.file).add(addition);
        }
+       
+       private void breakCodeLines(ArrayList<String> newCode, String code) {
+               int begin = 0, end = 0;
+               while (end < code.length()) {
+                       if (code.charAt(end) == '\n') {
+                               String line = code.substring(begin, end);
+                               newCode.add(line);
+                               begin = end + 1;
+                       }
+                       end++;
+               }
+       }
+       
+       private void printCode(ArrayList<String> code) {
+               for (int i = 0; i < code.size(); i++) {
+                       System.out.println(code.get(i));
+               }
+       }
 
        private void interface2Code(SpecConstruct inst) {
                int lineNum = inst.endLineNum + 1;
index ef0a815..094361a 100644 (file)
@@ -4,12 +4,12 @@ import java.util.HashMap;
 import java.util.HashSet;
 
 public class GlobalConstruct extends Construct {
-       public final String code;
+       public final SequentialDefineSubConstruct code;
        private final HashMap<String, HashSet<ConditionalInterface>> interfaceCluster;
        private final HashMap<ConditionalInterface, HashSet<ConditionalInterface>> originalHBRelations;
        public final HashMap<ConditionalInterface, HashSet<ConditionalInterface>> hbRelations;
        
-       public GlobalConstruct(String code) {
+       public GlobalConstruct(SequentialDefineSubConstruct code) {
                this.code = code;
                this.interfaceCluster = new HashMap<String, HashSet<ConditionalInterface>>();
                this.originalHBRelations = new HashMap<ConditionalInterface, HashSet<ConditionalInterface>>();
diff --git a/src/edu/uci/eecs/specCompiler/specExtraction/SequentialDefineSubConstruct.java b/src/edu/uci/eecs/specCompiler/specExtraction/SequentialDefineSubConstruct.java
new file mode 100644 (file)
index 0000000..743a9d6
--- /dev/null
@@ -0,0 +1,25 @@
+package edu.uci.eecs.specCompiler.specExtraction;
+
+public class SequentialDefineSubConstruct {
+       public final String declareVar;
+       public final String initVar;
+       public final String defineFunc;
+       
+       public SequentialDefineSubConstruct(String declareVar, String initVar, String defineFunc) {
+               this.declareVar = declareVar;
+               this.initVar = initVar;
+               this.defineFunc = defineFunc;
+       }
+       
+       public String toString() {
+               StringBuffer res = new StringBuffer();
+               res.append("@Sequential_define:\n");
+               res.append("\t@DeclareVar:\n");
+               res.append(declareVar);
+               res.append("\t@InitVar:\n");
+               res.append(initVar);
+               res.append("\t@DefineFunc:\n");
+               res.append(defineFunc);
+               return res.toString();
+       }
+}