From: Peizhao Ou <peizhaoo@uci.edu>
Date: Fri, 21 Mar 2014 23:20:25 +0000 (-0700)
Subject: minor fix
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=635b0659aadff512de8d0ca508ecd98cce4f845c;p=cdsspec-compiler.git
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<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 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<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 ee3950d..d482c9e 100644
--- 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 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 <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
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