minor fix

diff --git a/benchmark/cliffc-hashtable/cliffc_hashtable.h b/benchmark/cliffc-hashtable/cliffc_hashtable.h
index 9ac59952580d26725aebe62ec10ea5b37d99ce6f..c3cea0d20fef1ae5130a603201508c7acfedc279 100644 (file)
--- a/benchmark/cliffc-hashtable/cliffc_hashtable.h
+++ b/benchmark/cliffc-hashtable/cliffc_hashtable.h
@@ -130,7 +130,7 @@ class cliffc_hashtable {
                                        *id2 = (id_tag_t*) ptr2;
                                if (id1 == NULL || id2 == NULL)
                                        return false;
-                               return *id1 == *id2;
+                               return (*id1).tag == (*id2).tag;
                        }
 
                        @DefineFunc:
@@ -399,6 +399,12 @@ 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(init_size);
                void *chm = (void*) new CHM(0);
                kvs->_data[0].store(chm, memory_order_relaxed);

diff --git a/benchmark/read-copy-update/rcu.cc b/benchmark/read-copy-update/rcu.cc
index cdd193f1385f4ec6d35266b0524d101ffe4cce20..6f791263c677abb002629a5c68c68afd9ccf3ba7 100644 (file)
--- a/benchmark/read-copy-update/rcu.cc
+++ b/benchmark/read-copy-update/rcu.cc
@@ -9,6 +9,7 @@
 #include <cdsannotate.h>
 #include <specannotation.h>
 #include <model_memory.h>
+#include "common.h" 
 
 #include "librace.h"
 
@@ -35,13 +36,14 @@ atomic<Data*> data;
                
                @DefineFunc:
                bool equals(Data *ptr1, Data *ptr2) {
-                       if (ptr1->data1 == ptr2->data1
-                               && ptr1->data2 == ptr2->data2
-                               && ptr1->data3 == ptr2->data3) {
-                               return true;
-                       } else {
-                               return false;
-                       }
+                       //if (ptr1->data1 == ptr2->data1
+                       //      && ptr1->data2 == ptr2->data2
+                       //      && ptr1->data3 == ptr2->data3) {
+                       //      return true;
+                       //} else {
+                       //      return false;
+                       //}
+                       return ptr1 == ptr2;
                }
 
        @Happens_before:
@@ -68,6 +70,7 @@ Data* read() {
                @Label: Read_Success_Point
                @End
        */
+       //model_print("Read: %d\n", res);
        return res;
 }
 
@@ -80,20 +83,19 @@ Data* read() {
        @End
 */
 void write(Data *new_data) {
-       while (true) {
-               Data *prev = data.load(memory_order_relaxed);
-               bool succ = data.compare_exchange_strong(prev, new_data,
+       Data *prev = data.load(memory_order_relaxed);
+       bool succ = false;
+       do {
+               succ = data.compare_exchange_strong(prev, new_data,
                        memory_order_release, memory_order_relaxed); 
                /**
                        @Begin
-                       @Commit_point_define_check: succ == true
+                       @Commit_point_define_check: succ
                        @Label: Write_Success_Point
                        @End
                */
-               if (succ) {
-                       break;
-               }
-       }
+       } while (!succ);
+       //model_print("Write: %d\n", new_data);
 }
 
 void threadA(void *arg) {
@@ -136,19 +138,19 @@ int user_main(int argc, char **argv) {
        thrd_t t1, t2, t3, t4;
        data.store(NULL, memory_order_relaxed);
        Data *data_init = (Data*) malloc(sizeof(Data));
-       data_init->data1 = 1;
-       data_init->data2 = 2;
-       data_init->data3 = 3;
+       data_init->data1 = 0;
+       data_init->data2 = 0;
+       data_init->data3 = 0;
        write(data_init);
 
        thrd_create(&t1, threadA, NULL);
        thrd_create(&t2, threadB, NULL);
-       //thrd_create(&t3, threadC, NULL);
+       thrd_create(&t3, threadC, NULL);
        thrd_create(&t4, threadD, NULL);
 
        thrd_join(t1);
        thrd_join(t2);
-       //thrd_join(t3);
+       thrd_join(t3);
        thrd_join(t4);
 
        return 0;