8 #include <cdsannotate.h>
9 #include <specannotation.h>
10 #include <model_memory.h>
14 std::atomic<mcs_node *> next;
15 std::atomic<int> gate;
26 // tail is null when lock is not held
27 std::atomic<mcs_node *> m_tail;
38 //ASSERT( m_tail.load() == NULL );
41 // Each thread will have their own guard.
45 mcs_node m_node; // node held on the stack
47 guard(mcs_mutex * t) : m_t(t) { t->lock(this); }
48 ~guard() { m_t->unlock(this); }
57 @DeclareVar: bool _lock_acquired;
58 @InitVar: _lock_acquired = false;
59 @Happens_before: Unlock -> Lock
66 @Commit_point_set: Lock_Enqueue_Point1 | Lock_Enqueue_Point2
67 @Check: _lock_acquired == false;
68 @Action: _lock_acquired = true;
71 void lock(guard * I) {
72 mcs_node * me = &(I->m_node);
75 // not published yet so relaxed :
76 me->next.store(NULL, std::mo_relaxed );
77 me->gate.store(1, std::mo_relaxed );
79 /********** Inadmissible **********/
80 /** Run this in the -Y mode to expose the HB bug */
81 // publish my node as the new tail :
82 mcs_node * pred = m_tail.exchange(me, std::mo_acq_rel);
85 @Commit_point_define_check: pred == NULL
86 @Label: Lock_Enqueue_Point1
91 // unlock of pred can see me in the tail before I fill next
93 // publish me to previous lock-holder :
94 // FIXME: detection miss, execution never ends
95 // If this is relaxed, the store 0 to gate will be read before and
96 // that lock will never ends.
97 pred->next.store(me, std::mo_release );
98 //printf("lock_miss1\n");
100 // (*2) pred not touched any more
102 // now this is the spin -
103 // wait on predecessor setting my flag -
104 rl::linear_backoff bo;
107 /********** Inadmissibility *********/
108 my_gate = me->gate.load(std::mo_acquire);
110 //printf("lock at gate!\n");
113 @Commit_point_define_check: my_gate == 0
114 @Label: Lock_Enqueue_Point2
125 @Commit_point_set: Unlock_Point_Success_1 | Unlock_Point_Success_2
126 @Check: _lock_acquired == true
127 @Action: _lock_acquired = false;
130 void unlock(guard * I) {
131 mcs_node * me = &(I->m_node);
133 // FIXME: detection miss, execution never ends
134 mcs_node * next = me->next.load(std::mo_acquire);
135 //printf("unlock_miss2\n");
138 mcs_node * tail_was_me = me;
141 /********** Inadmissible **********/
142 success = m_tail.compare_exchange_strong(
143 tail_was_me,NULL,std::mo_acq_rel);
146 @Commit_point_define_check: success == true
147 @Label: Unlock_Point_Success_1
152 // got null in tail, mutex is unlocked
156 // (*1) catch the race :
157 rl::linear_backoff bo;
159 // FIXME: detection miss, execution never ends
160 next = me->next.load(std::mo_acquire);
161 //printf("unlock_miss3\n");
168 // (*2) - store to next must be done,
169 // so no locker can be viewing my node any more
171 /********** Inadmissible **********/
173 next->gate.store( 0, std::mo_release );
176 @Commit_point_define_check: true
177 @Label: Unlock_Point_Success_2