Characterizing Progress Properties via Contextual Refinements 231 1 inc(){ 1inc(){ 1inc(){x:=x+1;J 2 while (i<10) 2 TestAndSet_lock(); 2dec(){x:=x-1;] 3 i:=1+1; x:=X+1; (a)Wait-Free (Ideal)Impl. 4 TestAndSet_unlock(); 5 x:=x+1; 51 1 inc(){ 61 2 (d)Deadlock-Free Impl. local t,b; 7 dec(){ 9 do{ 8 while (i>0){ 1 inc(){ t:=X; 9 1:=1-1; 2 Bakery_lock(); 6 b :cas(&x,t,t+1); 10 ] X:=X+1; 6 while(!b); 11 x:=x-1; Bakery_unlock(); 7} 123 5 (b)Lock-Free Impl. (c)Obstruction-Free Impl. (e)Starvation-Free Impl. Fig.2.Counter Objects with Methods inc and dec Wait-freedom,lock-freedom,and obstruction-freedom are progress properties for non-blocking implementations,where a delay of a thread cannot prevent other threads from making progress.In contrast,deadlock-freedom and starvation- freedom are progress properties for lock-based implementations.A delay of a thread holding a lock will block other threads which request the lock. Deadlock-freedom and starvation-freedom are often defined in terms of locks and critical sections.Deadlock-freedom guarantees that some thread will succeed in acquiring the lock,and starvation-freedom states that every thread attempting to acquire the lock will eventually succeed 9.For example,a test-and-set spin lock is deadlock-free but not starvation-free.In a concurrent access,some thread will successfully set the bit and get the lock,but there might be a thread that is continuously failing to get the lock.Lamport's bakery lock is starvation-free. It ensures that threads can acquire locks in the order of their requests. However,as noted by Herlihy and Shavit [10,the above definitions based on locks are unsatisfactory,because it is often difficult to identify a particular field in the object as a lock.Instead,they suggest defining them in terms of method calls.They also notice that the above definitions implicitly assume that every thread acquiring the lock will eventually release it.This assumption requires fair scheduling,i.e.,every thread gets eventually executed. Following Herlihy and Shavit [10,we say an object is deadlock-free,if in each fair execution there always exists some method call that can finish.As an example in Figure 2(d),we use a test-and-set lock to synchronize the incre- ments of the counter.Since some thread is guaranteed to acquire the test-and-set lock,the method call of that thread is guaranteed to finish.Thus the object is deadlock-free.Similarly,a starvation-free object guarantees that every method call can finish in fair executions.Figure 2(e)shows a counter implemented with Lamport's bakery lock.It is starvation-free since the bakery lock ensures that every thread can acquire the lock and hence every method call can eventually complete.Characterizing Progress Properties via Contextual Refinements 231 1 inc() { x := x + 1; } 2 dec() { x := x - 1; } (a) Wait-Free (Ideal) Impl. 1 inc() { 2 local t, b; 3 do { 4 t := x; 5 b := cas(&x,t,t+1); 6 } while(!b); 7 } (b) Lock-Free Impl. 1 inc() { 2 while (i < 10) { 3 i := i + 1; 4 } 5 x := x + 1; 6 } 7 dec() { 8 while (i > 0) { 9 i := i - 1; 10 } 11 x := x - 1; 12 } (c) Obstruction-Free Impl. 1 inc() { 2 TestAndSet_lock(); 3 x := x + 1; 4 TestAndSet_unlock(); 5 } (d) Deadlock-Free Impl. 1 inc() { 2 Bakery_lock(); 3 x := x + 1; 4 Bakery_unlock(); 5 } (e) Starvation-Free Impl. Fig. 2. Counter Objects with Methods inc and dec Wait-freedom, lock-freedom, and obstruction-freedom are progress properties for non-blocking implementations, where a delay of a thread cannot prevent other threads from making progress. In contrast, deadlock-freedom and starvation￾freedom are progress properties for lock-based implementations. A delay of a thread holding a lock will block other threads which request the lock. Deadlock-freedom and starvation-freedom are often defined in terms of locks and critical sections. Deadlock-freedom guarantees that some thread will succeed in acquiring the lock, and starvation-freedom states that every thread attempting to acquire the lock will eventually succeed [9]. For example, a test-and-set spin lock is deadlock-free but not starvation-free. In a concurrent access, some thread will successfully set the bit and get the lock, but there might be a thread that is continuously failing to get the lock. Lamport’s bakery lock is starvation-free. It ensures that threads can acquire locks in the order of their requests. However, as noted by Herlihy and Shavit [10], the above definitions based on locks are unsatisfactory, because it is often difficult to identify a particular field in the object as a lock. Instead, they suggest defining them in terms of method calls. They also notice that the above definitions implicitly assume that every thread acquiring the lock will eventually release it. This assumption requires fair scheduling, i.e., every thread gets eventually executed. Following Herlihy and Shavit [10], we say an object is deadlock-free, if in each fair execution there always exists some method call that can finish. As an example in Figure 2(d), we use a test-and-set lock to synchronize the incre￾ments of the counter. Since some thread is guaranteed to acquire the test-and-set lock, the method call of that thread is guaranteed to finish. Thus the object is deadlock-free. Similarly, a starvation-free object guarantees that every method call can finish in fair executions. Figure 2(e) shows a counter implemented with Lamport’s bakery lock. It is starvation-free since the bakery lock ensures that every thread can acquire the lock and hence every method call can eventually complete