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 m_read.fetch_add(1,mo_release);
149 @Commit_point_define_check: true
150 @Label: Consume_Point
155 //-----------------------------------------------------
160 @Commit_point_set: Prepare_Full_Point | Prepare_Succ_Point
161 @ID: (call_id_t) __RET__
163 //prepare_check(__RET__, __TID__)
165 //push_back(list, __RET__);
168 t_element * write_prepare() {
169 // Try weaker semantics
170 //unsigned int rdwr = m_rdwr.load(mo_acquire);
171 unsigned int rdwr = m_rdwr.load(mo_relaxed);
174 @Potential_commit_point_define: true
175 @Label: Prepare_Potential_Point
180 rd = (rdwr>>16) & 0xFFFF;
183 if ( wr == ((rd + t_size)&0xFFFF) ) { // full
187 @Commit_point_define: true
188 @Potential_commit_point_label: Prepare_Potential_Point
189 @Label: Prepare_Full_Point
195 bool succ = m_rdwr.compare_exchange_weak(rdwr,(rd<<16) |
196 ((wr+1)&0xFFFF),mo_acq_rel);
199 @Commit_point_define_check: succ == true
200 @Label: Prepare_Succ_Point
211 while ( (m_read.load(mo_acquire) & 0xFFFF) != rd ) {
215 t_element * p = & ( m_array[ wr % t_size ] );
223 @Commit_point_set: Publish_Point
226 //publish_check(__TID__)
231 void write_publish(t_element *bin)
233 m_written.fetch_add(1,mo_release);
236 @Commit_point_define_check: true
237 @Label: Publish_Point
242 //-----------------------------------------------------