#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
{
mpmc_boundq_1_alt()
{
+ /**
+ @Begin
+ @Entry_point
+ @End
+ */
m_rdwr = 0;
m_read = 0;
m_written = 0;
/**
- @Global_define:
- Order_queue<unsigned int*> spec_queue;
+ @Begin
+ @Options:
+ 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;
+ //id_tag_t *tag;
+ @InitVar:
+ list = new_spec_list();
+ //tag = new_id_tag();
+ @Happens_before:
+ Publish -> Fetch
+ Consume -> Prepare
+ @End
*/
//-----------------------------------------------------
+ /**
+ @Begin
+ @Interface: Fetch
+ @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__)
+ @End
+ */
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);
+ /**
+ @Begin
+ @Potential_commit_point_define: true
+ @Label: Fetch_Potential_RW_Load
+ @End
+ */
unsigned int rd,wr;
for(;;) {
rd = (rdwr>>16) & 0xFFFF;
wr = rdwr & 0xFFFF;
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;
}
-
- if ( m_rdwr.compare_exchange_weak(rdwr,rdwr+(1<<16),mo_acq_rel) )
+
+ 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)
break;
else
thrd_yield();
// (*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;
+ }
}
-
- t_element * p = & ( m_array[ rd % t_size ] );
/**
- @Commit_point_Check: true
- @Label: ANY
- @Check:
- spec_queue.peak() == p
+ @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 ] );
+
return p;
}
- void read_consume() {
+ /**
+ @Begin
+ @Interface: Consume
+ @Commit_point_set: Consume_R_RMW
+ @ID: (call_id_t) bin
+ //@Check:
+ // consume_check(__TID__)
+ //@Action:
+ //consume(__TID__);
+ @End
+ */
+ void read_consume(t_element *bin) {
+ /**** FIXME: miss ****/
m_read.fetch_add(1,mo_release);
/**
- @Commit_point_define: true
- @Label: Read_Consume_Success
- @Check:
- spec_queue.size() > 0
- @Action:
- spec_queue.remove();
+ @Begin
+ @Commit_point_define_check: true
+ @Label: Consume_R_RMW
+ @End
*/
}
//-----------------------------------------------------
+ /**
+ @Begin
+ @Interface: Prepare
+ @Commit_point_set: Prepare_RW_Load_Full | Prepare_RW_RMW | Prepare_R_Load
+ @ID: (call_id_t) __RET__
+ //@Check:
+ //prepare_check(__RET__, __TID__)
+ //@Action:
+ //push_back(list, __RET__);
+ @End
+ */
t_element * write_prepare() {
+ // Try weaker semantics
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_RW_Load
+ @End
+ */
unsigned int rd,wr;
for(;;) {
rd = (rdwr>>16) & 0xFFFF;
wr = rdwr & 0xFFFF;
- if ( wr == ((rd + t_size)&0xFFFF) ) // full
- return NULL;
+ if ( wr == ((rd + t_size)&0xFFFF) ) { // full
- if ( m_rdwr.compare_exchange_weak(rdwr,(rd<<16) | ((wr+1)&0xFFFF),mo_acq_rel) )
+ /**
+ @Begin
+ @Commit_point_define: true
+ @Potential_commit_point_label: Prepare_Potential_RW_Load
+ @Label: Prepare_RW_Load_Full
+ @End
+ */
+ return NULL;
+ }
+
+ bool succ = m_rdwr.compare_exchange_weak(rdwr,(rd<<16) |
+ ((wr+1)&0xFFFF),mo_acq_rel);
+ /**
+ @Begin
+ @Commit_point_define_check: succ
+ @Label: Prepare_RW_RMW
+ @End
+ */
+ if (succ)
break;
else
thrd_yield();
// (*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 ] );
- /**
- @Commit_point_check: ANY
- @Action: spec_queue.add(p);
- */
return p;
}
- void write_publish()
+ /**
+ @Begin
+ @Interface: Publish
+ @Commit_point_set: Publish_W_RMW
+ @ID: (call_id_t) bin
+ //@Check:
+ //publish_check(__TID__)
+ //@Action:
+ //publish(__TID__);
+ @End
+ */
+ void write_publish(t_element *bin)
{
+ /**** hb violation ****/
m_written.fetch_add(1,mo_release);
+ /**
+ @Begin
+ @Commit_point_define_check: true
+ @Label: Publish_W_RMW
+ @End
+ */
}
//-----------------------------------------------------
};
+/**
+ @Begin
+ @Class_end
+ @End
+*/
projects / cdsspec-compiler.git / blobdiff