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;
+ //@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();
+ // @InitVar:
+ // list = new_spec_list();
//tag = new_id_tag();
+ // @Cleanup:
+// if (list)
+// free_spec_list();
@Happens_before:
Publish -> Fetch
Consume -> Prepare
/**
@Begin
@Interface: Fetch
- @Commit_point_set: Fetch_Empty_Point | Fetch_Succ_Point
+ @Commit_point_set: Fetch_RW_Load_Empty | Fetch_RW_RMW | Fetch_W_Load
@ID: (call_id_t) __RET__
//@Check:
//__RET__ == NULL || has_elem(list, __RET__)
*/
t_element * read_fetch() {
// Try this new weaker semantics
- //unsigned int rdwr = m_rdwr.load(mo_acquire);
- unsigned int rdwr = m_rdwr.load(mo_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_Point
+ @Label: Fetch_Potential_RW_Load
@End
*/
unsigned int rd,wr;
/**
@Begin
@Commit_point_define: true
- @Potential_commit_point_label: Fetch_Potential_Point
- @Label: Fetch_Empty_Point
+ @Potential_commit_point_label: Fetch_Potential_RW_Load
+ @Label: Fetch_RW_Load_Empty
@End
*/
bool succ = m_rdwr.compare_exchange_weak(rdwr,rdwr+(1<<16),mo_acq_rel);
/**
@Begin
- @Commit_point_define_check: succ == true
- @Label: Fetch_Succ_Point
+ @Commit_point_define_check: succ
+ @Label: Fetch_RW_RMW
@End
*/
if (succ)
// (*1)
rl::backoff bo;
- while ( (m_written.load(mo_acquire) & 0xFFFF) != wr ) {
- thrd_yield();
+ while (true) {
+ int written = m_written.load(mo_acquire);
+ /**
+ @Begin
+ @Potential_commit_point_define: true
+ @Label: Fetch_Potential_W_Load
+ @End
+ */
+ if ((written & 0xFFFF) != wr) {
+ thrd_yield();
+ } else {
+ break;
+ }
}
+
+ /**
+ @Begin
+ @Commit_point_define: true
+ @Potential_commit_point_label: Fetch_Potential_W_Load
+ @Label: Fetch_W_Load
+ @End
+ */
t_element * p = & ( m_array[ rd % t_size ] );
/**
@Begin
@Interface: Consume
- @Commit_point_set: Consume_Point
+ @Commit_point_set: Consume_R_RMW
@ID: (call_id_t) bin
//@Check:
// consume_check(__TID__)
@End
*/
void read_consume(t_element *bin) {
+ /**** FIXME: miss ****/
m_read.fetch_add(1,mo_release);
/**
@Begin
@Commit_point_define_check: true
- @Label: Consume_Point
+ @Label: Consume_R_RMW
@End
*/
}
/**
@Begin
@Interface: Prepare
- @Commit_point_set: Prepare_Full_Point | Prepare_Succ_Point
+ @Commit_point_set: Prepare_RW_Load_Full | Prepare_RW_RMW | Prepare_R_Load
@ID: (call_id_t) __RET__
//@Check:
//prepare_check(__RET__, __TID__)
*/
t_element * write_prepare() {
// Try weaker semantics
- //unsigned int rdwr = m_rdwr.load(mo_acquire);
- unsigned int rdwr = m_rdwr.load(mo_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_Point
+ @Label: Prepare_Potential_RW_Load
@End
*/
unsigned int rd,wr;
/**
@Begin
@Commit_point_define: true
- @Potential_commit_point_label: Prepare_Potential_Point
- @Label: Prepare_Full_Point
+ @Potential_commit_point_label: Prepare_Potential_RW_Load
+ @Label: Prepare_RW_Load_Full
@End
*/
return NULL;
((wr+1)&0xFFFF),mo_acq_rel);
/**
@Begin
- @Commit_point_define_check: succ == true
- @Label: Prepare_Succ_Point
+ @Commit_point_define_check: succ
+ @Label: Prepare_RW_RMW
@End
*/
if (succ)
// (*1)
rl::backoff bo;
- while ( (m_read.load(mo_acquire) & 0xFFFF) != rd ) {
- thrd_yield();
+ while (true) {
+ int read = m_read.load(mo_acquire);
+ /**
+ @Begin
+ @Potential_commit_point_define: true
+ @Label: Prepare_Potential_R_Load
+ @End
+ */
+ if ((read & 0xFFFF) != rd)
+ thrd_yield();
+ else
+ break;
}
+ /**
+ @Begin
+ @Commit_point_define: true
+ @Potential_commit_point_label: Prepare_Potential_R_Load
+ @Label: Prepare_R_Load
+ @End
+ */
+
t_element * p = & ( m_array[ wr % t_size ] );
return p;
/**
@Begin
@Interface: Publish
- @Commit_point_set: Publish_Point
+ @Commit_point_set: Publish_W_RMW
@ID: (call_id_t) bin
//@Check:
//publish_check(__TID__)
*/
void write_publish(t_element *bin)
{
+ /**** hb violation ****/
m_written.fetch_add(1,mo_release);
/**
@Begin
@Commit_point_define_check: true
- @Label: Publish_Point
+ @Label: Publish_W_RMW
@End
*/
}