From: Peizhao Ou <peizhaoo@uci.edu>
Date: Fri, 21 Mar 2014 01:41:20 +0000 (-0700)
Subject: save
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=d8379bc0ab37f46daad7fd5fa7538435591ef836;p=cdsspec-compiler.git
save
---
diff --git a/benchmark/chase-lev-deque-bugfix/deque.c b/benchmark/chase-lev-deque-bugfix/deque.c
index 7c32656..e94da48 100644
--- a/benchmark/chase-lev-deque-bugfix/deque.c
+++ b/benchmark/chase-lev-deque-bugfix/deque.c
@@ -45,11 +45,12 @@ int take(Deque *q) {
*/
if (t == b) {
/* Single last element in queue. */
+ //FIXME: weaken the following seq_cst causes no spec problem
bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t +
1, memory_order_seq_cst, memory_order_relaxed);
/**
@Begin
- @Commit_point_define_check: succ
+ @Commit_point_define_check: true
@Label: Take_Point3
@End
*/
@@ -116,6 +117,7 @@ void push(Deque *q, int x) {
@End
*/
int steal(Deque *q) {
+ //FIXME: weaken the following acquire causes no spec problem
size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
atomic_thread_fence(memory_order_seq_cst);
size_t b = atomic_load_explicit(&q->bottom, memory_order_acquire);
@@ -143,7 +145,7 @@ int steal(Deque *q) {
/**
@Begin
@Commit_point_define_check: !succ
- @Label: Steal_Point4
+ @Label: Steal_Point2
@End
*/
diff --git a/benchmark/chase-lev-deque-bugfix/deque.h b/benchmark/chase-lev-deque-bugfix/deque.h
index 5861eb0..6bb4698 100644
--- a/benchmark/chase-lev-deque-bugfix/deque.h
+++ b/benchmark/chase-lev-deque-bugfix/deque.h
@@ -70,9 +70,11 @@ void resize(Deque *q);
@ID: __RET__ == EMPTY ? DEFAULT_CALL_ID : get_id(back(__deque))
@Action:
int _Old_Val = EMPTY;
- if (size(__deque) > 0) {
- _Old_Val = get_data(back(__deque));
- pop_back(__deque);
+ if (__RET__ != EMPTY) {
+ if (size(__deque) > 0) {
+ _Old_Val = get_data(back(__deque));
+ pop_back(__deque);
+ }
}
@Post_check:
_Old_Val == __RET__
@@ -95,16 +97,18 @@ void push(Deque *q, int x);
/**
@Begin
@Interface: Steal
- @Commit_point_set: Steal_Point1 | Steal_Point2
+ @Commit_point_set: Steal_Point1 | Steal_Point2 | Steal_Point3
@ID: (__RET__ == EMPTY || __RET__ == ABORT) ? DEFAULT_CALL_ID : get_id(front(__deque))
@Action:
int _Old_Val = EMPTY;
- if (size(__deque) > 0) {
- _Old_Val = get_data(front(__deque));
- pop_front(__deque);
+ if (__RET__ != EMPTY && __RET__ != ABORT) {
+ if (size(__deque) > 0) {
+ _Old_Val = get_data(front(__deque));
+ pop_front(__deque);
+ }
}
@Post_check:
- _Old_Val == __RET__
+ _Old_Val == __RET__ || __RET__ == EMPTY || __RET__ == ABORT
@End
*/
int steal(Deque *q);
diff --git a/benchmark/cliffc-hashtable/cliffc_hashtable.h b/benchmark/cliffc-hashtable/cliffc_hashtable.h
index 536f1c4..738201c 100644
--- a/benchmark/cliffc-hashtable/cliffc_hashtable.h
+++ b/benchmark/cliffc-hashtable/cliffc_hashtable.h
@@ -391,9 +391,12 @@ friend class CHM;
// For other CHM in kvs_data, they should be initialzed in resize()
// because the size is determined dynamically
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) {
diff --git a/benchmark/cliffc-hashtable/main.cc b/benchmark/cliffc-hashtable/main.cc
index cecaa0c..517e4a7 100644
--- a/benchmark/cliffc-hashtable/main.cc
+++ b/benchmark/cliffc-hashtable/main.cc
@@ -53,6 +53,7 @@ cliffc_hashtable<IntWrapper, IntWrapper> *table;
IntWrapper *val1, *val2;
void threadA(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),
@@ -61,52 +62,51 @@ void threadA(void *arg) {
table->put(k2, v2);
val1 = table->get(k3);
table->put(k3, v3);
+ */
}
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);
val1 = table->get(k2);
-}
-
-void threadC(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, v1);
- table->put(k2, v2);
- val2 = table->get(k1);
+ */
}
void threadMain(void *arg) {
- for (int i = 200; i < 300; i++) {
+ /*
+ 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(k1, v3);
+ val1 = table->get(k2);
}
int user_main(int argc, char *argv[]) {
- thrd_t t1, t2, t3, t4;
+ thrd_t t1, t2;
table = new cliffc_hashtable<IntWrapper, IntWrapper>();
val1 = NULL;
val2 = NULL;
- threadMain(NULL);
+ //threadMain(NULL);
thrd_create(&t1, threadA, NULL);
thrd_create(&t2, threadB, NULL);
- //thrd_create(&t3, threadC, NULL);
- //thrd_create(&t4, threadD, NULL);
+ threadMain(NULL);
thrd_join(t1);
thrd_join(t2);
- //thrd_join(t3);
- //thrd_join(t4);
-
+ /*
if (val1 == NULL) {
cout << "val1: NULL" << endl;
} else {
@@ -118,6 +118,7 @@ int user_main(int argc, char *argv[]) {
} else {
cout << val2->get() << endl;
}
+ */
return 0;
}
diff --git a/benchmark/mcs-lock/mcs-lock.h b/benchmark/mcs-lock/mcs-lock.h
index e08a0e7..27db469 100644
--- a/benchmark/mcs-lock/mcs-lock.h
+++ b/benchmark/mcs-lock/mcs-lock.h
@@ -83,6 +83,7 @@ public:
// publish my node as the new tail :
mcs_node * pred = m_tail.exchange(me, std::mo_acq_rel);
+ // FIXME: Only weakening the mo_acq_rel cause the spec error
/**
@Begin
@Commit_point_define_check: pred == NULL
@@ -136,6 +137,7 @@ public:
bool success;
success = m_tail.compare_exchange_strong(
tail_was_me,NULL,std::mo_acq_rel);
+ // FIXME: Only weakening the mo_acq_rel cause the spec error
/**
@Begin
@Commit_point_define_check: success == true
diff --git a/benchmark/mpmc-queue/mpmc-queue.h b/benchmark/mpmc-queue/mpmc-queue.h
index 5d20f30..823603f 100644
--- a/benchmark/mpmc-queue/mpmc-queue.h
+++ b/benchmark/mpmc-queue/mpmc-queue.h
@@ -101,16 +101,17 @@ public:
// (*1)
rl::backoff bo;
+
while ( true ) {
- unsigned int tmp = m_written.load(mo_acquire);
- /**
- @Begin
- @Commit_point_define_check: (tmp & 0xFFFF) == wr
- @Label: Fetch_Succ_Point
- @End
- */
- if ((tmp & 0xFFFF) == wr)
+ if ((m_written.load(mo_acquire) & 0xFFFF) == wr) {
+ /**
+ @Begin
+ @Commit_point_define_check: true
+ @Label: Fetch_Succ_Point
+ @End
+ */
break;
+ }
thrd_yield();
}
diff --git a/benchmark/read-copy-update/rcu.cc b/benchmark/read-copy-update/rcu.cc
index 44ce986..cc512d6 100644
--- a/benchmark/read-copy-update/rcu.cc
+++ b/benchmark/read-copy-update/rcu.cc
@@ -53,7 +53,7 @@ atomic<Data*> data;
@Happens_before:
Write -> Read
- //Write -> Write
+ Write -> Write
@End
*/
@@ -107,7 +107,7 @@ Data* write(int d1, int d2, int d3) {
tmp->data2 = prev->data2 + d2;
tmp->data3 = prev->data3 + d3;
succ = data.compare_exchange_strong(prev, tmp,
- memory_order_release, memory_order_acquire);
+ memory_order_acq_rel, memory_order_acquire);
/**
@Begin
@Commit_point_define_check: succ
@@ -149,7 +149,7 @@ int user_main(int argc, char **argv) {
dataInit->data2 = 0;
dataInit->data3 = 0;
atomic_init(&data, dataInit);
- //write(0, 0, 0);
+ write(0, 0, 0);
thrd_create(&t1, threadA, NULL);
thrd_create(&t2, threadB, NULL);