X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=blobdiff_plain;f=benchmark%2Fmpmc-queue%2Fmpmc-queue.h;h=ff6a168f1c248cc2db457f8fa7b7da8dc818f91a;hp=1b737bdcf6af9a94032c4025905eaf511eccd81b;hb=7537757f9cbddcfa61076053bea0bddad28e37ad;hpb=903198262494ab58a885eed90d6310ea7ec917ac diff --git a/benchmark/mpmc-queue/mpmc-queue.h b/benchmark/mpmc-queue/mpmc-queue.h index 1b737bd..ff6a168 100644 --- a/benchmark/mpmc-queue/mpmc-queue.h +++ b/benchmark/mpmc-queue/mpmc-queue.h @@ -17,7 +17,11 @@ template 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]; @@ -29,7 +33,7 @@ private: public: - mpmc_boundq_1_alt() + mpmc_boundq_1_alt(int _MASK = 0xFFFF) { /** @Begin @@ -39,6 +43,9 @@ public: m_rdwr = 0; m_read = 0; m_written = 0; + // For this we want MASK = 1; MASK wrap around + MASK = _MASK; //0x11; + arr = m_array; } @@ -48,23 +55,28 @@ public: LANG = CPP; CLASS = mpmc_boundq_1_alt; @Global_define: - @DeclareStruct: - typedef struct elem { - t_element *pos; - bool written; - thread_id_t tid; - thread_id_t fetch_tid; - call_id_t id; - } elem; - @DeclareVar: - spec_list *list; - //id_tag_t *tag; - @InitVar: - list = new_spec_list(); - //tag = new_id_tag(); - @Happens_before: - Publish -> Fetch - Consume -> Prepare + @Happens_before: + Publish -> Fetch + Consume -> Prepare + @Commutativity: Prepare <-> Prepare: _Method1.__RET__ != + _Method2.__RET__ || !_Method1.__RET__ || !_Method2.__RET__ + @Commutativity: Prepare <-> Publish: _Method1.__RET__ != _Method2.bin || + !_Method1.__RET__ + @Commutativity: Prepare <-> Fetch: _Method1.__RET__ != _Method2.__RET__ + || !_Method1.__RET__ || !_Method2.__RET__ + @Commutativity: Prepare <-> Consume : _Method1.__RET__ != _Method2.bin || !_Method1.__RET__ + + @Commutativity: Publish <-> Publish: _Method1.bin != _Method2.bin + @Commutativity: Publish <-> Fetch: _Method1.bin != _Method2.__RET__ || + !_Method2.__RET__ + @Commutativity: Publish <-> Consume : _Method1.bin != _Method2.bin + + @Commutativity: Fetch <-> Fetch: _Method1.__RET__ != _Method2.__RET__ || + !_Method1.__RET__ || !_Method2.__RET__ + @Commutativity: Fetch <-> Consume : _Method1.__RET__ != _Method2.bin || !_Method1.__RET__ + + @Commutativity: Consume <-> Consume : _Method1.bin != _Method2.bin + @End */ @@ -73,79 +85,81 @@ 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__ - //@Check: - //__RET__ == NULL || has_elem(list, __RET__) + //@Action: model_print("Fetch: %d\n", __RET__); @End */ t_element * read_fetch() { - // Try this new weaker semantics + // Since we have a lool to CAS the value of m_rdwr, this can be relaxed unsigned int rdwr = m_rdwr.load(mo_acquire); //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; for(;;) { - rd = (rdwr>>16) & 0xFFFF; - wr = rdwr & 0xFFFF; + rd = (rdwr>>16) & MASK; + wr = rdwr & MASK; if ( wr == rd ) { // empty - + return false; + } + /**** Inadmissibility (testcase2.cc, MASK = 1, size = 1) ****/ + bool succ = + m_rdwr.compare_exchange_weak(rdwr,rdwr+(1<<16),mo_acq_rel); + if (succ) { + break; + } else { /** @Begin - @Commit_point_define: true - @Potential_commit_point_label: Fetch_Potential_RW_Load - @Label: Fetch_RW_Load_Empty + @Commit_point_clear: true + @Label: FetchClear1 @End */ - return false; - } - - 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) - break; - else + /** + @Begin + @Commit_point_define_check: true + @Label: FetchReadRW2 + @End + */ thrd_yield(); + } } // (*1) rl::backoff bo; while (true) { + /**** Inadmissibility ****/ int written = m_written.load(mo_acquire); - /** - @Begin - @Potential_commit_point_define: true - @Label: Fetch_Potential_W_Load - @End - */ - if ((written & 0xFFFF) != wr) { + if ((written & MASK) != wr) { thrd_yield(); } else { + printf("Fetch: m_written=%d\n", written); 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; } @@ -153,21 +167,18 @@ public: /** @Begin @Interface: Consume - @Commit_point_set: Consume_R_RMW + @Commit_point_set: ConsumeFetchAdd @ID: (call_id_t) bin - //@Check: - // consume_check(__TID__) - //@Action: - //consume(__TID__); + //@Action: model_print("Consume: %d\n", bin); @End */ void read_consume(t_element *bin) { - /**** FIXME: miss ****/ + /**** Inadmissibility ****/ m_read.fetch_add(1,mo_release); /** @Begin @Commit_point_define_check: true - @Label: Consume_R_RMW + @Label: ConsumeFetchAdd @End */ } @@ -177,80 +188,84 @@ 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__ - //@Check: - //prepare_check(__RET__, __TID__) - //@Action: - //push_back(list, __RET__); + //@Action: model_print("Prepare: %d\n", __RET__); @End */ t_element * write_prepare() { // Try weaker semantics + // Since we have a lool to CAS the value of m_rdwr, this can be relaxed unsigned int rdwr = m_rdwr.load(mo_acquire); //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; for(;;) { - rd = (rdwr>>16) & 0xFFFF; - wr = rdwr & 0xFFFF; + rd = (rdwr>>16) & MASK; + wr = rdwr & MASK; + //printf("write_prepare: rd=%d, wr=%d\n", rd, wr); - if ( wr == ((rd + t_size)&0xFFFF) ) { // full - - /** - @Begin - @Commit_point_define: true - @Potential_commit_point_label: Prepare_Potential_RW_Load - @Label: Prepare_RW_Load_Full - @End - */ + if ( wr == ((rd + t_size)&MASK) ) { // full return NULL; } + /**** Inadmissibility (testcase3.cc, MASK = 1, size = 1) ****/ bool succ = m_rdwr.compare_exchange_weak(rdwr,(rd<<16) | - ((wr+1)&0xFFFF),mo_acq_rel); - /** - @Begin - @Commit_point_define_check: succ - @Label: Prepare_RW_RMW - @End - */ - if (succ) + ((wr+1)&MASK),mo_acq_rel); + //printf("wr=%d\n", (wr+1)&MASK); + 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) rl::backoff bo; while (true) { + /**** Inadmissibility ****/ int read = m_read.load(mo_acquire); - /** - @Begin - @Potential_commit_point_define: true - @Label: Prepare_Potential_R_Load - @End - */ - if ((read & 0xFFFF) != rd) + 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; } @@ -260,22 +275,20 @@ public: @Interface: Publish @Commit_point_set: Publish_W_RMW @ID: (call_id_t) bin - //@Check: - //publish_check(__TID__) - //@Action: - //publish(__TID__); + //@Action: model_print("Publish: %d\n", bin); @End */ void write_publish(t_element *bin) { - /**** hb violation ****/ - m_written.fetch_add(1,mo_release); + /**** Inadmissibility ****/ + int tmp = m_written.fetch_add(1,mo_release); /** @Begin @Commit_point_define_check: true @Label: Publish_W_RMW @End */ + printf("publish: m_written=%d\n", tmp + 1); } //-----------------------------------------------------