add Commit point clear construct
authorPeizhao Ou <peizhaoo@uci.edu>
Tue, 25 Mar 2014 18:52:46 +0000 (11:52 -0700)
committerPeizhao Ou <peizhaoo@uci.edu>
Tue, 25 Mar 2014 18:52:46 +0000 (11:52 -0700)
benchmark/chase-lev-deque-bugfix/deque.c
benchmark/cliffc-hashtable/.cliffc_hashtable.h.swp [deleted file]
benchmark/cliffc-hashtable/cliffc_hashtable.h
benchmark/cliffc-hashtable/main.cc
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/CPClearConstruct.java [new file with mode: 0644]
src/edu/uci/eecs/specCompiler/specExtraction/CPDefineCheckConstruct.java

index 11e5e99..c9fc8a9 100644 (file)
@@ -30,7 +30,7 @@ int take(Deque *q) {
        /**
                @Begin
                @Commit_point_define_check: t > b
-               @Label: Take_Point_1
+               @Label: Take_Point1
                @End
        */
        int x;
diff --git a/benchmark/cliffc-hashtable/.cliffc_hashtable.h.swp b/benchmark/cliffc-hashtable/.cliffc_hashtable.h.swp
deleted file mode 100644 (file)
index a868efd..0000000
Binary files a/benchmark/cliffc-hashtable/.cliffc_hashtable.h.swp and /dev/null differ
index 5c32ca0..3cef980 100644 (file)
@@ -151,27 +151,7 @@ class cliffc_hashtable {
                                        return res;
                                }
                        }
-               
-               @Interface_cluster:
-                       Read_interface = {
-                               Get,
-                               PutIfAbsent,
-                               RemoveAny,
-                               RemoveIfMatch,
-                               ReplaceAny,
-                               ReplaceIfMatch
-                       }
-                       
-                       Write_interface = {
-                               Put,
-                               PutIfAbsent(COND_PutIfAbsentSucc),
-                               RemoveAny,
-                               RemoveIfMatch(COND_RemoveIfMatchSucc),
-                               ReplaceAny,
-                               ReplaceIfMatch(COND_ReplaceIfMatchSucc)
-                       }
                @Happens_before:
-                       //Write_interface -> Read_interface
                        Put->Get
                        Put->Put
                @End
@@ -222,6 +202,7 @@ friend class CHM;
        
                kvs_data* resize(cliffc_hashtable *topmap, kvs_data *kvs) {
                        //model_print("resizing...\n");
+                       /**** FIXME: miss ****/
                        kvs_data *newkvs = _newkvs.load(memory_order_acquire);
                        if (newkvs != NULL)
                                return newkvs;
@@ -244,6 +225,7 @@ friend class CHM;
                        if (newsz < oldlen) newsz = oldlen;
        
                        // Last check cause the 'new' below is expensive
+                       /**** FIXME: miss ****/
                        newkvs = _newkvs.load(memory_order_acquire);
                        //model_print("hey1\n");
                        if (newkvs != NULL) return newkvs;
@@ -255,15 +237,19 @@ friend class CHM;
        
                        kvs_data *cur_newkvs; 
                        // Another check after the slow allocation
+                       /**** FIXME: miss ****/
                        if ((cur_newkvs = _newkvs.load(memory_order_acquire)) != NULL)
                                return cur_newkvs;
                        // CAS the _newkvs to the allocated table
                        kvs_data *desired = (kvs_data*) NULL;
                        kvs_data *expected = (kvs_data*) newkvs; 
+                       /**** FIXME: miss ****/
+                       //model_print("release in resize!\n"); 
                        if (!_newkvs.compare_exchange_strong(desired, expected, memory_order_release,
                                        memory_order_relaxed)) {
                                // Should clean the allocated area
                                delete newkvs;
+                               /**** FIXME: miss ****/
                                newkvs = _newkvs.load(memory_order_acquire);
                        }
                        return newkvs;
@@ -272,6 +258,7 @@ friend class CHM;
                void help_copy_impl(cliffc_hashtable *topmap, kvs_data *oldkvs,
                        bool copy_all) {
                        MODEL_ASSERT (get_chm(oldkvs) == this);
+                       /**** FIXME: miss ****/
                        kvs_data *newkvs = _newkvs.load(memory_order_acquire);
                        int oldlen = oldkvs->_size;
                        int min_copy_work = oldlen > 1024 ? 1024 : oldlen;
@@ -285,7 +272,7 @@ friend class CHM;
                                        copyidx = _copy_idx.load(memory_order_relaxed);
                                        while (copyidx < (oldlen << 1) &&
                                                !_copy_idx.compare_exchange_strong(copyidx, copyidx +
-                                                       min_copy_work, memory_order_release, memory_order_relaxed))
+                                                       min_copy_work, memory_order_relaxed, memory_order_relaxed))
                                                copyidx = _copy_idx.load(memory_order_relaxed);
                                        if (!(copyidx < (oldlen << 1)))
                                                panic_start = copyidx;
@@ -309,6 +296,7 @@ friend class CHM;
        
                kvs_data* copy_slot_and_check(cliffc_hashtable *topmap, kvs_data
                        *oldkvs, int idx, void *should_help) {
+                       /**** FIXME: miss ****/
                        kvs_data *newkvs = _newkvs.load(memory_order_acquire);
                        // We're only here cause the caller saw a Prime
                        if (copy_slot(topmap, idx, oldkvs, newkvs))
@@ -332,7 +320,9 @@ friend class CHM;
                        // Promote the new table to the current table
                        if (copyDone + workdone == oldlen &&
                                topmap->_kvs.load(memory_order_relaxed) == oldkvs) {
+                               /**** FIXME: miss ****/
                                kvs_data *newkvs = _newkvs.load(memory_order_acquire);
+                               /**** CDSChecker error ****/
                                topmap->_kvs.compare_exchange_strong(oldkvs, newkvs, memory_order_release,
                                        memory_order_relaxed);
                        }
@@ -423,7 +413,8 @@ friend class CHM;
        /**
                @Begin
                @Interface: Get
-               @Commit_point_set: Get_Success_Point1 | Get_Success_Point2 | Get_Success_Point3 
+               //@Commit_point_set: Get_Point1 | Get_Point2 | Get_Point3 | Get_ReadKVS
+               @Commit_point_set: Get_Point1 | Get_Point2 | Get_Point3
                @ID: getKeyTag(key)
                @Action:
                        TypeV *_Old_Val = (TypeV*) spec_table_get(map, key);
@@ -443,7 +434,14 @@ friend class CHM;
        TypeV* get(TypeK *key) {
                slot *key_slot = new slot(false, key);
                int fullhash = hash(key_slot);
+               /**** CDSChecker error ****/
                kvs_data *kvs = _kvs.load(memory_order_acquire);
+               /**
+                       //@Begin
+                       @Commit_point_define_check: true
+                       @Label: Get_ReadKVS
+                       @End
+               */
                slot *V = get_impl(this, kvs, key_slot, fullhash);
                if (V == NULL) return NULL;
                MODEL_ASSERT (!is_prime(V));
@@ -453,7 +451,7 @@ friend class CHM;
        /**
                @Begin
                @Interface: Put
-               @Commit_point_set: Write_Success_Point
+               @Commit_point_set: Put_Point
                @ID: getKeyTag(key)
                @Action:
                        # Remember this old value at checking point
@@ -612,6 +610,7 @@ friend class CHM;
                MODEL_ASSERT (idx >= 0 && idx < kvs->_size);
                // Corresponding to the volatile read in get_impl() and putIfMatch in
                // Cliff Click's Java implementation
+               /**** CDSChecker error & hb violation ****/
                slot *res = (slot*) kvs->_data[idx * 2 + 3].load(memory_order_acquire);
                /**
                        @Begin
@@ -674,8 +673,17 @@ friend class CHM;
        // Together with key() preserve the happens-before relationship on newly
        // inserted keys
        static inline bool CAS_key(kvs_data *kvs, int idx, void *expected, void *desired) {
-               return kvs->_data[2 * idx + 2].compare_exchange_strong(expected,
+               bool res = kvs->_data[2 * idx + 2].compare_exchange_strong(expected,
                        desired, memory_order_relaxed, memory_order_relaxed);
+               /**
+                       # If it is a successful put instead of a copy or any other internal
+                       # operantions, expected != NULL
+                       @Begin
+                       @Potential_commit_point_define: res
+                       @Label: Write_Key_Point
+                       @End
+               */
+               return res;
        }
 
        /**
@@ -686,6 +694,7 @@ friend class CHM;
        // inserted values
        static inline bool CAS_val(kvs_data *kvs, int idx, void *expected, void
                *desired) {
+               /**** CDSChecker error & HB violation ****/
                bool res =  kvs->_data[2 * idx + 3].compare_exchange_strong(expected,
                        desired, memory_order_acq_rel, memory_order_relaxed);
                /**
@@ -713,12 +722,11 @@ friend class CHM;
                                @Begin
                                @Commit_point_define: K == NULL
                                @Potential_commit_point_label: Read_Key_Point
-                               @Label: Get_Success_Point_1
+                               @Label: Get_Point1
                                @End
                        */
                        slot *V = val(kvs, idx);
                        
-
                        if (K == NULL) {
                                //model_print("Key is null\n");
                                return NULL; // A miss
@@ -731,7 +739,7 @@ friend class CHM;
                                                @Begin
                                                @Commit_point_define: true
                                                @Potential_commit_point_label: Read_Val_Point
-                                               @Label: Get_Success_Point_2
+                                               @Label: Get_Point2
                                                @End
                                        */
                                        return (V == TOMBSTONE) ? NULL : V; // Return this value
@@ -745,11 +753,12 @@ friend class CHM;
                                key_slot == TOMBSTONE) {
                                // Retry in new table
                                // Atomic read can be here 
+                               /**** FIXME: miss ****/
                                kvs_data *newkvs = chm->_newkvs.load(memory_order_acquire);
                                /**
                                        @Begin
                                        @Commit_point_define_check: newkvs == NULL
-                                       @Label: Get_Success_Point_3
+                                       @Label: Get_Point3
                                        @End
                                */
                                return newkvs == NULL ? NULL : get_impl(topmap,
@@ -769,7 +778,14 @@ friend class CHM;
                slot *key_slot = new slot(false, key);
 
                slot *value_slot = new slot(false, value);
+               /**** FIXME: miss ****/
                kvs_data *kvs = _kvs.load(memory_order_acquire);
+               /**
+                       //@Begin
+                       @Commit_point_define_check: true
+                       @Label: Put_ReadKVS
+                       @End
+               */
                slot *res = putIfMatch(this, kvs, key_slot, value_slot, old_val);
                // Only when copy_slot() call putIfMatch() will it return NULL
                MODEL_ASSERT (res != NULL); 
@@ -840,6 +856,7 @@ friend class CHM;
        
                // Here it tries to resize cause it doesn't want other threads to stop
                // its progress (eagerly try to resize soon)
+               /**** FIXME: miss ****/
                newkvs = chm->_newkvs.load(memory_order_acquire);
                if (newkvs == NULL &&
                        ((V == NULL && chm->table_full(reprobe_cnt, len)) || is_prime(V))) {
@@ -862,7 +879,7 @@ friend class CHM;
                                !(V == NULL && expVal == TOMBSTONE) &&
                                (expVal == NULL || !valeq(expVal, V))) {
                                /**
-                                       @Begin
+                                       //@Begin
                                        @Commit_point_define: expVal == TOMBSTONE
                                        @Potential_commit_point_label: Read_Val_Point
                                        @Label: PutIfAbsent_Fail_Point
@@ -871,14 +888,14 @@ friend class CHM;
                                        @End
                                */
                                /**
-                                       @Begin
+                                       //@Begin
                                        @Commit_point_define: expVal != NULL && val_slot == TOMBSTONE
                                        @Potential_commit_point_label: Read_Val_Point
                                        @Label: RemoveIfMatch_Fail_Point
                                        @End
                                */
                                /**
-                                       @Begin
+                                       //@Begin
                                        @Commit_point_define: expVal != NULL && !valeq(expVal, V)
                                        @Potential_commit_point_label: Read_Val_Point
                                        @Label: ReplaceIfMatch_Fail_Point
@@ -893,7 +910,7 @@ friend class CHM;
                                        # The only point where a successful put happens
                                        @Commit_point_define: true
                                        @Potential_commit_point_label: Write_Val_Point
-                                       @Label: Write_Success_Point
+                                       @Label: Put_Point
                                        @End
                                */
                                if (expVal != NULL) { // Not called by a table-copy
@@ -919,6 +936,7 @@ friend class CHM;
 
        // Help along an existing table-resize. This is a fast cut-out wrapper.
        kvs_data* help_copy(kvs_data *helper) {
+               /**** FIXME: miss ****/
                kvs_data *topkvs = _kvs.load(memory_order_acquire);
                CHM *topchm = get_chm(topkvs);
                // No cpy in progress
index 3e52744..7e7a305 100644 (file)
@@ -55,8 +55,8 @@ IntWrapper *k0, *k1, *k2, *k3, *k4, *k5;
 IntWrapper *v0, *v1, *v2, *v3, *v4, *v5;
 
 void threadA(void *arg) {
-       table->put(k3, v3);
        table->put(k1, v4);
+       table->put(k3, v3);
        //table->put(k2, v2);
        //table->put(k3, v3);
        /*
index 37749aa..43faebf 100644 (file)
        @Label: ...
        @End
 
+       // Commit point clear (just as a normal commit point, but it is used to
+       // clear all commit points)
+       @Begin
+       @Commit_point_clear: ...
+       @Label: ...
+       @End
+
        e) Entry point construct
        @Begin
        @Entry_point
@@ -122,6 +129,7 @@ import edu.uci.eecs.specCompiler.specExtraction.InterfaceConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.PotentialCPDefineConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.CPDefineConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct;
+import edu.uci.eecs.specCompiler.specExtraction.CPClearConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface;
 import edu.uci.eecs.specCompiler.specExtraction.SequentialDefineSubConstruct;
 import edu.uci.eecs.specCompiler.specExtraction.InterfaceDefineConstruct;
@@ -373,6 +381,8 @@ SKIP : {
        <COMMIT_POINT_DEFINE_CHECK: "@Commit_point_define_check:">
 |
        <COMMIT_POINT_DEFINE: "@Commit_point_define:">
+|
+       <COMMIT_POINT_CLEAR: "@Commit_point_clear:">
 |
        <POTENTIAL_COMMIT_POINT_LABEL: "@Potential_commit_point_label:">
 }
@@ -885,6 +895,7 @@ Construct ParseSpec() :
        LOOKAHEAD(2) res = Potential_commit_point_define() |
        LOOKAHEAD(2) res = Commit_point_define() |
        LOOKAHEAD(2) res = Commit_point_define_check() |
+       LOOKAHEAD(2) res = Commit_point_clear() |
        LOOKAHEAD(2) res = Entry_point() |
        LOOKAHEAD(2) res = Class_begin() |
        LOOKAHEAD(2) res = Class_end() |
@@ -1120,6 +1131,25 @@ CPDefineConstruct Commit_point_define() :
        }
 }
 
+CPClearConstruct Commit_point_clear() :
+{
+       CPClearConstruct res;   
+       String label, condition;
+       ArrayList<String> content;
+}
+{
+
+       { res = null; }
+               <BEGIN> 
+                       <COMMIT_POINT_CLEAR> (content = C_CPP_CODE(null) { condition = stringArray2String(content); })
+                       <LABEL> (label = <IDENTIFIER>.image)
+               <END>
+       {
+               res = new CPClearConstruct(_file, _content.size(), label, condition);
+               return res;
+       }
+}
+
 
 CPDefineCheckConstruct Commit_point_define_check() :
 {
index ba28579..dfa5976 100644 (file)
@@ -11,6 +11,7 @@ import java.util.HashMap;
 import java.util.HashSet;
 import java.util.Iterator;
 
+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.ClassEndConstruct;
@@ -183,6 +184,19 @@ public class CodeGenerator {
                }
                codeAdditions.get(construct.file).add(addition);
        }
+       
+       private void CPClear2Code(CPClearConstruct construct) {
+               int lineNum = construct.beginLineNum;
+               ArrayList<String> newCode = CodeVariables.generateCPClear(
+                               _semantics, construct);
+
+               CodeAddition addition = new CodeAddition(lineNum, newCode);
+               if (!codeAdditions.containsKey(construct.file)) {
+                       codeAdditions.put(construct.file, new ArrayList<CodeAddition>());
+               }
+               codeAdditions.get(construct.file).add(addition);
+       }
+       
 
        /**
         * private void ClassEnd2Code(ClassEndConstruct construct) { int lineNum =
@@ -243,6 +257,8 @@ public class CodeGenerator {
                                CPDefine2Code((CPDefineConstruct) construct);
                        } else if (construct instanceof CPDefineCheckConstruct) {
                                CPDefineCheck2Code((CPDefineCheckConstruct) construct);
+                       } else if (construct instanceof CPClearConstruct) {
+                               CPClear2Code((CPClearConstruct) construct);
                        } else if (construct instanceof EntryPointConstruct) {
                                EntryPoint2Code((EntryPointConstruct) construct);
                        }
index d0a935c..fb1b520 100644 (file)
@@ -7,6 +7,7 @@ import java.io.File;
 
 import edu.uci.eecs.specCompiler.grammerParser.utilParser.UtilParser;
 import edu.uci.eecs.specCompiler.grammerParser.utilParser.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.ConditionalInterface;
@@ -60,6 +61,7 @@ public class CodeVariables {
        public static final String ANNO_POTENTIAL_CP_DEFINE = "anno_potential_cp_define";
        public static final String ANNO_CP_DEFINE = "anno_cp_define";
        public static final String ANNO_CP_DEFINE_CHECK = "anno_cp_define_check";
+       public static final String ANNO_CP_CLEAR = "anno_cp_clear";
        public static final String ANNO_HB_CONDITION = "anno_hb_condition";
 
        // Specification variables
@@ -766,7 +768,26 @@ public class CodeVariables {
                newCode.add("\t" + "}");
                return newCode;
        }
-
+       
+       public static String getCPInterfaceNum(SemanticsChecker semantics, String commitPointLabel) {
+               HashMap<String, InterfaceConstruct> cp2Interface = semantics.CPLabel2InterfaceConstruct;
+               InterfaceConstruct iConstruct = cp2Interface.get(commitPointLabel);
+               String interfaceName = iConstruct.name;
+               String interfaceNum = Integer.toString(semantics.interface2Num
+                               .get(interfaceName));
+               return interfaceNum;
+       }
+
+       /**
+        * <p>
+        * Commit point define check should be unique to each interface, meaning that they
+        * are not shared between different interfaces
+        * </p>
+        * 
+        * @param semantics
+        * @param construct
+        * @return
+        */
        public static ArrayList<String> generateCPDefineCheck(
                        SemanticsChecker semantics, CPDefineCheckConstruct construct) {
                ArrayList<String> newCode = new ArrayList<String>();
@@ -780,13 +801,58 @@ public class CodeVariables {
                                                + construct.label));
                newCode.add("");
                // Add annotation
+               
                newCode.add("\t" + "if (" + construct.condition + ") {");
                String structName = "cp_define_check", anno = "annotation_cp_define_check";
                newCode.add("\t\t"
                                + STRUCT_NEW_DECLARE_DEFINE(ANNO_CP_DEFINE_CHECK, structName));
                String labelNum = Integer.toString(semantics.commitPointLabel2Num
                                .get(construct.label));
+               String interfaceNum = getCPInterfaceNum(semantics, construct.label);
+               newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "label_num", labelNum));
+               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));
+               newCode.add("\t\t" + ASSIGN_TO_PTR(anno, "annotation", structName));
+               newCode.add("\t\t" + ANNOTATE(semantics, anno));
+               newCode.add("\t" + "}");
+               return newCode;
+       }
+       
+       /**
+        * <p>
+        * Commit point define check should be unique to each interface, meaning that they
+        * are not shared between different interfaces
+        * </p>
+        * 
+        * @param semantics
+        * @param construct
+        * @return
+        */
+       public static ArrayList<String> generateCPClear(
+                       SemanticsChecker semantics, CPClearConstruct construct) {
+               ArrayList<String> newCode = new ArrayList<String>();
+               // Add atomic return variable if the predicate accesses to it
+               if (construct.condition.indexOf(MACRO_ATOMIC_RETURN) != -1) {
+                       addAtomicReturn(semantics, construct);
+               }
+               // Generate redundant header files
+               newCode.add("\t"
+                               + COMMENT("Automatically generated code for commit point clear: "
+                                               + construct.label));
+               newCode.add("");
+               // Add annotation
+               
+               newCode.add("\t" + "if (" + construct.condition + ") {");
+               String structName = "cp_clear", anno = "annotation_cp_clear";
+               newCode.add("\t\t"
+                               + STRUCT_NEW_DECLARE_DEFINE(ANNO_CP_CLEAR, structName));
+               String labelNum = Integer.toString(semantics.commitPointLabel2Num
+                               .get(construct.label));
+               String interfaceNum = getCPInterfaceNum(semantics, construct.label);
                newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "label_num", labelNum));
+               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));
@@ -796,6 +862,16 @@ public class CodeVariables {
                return newCode;
        }
 
+       /**
+        * <p>
+        * Commit point define should be unique to each interface, meaning that they
+        * are not shared between different interfaces
+        * </p>
+        * 
+        * @param semantics
+        * @param construct
+        * @return
+        */
        public static ArrayList<String> generateCPDefine(
                        SemanticsChecker semantics, CPDefineConstruct construct) {
                ArrayList<String> newCode = new ArrayList<String>();
@@ -811,6 +887,7 @@ public class CodeVariables {
                                + STRUCT_NEW_DECLARE_DEFINE(ANNO_CP_DEFINE, structName));
                String labelNum = Integer.toString(semantics.commitPointLabel2Num
                                .get(construct.label));
+               String interfaceNum = getCPInterfaceNum(semantics, construct.label);
                String potentialLabelNum = Integer
                                .toString(semantics.commitPointLabel2Num
                                                .get(construct.potentialCPLabel));
@@ -818,6 +895,7 @@ public class CodeVariables {
                newCode.add("\t\t"
                                + ASSIGN_TO_PTR(structName, "potential_cp_label_num",
                                                potentialLabelNum));
+               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));
index cb5792a..e5b5f9d 100644 (file)
@@ -28,7 +28,7 @@ public class SemanticsChecker {
        public final HashMap<String, PotentialCPDefineConstruct> potentialCPLabel2Construct;
        public final HashMap<String, InterfaceConstruct> interfaceName2Construct;
        public final HashMap<String, InterfaceDefineConstruct> interfaceName2DefineConstruct;
-       public final HashMap<String, ArrayList<InterfaceConstruct>> CPLabel2InterfaceConstruct;
+       public final HashMap<String, InterfaceConstruct> CPLabel2InterfaceConstruct;
 
        public final HashMap<String, Integer> interface2Num;
        public final HashMap<Integer, String> num2Interface;
@@ -59,7 +59,7 @@ public class SemanticsChecker {
                this.potentialCPLabel2Construct = new HashMap<String, PotentialCPDefineConstruct>();
                this.interfaceName2Construct = new HashMap<String, InterfaceConstruct>();
                this.interfaceName2DefineConstruct = new HashMap<String, InterfaceDefineConstruct>();
-               this.CPLabel2InterfaceConstruct = new HashMap<String, ArrayList<InterfaceConstruct>>();
+               this.CPLabel2InterfaceConstruct = new HashMap<String, InterfaceConstruct>();
                this.entryPointConstructs = new ArrayList<EntryPointConstruct>();
                this.classBeginConstruct = null;
                this.classEndConstruct = null;
@@ -211,11 +211,18 @@ public class SemanticsChecker {
 
                                for (int j = 0; j < iConstruct.commitPointSet.size(); j++) {
                                        String label = iConstruct.commitPointSet.get(j);
+//                                     if (!CPLabel2InterfaceConstruct.containsKey(label)) {
+//                                             CPLabel2InterfaceConstruct.put(label,
+//                                                             new ArrayList<InterfaceConstruct>());
+//                                     }
+//                                     CPLabel2InterfaceConstruct.get(label).add(iConstruct);
                                        if (!CPLabel2InterfaceConstruct.containsKey(label)) {
-                                               CPLabel2InterfaceConstruct.put(label,
-                                                               new ArrayList<InterfaceConstruct>());
+                                               CPLabel2InterfaceConstruct.put(label, iConstruct);
+                                       } else {
+                                               throw new SemanticsCheckerException(
+                                                               "Commit point has multiple interfaces!");
                                        }
-                                       CPLabel2InterfaceConstruct.get(label).add(iConstruct);
+                                       
                                }
                        }
                }
diff --git a/src/edu/uci/eecs/specCompiler/specExtraction/CPClearConstruct.java b/src/edu/uci/eecs/specCompiler/specExtraction/CPClearConstruct.java
new file mode 100644 (file)
index 0000000..f533b3a
--- /dev/null
@@ -0,0 +1,23 @@
+package edu.uci.eecs.specCompiler.specExtraction;
+
+import java.io.File;
+
+public class CPClearConstruct extends Construct {
+       public final String label;
+       public final String condition;
+
+       public CPClearConstruct(File file, int beginLineNum, String label,
+                       String condition) {
+               super(file, beginLineNum);
+               this.label = label;
+               this.condition = condition;
+       }
+
+       public String toString() {
+               StringBuffer res = new StringBuffer();
+               res.append("@Commit_point_define_check:\n");
+               res.append("Label: " + label + "\n");
+               res.append("Condition: " + condition + "\n");
+               return res.toString();
+       }
+}
index 99f8fc8..680e48c 100644 (file)
@@ -15,7 +15,7 @@ public class CPDefineCheckConstruct extends Construct {
 
        public String toString() {
                StringBuffer res = new StringBuffer();
-               res.append("@Commit_point_define_check:\n");
+               res.append("@Commit_point_clear:\n");
                res.append("Label: " + label + "\n");
                res.append("Condition: " + condition + "\n");
                return res.toString();