/**
@Begin
@Interface: Get
- @Commit_point_set: GetReadValue1 | GetReadEntry | GetReadValue2
+ @Commit_point_set: GetReadValue1 | GetReadValue2 | GetReadNothing
@ID: __RET__
@Action:
int res = getIntegerMap(__map, key);
// 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
// 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) {
}
}
seg->unlock(); // Critical region ends
+ /**
+ @Begin
+ @Commit_point_define_check: true
+ @Label: GetReadNothing
+ @End
+ */
return 0;
}
// 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
// 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
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
m_read = 0;
m_written = 0;
// For this we want MASK = 1; MASK wrap around
- MASK = 0x1; // 11
+ MASK = _MASK; //0x11;
+ arr = m_array;
}
/**
@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
//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;
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)
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 {
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;
}
/**
@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
/**
@Begin
@Commit_point_define_check: true
- @Label: Consume_R_RMW
+ @Label: ConsumeFetchAdd
@End
*/
}
/**
@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
//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;
//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)
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;
}