From 7537757f9cbddcfa61076053bea0bddad28e37ad Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Thu, 19 Nov 2015 14:16:13 -0800 Subject: [PATCH] edits --- benchmark/concurrent-hashmap/hashmap.h | 29 +++-- benchmark/mpmc-queue/mpmc-queue.h | 142 +++++++++++++------------ benchmark/mpmc-queue/testcase2.cc | 2 +- benchmark/mpmc-queue/testcase3.cc | 2 +- 4 files changed, 93 insertions(+), 82 deletions(-) diff --git a/benchmark/concurrent-hashmap/hashmap.h b/benchmark/concurrent-hashmap/hashmap.h index 904d0b8..99973e3 100644 --- a/benchmark/concurrent-hashmap/hashmap.h +++ b/benchmark/concurrent-hashmap/hashmap.h @@ -130,7 +130,7 @@ class HashMap { /** @Begin @Interface: Get - @Commit_point_set: GetReadValue1 | GetReadEntry | GetReadValue2 + @Commit_point_set: GetReadValue1 | GetReadValue2 | GetReadNothing @ID: __RET__ @Action: int res = getIntegerMap(__map, key); @@ -156,13 +156,13 @@ class HashMap { // lock, we ignore this operation for the SC analysis, and otherwise we // take it into consideration - /**** UL ****/ + /**** UL (main.cc) ****/ Entry *firstPtr = first->load(acquire); e = firstPtr; while (e != NULL) { if (key, e->key) { - /**** inadmissible ****/ + /**** inadmissible (testcase1.cc) ****/ res = e->value.load(seq_cst); /** @Begin @@ -187,12 +187,6 @@ class HashMap { // Synchronized by locking, no need to be load acquire Entry *newFirstPtr = first->load(relaxed); - /** - @Begin - @Commit_point_define_check: true - @Label: GetReadEntry - @End - */ if (e != NULL || firstPtr != newFirstPtr) { e = newFirstPtr; while (e != NULL) { @@ -213,6 +207,12 @@ class HashMap { } } seg->unlock(); // Critical region ends + /** + @Begin + @Commit_point_define_check: true + @Label: GetReadNothing + @End + */ return 0; } @@ -249,7 +249,7 @@ class HashMap { // with the previous put()), no need to be acquire oldValue = e->value.load(relaxed); - /**** inadmissible ****/ + /**** inadmissible (testcase1.cc) ****/ e->value.store(value, seq_cst); /** @Begin @@ -267,9 +267,16 @@ class HashMap { // Add to front of list Entry *newEntry = new Entry(hash, key, value, firstPtr); - /**** UL ****/ + /**** UL (main.cc) ****/ // Publish the newEntry to others first->store(newEntry, release); + /** + @Begin + @Commit_point_clear: true + @Label: PutClear + @End + */ + /** @Begin @Commit_point_define_check: true diff --git a/benchmark/mpmc-queue/mpmc-queue.h b/benchmark/mpmc-queue/mpmc-queue.h index dff6777..ff6a168 100644 --- a/benchmark/mpmc-queue/mpmc-queue.h +++ b/benchmark/mpmc-queue/mpmc-queue.h @@ -19,7 +19,9 @@ struct mpmc_boundq_1_alt private: unsigned int MASK; - + + atomic arr; + // elements should generally be cache-line-size padded : t_element m_array[t_size]; @@ -31,7 +33,7 @@ private: public: - mpmc_boundq_1_alt() + mpmc_boundq_1_alt(int _MASK = 0xFFFF) { /** @Begin @@ -42,7 +44,8 @@ public: m_read = 0; m_written = 0; // For this we want MASK = 1; MASK wrap around - MASK = 0x1; // 11 + MASK = _MASK; //0x11; + arr = m_array; } @@ -82,7 +85,7 @@ public: /** @Begin @Interface: Fetch - @Commit_point_set: Fetch_RW_Load_Empty | Fetch_RW_RMW | Fetch_W_Load + @Commit_point_set: FetchReadRW1 | FetchReadRW2 | FetchReadPointer @ID: (call_id_t) __RET__ //@Action: model_print("Fetch: %d\n", __RET__); @End @@ -93,8 +96,8 @@ public: //unsigned int rdwr = m_rdwr.load(mo_relaxed); /** @Begin - @Potential_commit_point_define: true - @Label: Fetch_Potential_RW_Load + @Commit_point_define_check: true + @Label: FetchReadRW1 @End */ unsigned int rd,wr; @@ -103,31 +106,29 @@ public: wr = rdwr & MASK; if ( wr == rd ) { // empty - - /** - @Begin - @Commit_point_define: true - @Potential_commit_point_label: Fetch_Potential_RW_Load - @Label: Fetch_RW_Load_Empty - @End - */ - return false; } - /**** Inadmissibility (testcase2.cc, MASK = 1, size = 1) ****/ bool succ = - m_rdwr.compare_exchange_weak(rdwr,rdwr+(1<<16),mo_acq_rel); - /** - @Begin - @Commit_point_define_check: succ - @Label: Fetch_RW_RMW - @End - */ - if (succ) + m_rdwr.compare_exchange_weak(rdwr,rdwr+(1<<16),mo_acq_rel); + if (succ) { break; - else + } else { + /** + @Begin + @Commit_point_clear: true + @Label: FetchClear1 + @End + */ + + /** + @Begin + @Commit_point_define_check: true + @Label: FetchReadRW2 + @End + */ thrd_yield(); + } } // (*1) @@ -135,12 +136,6 @@ public: while (true) { /**** Inadmissibility ****/ int written = m_written.load(mo_acquire); - /** - @Begin - @Potential_commit_point_define: true - @Label: Fetch_Potential_W_Load - @End - */ if ((written & MASK) != wr) { thrd_yield(); } else { @@ -148,16 +143,23 @@ public: break; } } - + t_element * p = & ( m_array[ rd % t_size ] ); + + // This is just a hack to tell the CDSChecker that we have a memory + // operation here + arr.load(memory_order_relaxed); /** @Begin - @Commit_point_define: true - @Potential_commit_point_label: Fetch_Potential_W_Load - @Label: Fetch_W_Load + @Commit_point_clear: true + @Label: FetchClear2 + @End + */ + /** + @Begin + @Commit_point_define_check: true + @Label: FetchReadPointer @End */ - - t_element * p = & ( m_array[ rd % t_size ] ); return p; } @@ -165,7 +167,7 @@ public: /** @Begin @Interface: Consume - @Commit_point_set: Consume_R_RMW + @Commit_point_set: ConsumeFetchAdd @ID: (call_id_t) bin //@Action: model_print("Consume: %d\n", bin); @End @@ -176,7 +178,7 @@ public: /** @Begin @Commit_point_define_check: true - @Label: Consume_R_RMW + @Label: ConsumeFetchAdd @End */ } @@ -186,7 +188,7 @@ public: /** @Begin @Interface: Prepare - @Commit_point_set: Prepare_RW_Load_Full | Prepare_RW_RMW | Prepare_R_Load + @Commit_point_set: PrepareReadRW1 | PrepareReadRW2 | PrepareReadPointer @ID: (call_id_t) __RET__ //@Action: model_print("Prepare: %d\n", __RET__); @End @@ -198,8 +200,8 @@ public: //unsigned int rdwr = m_rdwr.load(mo_relaxed); /** @Begin - @Potential_commit_point_define: true - @Label: Prepare_Potential_RW_Load + @Commit_point_define_check: true + @Label: PrepareReadRW1 @End */ unsigned int rd,wr; @@ -209,31 +211,31 @@ public: //printf("write_prepare: rd=%d, wr=%d\n", rd, wr); if ( wr == ((rd + t_size)&MASK) ) { // full - - /** - @Begin - @Commit_point_define: true - @Potential_commit_point_label: Prepare_Potential_RW_Load - @Label: Prepare_RW_Load_Full - @End - */ return NULL; } /**** Inadmissibility (testcase3.cc, MASK = 1, size = 1) ****/ bool succ = m_rdwr.compare_exchange_weak(rdwr,(rd<<16) | ((wr+1)&MASK),mo_acq_rel); - /** - @Begin - @Commit_point_define_check: succ - @Label: Prepare_RW_RMW - @End - */ //printf("wr=%d\n", (wr+1)&MASK); - if (succ) + if (succ) { break; - else + } else { + /** + @Begin + @Commit_point_clear: true + @Label: PrepareClear1 + @End + */ + + /** + @Begin + @Commit_point_define_check: true + @Label: PrepareReadRW2 + @End + */ thrd_yield(); + } } // (*1) @@ -241,27 +243,29 @@ public: while (true) { /**** Inadmissibility ****/ int read = m_read.load(mo_acquire); - /** - @Begin - @Potential_commit_point_define: true - @Label: Prepare_Potential_R_Load - @End - */ if ((read & MASK) != rd) thrd_yield(); else break; } + t_element * p = & ( m_array[ wr % t_size ] ); + + // This is also just a hack to tell the CDSChecker that we have a memory + // operation here + arr.load(memory_order_relaxed); /** @Begin - @Commit_point_define: true - @Potential_commit_point_label: Prepare_Potential_R_Load - @Label: Prepare_R_Load + @Commit_point_clear: true + @Label: PrepareClear2 + @End + */ + /** + @Begin + @Commit_point_define_check: true + @Label: PrepareReadPointer @End */ - - t_element * p = & ( m_array[ wr % t_size ] ); return p; } diff --git a/benchmark/mpmc-queue/testcase2.cc b/benchmark/mpmc-queue/testcase2.cc index a26f981..f03ea41 100644 --- a/benchmark/mpmc-queue/testcase2.cc +++ b/benchmark/mpmc-queue/testcase2.cc @@ -61,7 +61,7 @@ void threadB(struct mpmc_boundq_1_alt *queue) int user_main(int argc, char **argv) { - struct mpmc_boundq_1_alt queue; + struct mpmc_boundq_1_alt queue(0x1); thrd_t A, A1, B; printf("Adding initial element\n"); diff --git a/benchmark/mpmc-queue/testcase3.cc b/benchmark/mpmc-queue/testcase3.cc index b171c75..a0a857e 100644 --- a/benchmark/mpmc-queue/testcase3.cc +++ b/benchmark/mpmc-queue/testcase3.cc @@ -74,7 +74,7 @@ void threadC(struct mpmc_boundq_1_alt *queue) int user_main(int argc, char **argv) { - struct mpmc_boundq_1_alt queue; + struct mpmc_boundq_1_alt queue(0x1); thrd_t A, A1, B, B1, C, C1; printf("Adding initial element\n"); -- 2.34.1