+++ /dev/null
-#include <stdatomic.h>
-#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
- @End
-*/
-template <typename t_element, size_t t_size>
-struct mpmc_boundq_1_alt
-{
-private:
-
- unsigned int MASK;
-
- atomic<t_element*> arr;
-
- // elements should generally be cache-line-size padded :
- t_element m_array[t_size];
-
- // rdwr counts the reads & writes that have started
- atomic<unsigned int> m_rdwr;
- // "read" and "written" count the number completed
- atomic<unsigned int> m_read;
- atomic<unsigned int> m_written;
-
-public:
-
- mpmc_boundq_1_alt(int _MASK = 0xFFFF)
- {
- /**
- @Begin
- @Entry_point
- @End
- */
- m_rdwr = 0;
- m_read = 0;
- m_written = 0;
- // For this we want MASK = 1; MASK wrap around
- MASK = _MASK; //0x11;
- arr = m_array;
- }
-
-
- /**
- @Begin
- @Options:
- LANG = CPP;
- CLASS = mpmc_boundq_1_alt;
- @Global_define:
- @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
- */
-
- //-----------------------------------------------------
-
- /**
- @Begin
- @Interface: Fetch
- @Commit_point_set: FetchReadRW1 | FetchReadRW2 | FetchReadPointer
- @ID: (call_id_t) __RET__
- //@Action: model_print("Fetch: %d\n", __RET__);
- @End
- */
- t_element * read_fetch() {
- // 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
- @Commit_point_define_check: true
- @Label: FetchReadRW1
- @End
- */
- unsigned int rd,wr;
- for(;;) {
- 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_clear: true
- @Label: FetchClear1
- @End
- */
-
- /**
- @Begin
- @Commit_point_define_check: true
- @Label: FetchReadRW2
- @End
- */
- thrd_yield();
- }
- }
-
- // (*1)
- rl::backoff bo;
- while (true) {
- /**** Inadmissibility (testcase2.c) ****/
- int written = m_written.load(mo_acquire);
- 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_clear: true
- @Label: FetchClear2
- @End
- */
- /**
- @Begin
- @Commit_point_define_check: true
- @Label: FetchReadPointer
- @End
- */
-
- return p;
- }
-
- /**
- @Begin
- @Interface: Consume
- @Commit_point_set: ConsumeFetchAdd
- @ID: (call_id_t) bin
- //@Action: model_print("Consume: %d\n", bin);
- @End
- */
- void read_consume(t_element *bin) {
- /**** Inadmissibility (testcase1.c) ****/
- m_read.fetch_add(1,mo_release);
- /**
- @Begin
- @Commit_point_define_check: true
- @Label: ConsumeFetchAdd
- @End
- */
- }
-
- //-----------------------------------------------------
-
- /**
- @Begin
- @Interface: Prepare
- @Commit_point_set: PrepareReadRW1 | PrepareReadRW2 | PrepareReadPointer
- @ID: (call_id_t) __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
- @Commit_point_define_check: true
- @Label: PrepareReadRW1
- @End
- */
- unsigned int rd,wr;
- for(;;) {
- rd = (rdwr>>16) & MASK;
- wr = rdwr & MASK;
- //printf("write_prepare: rd=%d, wr=%d\n", rd, wr);
-
- if ( wr == ((rd + t_size)&MASK) ) { // full
- return NULL;
- }
-
- // FIXME: Theoretically we have a bug here, it is not so likely to
- // happen!!! The following acq_rel can not guarantee that the load
- // acquire on m_read to read the most recent value. However, it can
- // decrease the chance of the load acquire of m_read to read a too
- // old value. Same as the case in read_fetch(). Maybe making things
- // SC can fix it. We can run testcase3.c to expose this bug (set the
- // array size = 1, the MASK = 1).
-
- /**** Inadmissibility (testcase3.cc, MASK = 1, size = 1) ****/
- bool succ = m_rdwr.compare_exchange_weak(rdwr,(rd<<16) |
- ((wr+1)&MASK),mo_acq_rel);
- //printf("wr=%d\n", (wr+1)&MASK);
- if (succ) {
- break;
- } 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 (testcase1.c) ****/
- int read = m_read.load(mo_acquire);
- 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_clear: true
- @Label: PrepareClear2
- @End
- */
- /**
- @Begin
- @Commit_point_define_check: true
- @Label: PrepareReadPointer
- @End
- */
-
- return p;
- }
-
- /**
- @Begin
- @Interface: Publish
- @Commit_point_set: PublishFetchAdd
- @ID: (call_id_t) bin
- //@Action: model_print("Publish: %d\n", bin);
- @End
- */
- void write_publish(t_element *bin)
- {
- /**** Inadmissibility (testcase2.c) ****/
- int tmp = m_written.fetch_add(1,mo_release);
- /**
- @Begin
- @Commit_point_define_check: true
- @Label: PublishFetchAdd
- @End
- */
- printf("publish: m_written=%d\n", tmp + 1);
- }
-
- //-----------------------------------------------------
-
-
-};
-/**
- @Begin
- @Class_end
- @End
-*/
projects / cdsspec-compiler.git / blobdiff