// (*1)
rl::backoff bo;
while (true) {
- /**** Inadmissibility ****/
+ /**** Inadmissibility (testcase2.c) ****/
int written = m_written.load(mo_acquire);
if ((written & MASK) != wr) {
thrd_yield();
@End
*/
void read_consume(t_element *bin) {
- /**** Inadmissibility ****/
+ /**** Inadmissibility (testcase1.c) ****/
m_read.fetch_add(1,mo_release);
/**
@Begin
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);
// (*1)
rl::backoff bo;
while (true) {
- /**** Inadmissibility ****/
+ /**** Inadmissibility (testcase1.c) ****/
int read = m_read.load(mo_acquire);
if ((read & MASK) != rd)
thrd_yield();
/**
@Begin
@Interface: Publish
- @Commit_point_set: Publish_W_RMW
+ @Commit_point_set: PublishFetchAdd
@ID: (call_id_t) bin
//@Action: model_print("Publish: %d\n", bin);
@End
*/
void write_publish(t_element *bin)
{
- /**** Inadmissibility ****/
+ /**** Inadmissibility (testcase2.c) ****/
int tmp = m_written.fetch_add(1,mo_release);
/**
@Begin
@Commit_point_define_check: true
- @Label: Publish_W_RMW
+ @Label: PublishFetchAdd
@End
*/
printf("publish: m_written=%d\n", tmp + 1);