LANG = CPP;
CLASS = mcs_mutex;
@Global_define:
- @DeclareVar:
- bool _lock_acquired;
- @InitVar:
- _lock_acquired = false;
- @Happens_before:
- Unlock -> Lock
+ @DeclareVar: bool _lock_acquired;
+ @InitVar: _lock_acquired = false;
+ @Happens_before: Unlock -> Lock
@End
*/
@Begin
@Interface: Lock
@Commit_point_set: Lock_Enqueue_Point1 | Lock_Enqueue_Point2
- @Check:
- _lock_acquired == false;
- @Action:
- _lock_acquired = true;
+ @Check: _lock_acquired == false;
+ @Action: _lock_acquired = true;
@End
*/
void lock(guard * I) {
me->next.store(NULL, std::mo_relaxed );
me->gate.store(1, std::mo_relaxed );
+ /** Run this in the -Y mode to expose the HB bug */
// publish my node as the new tail :
- // FIXME: Only weakening the mo_acq_rel cause the spec error
mcs_node * pred = m_tail.exchange(me, std::mo_acq_rel);
/**
@Begin
// unlock of pred can see me in the tail before I fill next
// publish me to previous lock-holder :
+ // FIXME: detection miss, execution never ends
+ // If this is relaxed, the store 0 to gate will be read before and
+ // that lock will never ends.
pred->next.store(me, std::mo_release );
+ //printf("lock_miss1\n");
// (*2) pred not touched any more
int my_gate = 1;
while (my_gate ) {
my_gate = me->gate.load(std::mo_acquire);
+ //if (my_gate == 0)
+ //printf("lock at gate!\n");
/**
@Begin
@Commit_point_define_check: my_gate == 0
/**
@Begin
@Interface: Unlock
- @Commit_point_set:
- Unlock_Point_Success_1 | Unlock_Point_Success_2
- @Check:
- _lock_acquired == true
- @Action:
- _lock_acquired = false;
+ @Commit_point_set: Unlock_Point_Success_1 | Unlock_Point_Success_2
+ @Check: _lock_acquired == true
+ @Action: _lock_acquired = false;
@End
*/
void unlock(guard * I) {
mcs_node * me = &(I->m_node);
+ // FIXME: detection miss, execution never ends
mcs_node * next = me->next.load(std::mo_acquire);
+ //printf("unlock_miss2\n");
if ( next == NULL )
{
mcs_node * tail_was_me = me;
bool success;
- // FIXME: Only weakening the mo_acq_rel cause the spec error
success = m_tail.compare_exchange_strong(
tail_was_me,NULL,std::mo_acq_rel);
/**
// (*1) catch the race :
rl::linear_backoff bo;
for(;;) {
+ // FIXME: detection miss, execution never ends
next = me->next.load(std::mo_acquire);
+ //printf("unlock_miss3\n");
if ( next != NULL )
break;
thrd_yield();