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_Empty_Point | Fetch_Succ_Point
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_Point
94 rd = (rdwr>>16) & 0xFFFF;
97 if ( wr == rd ) { // empty
101 @Commit_point_define: true
102 @Potential_commit_point_label: Fetch_Potential_Point
103 @Label: Fetch_Empty_Point
110 bool succ = m_rdwr.compare_exchange_weak(rdwr,rdwr+(1<<16),mo_acq_rel);
113 @Commit_point_define_check: succ == true
114 @Label: Fetch_Succ_Point
125 while ( (m_written.load(mo_acquire) & 0xFFFF) != wr ) {
129 t_element * p = & ( m_array[ rd % t_size ] );
137 @Commit_point_set: Consume_Point
140 // consume_check(__TID__)
145 void read_consume(t_element *bin) {
146 /**** FIXME: miss ****/
147 m_read.fetch_add(1,mo_release);
150 @Commit_point_define_check: true
151 @Label: Consume_Point
156 //-----------------------------------------------------
161 @Commit_point_set: Prepare_Full_Point | Prepare_Succ_Point
162 @ID: (call_id_t) __RET__
164 //prepare_check(__RET__, __TID__)
166 //push_back(list, __RET__);
169 t_element * write_prepare() {
170 // Try weaker semantics
171 unsigned int rdwr = m_rdwr.load(mo_acquire);
172 //unsigned int rdwr = m_rdwr.load(mo_relaxed);
175 @Potential_commit_point_define: true
176 @Label: Prepare_Potential_Point
181 rd = (rdwr>>16) & 0xFFFF;
184 if ( wr == ((rd + t_size)&0xFFFF) ) { // full
188 @Commit_point_define: true
189 @Potential_commit_point_label: Prepare_Potential_Point
190 @Label: Prepare_Full_Point
196 bool succ = m_rdwr.compare_exchange_weak(rdwr,(rd<<16) |
197 ((wr+1)&0xFFFF),mo_acq_rel);
200 @Commit_point_define_check: succ == true
201 @Label: Prepare_Succ_Point
212 while ( (m_read.load(mo_acquire) & 0xFFFF) != rd ) {
216 t_element * p = & ( m_array[ wr % t_size ] );
224 @Commit_point_set: Publish_Point
227 //publish_check(__TID__)
232 void write_publish(t_element *bin)
234 /**** hb violation ****/
235 m_written.fetch_add(1,mo_release);
238 @Commit_point_define_check: true
239 @Label: Publish_Point
244 //-----------------------------------------------------