save

diff --git a/benchmark/cliffc-hashtable/cliffc_hashtable.h b/benchmark/cliffc-hashtable/cliffc_hashtable.h
index 738201cea156b98161bbc5b4d389b1f59553e359..3830eed081ad302ff912a57541074ac4401370e5 100644 (file)
--- a/benchmark/cliffc-hashtable/cliffc_hashtable.h
+++ b/benchmark/cliffc-hashtable/cliffc_hashtable.h
@@ -138,16 +138,15 @@ class cliffc_hashtable {
                        # 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.
-                       id_tag_t getKeyTag(TypeK *key) {
-                               if (spec_table_contains(id_map, key)) {
-                                       id_tag_t *cur_tag = MODEL_MALLOC(sizeof(id_tag_t));
-                                       *cur_tag = current(tag);
-                                       spec_table_put(id_map, key, cur_tag);
+                       call_id_t getKeyTag(TypeK *key) {
+                               if (!spec_table_contains(id_map, key)) {
+                                       call_id_t cur_id = current(tag);
+                                       spec_table_put(id_map, key, (void*) cur_id);
                                        next(tag);
-                                       return cur_tag;
+                                       return cur_id;
                                } else {
-                                       id_tag_t *res = (id_tag_t*) spec_table_get(id_map, key);
-                                       return *res;
+                                       call_id_t res = (call_id_t) spec_table_get(id_map, key);
+                                       return res;
                                }
                        }
                
@@ -390,25 +389,27 @@ friend class CHM;
                // Should initialize the CHM for the construction of the table
                // For other CHM in kvs_data, they should be initialzed in resize()
                // because the size is determined dynamically
+               /**
+                       @Begin
+                       @Entry_point
+                       @End
+               */
                kvs_data *kvs = new kvs_data(Default_Init_Size);
-               
-               /*
                void *chm = (void*) new CHM(0);
                kvs->_data[0].store(chm, memory_order_relaxed);
                _kvs.store(kvs, memory_order_release);
-               */
        }
 
        cliffc_hashtable(int init_size) {
                // Should initialize the CHM for the construction of the table
                // For other CHM in kvs_data, they should be initialzed in resize()
                // because the size is determined dynamically
+
                /**
                        @Begin
                        @Entry_point
                        @End
                */
-
                kvs_data *kvs = new kvs_data(init_size);
                void *chm = (void*) new CHM(0);
                kvs->_data[0].store(chm, memory_order_relaxed);
@@ -793,6 +794,7 @@ friend class CHM;
                        if (++reprobe_cnt >= reprobe_limit(len) ||
                                K == TOMBSTONE) { // Found a Tombstone key, no more keys
                                newkvs = chm->resize(topmap, kvs);
+                               model_print("resize1\n");
                                // Help along an existing copy
                                if (expVal != NULL) topmap->help_copy(newkvs);
                                return putIfMatch(topmap, newkvs, key_slot, val_slot, expVal);
@@ -807,8 +809,10 @@ friend class CHM;
                // its progress (eagerly try to resize soon)
                newkvs = chm->_newkvs.load(memory_order_acquire);
                if (newkvs == NULL &&
-                       ((V == NULL && chm->table_full(reprobe_cnt, len)) || is_prime(V)))
+                       ((V == NULL && chm->table_full(reprobe_cnt, len)) || is_prime(V))) {
+                       model_print("resize2\n");
                        newkvs = chm->resize(topmap, kvs); // Force the copy to start
+               }
                
                // Finish the copy and then put it in the new table
                if (newkvs != NULL)
@@ -842,7 +846,7 @@ friend class CHM;
                                */
                                /**
                                        @Begin
-                                       @Commit_point_define: !valeq(expVal, V)
+                                       @Commit_point_define: expVal != NULL && !valeq(expVal, V)
                                        @Potential_commit_point_label: Read_Val_Point
                                        @Label: ReplaceIfMatch_Fail_Point
                                        @End

diff --git a/benchmark/cliffc-hashtable/main.cc b/benchmark/cliffc-hashtable/main.cc
index 517e4a7b895bb81fa193ca4ea685ccd4fbd668f2..f18064db98e398ed7eb8a555db1ad866cab3010f 100644 (file)
--- a/benchmark/cliffc-hashtable/main.cc
+++ b/benchmark/cliffc-hashtable/main.cc
@@ -53,16 +53,24 @@ cliffc_hashtable<IntWrapper, IntWrapper> *table;
 IntWrapper *val1, *val2;
 
 void threadA(void *arg) {
-       /*
-       IntWrapper *k1 = new IntWrapper(3), *k2 = new IntWrapper(5),
+       
+       IntWrapper *k1 = new IntWrapper(3), *k2 = new IntWrapper(2),
                *k3 = new IntWrapper(1024), *k4 = new IntWrapper(1025);
        IntWrapper *v1 = new IntWrapper(1024), *v2 = new IntWrapper(1025),
                *v3 = new IntWrapper(73), *v4 = new IntWrapper(81);
+       
        table->put(k1, v1);
        table->put(k2, v2);
+       //table->put(k4, v3);
+       //table->put(v3, v3);
+       
        val1 = table->get(k3);
-       table->put(k3, v3);
-       */
+       if (val1 != NULL)
+               model_print("val1: %d\n", val1->_val);
+       else
+               model_print("val1: NULL\n");
+       //table->put(k3, v3);
+       
 }
 
 void threadB(void *arg) {
@@ -89,13 +97,13 @@ void threadMain(void *arg) {
                *k3 = new IntWrapper(1024), *k4 = new IntWrapper(1025);
        IntWrapper *v1 = new IntWrapper(1024), *v2 = new IntWrapper(1025),
                *v3 = new IntWrapper(73), *v4 = new IntWrapper(81);
-       table->put(k1, v3);
-       val1 = table->get(k2);
+       table->put(k3, v3);
+       //val1 = table->get(k2);
 }
 
 int user_main(int argc, char *argv[]) {
        thrd_t t1, t2;
-       table = new cliffc_hashtable<IntWrapper, IntWrapper>();
+       table = new cliffc_hashtable<IntWrapper, IntWrapper>(2);
        val1 = NULL;
        val2 = NULL;
        //threadMain(NULL);

diff --git a/benchmark/mpmc-queue/mpmc-queue.h b/benchmark/mpmc-queue/mpmc-queue.h
index 823603fe4a566abd1aa1d6bdf5fe40b881770729..0c94b6ef5133cf7226a2269dedacd53c9333b086 100644 (file)
--- a/benchmark/mpmc-queue/mpmc-queue.h
+++ b/benchmark/mpmc-queue/mpmc-queue.h
@@ -71,8 +71,8 @@ public:
                unsigned int rdwr = m_rdwr.load(mo_acquire);
                /**
                        @Begin
-                       @Potential_commit_point_define: true
-                       @Label: Fetch_Potential_Point
+                       @Commit_point_define_check: (unsigned int) ((rdwr>>16) & 0xFFFF) == (unsigned int) (rdwr & 0xFFFF)
+                       @Label: Fetch_Fail_Point
                        @End
                */
                unsigned int rd,wr;
@@ -80,14 +80,18 @@ public:
                        rd = (rdwr>>16) & 0xFFFF;
                        wr = rdwr & 0xFFFF;
 
+                       //model_print("cond: %d\n", (unsigned int) ((rdwr>>16) & 0xFFFF) ==
+                       //(unsigned int) (rdwr & 0xFFFF));
+                       //model_print("cond: %d\n", wr == rd);
                        if ( wr == rd ) { // empty
                                /**
-                                       @Begin
+                                       //@Begin
                                        @Commit_point_define: true
                                        @Potential_commit_point_label: Fetch_Potential_Point 
                                        @Label: Fetch_Fail_Point
                                        @End
                                */
+                               model_print("in cond\n");
                                return false;
                        }
                        

diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
index 1d78d6d72e1bae1493f930fffb3527bc41fcc26a..0ada8dd96710437d63cf42646816f4c539175bc3 100644 (file)
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
@@ -306,10 +306,10 @@ public class CodeGenerator {
                                new File(homeDir + "/benchmark/mpmc-queue/mpmc-queue.h"),
                                new File(homeDir + "/benchmark/mpmc-queue/mpmc-queue.cc") };
 
-               File[][] sources = { srcLinuxRWLocks, srcHashtable, srcMSQueue, srcRCU,
-                               srcDeque, srcMCSLock, srcSPSCQueue, srcMPMCQueue };
+               File[][] sources = { srcLinuxRWLocks,  srcMSQueue, srcRCU,
+                               srcDeque, srcMCSLock, srcSPSCQueue, srcMPMCQueue, srcHashtable };
 
-//              File[][] sources = { srcDeque };
+//              File[][] sources = { srcMPMCQueue };
                // Compile all the benchmarks
                for (int i = 0; i < sources.length; i++) {
                        CodeGenerator gen = new CodeGenerator(sources[i]);