New progress properties Different impl exhibit different progress properties Example: Test-and-Set(TAS)locks Example: Ticket locks TAS locks acq()( q0 local suc E2K i: getAndlnc( next succ: s false while( i l= serving )(; while(! succ succ: cas(L, 0, 1): rel(lI serving: serving 1; 1 Ticket locks Unfair! Queue management in banks How to distinguish them?New progress properties Different impl exhibit different progress properties How to distinguish them?