minor fix

diff --git a/benchmark/cliffc-hashtable/cliffc_hashtable.h b/benchmark/cliffc-hashtable/cliffc_hashtable.h
index 3830eed081ad302ff912a57541074ac4401370e5..fb505834da85134b2a06ffa0c1922f004a93a134 100644 (file)
--- a/benchmark/cliffc-hashtable/cliffc_hashtable.h
+++ b/benchmark/cliffc-hashtable/cliffc_hashtable.h
@@ -118,6 +118,8 @@ class cliffc_hashtable {
                        
                        @DefineFunc:
                        bool equals_val(void *ptr1, void *ptr2) {
+                               if (ptr1 == ptr2)
+                                       return true;
                                TypeV *val1 = (TypeV*) ptr1,
                                        *val2 = (TypeV*) ptr2;
                                if (val1 == NULL || val2 == NULL)
@@ -683,7 +685,7 @@ friend class CHM;
                        slot *V = val(kvs, idx);
                        /**
                                @Begin
-                               @Commit_point_define: V == NULL
+                               @Commit_point_define: K == NULL
                                @Potential_commit_point_label: Read_Val_Point
                                @Label: Get_Success_Point_1
                                @End

diff --git a/benchmark/cliffc-hashtable/main.cc b/benchmark/cliffc-hashtable/main.cc
index f18064db98e398ed7eb8a555db1ad866cab3010f..351c0da7989fecad5c0ec98b20f5da768541d20b 100644 (file)
--- a/benchmark/cliffc-hashtable/main.cc
+++ b/benchmark/cliffc-hashtable/main.cc
@@ -51,16 +51,11 @@ class IntWrapper {
 
 cliffc_hashtable<IntWrapper, IntWrapper> *table;
 IntWrapper *val1, *val2;
+IntWrapper *k1, *k2, *k3, *k4, *k5;
+IntWrapper *v1, *v2, *v3, *v4, *v5;
 
 void threadA(void *arg) {
-       
-       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);
        
@@ -75,10 +70,6 @@ void threadA(void *arg) {
 
 void threadB(void *arg) {
        /*
-       IntWrapper *k1 = new IntWrapper(3), *k2 = new IntWrapper(5),
-               *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(k2, v4);
@@ -87,26 +78,28 @@ void threadB(void *arg) {
 }
 
 void threadMain(void *arg) {
-       /*
-       for (int i = 0; i < 5; i++) {
-               IntWrapper *k = new IntWrapper(i), *v = new IntWrapper(i * 2);
-               table->put(k, v);
-       }
-       */
-       IntWrapper *k1 = new IntWrapper(3), *k2 = new IntWrapper(5),
-               *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(k3, v3);
-       //val1 = table->get(k2);
+       val1 = table->get(k1);
+       if (val1 != NULL)
+               model_print("val1: %d\n", val1->_val);
+       else
+               model_print("val1: NULL\n");
 }
 
 int user_main(int argc, char *argv[]) {
        thrd_t t1, t2;
        table = new cliffc_hashtable<IntWrapper, IntWrapper>(2);
-       val1 = NULL;
-       val2 = NULL;
-       //threadMain(NULL);
+    k1 = new IntWrapper(3);
+       k2 = new IntWrapper(5);
+       k3 = new IntWrapper(11);
+       k4 = new IntWrapper(7);
+       k5 = new IntWrapper(13);
+
+       v1 = new IntWrapper(1024);
+       v2 = new IntWrapper(47);
+       v3 = new IntWrapper(73);
+       v4 = new IntWrapper(81);
+       v5 = new IntWrapper(99);
 
        thrd_create(&t1, threadA, NULL);
        thrd_create(&t2, threadB, NULL);

diff --git a/benchmark/mpmc-queue/mpmc-queue.cc b/benchmark/mpmc-queue/mpmc-queue.cc
index 0785711ff6c86dd34335132f1f16b8747ae43bf3..bf172ea1ef4f4900361d27f72274cd791891335c 100644 (file)
--- a/benchmark/mpmc-queue/mpmc-queue.cc
+++ b/benchmark/mpmc-queue/mpmc-queue.cc
@@ -11,7 +11,8 @@
 void threadA(struct mpmc_boundq_1_alt<int32_t, sizeof(int32_t)> *queue)
 {
        int32_t *bin = queue->write_prepare();
-       store_32(bin, 1);
+       //store_32(bin, 1);
+       *bin = 1;
        printf("write_bin %d, val %d\n", bin, 1);
        queue->write_publish(bin);
 }
@@ -20,21 +21,24 @@ void threadB(struct mpmc_boundq_1_alt<int32_t, sizeof(int32_t)> *queue)
 {
        int32_t *bin;
        while (bin = queue->read_fetch()) {
-               printf("Read: %d\n", load_32(bin));
-               printf("read_bin %d, val %d\n", bin, load_32(bin));
-               queue->read_consume();
+               //printf("Read: %d\n", load_32(bin));
+               //printf("read_bin %d, val %d\n", bin, load_32(bin));
+               printf("Read: %d\n", *bin);
+               queue->read_consume(bin);
        }
 }
 
 void threadC(struct mpmc_boundq_1_alt<int32_t, sizeof(int32_t)> *queue)
 {
        int32_t *bin = queue->write_prepare();
-       store_32(bin, 1);
+       //store_32(bin, 1);
+       *bin = 1;
        queue->write_publish(bin);
 
        while (bin = queue->read_fetch()) {
-               printf("Read: %d\n", load_32(bin));
-               queue->read_consume();
+               //printf("Read: %d\n", load_32(bin));
+               printf("Read: %d\n", *bin);
+               queue->read_consume(bin);
        }
 }
 
@@ -104,7 +108,7 @@ void process_params(int argc, char **argv)
 
 int user_main(int argc, char **argv)
 {
-       struct mpmc_boundq_1_alt<int32_t, sizeof(int32_t)> queue;
+       struct mpmc_boundq_1_alt<int32_t, 2> queue;
        thrd_t A[MAXWRITERS], B[MAXREADERS], C[MAXRDWR];
 
        /* Note: optarg() / optind is broken in model-checker - workaround is
@@ -115,7 +119,8 @@ int user_main(int argc, char **argv)
 #ifndef CONFIG_MPMC_NO_INITIAL_ELEMENT
        printf("Adding initial element\n");
        int32_t *bin = queue.write_prepare();
-       store_32(bin, 17);
+       //store_32(bin, 17);
+       *bin, 17;
        printf("init_write_bin %d, val %d\n", bin, 17);
        queue.write_publish(bin);
 #endif

diff --git a/benchmark/mpmc-queue/mpmc-queue.h b/benchmark/mpmc-queue/mpmc-queue.h
index ee3950d8219d14dcc7a2ed2b7924e1d07c7bbdb7..d482c9e9790b62d430637b1ec9c222a386199b4a 100644 (file)
--- a/benchmark/mpmc-queue/mpmc-queue.h
+++ b/benchmark/mpmc-queue/mpmc-queue.h
@@ -2,6 +2,12 @@
 #include <unrelacy.h>
 #include <common.h>
 
+#include <spec_lib.h>
+#include <stdlib.h>
+#include <cdsannotate.h>
+#include <specannotation.h>
+#include <model_memory.h>
+
 /**
        @Begin
        @Class_begin
@@ -52,199 +58,13 @@ public:
                        } elem;
                @DeclareVar:
                        spec_list *list;
-                       id_tag_t *tag;
+                       //id_tag_t *tag;
                @InitVar:
                        list = new_spec_list();
-                       tag = new_id_tag();
-               @DefineFunc:
-                       elem* new_elem(t_element *pos, call_id_t id, thread_id_t tid) {
-                               elem *e = (elem*) MODEL_MALLOC(sizeof(elem));
-                               e->pos = pos;
-                               e->written = false;
-                               e->id = id;
-                               e->tid = tid;
-                               e->fetch_tid = -1;
-                       }
-               @DefineFunc:
-                       elem* get_elem_by_pos(t_element *pos) {
-                               for (int i = 0; i < size(list); i++) {
-                                       elem *e = (elem*) elem_at_index(list, i);
-                                       if (e->pos == pos) {
-                                               return e;
-                                       }
-                               }
-                               return NULL;
-                       }
-               @DefineFunc:
-                       void show_list() {
-                               //model_print("Status:\n");
-                               for (int i = 0; i < size(list); i++) {
-                                       elem *e = (elem*) elem_at_index(list, i);
-                                       //model_print("%d: pos %d, written %d, tid %d, fetch_tid %d, call_id %d\n", i, e->pos, e->written, e->tid, e->fetch_tid, e->id); 
-                               }
-                       }
-               @DefineFunc:
-                       elem* get_elem_by_tid(thread_id_t tid) {
-                               for (int i = 0; i < size(list); i++) {
-                                       elem *e = (elem*) elem_at_index(list, i);
-                                       if (e->tid== tid) {
-                                               return e;
-                                       }
-                               }
-                               return NULL;
-                       }
-               @DefineFunc:
-                       elem* get_elem_by_fetch_tid(thread_id_t fetch_tid) {
-                               for (int i = 0; i < size(list); i++) {
-                                       elem *e = (elem*) elem_at_index(list, i);
-                                       if (e->fetch_tid== fetch_tid) {
-                                               return e;
-                                       }
-                               }
-                               return NULL;
-                       }
-               @DefineFunc:
-                       int elem_idx_by_pos(t_element *pos) {
-                               for (int i = 0; i < size(list); i++) {
-                                       elem *existing = (elem*) elem_at_index(list, i);
-                                       if (pos == existing->pos) {
-                                               return i;
-                                       }
-                               }
-                               return -1;
-                       }
-               @DefineFunc:
-                       int elem_idx_by_tid(thread_id_t tid) {
-                               for (int i = 0; i < size(list); i++) {
-                                       elem *existing = (elem*) elem_at_index(list, i);
-                                       if (tid == existing->tid) {
-                                               return i;
-                                       }
-                               }
-                               return -1;
-                       }
-               @DefineFunc:
-                       int elem_idx_by_fetch_tid(thread_id_t fetch_tid) {
-                               for (int i = 0; i < size(list); i++) {
-                                       elem *existing = (elem*) elem_at_index(list, i);
-                                       if (fetch_tid == existing->fetch_tid) {
-                                               return i;
-                                       }
-                               }
-                               return -1;
-                       }
-               @DefineFunc:
-                       int elem_num(t_element *pos) {
-                               int cnt = 0;
-                               for (int i = 0; i < size(list); i++) {
-                                       elem *existing = (elem*) elem_at_index(list, i);
-                                       if (pos == existing->pos) {
-                                               cnt++;
-                                       }
-                               }
-                               return cnt;
-                       }
-               @DefineFunc:
-                       call_id_t prepare_id() {
-                               call_id_t res = get_and_inc(tag);
-                               //model_print("prepare_id: %d\n", res);
-                               return res;
-                       }
-               @DefineFunc:
-                       bool prepare_check(t_element *pos, thread_id_t tid) {
-                               show_list();
-                               elem *e = get_elem_by_pos(pos);
-                               //model_print("prepare_check: e %d\n", e);
-                               return NULL == e;
-                       }
-               @DefineFunc:
-                       void prepare(call_id_t id, t_element *pos, thread_id_t tid) {
-                               //model_print("prepare: id %d, pos %d, tid %d\n", id, pos, tid);
-                               elem *e = new_elem(pos, id, tid);
-                               push_back(list, e);
-                       }
-               @DefineFunc:
-                       call_id_t publish_id(thread_id_t tid) {
-                               elem *e = get_elem_by_tid(tid);
-                               //model_print("publish_id: id %d\n", e == NULL ? 0 : e->id);
-                               if (NULL == e)
-                                       return DEFAULT_CALL_ID;
-                               return e->id;
-                       }
-               @DefineFunc:
-                       bool publish_check(thread_id_t tid) {
-                               show_list();
-                               elem *e = get_elem_by_tid(tid);
-                               //model_print("publish_check: tid %d\n", tid);
-                               if (NULL == e)
-                                       return false;
-                               if (elem_num(e->pos) > 1)
-                                       return false;
-                               return !e->written;
-                       }
-               @DefineFunc:
-                       void publish(thread_id_t tid) {
-                               //model_print("publish: tid %d\n", tid);
-                               elem *e = get_elem_by_tid(tid);
-                               e->written = true;
-                       }
-               @DefineFunc:
-                       call_id_t fetch_id(t_element *pos) {
-                               elem *e = get_elem_by_pos(pos);
-                               //model_print("fetch_id: id %d\n", e == NULL ? 0 : e->id);
-                               if (NULL == e)
-                                       return DEFAULT_CALL_ID;
-                               return e->id;
-                       }
-               @DefineFunc:
-                       bool fetch_check(t_element *pos) {
-                               show_list();
-                               if (pos == NULL) return true;
-                               elem *e = get_elem_by_pos(pos);
-                               //model_print("fetch_check: pos %d, e %d\n", pos, e);
-                               if (e == NULL) return false;
-                               if (elem_num(e->pos) > 1)
-                                       return false;
-                               return true;
-                       }
-               @DefineFunc:
-                       void fetch(t_element *pos, thread_id_t tid) {
-                               if (pos == NULL) return;
-                               elem *e = (elem*) get_elem_by_pos(pos);
-                               //model_print("fetch: pos %d, tid %d\n", pos, tid);
-                               // Remember the thread that fetches the position
-                               e->fetch_tid = tid;
-                       }
-               @DefineFunc:
-                       bool consume_check(thread_id_t tid) {
-                               show_list();
-                               elem *e = get_elem_by_fetch_tid(tid);
-                               //model_print("consume_check: tid %d, e %d\n", tid, e);
-                               if (NULL == e)
-                                       return false;
-                               if (elem_num(e->pos) > 1)
-                                       return false;
-                               return e->written;
-                       }
-               @DefineFunc:
-                       call_id_t consume_id(thread_id_t tid) {
-                               elem *e = get_elem_by_fetch_tid(tid);
-                               //model_print("consume_id: id %d\n", e == NULL ? 0 : e->id);
-                               if (NULL == e)
-                                       return DEFAULT_CALL_ID;
-                               return e->id;
-                       }
-               @DefineFunc:
-                       void consume(thread_id_t tid) {
-                               //model_print("consume: tid %d\n", tid);
-                               int idx = elem_idx_by_fetch_tid(tid);
-                               if (idx == -1)
-                                       return;
-                               remove_at_index(list, idx);
-                       }
+                       //tag = new_id_tag();
        @Happens_before:
-               Prepare -> Fetch
-               Publish -> Consume
+               Publish -> Fetch
+               Consume -> Prepare
        @End
        */
 
@@ -254,15 +74,15 @@ public:
                @Begin
                @Interface: Fetch
                @Commit_point_set: Fetch_Empty_Point | Fetch_Succ_Point
-               @ID: fetch_id(__RET__)
-               @Check:
-                       fetch_check(__RET__)
-               @Action:
-                       fetch(__RET__, __TID__);
+               @ID: (call_id_t) __RET__
+               //@Check:
+                       //__RET__ == NULL || has_elem(list, __RET__)
                @End
        */
        t_element * read_fetch() {
-               unsigned int rdwr = m_rdwr.load(mo_acquire);
+               // Try this new weaker semantics
+               //unsigned int rdwr = m_rdwr.load(mo_acquire);
+               unsigned int rdwr = m_rdwr.load(mo_relaxed);
                /**
                        @Begin
                        @Potential_commit_point_define: true
@@ -275,6 +95,7 @@ public:
                        wr = rdwr & 0xFFFF;
 
                        if ( wr == rd ) { // empty
+
                                /**
                                        @Begin
                                        @Commit_point_define: true
@@ -282,6 +103,7 @@ public:
                                        @Label: Fetch_Empty_Point
                                        @End
                                */
+
                                return false;
                        }
                        
@@ -313,14 +135,14 @@ public:
                @Begin
                @Interface: Consume
                @Commit_point_set: Consume_Point
-               @ID: consume_id(__TID__)
-               @Check:
-                       consume_check(__TID__)
-               @Action:
-                       consume(__TID__);
+               @ID: (call_id_t) bin 
+               //@Check:
+               //      consume_check(__TID__)
+               //@Action:
+                       //consume(__TID__);
                @End
        */
-       void read_consume() {
+       void read_consume(t_element *bin) {
                m_read.fetch_add(1,mo_release);
                /**
                        @Begin
@@ -336,15 +158,17 @@ public:
                @Begin
                @Interface: Prepare 
                @Commit_point_set: Prepare_Full_Point | Prepare_Succ_Point
-               @ID: prepare_id()
-               @Check:
-                       prepare_check(__RET__, __TID__)
-               @Action:
-                       prepare(__ID__, __RET__, __TID__);
+               @ID: (call_id_t) __RET__
+               //@Check:
+                       //prepare_check(__RET__, __TID__)
+               //@Action:
+                       //push_back(list, __RET__);
                @End
        */
        t_element * write_prepare() {
-               unsigned int rdwr = m_rdwr.load(mo_acquire);
+               // Try weaker semantics
+               //unsigned int rdwr = m_rdwr.load(mo_acquire);
+               unsigned int rdwr = m_rdwr.load(mo_relaxed);
                /**
                        @Begin
                        @Potential_commit_point_define: true
@@ -357,6 +181,7 @@ public:
                        wr = rdwr & 0xFFFF;
 
                        if ( wr == ((rd + t_size)&0xFFFF) ) { // full
+
                                /**
                                        @Begin
                                        @Commit_point_define: true
@@ -396,14 +221,14 @@ public:
                @Begin
                @Interface: Publish 
                @Commit_point_set: Publish_Point
-               @ID: publish_id(__TID__)
-               @Check:
-                       publish_check(__TID__)
-               @Action:
-                       publish(__TID__);
+               @ID: (call_id_t) bin 
+               //@Check:
+                       //publish_check(__TID__)
+               //@Action:
+                       //publish(__TID__);
                @End
        */
-       void write_publish()
+       void write_publish(t_element *bin)
        {
                m_written.fetch_add(1,mo_release);
                /**

diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
index 0ada8dd96710437d63cf42646816f4c539175bc3..640ddd1c0f09dcd5e32ff4e299b6bf56c61eb785 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,  srcMSQueue, srcRCU,
-                               srcDeque, srcMCSLock, srcSPSCQueue, srcMPMCQueue, srcHashtable };
+//             File[][] sources = { srcLinuxRWLocks,  srcMSQueue, srcRCU,
+//                             srcDeque, srcMCSLock, srcSPSCQueue, srcMPMCQueue, srcHashtable };
 
-//              File[][] sources = { srcMPMCQueue };
+                File[][] sources = { srcHashtable, srcMPMCQueue };
                // Compile all the benchmarks
                for (int i = 0; i < sources.length; i++) {
                        CodeGenerator gen = new CodeGenerator(sources[i]);

diff --git a/test.c b/test.c
deleted file mode 100644 (file)
index d771ce4..0000000
--- a/test.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <stdio.h>
-
-int test();
-
-int main() {
-       int a = test();
-       printf("%d\n", a);
-       return 1;
-}

diff --git a/test.cc b/test.cc
deleted file mode 100644 (file)
index 56bc554..0000000
--- a/test.cc
+++ /dev/null
@@ -1,3 +0,0 @@
-extern int test() {
-       return 10;
-}

diff --git a/test.h b/test.h
deleted file mode 100644 (file)
index b8182e5..0000000
--- a/test.h
+++ /dev/null
@@ -1,5 +0,0 @@
-#ifndef _TEST_H
-#define _TEST_H
-
-
-#endif