#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];
public:
- mpmc_boundq_1_alt()
+ 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;
}
/**
- @Global_define:
+ @Begin
@Options:
LANG = CPP;
CLASS = mpmc_boundq_1_alt;
- @DeclareStruct:
- typedef struct elem {
- t_element* pos;
- boolean written;
- call_id_t id;
- } elem;
- @DeclareVar:
- spec_list *list;
- id_tag_t *tag;
- @InitVar:
- list = new_spec_list();
- tag = new_id_tag();
- @DefineFunc:
- elem* new_elem(t_element *pos, call_id_t id) {
- elem *e = (elem*) MODEL_MALLOC(sizeof(elem));
- e->pos = pos;
- e->written = false;
- e->id = id;
- }
- @DefineFunc:
- elem* get_elem(t_element *pos) {
- for (int i = 0; i < size(list); i++) {
- elem *e = (elem*) elem_at_index(list, i);
- if (e->pos == pos) {
- return e;
- }
- }
- return NULL;
- }
- @DefineFunc:
- int has_elem(t_element *pos) {
- for (int i = 0; i < size(list); i++) {
- elem *existing = (elem*) elem_at_index(list, i);
- if (pos == existing->pos) {
- return i;
- }
- }
- return -1;
- }
- @DefineFunc:
- void prepare(t_element *pos) {
- elem *e = new_elem(
- push_back(list, e);
- }
- @DefineFunc:
- void publish(t_element *pos) {
- elem *e = new_elem(
- push_back(list, e);
- }
- @DefineFunc:
- void consume_elem(t_element *pos) {
- int idx = has_elem(pos);
- if (idx == -1)
- return;
- remove_at_index(list, idx);
- }
+ @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) & 0xFFFF;
- wr = rdwr & 0xFFFF;
+ rd = (rdwr>>16) & MASK;
+ wr = rdwr & MASK;
if ( wr == rd ) { // empty
return false;
}
-
- if ( m_rdwr.compare_exchange_weak(rdwr,rdwr+(1<<16),mo_acq_rel) )
+ /**** 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
+ } 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 ( (m_written.load(mo_acquire) & 0xFFFF) != wr ) {
- thrd_yield();
+ 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;
}
- void read_consume() {
+ /**
+ @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) & 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
+ if ( wr == ((rd + t_size)&MASK) ) { // full
return NULL;
-
- if ( m_rdwr.compare_exchange_weak(rdwr,(rd<<16) | ((wr+1)&0xFFFF),mo_acq_rel) )
+ }
+
+ // 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
+ } 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 ( (m_read.load(mo_acquire) & 0xFFFF) != rd ) {
- thrd_yield();
+ 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;
}
- void write_publish()
+ /**
+ @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)
{
- m_written.fetch_add(1,mo_release);
+ /**** 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