me->gate.store(1, std::mo_relaxed );
// 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, don't think it's necessary
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
void unlock(guard * I) {
mcs_node * me = &(I->m_node);
+ // FIXME: detection miss, don't think it's necessary
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, don't think it's necessary
next = me->next.load(std::mo_acquire);
+ printf("unlock_miss3\n");
if ( next != NULL )
break;
thrd_yield();