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 );
+ /********** Inadmissible **********/
+ /** Run this in the -Y mode to expose the HB bug */
// publish my node as the new tail :
mcs_node * pred = m_tail.exchange(me, std::mo_acq_rel);
/**
// unlock of pred can see me in the tail before I fill next
// publish me to previous lock-holder :
- // FIXME: detection miss
+ // 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
rl::linear_backoff bo;
int my_gate = 1;
while (my_gate ) {
+ /********** Inadmissibility *********/
my_gate = me->gate.load(std::mo_acquire);
- if (my_gate == 0)
- printf("lock at gate!\n");
+ //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
+ // 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;
+
+ /********** Inadmissible **********/
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
+ // FIXME: detection miss, execution never ends
next = me->next.load(std::mo_acquire);
+ //printf("unlock_miss3\n");
if ( next != NULL )
break;
thrd_yield();
// (*2) - store to next must be done,
// so no locker can be viewing my node any more
+ /********** Inadmissible **********/
// let next guy in :
next->gate.store( 0, std::mo_release );
/**