New progress properties TAS lock client: acq i acq while(true)t local succ. acq succ: false rel(; print(1) e(); while(! succ i succ: =cas(L, 0, 1): It may not print 1 (even with fair scheduling re But there always exists a method call that returns unless the lock is never released Rule out non-termination caused by"bad"clientsNew progress properties acq() { local succ; succ := false; while( ! succ ) { succ := cas(L, 0, 1); } } rel() { L := 0; } TAS lock acq(); rel(); print(1); while(true){ acq(); rel(); } client: It may not print 1 (even with fair scheduling). But there always exists a method call that returns, unless the lock is never released. Rule out non-termination caused by “bad” clients