fix cp clear
authorPeizhao Ou <peizhaoo@uci.edu>
Tue, 25 Mar 2014 19:10:03 +0000 (12:10 -0700)
committerPeizhao Ou <peizhaoo@uci.edu>
Tue, 25 Mar 2014 19:10:03 +0000 (12:10 -0700)
benchmark/linuxrwlocks/linuxrwlocks.c
src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java

index 0a1a7b2..a4e58b6 100644 (file)
@@ -269,7 +269,7 @@ static inline void read_unlock(rwlock_t *rw)
 /**
        @Begin
        @Interface: Write_Unlock
-       @Commit_point_set: Write_Unlock_Point
+       @Commit_point_set: Write_Unlock_Point | Write_Unlock_Clear
        @Check:
                reader_lock_cnt == 0 && writer_lock_acquired
        @Action: 
@@ -285,6 +285,13 @@ static inline void write_unlock(rwlock_t *rw)
                @Label: Write_Unlock_Point
                @End
        */
+
+       /**
+               //@Begin
+               @Commit_point_clear: true
+               @Label: Write_Unlock_Clear
+               @End
+       */
 }
 
 rwlock_t mylock;
index fb1b520..4c4fc87 100644 (file)
@@ -49,6 +49,7 @@ public class CodeVariables {
        public static final String SPEC_ANNO_TYPE_INTERFACE_END = "INTERFACE_END";
        public static final String SPEC_ANNO_TYPE_POTENTIAL_CP_DEFINE = "POTENTIAL_CP_DEFINE";
        public static final String SPEC_ANNO_TYPE_CP_DEFINE_CHECK = "CP_DEFINE_CHECK";
+       public static final String SPEC_ANNO_TYPE_CP_CLEAR = "CP_CLEAR";
        public static final String SPEC_ANNO_TYPE_CP_DEFINE = "CP_DEFINE";
        public static final String SPEC_ANNOTATION = "spec_annotation";
        public static final String SPEC_ANNOTATION_FIELD_TYPE = "type";
@@ -855,7 +856,7 @@ public class CodeVariables {
                newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "interface_num", interfaceNum));
                newCode.add("\t\t" + STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno));
                newCode.add("\t\t"
-                               + ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_CP_DEFINE_CHECK));
+                               + ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_CP_CLEAR));
                newCode.add("\t\t" + ASSIGN_TO_PTR(anno, "annotation", structName));
                newCode.add("\t\t" + ANNOTATE(semantics, anno));
                newCode.add("\t" + "}");
index e5b5f9d..23dad2f 100644 (file)
@@ -6,6 +6,7 @@ import java.util.HashMap;
 import java.util.HashSet;
 
 import edu.uci.eecs.specCompiler.grammerParser.ParseException;
+import edu.uci.eecs.specCompiler.specExtraction.CPClearConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.CPDefineConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.ClassBeginConstruct;
@@ -270,6 +271,15 @@ public class SemanticsChecker {
                                commitPointLabel2Num.put(label, _commitPointNum++);
                                num2CommitPointLabel.put(_commitPointNum, label);
 
+                               CPLabel2Construct.put(label, construct);
+                       } else if (construct instanceof CPClearConstruct) {
+                               CPClearConstruct theConstruct = (CPClearConstruct) construct;
+                               label = theConstruct.label;
+                               checkLabelDuplication(construct, label);
+                               // Number the commit point define check label
+                               commitPointLabel2Num.put(label, _commitPointNum++);
+                               num2CommitPointLabel.put(_commitPointNum, label);
+
                                CPLabel2Construct.put(label, construct);
                        } else if (construct instanceof CPDefineConstruct) {
                                CPDefineConstruct theConstruct = (CPDefineConstruct) construct;