From: Peizhao Ou Date: Fri, 21 Mar 2014 23:20:25 +0000 (-0700) Subject: minor fix X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=635b0659aadff512de8d0ca508ecd98cce4f845c minor fix --- diff --git a/benchmark/cliffc-hashtable/cliffc_hashtable.h b/benchmark/cliffc-hashtable/cliffc_hashtable.h index 3830eed..fb50583 100644 --- 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 f18064d..351c0da 100644 --- a/benchmark/cliffc-hashtable/main.cc +++ b/benchmark/cliffc-hashtable/main.cc @@ -51,16 +51,11 @@ class IntWrapper { cliffc_hashtable *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(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 0785711..bf172ea 100644 --- 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 *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 *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 *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 queue; + struct mpmc_boundq_1_alt 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 ee3950d..d482c9e 100644 --- a/benchmark/mpmc-queue/mpmc-queue.h +++ b/benchmark/mpmc-queue/mpmc-queue.h @@ -2,6 +2,12 @@ #include #include +#include +#include +#include +#include +#include + /** @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 0ada8dd..640ddd1 100644 --- 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 index d771ce4..0000000 --- a/test.c +++ /dev/null @@ -1,9 +0,0 @@ -#include - -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 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 index b8182e5..0000000 --- a/test.h +++ /dev/null @@ -1,5 +0,0 @@ -#ifndef _TEST_H -#define _TEST_H - - -#endif