From: Peizhao Ou 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 *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(); 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; @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);