7 #include <cdsannotate.h>
8 #include <specannotation.h>
9 #include <model_memory.h>
16 template <typename t_element, size_t t_size>
17 struct mpmc_boundq_1_alt
21 // elements should generally be cache-line-size padded :
22 t_element m_array[t_size];
24 // rdwr counts the reads & writes that have started
25 atomic<unsigned int> m_rdwr;
26 // "read" and "written" count the number completed
27 atomic<unsigned int> m_read;
28 atomic<unsigned int> m_written;
49 CLASS = mpmc_boundq_1_alt;
56 thread_id_t fetch_tid;
63 list = new_spec_list();
71 //-----------------------------------------------------
76 @Commit_point_set: Fetch_RW_Load_Empty | Fetch_RW_RMW | Fetch_W_Load
77 @ID: (call_id_t) __RET__
79 //__RET__ == NULL || has_elem(list, __RET__)
82 t_element * read_fetch() {
83 // Try this new weaker semantics
84 unsigned int rdwr = m_rdwr.load(mo_acquire);
85 //unsigned int rdwr = m_rdwr.load(mo_relaxed);
88 @Potential_commit_point_define: true
89 @Label: Fetch_Potential_RW_Load
94 rd = (rdwr>>16) & 0xFFFF;
97 if ( wr == rd ) { // empty
101 @Commit_point_define: true
102 @Potential_commit_point_label: Fetch_Potential_RW_Load
103 @Label: Fetch_RW_Load_Empty
110 bool succ = m_rdwr.compare_exchange_weak(rdwr,rdwr+(1<<16),mo_acq_rel);
113 @Commit_point_define_check: succ
126 int written = m_written.load(mo_acquire);
129 @Potential_commit_point_define: true
130 @Label: Fetch_Potential_W_Load
133 if ((written & 0xFFFF) != wr) {
142 @Commit_point_define: true
143 @Potential_commit_point_label: Fetch_Potential_W_Load
148 t_element * p = & ( m_array[ rd % t_size ] );
156 @Commit_point_set: Consume_R_RMW
159 // consume_check(__TID__)
164 void read_consume(t_element *bin) {
165 /**** FIXME: miss ****/
166 m_read.fetch_add(1,mo_release);
169 @Commit_point_define_check: true
170 @Label: Consume_R_RMW
175 //-----------------------------------------------------
180 @Commit_point_set: Prepare_RW_Load_Full | Prepare_RW_RMW | Prepare_R_Load
181 @ID: (call_id_t) __RET__
183 //prepare_check(__RET__, __TID__)
185 //push_back(list, __RET__);
188 t_element * write_prepare() {
189 // Try weaker semantics
190 unsigned int rdwr = m_rdwr.load(mo_acquire);
191 //unsigned int rdwr = m_rdwr.load(mo_relaxed);
194 @Potential_commit_point_define: true
195 @Label: Prepare_Potential_RW_Load
200 rd = (rdwr>>16) & 0xFFFF;
203 if ( wr == ((rd + t_size)&0xFFFF) ) { // full
207 @Commit_point_define: true
208 @Potential_commit_point_label: Prepare_Potential_RW_Load
209 @Label: Prepare_RW_Load_Full
215 bool succ = m_rdwr.compare_exchange_weak(rdwr,(rd<<16) |
216 ((wr+1)&0xFFFF),mo_acq_rel);
219 @Commit_point_define_check: succ
220 @Label: Prepare_RW_RMW
232 int read = m_read.load(mo_acquire);
235 @Potential_commit_point_define: true
236 @Label: Prepare_Potential_R_Load
239 if ((read & 0xFFFF) != rd)
247 @Commit_point_define: true
248 @Potential_commit_point_label: Prepare_Potential_R_Load
249 @Label: Prepare_R_Load
253 t_element * p = & ( m_array[ wr % t_size ] );
261 @Commit_point_set: Publish_W_RMW
264 //publish_check(__TID__)
269 void write_publish(t_element *bin)
271 /**** hb violation ****/
272 m_written.fetch_add(1,mo_release);
275 @Commit_point_define_check: true
276 @Label: Publish_W_RMW
281 //-----------------------------------------------------