From 1ea8394d222ead2d8e413359d536fb5c2b1f14f4 Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Wed, 16 Oct 2013 12:47:41 -0700 Subject: [PATCH] try to generate in-place code --- .../simplified_cliffc_hashtable.h | 86 ++++++++++--------- benchmark/linuxrwlocks/linuxrwlocks.c | 38 ++++---- benchmark/ms-queue/my_queue.c | 16 ++-- grammer/spec-compiler.jj | 30 +++++-- .../codeGenerator/CodeGenerator.java | 42 ++++++--- .../specExtraction/GlobalConstruct.java | 4 +- .../SequentialDefineSubConstruct.java | 25 ++++++ 7 files changed, 159 insertions(+), 82 deletions(-) create mode 100644 src/edu/uci/eecs/specCompiler/specExtraction/SequentialDefineSubConstruct.java diff --git a/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h b/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h index 0e7031e..89efb8f 100644 --- a/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h +++ b/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h @@ -84,26 +84,30 @@ class cliffc_hashtable { @Begin @Global_define: - - spec_hashtable __map; - spec_hashtable __id_map; - Tag __tag; - - static bool _val_equals(TypeV *ptr1, TypeV *ptr2) { + @DeclareVar: + spec_hashtable map; + spec_hashtable id_map; + Tag tag; + @InitVar: + map = spec_hashtable(); + id_map = spec_hashtable(); + 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 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 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 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 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 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) { diff --git a/benchmark/linuxrwlocks/linuxrwlocks.c b/benchmark/linuxrwlocks/linuxrwlocks.c index 7fb604c..9dd2bf8 100644 --- a/benchmark/linuxrwlocks/linuxrwlocks.c +++ b/benchmark/linuxrwlocks/linuxrwlocks.c @@ -39,9 +39,13 @@ /** @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 */ diff --git a/benchmark/ms-queue/my_queue.c b/benchmark/ms-queue/my_queue.c index fc8e02a..6a2737f 100644 --- a/benchmark/ms-queue/my_queue.c +++ b/benchmark/ms-queue/my_queue.c @@ -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 __queue; - Tag __tag; + spec_queue queue; + Tag tag; + @InitVar: + queue = spec_queue(); + 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 diff --git a/grammer/spec-compiler.jj b/grammer/spec-compiler.jj index 2238268..6776986 100644 --- a/grammer/spec-compiler.jj +++ b/grammer/spec-compiler.jj @@ -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 : | +| + +| + +| + | | @@ -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; } { - (code = C_CPP_CODE()) { - return code; + declareVar = ""; + initVar = ""; + defineFunc = ""; + } + + ( (declareVar = C_CPP_CODE()))? + ( (initVar = C_CPP_CODE()))? + ( (defineFunc = C_CPP_CODE()))? + { + SequentialDefineSubConstruct res = new SequentialDefineSubConstruct(declareVar, initVar, defineFunc); + //System.out.println(res); + return res; } } diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java index b53b482..ab3e7ec 100644 --- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java +++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java @@ -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 newCode = new ArrayList(); + // 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()); } codeAdditions.get(inst.file).add(addition); } + + private void breakCodeLines(ArrayList 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 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; diff --git a/src/edu/uci/eecs/specCompiler/specExtraction/GlobalConstruct.java b/src/edu/uci/eecs/specCompiler/specExtraction/GlobalConstruct.java index ef0a815..094361a 100644 --- a/src/edu/uci/eecs/specCompiler/specExtraction/GlobalConstruct.java +++ b/src/edu/uci/eecs/specCompiler/specExtraction/GlobalConstruct.java @@ -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> interfaceCluster; private final HashMap> originalHBRelations; public final HashMap> hbRelations; - public GlobalConstruct(String code) { + public GlobalConstruct(SequentialDefineSubConstruct code) { this.code = code; this.interfaceCluster = new HashMap>(); this.originalHBRelations = new HashMap>(); diff --git a/src/edu/uci/eecs/specCompiler/specExtraction/SequentialDefineSubConstruct.java b/src/edu/uci/eecs/specCompiler/specExtraction/SequentialDefineSubConstruct.java new file mode 100644 index 0000000..743a9d6 --- /dev/null +++ b/src/edu/uci/eecs/specCompiler/specExtraction/SequentialDefineSubConstruct.java @@ -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(); + } +} -- 2.34.1