@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);
}
}
@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) {
@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) {
@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) {
@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) {
@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) {
@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) {
@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) {
/**
@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.
@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)
@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)
@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)
@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)
@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--;
reader_lock_cnt == 0 && writer_lock_acquired
@Action:
@Code:
- __writer_lock_acquired = false;
+ __sequential.writer_lock_acquired = false;
@End
*/
/**
@Begin
@Global_define:
+ @DeclareVar:
typedef struct tag_elem {
Tag id;
unsigned int data;
}
} 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
@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)
@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
a) Global construct
@Begin
@Global_define:
+ @DeclareVar:
+ @InitVar:
+ @DefineFunc:
...
@Interface_cluster:
...
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)
<END: "@End">
|
<GLOBAL_DEFINE: "@Global_define:">
+|
+ <DECLARE_VAR: "@DeclareVar:">
+|
+ <INIT_VAR: "@InitVar:">
+|
+ <DEFINE_FUNC: "@DefineFunc:">
|
<INTERFACE_CLUSTER: "@Interface_cluster:">
|
GlobalConstruct Global_construct() :
{
GlobalConstruct res;
- String code;
+ SequentialDefineSubConstruct code;
}
{
{ res = null; }
}
}
-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;
}
}
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;
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;
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>>();
--- /dev/null
+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();
+ }
+}